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

Написать спецификации, отражающие данные требования.
Читать далее «Четвёртая домашняя работа блока спецификации»

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

Написать спецификацию, отражающую следующие требования.
Читать далее «Третья домашняя работа блока спецификации»

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

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

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

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

Написать спецификацию, отражающие следующие требования.
Читать далее «Вторая домашняя работа блока спецификации»

Лекция 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 марта.

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

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