- Доказать, что заданная блок-схема успешно завершается при заданном предусловии при помощи метода фундированных множеств Флойда. Доменом всех переменных является множество целых чисел.
Читать далее «Третья домашняя работа блока методов Флойда»
Автор: Денис Буздалов
Лекция 25 февраля
Состоялась лекция «Метод фундированных множеств Флойда».
Были рассмотрены следующие вопросы:
- понятие частичного порядка;
- понятие фундированного множества;
- метод оценочных функций Флойда;
- понятие оценочной функции;
- индуктивные утверждения и соответствующие условия верификации;
- понятие условия корректности определения оценочной функции;
- понятие условия завершимости;
- понятие условия успешной выполнимости оператора;
- теорема Флойда о завершимости.
Вторая домашняя работа блока методов Флойда
Стоит доделать задание, которое разбиралось на семинаре.
Основное задание:
доказать методом индуктивных утверждений Флойда частичную корректность следующей блок-схемы относительно заданной спецификации.
Лекция 18 февраля
Состоялась лекция «Метод индуктивных утверждений Флойда»
Были рассмотрены следующие вопросы:
- понятие пути в блок-схеме;
- понятия предиката пути и функции пути;
- понятие точки сечения;
- понятия базового, промежуточного, начального и конечного путей для заданного множества точек сечения;
- достаточность множества точек сечения для методов Флойда (покрытие блок-схемы базовыми путями);
- метод индуктивных утверждений Флойда;
- понятие индуктивного утверждения;
- условия верификации для промежуточных, начальных и конечных базовых путей;
- теорема Флойда о частичной корректности.
Первая домашняя работа блока методов Флойда
Доменом всех используемых в блок-схемах переменных является множество целых чисел. В блок-схемах разрешается использовать только сложение, вычитание, умножение, целочисленное деление, взятие остатка от деления и все виды арифметических сравнений (равно, не равно, больше, меньше и т.п.).
Лекция 11 февраля
Состоялась лекция «Основные понятия дедуктивной верификации».
Были рассмотрены следующие вопросы:
- понятие корректности программы;
- понятие формальной корректности математической модели программы над
- математической моделью требований;
- блок-схема как математическая модель программы;
- пред- и постусловия в виде предикатов как математическая модель требований;
- понятие вычисления блок-схемы;
- функция M[P] результата вычисления блок-схемы;
- понятие завершимости программы относительно заданных требований;
- понятие частичной корректности программы относительно заданных требований;
- понятие полной корректности программы относительно заданных требований;
- лемма о сведении полной корректности к частичной корректности и завершаемости.