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

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

• при описании требований к функции у одних и тех же переменных и областей памяти может быть разное состояние (значение);
• стандартные метки памяти (метки Here, Pre, Post), обычные метки Си;
• в каком состоянии используется переменная в каждом из типов выражений ACSL (т.е. значение метки Here для тех или иных выражений);
• как специфицировать произвольное состояние переменной (выражение \at), состояние при входе в функцию (выражение \old);
• требования к функции могут запрещать изменять ей некоторую память;
  • если некоторая память не запрещена спецификацией к изменению и нет других ограничений, то эта память может быть изменена произвольно (т.е. по умолчанию всё разрешается);
  • как специфицировать какую именно память разрешено изменять функции (конструкции assigns и loop assigns);
  • что в спецификации памяти, разрешённой на изменение, используется lvalue;
• спецификация возможности разыменовывания указателя (конструкция \valid);

Читать далее «Лекция 24 марта»

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

• где инструмент расставляет точки сечения у циклов;
• как выразить индуктивное утверждение в автоматических точках сечения
  (конструкции loop invariant);
• как добавлять свои утверждения в формулу пути (конструкция assert);
• какие новые условия верификации добавляет конструкция assert;
• какое фундированное множество выбрано в инструменте;
• как выразить оценочную функцию в точках сечения (конструкция loop variant);
• логические функции и предикаты:
  • явное объявление именованных предикатов и логических функций;
  • использование предикатов и логических функций в выражениях;
  • о порядке логики в логических функциях и предикатах;
  • индуктивное задание предикатов;
  • аксиоматическое задание логических функций и предикатов;
  • тотальность логических функций и предикатов.

Состоялась вводная лекция, посвящённая инструментарию frama-c→jessie2→why3 и языку спецификации ACSL. Были рассмотрены:

• идея автоматизации применения методов Флойда для функции на языке Си (в
  качестве модели программы) и контракта ACSL (в качестве модели требований);
• примеры применения связки инструментов для доказательства полной коррекности;
• аннотирование спецификационными комментариями ACSL;
• базовые элементы контрактов ACSL:
  • способ выражения пред- и постусловий (конструкции requires и ensures);
  • обращение к входным переменным (по имени) и результату (выражение \result);
  • идея о недоступности изменённых входных переменных-параметров функции из постусловия, т.е. что в постусловии используются значения, переданные при вызове;
  • использование кванторов в предикатах (выражения \forall, \exists);
• разница между математическим целым (integer) и машинным целым (int) в ACSL.

Состоялась лекция «Расширение блок-схем и методов Флойда на поддержку вызова других блок-схем». Были рассмотрены следующие вопросы:

• расширенная модель программы: блок-схемы, вызывающие другие блок-схемы;
• идея раздельного доказательства корректности вызывающей и вызываемых блок-схем;
• понятие сигнатуры блок-схемы;
• оператор CALL вызова блок-схемы;
• означивание блок-схем сигнатурам (функция μ(s));
• спецификация сигнатур блок-схем (функция γ(s));
• условие корректности вызова блок-схемы;
• модифицированные определения частичной и полной корректности.

Состоялась лекция «Метод фундированных множеств Флойда».
Были рассмотрены следующие вопросы:

• понятие частичного порядка;
• понятие фундированного множества;
• метод оценочных функций Флойда;
  • понятие оценочной функции;
  • индуктивные утверждения и соответствующие условия верификации;
  • понятие условия корректности определения оценочной функции;
  • понятие условия завершимости;
  • понятие условия успешной выполнимости оператора;
• теорема Флойда о завершимости.