Правила верификации К. Хоара

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

A1. Аксиома присваивания: {R_o} x := Е {R}

Неформальное объяснение аксиомы: так как x после выполнения будет содержать значение Е, то R будет истинно после выполнения, если результат подстановки Е вместо x в R истинен перед выполнением. Таким образом, R_o = R(x) при x = E. Для R_o вводится обозначение: R_o = R^x_Е (у Вирта) или R_x→Е (у Дейкстры), что означает, что x заменяется на Е.

Аксиома присваивания будет иметь вид:{R^x_Е} 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 elseS2 {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 B do 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;