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

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

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

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

Добавить комментарий

Ваш e-mail не будет опубликован. Обязательные поля помечены *