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