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

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

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

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

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

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

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

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


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

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

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

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

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

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

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