Программа как математический объект: Методические указания для самостоятельного изучения темы и выполнения РГР, страница 17

Например, дана программа if p then g elseh fi; при чтении мы предполагаем, что программа имеет функцию f. Задача верификации в этом случае заключается в доказательстве  того, что мы сделали верное предположение

                                       f = [if p then g else h fi]

Если перед нами стоит задача проектирования, то, как правило, нам известна функция и нам надо раскрыть её с помощью такой элементарной программы, программная функция которой совпадала  бы с исходной.

                                      f = [if p then g else h fi]

Часто задача ставится таким образом, что нам известна функция и известна программа, возможно её реализующая, и нам необходимо доказать это соответствие или опровергнуть его. И опять нам необходимо доказать выше приведённое равенство: f = [if p then g elseh fi]. Таким образом, во всех трёх случаях задачи верификации ( т.е. доказательство правильности программы) идентичны.

4.2 Алгебра корректности структурированных программ

Когда речь идёт о правильности программ, задача доказательства правильности программы связана с ответом на один из двух вопросов:

верно ли, что

 1) f = [P]?     или       2) f  Ì [P]?

Первый вопрос  является вопросом полной правильности, второй вопрос - вопросом достаточной правильности. При полной правильности программа P вычисляет только правильные значения функции f от её аргументов, ( т. е., P не определена для аргументов, не принадлежащих области определения f). В случае достаточной правильности P может вычислять значения функции для аргументов, нее принадлежащих области определения f. Например,

F₁ = ( x ¹ y ® x, y := y, x)

P1 = while x ³ y do x, y := y, x od

P2 = do x, y := y, x until x ¹ y od

P3 = if x ³ y then x, y := y, x fi

Программные функции:

[P1]={(X,Y)|(x>y®x, y:= y, x | x<y®x, y:= x, y)=(x¹y®x, y:=min(x, y), max( y, x) }

[P2] = {(X, Y)|(x ¹  y® x, y := y, x )}

[P3]={(X,Y)|(x³ y® x, y := y, x | истина® x, y := x, y)=(x, y:=min(x, y),max(x, y)}

Следовательно, из перечисленных выше программ, только P2 удовлетворяет полной правильности F₁ = [P2], остальные не удовлетворяют даже достаточной правильности. Если рассмотреть функцию F₂ = (x ³ y ®x, y := y, x) ,то программа P2 удовлетворяет достаточной правильности f ₂ Ì [P3]

Если P не является элементарной программой, но является структурированной программой, то благодаря  алгебре структурированных программ возможна декомпозиция P на элементарные составляющие. Декомпозиция ведёт к снижению трудоёмкости доказательства правильности программы P.  Допустим, например, необходимо доказать, что составная программа F = if p then GelseH fi выполняет нужную функцию f. При этом G, H в свою очередь являются программами. Вместо того чтобы попытаться доказать правильность сложной программы, что может быть весьма затруднительным, предположим вид функций [G] и [H] и попытаемся доказать полную правильность составляющих  программ, т.е. то, что g =[G] и h = [H].

В случае успешного доказательства можно, используя аксиому замещения, упростить исходную программу и свести задачу к доказательству следующего равенства:  f = [if p theng else h fi].

Если это равенство будет доказано, то тем самым будет доказана полная правильность, т.е. равенство f = [F]. Однако, если какая-нибудь из трёх программ удовлетворяет только условию достаточной правильности, то программа F будет лишь достаточной правильной. Например, для программы

SUB = whilex>0 L y>0  do x:= x - 1; y:= y - 1 od;

if y > 0 then x := -y fi ; free y

схема доказательства  будет следующей:

полная правильность                                достаточная правильность

1) s = [if y > 0 then x := -y fi ]                    s Ì [if y > 0 then x := -y fi ]

2) d = [ x:= x -1; y:= y -1]                           d Ì [ x:= x -1; y:= y -1]

3) m = [while  x>0 L y>0  do  d  od]         m Ì [while  x>0 L y>0  do  d  od]