Автор: Денис Буздалов

Обновление инструментов

Инструменты обновились сегодня. Настоятельно рекомендуется обновить их перед использованием. Для этого используйте команды opam update и opam upgrade.

Контрольная работа №2-бис

10 июня в 10:00 состоится вторая контрольная работа по блоку спецификации для пропустивших её 28 апреля. Аудитория проведения станет известна в день проведения, узнавать в 718. Время работы 30 мин.

Дата экзамена

Экзамен обеих групп состоится 16 июня. Экзамен письменный, проводится с 10:00, длительность ориентировочно три часа. Экзамен проверяется в тот же день, показ работ после проверки, ближе к вечеру.

UPD: После начала экзамена (непосредственно после раздачи заданий) можно проставить автоматы.

Верификационная часть практического задания

Для получения верификационной части практического задания (после успешного выполнения спецификационной части) необходимо добавить вашу спецификацию к файлу map.h и прислать его. К функциям, не присутствующим в вашем варианте, не стоит добавлять никаких спецификационных комментариев.

Обратите внимание, что файл map.h со спецификацией нельзя менять во время выполнения верификационной части. Также, в выданных вам *.c-файлах все изменения должны составлять добавление спецификационных комментариев в отдельных строках этого файла. Остальные изменения файлов должны быть предварительно согласованы.

В реализации могут быть ошибки. При обнаружении ошибок, необходимо предложить исправление, согласовать его и только после этого продолжать верификацию.

Занятие 19 мая

Ближайшее занятие (19 мая) переносится из аудитории 609 в другую из-за проходящего госэкзамена. В какую именно должно быть написано на самой аудитории. Если ничего написано не будет, приходите в аудиторию 718.

Занятие 14 апреля

Состоялось практическое занятие по пользованию связкой инструментов frama-c – jessie2 – why3.

Были рассмотрены вопросы:

  • установка инструмента:
    • установка OCaml и OPAM;
    • включение OPAM командой в терминале или в .bashrc;
  • использование инструмента;
    • запуск инструмента на заданном файле;
    • набор утверждений верхнего уровня (утверждения *_safety, *_behaviors);
    • отличие условий верификации для default behaviors от условий для именованых поведений;
    • разбиение утверждения по конъюнктам в посыле импликации (split);
    • подстановка функций с условии верификации (inline);
    • полезность выполнения split после inline;
    • сохранение статуса доказанности условий верификации (сохранение сессии);
  • спецификация операций с переполнениями в логических выражениях и в коде.

Практическое занятие 14 апреля

Напоминаю, что 14 апреля на лекции будет практическое занятие по пользованию связкой инструментов frama-c — jessie2 — why3. Постарайтесь, чтобы у всех были ноутбуки. Максимально желательно, чтобы вы попробовали установить связку инструментов. Инструкция по установке.

Лекция 7 апреля

Состоялась лекция, посвящённая особенностям спецификации структур. Были рассмотрены вопросы:

  • спецификация инвариантов типов:
    • потребность в выражении свойств, относящихся ко всему типу (т.е., к любой функции, работающей со значением данного типа);
    • различие между сильными и слабыми инвариантами (аналогично глобальным инвариантам);
    • возможность выражение инвариантов типов при помощи глобальных инвариантов;
    • ограничения данного подхода по сравнению с «настоящими» инвариантами типов;
  • ghost-переменные и ghost-выражения;
    • потребность в выражении некоторых свойств;
    • ограничения, накладываемые для ghost-выражения для обеспечения безопасности;
    • использование ghost-выражений для моделирования внешнего состояния, используемого для уточнения спецификации (например, для выражения наличия свободной памяти для функций malloc и free).

Четвёртая домашняя работа блока спецификации

Написать спецификации, отражающие данные требования.
Читать далее «Четвёртая домашняя работа блока спецификации»