Занятие 19 мая

Ближайшее занятие (19 мая) переносится из аудитории 609 в другую из-за проходящего госэкзамена. В какую именно должно быть написано на самой аудитории. Если ничего написано не будет, приходите в аудиторию 718.

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

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

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

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

Практическое занятие 14 апреля

Напоминаю, что 14 апреля на лекции будет практическое занятие по пользованию связкой инструментов frama-c — jessie2 — why3. Постарайтесь, чтобы у всех были ноутбуки. Максимально желательно, чтобы вы попробовали установить связку инструментов. Инструкция по установке.

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