Занятие 14 апреля

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

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

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

Лекция 7 апреля

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

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

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

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

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

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

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

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

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

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

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

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

  • понятие пути в блок-схеме;
  • понятия предиката пути и функции пути;
  • понятие точки сечения;
  • понятия базового, промежуточного, начального и конечного путей для заданного множества точек сечения;
  • достаточность множества точек сечения для методов Флойда (покрытие блок-схемы базовыми путями);
  • метод индуктивных утверждений Флойда;
    • понятие индуктивного утверждения;
    • условия верификации для промежуточных, начальных и конечных базовых путей;
  • теорема Флойда о частичной корректности.

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

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

  • понятие корректности программы;
  • понятие формальной корректности математической модели программы над
  • математической моделью требований;
  • блок-схема как математическая модель программы;
  • пред- и постусловия в виде предикатов как математическая модель требований;
  • понятие вычисления блок-схемы;
  • функция M[P] результата вычисления блок-схемы;
  • понятие завершимости программы относительно заданных требований;
  • понятие частичной корректности программы относительно заданных требований;
  • понятие полной корректности программы относительно заданных требований;
  • лемма о сведении полной корректности к частичной корректности и завершаемости.