Сложное практическое задание

Сложное практическое задание состоит из двух этапов:

  • Этап 1 («разработка модели»): вам дадут описание интерфейса класса (требования), вам нужно точно формализовать требования на языке JML.
  • Этап 2 («доказательство правильности реализации относительно модели»): вам дадут реализацию класса, вам нужно формально доказать при помощи инструментов Krakatoa (Frama-C), Jessie, Why3 и солверов, что эта реализация соответствует формальной модели требований с первого этапа.

За выполнение сложного практического задания можно получить до 80 баллов. Этапы оцениваются независимо. Второй этап можно выполнять только после успешного выполнения первого этапа.

Те, кто согласятся на выполнение сложного задания, лишаются возможности написать коллоквиум, но не лишаются возможности выполнять простое практическое задание.

Поскольку сейчас основные силы разработчиков инструмента Krakatoa переброшены на инструмент Frama-C (это его аналог, только для языка Си), то найденные баги в Krakatoa исправлять там некому (и, наверное, некогда). По мере возможностей мы (преподаватели) будем исправлять обнаруженные критичные баги, но на это может потребоваться некоторое время. Есть мнение, что сейчас инструмент Frama-C содержит меньшее количество незакрытых багов, поэтому работа с ним может быть более продуктивной. Мы разрешаем вам использовать Frama-C вместо Krakatoa, но хотим обратить внимание, что вам придется дополнительно изучить особенности формальной спецификации на языке Си и модель памяти на языке Си.

Последнее изменение: суббота, 1 ноября 2014, 23:18