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

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

Рубрика: Домашние задания | Добавить комментарий

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

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

Рубрика: Домашние задания | Добавить комментарий

Лекция 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);

Читать далее

Рубрика: Лекции | Добавить комментарий

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

Написать контракт 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 марта.

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

Читать далее

Рубрика: Домашние задания | Добавить комментарий

Первая контрольная работа

Напоминаю, что на семинаре 10 марта состоится контрольная работа по методам Флойда.

Рубрика: Новости | Добавить комментарий