Составители:
Рубрика:
1
0
1
q
r
p=
Рис. 2.9.
Рис. 2.10.
1
0
f
1
r
q
f
1
В этом примере один узел 1, для которого определяем функцию f
1
,
исходя из E-схемы на рис.2.10:
(2.14)
f ={(X,Y) ⎥ r(X) →f
1 1
° q(X) ; ⎯r(X) →Y=X}.
Очевидно, что выполняется соотношение [P]=f
1
. Однако
определение [P] таким образом не всегда возможно, т.к. не удается
разрешить выражение типа (2.14) относительно f
.
1
Второй подход основан на использовании инвариантов цикла.
Пусть в предыдущем примере (рис.2.8) имеем поле данных (u,v),
предикат p="v≠0", а функцию блока q конкретизируем как
u,v:= u+1, v-1. Предикат u+v= u
+v , где u ,v
0 0 0 0
- начальные значения u
и v, принимает значение "истинно" в трех случаях:
• при входе в цикл,
• при каждой итерации,
• при выходе из цикла.
+v
Следовательно, предикат u+v= u
0 0
является инвариантом. При
выходе из цикла v=0, откуда u+0=u
+v и u=u +v
0 0 0 0
. Следовательно,
функция программы
[P]=(u,v≥0 → u,v:=u+v,0).
Дополнительные сведения по логике предикатов можно найти в
[5, 7, 10, 11]. Методика верификации алгоритмов и программ
рассмотрена подробно в [6].
Глава 3
119
Страницы
- « первая
- ‹ предыдущая
- …
- 33
- 34
- 35
- 36
- 37
- …
- следующая ›
- последняя »
