Теоретическое введение

Данное руководство создано на основе Практикума по дедуктивной верификации программ ВМК МГУ и является введением в методы дедуктивной верификации последовательных программ (или, как ее еще называют, аналитической верификации).

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

Далее, без ограничения общности, под «методами верификации» будут пониматься «дедуктивные методы верификации».

Поскольку дедуктивная верификация основана на использовании логических (математических) заключений, она должна оперировать с математическими («формальными») моделями как программ, требований, так и с формально определенным отношением их соответствия.

Мы начнем рассмотрение методов верификации на простейших моделях последовательных программ. Первая модель будет соответствовать программам, написанным на структурном языке программирования

Методы верификации рекурсивных программ не входят в материал данных статей.

Программы, взаимодействующие с окружением, относятся к параллельным (или, как их еще называют, реактивным) программам и мы их тоже пока не рассматриваем.

Мы рассмотрим методы верификации  последовательных программ, которые называют методами Флойда (или методами Флойда-Хоара). Корни этих методов уходят к Алану Тьюрингу, который в своей лекции Лондонскому математическому обществу в 1947 впервые озвучил идею индуктивных утверждений. До полноценных методов верификации эта идея была доведена независимо Робертом Флойдом и Тони Хоаром в конце 60-х годов 20 века.

Математическая модель программы

Описание математической модели программы

Математическая модель требований

Описание математической модели требований к программе

Задача верификации

Описание задачи верификации

Методы Флойда

Формулировка методов Флойда для доказательства корректности программ