Автор: Евгений Корныхин

Контрольная работа по методам Флойда

На семинаре 15 марта будет проведена контрольная работа по методам Флойда. Длительность контрольной — 1,5 часа. За это время нужно будет доказать полную корректность некоторой блок-схемы относительно некоторой спецификации при помощи методов Флойда. Можно пользоваться любыми письменными материалами и книгами. Нельзя пользоваться электронными устройствами.

Домашняя работа по методам Флойда с частичными функциями

Докажите, что эта блок-схема (картинка) полностью корректна относительно этой спецификации при помощи методов Флойда. Решение присылайте на почту до 12:00 17 марта в виде двух файлов: файла *.py с индуктивными утверждениями и оценочными функциями в формате PyFloyd и 2 файла *.prf с PVS доказательством истинности условий из метода индуктивных утверждений и метода фундированных множеств. Индуктивные утверждения в файле *.py должны годиться и для доказательства частичной корректности, и для доказательства завершаемости.

Обратите внимание, что команда PVS (grind) не применяет аксиомы и леммы. При необходимости можно добавить аксиому или лемму в список антецедентов при помощи команды (lemma) и продолжить доказательство при помощи (grind).

Для поддержки частичных функций обновите инструмент PyFloyd.

Еще одно пособие

Вашему вниманию предлагается пособие Камкина Александра Сергеевича «Введение в формальные методы верификации программ». В нем рассмотрены различные вопросы и методы формальной верификации программ, в частности, методы дедуктивной верификации, язык спецификации ACSL и инструменты Frama-C и Jessie. Пособие можно скачать на сайте кафедры СП.

Домашняя работа по методу фундированных множеств

Докажите, что эта блок-схема (картинка) завершается на этом предусловии при помощи метода фундированных множеств. Решение присылайте на почту до 12:00 5 марта в виде двух файлов: файла *.py с индуктивными утверждениями и оценочными функциями в формате PyFloyd и файла *.prf с PVS доказательством истинности условий верификации.

Обратите внимание, что инструмент PyFloyd поддерживает (пока) единственное фундированное множество: неотрицательные целые числа и арифметическое сравнение «меньше», а множеством значений всех оценочных функций является множество всех целых чисел.

Домашняя работа по методу индуктивных утверждений Флойда

Докажите, что эта блок-схема (картинка) частично корректна относительно этой спецификации при помощи метода индуктивных утверждений Флойда. Решение присылайте на почту до 12:00 26 февраля в виде двух файлов: файла *.py с индуктивными утверждениями в формате PyFloyd и файла *.prf с PVS доказательством истинности условий верификации.

Экзамен

15 июня состоится экзамен. Он пройдет в письменной форме. Экзамен начнется в 9:00 и будет проходить в течение 120 минут в аудитории 713. На экзамене вы можете использовать письменные и печатные материалы, но не можете использовать электронную технику и средства связи.

Вариант экзамена состоит из двух частей. В первой части вам нужно будет доказывать полную корректность блок-схем при помощи методов Флойда. Во второй части вам нужно будет работать с требованиями и спецификациями на языке ACSL.

Если будет много желающих писать экзамен, показ работ придется перенести на 16 июня.

Если вы хотите просто проставить оценку за работу в семестре, подходите в течение экзамена. Можно передать зачетную книжку через других студентов.

Отмена занятия

18 мая занятия не состоятся. Для согласования времени встреч для сдачи практического задания пишите мне на почту .

Контрольная работа по ACSL

4 мая в 14:35 состоится контрольная работа по ACSL. Можно пользоваться любыми печатными и письменными материалами, нельзя пользоваться компьютерами и телефонами. Длительность работы — 40 минут. После этого можно будет сдавать первый этап практического задания.