Архив рубрики: Лекции

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

Состоялось практическое занятие по пользованию связкой инструментов frama-c – jessie2 – why3. Были рассмотрены вопросы: установка инструмента: установка OCaml и OPAM; включение OPAM командой в терминале или в .bashrc; использование инструмента; запуск инструмента на заданном файле; набор утверждений верхнего уровня (утверждения *_safety, … Читать далее

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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