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

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

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

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

  1. Доказать, что заданная блок-схема успешно завершается при заданном предусловии при помощи метода фундированных множеств Флойда. Доменом всех переменных является множество целых чисел.
    Читать далее «Третья домашняя работа блока методов Флойда»

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

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

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

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

Стоит доделать задание, которое разбиралось на семинаре.

Основное задание:
доказать методом индуктивных утверждений Флойда частичную корректность следующей блок-схемы относительно заданной спецификации.

Читать далее «Вторая домашняя работа блока методов Флойда»

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

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

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

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


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

Читать далее «Первая домашняя работа блока методов Флойда»

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

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

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

О начале курсов

В весеннем семестре 2015/2016 года на факультете ВМК МГУ имени М.В. Ломоносова начинается ежегодное чтение курсов по формальной спецификации программ и дедуктивной верификации программ для магистров 1 года.