Сформулируем правила (аксиомы) К.Хоара, которые определяют предусловия как достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желаемым постусловиям.
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