Правила верификации К. Хоара
Сформулируем правила (аксиомы) К.Хоара, которые определяют предусловия как достаточные предусловия, гарантирующие, что исполнение соответствующего оператора при успешном завершении приведет к желаемым постусловиям.
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 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 => q = (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 }.
9.Применяя правило A4 к результатам пунктов 7 и 8, получим
{ x = (r - y) + y* (q + 1)} r:= r - y; q:= q + 1 { x = r + y*q }.
10.Применяя правило A2 к результатам пунктов 6 и 9, получим
{ x = r + y*q AND y r } r:= r - y; q:= q + 1 { x = r + y*q }.
11.Применяя правило 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 является инвариантом цикла, так как значение его остается истинным до цикла и после выполнения каждого шага цикла.
12.Применяя правило 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 и циклический процесс завершится.
Дата добавления: 2015-12-20; просмотров: 18; Мы поможем в написании вашей работы! |
Мы поможем в написании ваших работ!