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