Правила верификации К. Хоара.
Использование утверждений в программах.
Утверждения используются для доказательства правильности программ. Тогда утверждения необходимо формулировать в некоторой формальной логической системе. Обычно используется исчисление предикатов первого порядка.
Исчисление - это метод или процесс рассуждений посредством вычислений над символами. В исчислении предикатов утверждения являются логическими переменными или выражениями, имеющими значение T - истина или F - ложь. Наша цель - при написании программы некоторым способом доказать истинность утверждения (2.2) - триады Хоара {Q} S {R}. Для этого нужно уметь записывать его в исчислении предикатов и формально доказывать его истинность.
Предикат, помещенный в программу, был нами назван утверждением. Утверждается, что он истинен в соответствующий момент выполнения программы. В предусловии Q нужно отражать тот факт, что входные переменные получили начальные значения. Для обозначения начальных значений будем использовать большие буквы.
Пример 2.8. Пусть надо определить приближенное значение квадратного корня: s = sqrt(n), где n, s Î Nat. Определим постусловие в виде:
R: s*s £ n < (s+1)*(s+1).
Пример 2.9. Даны целочисленные n > 0 и массив a[1,...,n]. Отсортировать массив, т.е. установить
R: (" i: 1 £ i < n: a[i] £ a[i+1]).
Пример 2.10. Определить x как максимальное значение массива a[1,...,n]. Определим постусловие:
R: {x = max({y | y Í a})}.
Для построения программы следует определить математическое понятие max. Тогда
R: {($ i: 1 £ i £ n: x = a[i]) AND (" i: 1 £ i £ n: a[i] = x)}.
Пример 2.11. Пусть имеем программу S обмена значениями двух целых переменных a и b. Сформулируем входное и выходное утверждения программы и представим программу S в виде предиката:
{ a = A AND b = B } S { a = B AND b = A }, (2.4)
где A, B - конкретные значения переменных a, b.
Программа вместе с утверждениями между каждой парой соседних операторов называется наброском доказательства. Последовательно, для каждого оператора программы формулируя предикат (2.4), можно доказать, что программа удовлетворяет своим спецификациям. Представим набросок доказательства для программы S:
{ a = A AND b = B }
r := a; { r = a AND a = A AND b = B };
a := b; { r = a AND a = B AND b = B };
b := r; { a = B AND b = A }.
Не обязательно набросок доказательства должен быть настолько полным. Для документирования программы нужно вставить достаточно утверждений, чтобы программа стала понимаемой.
Программа, содержащая утверждения для ее документирования, называется аннотированной программой. Чтобы использовать утверждения для доказательства правильности программы, необходимы соответствующие правила верификации.
Сформулируем правила (аксиомы) К.Хоара, которые определяют предусловия как достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желаемым постусловиям.
A1. Аксиома присваивания: { Ro } x := Е { R }
Неформальное объяснение аксиомы: так как x после выполнения будет содержать значение Е, то R будет истинно после выполнения, если результат подстановки Е вместо x в R истинен перед выполнением. Таким образом, Ro = R(x) при x = E. Для Ro вводится обозначение: Ro = RxЕ (у Вирта) или Rx→Е (у Дейкстры), что означает, что x заменяется на Е.
Аксиома присваивания будет иметь вид:{RxЕ} x := Е {R}.
Сформулируем два очевидных правила монотонности.
A2. Если известно: { Q } S { P } и { P } => { R }, то { Q } S { R }
A3. Если известно: { Q } S { P } и { R } => { Q }, то { R } S { P }
Пусть S - это последовательность из двух операторов S1; S2 (составной оператор).
A4. Если известно:{ Q } S1 { P1 } и { P1 } S2 { R }, то { Q } S { R }.
Это правило можно сформулировать для последовательности, состоящей из n операторов.
Сформулируем правило для условного оператора (краткая форма).
A5. Если известно:
{ Q AND B } S1 { R } и { Q NOT B } => { R },то { Q } if B then S1 { R }.
Правило A5 соответствует интерпретации условного оператора в языке программирования.
Сформулируем правило для альтернативного оператора (полная форма условного оператора).
A6. Если известно: { Q AND B } S1 { R } и { Q NOT B } S2 { R },то { Q } if B then S1 else S2 { R }.
Сформулируем правила для операторов цикла.
Предусловия и постусловия циклаuntil удовлетворяют правилу:
A7. Если известно: { Q AND NOT B } S1 { Q }, то { Q }repeat S1 until B { Q AND NOT B }
Правило отражает инвариантность цикла. В данном случае единственная операция - это выполнение шага цикла при условии истинности Q вначале.
Предусловия и постусловия цикла while удовлетворяют правилу:
A8. Если известно: { Q AND B } S1 { Q } , то { Q } while Bdo S1 { Q AND NOT B }
Правила A1 - A8 можно использовать для проверки согласованности передачи данных от оператора к оператору, для анализа структурных свойств текстов программ, для установления условий окончания цикла и для анализа результатов выполнения программы.
Пример 2.12. Пусть надо определить частное q и остаток r от деления x на y.
Входные данные x, y и выходные данные q, r Î Nat, причем y > 0.
Задать(x,y); /* x,y получают конкретные значения X,Y */
r := x; q := 0;
while y £ r do