Домашняя работа №1 по языку Си

В домашней работе два задания. Второе задание выполняется только после успешного выполнения первого задания.

1) Напишите заголовочный файл *.h c формальной спецификацией на ACSL функции, вычисляющей ближайшее снизу целое число к квадратному корню данного целого числа. Файл должен приниматься Frama-c + Jessie. Пришлите его на почту

2) Докажите полную корректность выданной преподавателем реализации этой функции относительно вашей спецификации при помощи инструментов Frama-c + Jessie. На почту нужно прислать zip-архив целиком директории, в которой находится файл *.h со спецификацией, файл *.c с реализацией, включающий заголовочный файл при помощи #include, и директория *.jessie, созданная инструментом. Для этого после успешного доказательства всех условий верификации сохраните сессию (File > Save session). Проверка будет выполняться открытием этой сессии и нажатием кнопки Replay.

Всё задание должно быть выполнено до 12:00 26 марта.

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

На семинаре 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 минут. После этого можно будет сдавать первый этап практического задания.