Архив автора: Денис Буздалов

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

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

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

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

Состоялась лекция, посвящённая различным аспектам спецификации состояния памяти в ACSL. Были рассмотрены вопросы: (напоминание) спецификация доступности памяти по указателям; как описывать в спецификации требования на возможность разыменовать указатель (функция \valid); возможность адресации области памяти (напр., работа с указателем как с … Читать далее

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

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

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

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

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

Состоялась лекция, посвящённая различным конструкциям языка спецификации ACSL. Были рассмотрены вопросы: при описании требований к функции у одних и тех же переменных и областей памяти может быть разное состояние (значение); стандартные метки памяти (метки Here, Pre, Post), обычные метки Си; … Читать далее

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

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

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

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

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

Состоялась лекция, посвящённая основам языка ACSL. Были рассмотрены вопросы: где инструмент расставляет точки сечения у циклов; как выразить индуктивное утверждение в автоматических точках сечения (конструкции loop invariant); как добавлять свои утверждения в формулу пути (конструкция assert); какие новые условия верификации … Читать далее

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

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

Состоялась вводная лекция, посвящённая инструментарию frama-c→jessie2→why3 и языку спецификации ACSL. Были рассмотрены: идея автоматизации применения методов Флойда для функции на языке Си (в качестве модели программы) и контракта ACSL (в качестве модели требований); примеры применения связки инструментов для доказательства полной коррекности; … Читать далее

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

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

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

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

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

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

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

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

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

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