Лекция 24 марта

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

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

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

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

Написать контракт ACSL для сигнатуры заданной функции, соответствующий данному требованию.

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

Лекция 17 марта

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

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

Лекция 10 марта

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

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

Четвёртая домашняя работа блока методов Флойда

Срок сдачи этой домашней работы — семинар 17 марта.

Доказать полную корректность блок-схемы относительно заданного контракта. Доменом всех переменных является множество целых чисел.

Читать далее «Четвёртая домашняя работа блока методов Флойда»

Лекция 3 марта

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

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

Третья домашняя работа блока методов Флойда

  1. Доказать, что заданная блок-схема успешно завершается при заданном предусловии при помощи метода фундированных множеств Флойда. Доменом всех переменных является множество целых чисел.
    Читать далее «Третья домашняя работа блока методов Флойда»

Лекция 25 февраля

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

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

Вторая домашняя работа блока методов Флойда

Стоит доделать задание, которое разбиралось на семинаре.

Основное задание:
доказать методом индуктивных утверждений Флойда частичную корректность следующей блок-схемы относительно заданной спецификации.

Читать далее «Вторая домашняя работа блока методов Флойда»