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

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

A1. Аксиома присваивания: { Ro } 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 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 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;

while y £ r do

Begin

r:= r - y; q:= q + 1

end;

выдать(q,r);

Сформулируем постусловие

R: (r < y) AND (x = y*q + r)

Нужно доказать, что

{y > 0 AND x/y} S {(r < y) AND (x = y*q + r)}.

Доказательство.

1. Очевидно, что Q => x = x + y * 0.

2. Применим аксиому A1 к оператору r:= x, тогда получим { x = x + y * 0 } r:= x { x = r + y * 0 }

3. Аналогично, применяя A1 к оператору q:= 0, получим: { x = r + y * 0 } q:= 0 { x = r + y*q }

4. Применяя правило A3 к результатам пунктов 1 и 2, получим { Q } r:= x { x = r + y * 0 }

5. Применяя правило A4 к результатам пунктов 4 и 3, получим { Q } r:= x; q:= 0 { x = r + y*q }

6. Выполним равносильное преобразование x = r + y * q AND y £ r => x = (r - y) + y*(q + 1)

7. Применяя правило A1 к оператору r:= r - y, получим {x = (r - y) + y*(q + 1)} r:= r - y {x = r+ y*(q+1)}

8. Для оператора q:= q + 1 аналогично получим { x = r + y*(q + 1) } q:= q + 1 { x = r + y*q }

Применяя правило A4 к результатам пунктов 7 и 8, получим

{ x = (r - y) + y*(q + 1) } r:= r - y; q:= q + 1 { x = r + y*q }

Применяя правило A2 к результатам пунктов 6 и 9, получим

{ x = r + y*q AND y £ r } r:= r - y; q:= q + 1 { x = r + y*q }

Применяя правило A8 к результату пункта 10, получим

{x = r + y*q } while y £ r do begin r:= r - y; q:= q + 1 end { NOT (y <= r) AND (x = r + y*q) }

Утверждение x = r + y*q является инвариантом цикла, так как значение его остается истинным до цикла и после выполнения каждого шага цикла.

Применяя правило A4 к результатам пунктов 5 и 11, получаем то, что требовалось доказать,

{ Q } S { NOT (y £ r) AND (x = r + y*q) }

Осталось доказать, что выполнение программы заканчивается.

Доказывать будем от противного, т.е. предположим, что программа не заканчивается. Тогда должна существовать бесконечная последовательность значений r и q, удовлетворяющая условиям

1) y £ r;

2) r, q Î Nat.

Но значение r на каждом шаге цикла уменьшается на положительную величину: r:= r - y (y > 0). Значит, последовательность значений r и q является конечной, т.е. найдется такое значение r, для которого не будет выполняться условие y £ r и циклический процесс завершится.

Теоретические модели вычислительных процессов