Метод индуктивных утверждений Флойда.

Исторически первой системой верификации программ явился метод ИУ Р.Флойда. Аналогичные мысли о верификации в те же годы высказал П. Наур.

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

Метод Флойда ориентирован на доказательство ПП из класса стандартных схем и стандартных схем с массивами. Объектом верификации выступают программы, представленные в виде блок-схем.

Метод ИУ Флойда, будучи исторически первой системой верификации, ориентирован на доказательство ПП довольно узкого класса и применим только для этой цели: он не позволяет в случае появления противоречия определить, является ли оно следствием ошибки в программе, или же ошибка содержится в самом доказательстве или в индуктивных утверждениях. Процесс демонстрации истинности условий верификации и их генерация осуществляется вручную и неудобен для автоматизации. Тем не менее с помощью этого метода удалось доказать правильность нескольких нетривиальных алгоритмов. Наиболее интересны доказательство Р. Лондоном алгоритма сортировки дерева, а также многочисленные числовые и нечисловые примеры Э Дейкстры. Подход Флойда используется при проектировании программ обработки данных методом формализованных технических заданий. В процессе проектирования обосновывается правильность результатов посредством установления соответствия между техническим заданием и его реализацией и приводятся определения различных свойств проектируемых объектов. Анализ результатов проектирования выполняется путем математического исследования и доказательства соответствующих утверждений.

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

1. Формулировка утверждений о состоянии переменных программы в некоторых ее точках.

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

3. Доказательство непротиворечивости полученных условий верификации.

4. Доказательство завершимости программы (в процессе доказательства правильности или отдельно).