Формальные методы разработки программ

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

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

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

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

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

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

• (напоминание) спецификация доступности памяти по указателям;
  • как описывать в спецификации требования на возможность разыменовать указатель (функция \valid);
  • возможность адресации области памяти (напр., работа с указателем как с массивом);
  • в выражении \valid используются указатели, в отличие от спецификации разрешённое на изменение памяти (в assigns и loop assigns);
  • как использовать невалидный указатель в спецификациях (специальное значение \null);
• модель памяти ACSL;
  • частичный порядок над указателями в ACSL;
  • несравнимость указателей, полученных разными выделениями памяти;
  • предположение о непересекаемости указателей по умолчанию;
  • явная спецификация непересекаемости указателей (функция \separated);
  • средства работы с областями памяти (фукнции \offset_min, \offset_max, \base_addr)
• аргумент состояния памяти в логических функциях:
  • для именованных предикатов и логических функций, использующих память по указателям, состояние памяти должно передаваться явно параметром-меткой;
  • если функция определена над значениями самих указателей, метка памяти не требуется;
  • при использовании функции с единственным параметром-меткой, эта метка может быть поставлена автоматически;
  • встроенная функция \valid тоже имеет параметр-метку, которая может быть использована явно (если это требуется);
  • именованные предикаты и логические функции могут иметь несколько параметров, описывающих состояние памяти;
  • какие свойства можно выражать при помощи предикатов и функций с несколькими параметрами-метками;
  • как объявить предикат или функцию с параметрами-метками и как их использовать;
  • аксиомы и леммы с метками памяти;
• спецификация выделения/освобождения памяти;
  • если не специфицировано выделение/освобождение памяти, то разрешается любое поведение в этом аспекте;
  • конструкции allocates и frees для явной спецификации разрешённых множеств;
  • места, в которых определены выражения в конструкциях allocates и frees (т.е. значение меток Here);
  • как специфицировать запрет на выделение/освобождение памяти.