nextupprevious
Next:2.3.5 Упражнения Up:2.3 Доказательство свойств программ
Previous:2.3.3 Утверждения как множества

2.3.4 Метод промежуточных утверждений

Пусть $Р$ -- некоторая последовательность операторов, а $\varphi$ и $\psi$ -- некоторые утверждения о значениях переменных, используемых в P$Р,$ соответственно в начальном и конечном состояниях выполнения P$Р$. $\varphi$ называется предусловием, а $\psi$ -- постусловием для $P.$

Говорят, что $Р$ является частично правильной относительно ее спецификации, заданной в виде утверждений $\varphi$ и $\psi$ (или, что то же самое, обладает свойством частичной правильности {$\varphi$}P{$\psi$}), если для любых начальных значений переменных, относительно которых справедливо $\varphi$, выполнение действия $Р$ (если оно определено) дает такие конечные значения переменных, для которых истинно утверждение $\psi$. Примеры свойств: 

$\{x=10\} x:=x+2 \{x=12\}$,
$\{x=3, y=5 \} z:=x+y \{x=3,y=5,z=8\}$,
$\{x=A, y=B\} x:=x+y \{x=A+B, y=A\}$ для любых $A$ и $B$.

Заметим, что частичная правильность ничего не говорит о завершаемости $P$. Так, например, в последнем свойстве оператор не применим, если сумма $A+B$ превышает MaxInt.

Свойство правильности программы $Р$ относительно внешней ее спецификации, заданной в виде утверждений $\varphi$ и $\psi$, означает справедливость свойства частичной правильности {$\varphi\} P \{\psi$}, а также свойства завершаемости программы $Р$ -- нормального завершения выполнения программы $Р$ на любом начальном состоянии, удовлетворяющем утверждению $\varphi$.

Идея метода промежуточных утверждений для доказательства частичной правильности Паскаль-программ состоит в построении исчисления свойств частичной правильности программ и их частей, аксиомами в котором выступают свойства элементарных операторов (операторов присваивания и пустых операторов), а правила вывода связаны с другими конструкциями языка и позволяют выводить свойства этих конструкций из свойств составляющих его компонент или операторов присваивания (как это имеет место для операторов ввода-вывода).

При этом ход построения доказательства заданного свойства частичной правильности всей Zonnon-программы (или ее части) может состоять в последовательном применении правил вывода свойств, сводящих исходное свойство к некоторым свойствам образующих ее частей -- в конечном счете к группе свойств частичной правильности составляющих ее операторов присваивания, либо в его выводе из свойств операторов присваивания. Цель -- построить вывод заданного свойства частичной правильности. В этом доказательстве (выводе) могут использоваться также все традиционные аксиомы и правила вывода соответствующего логического исчисления и той области (например, арифметики), к которой относится задача, решаемая программой.

Семантика пустого оператора $S$ описывается очевидной аксиомой пустого оператора: {$\varphi$}$S${$\varphi$} для любого утверждения $\varphi.$

В соответствии с семантикой оператора присваивания $V := Е$ имеем следующую аксиому оператора присваивания: {$\varphi\}V := E \{\psi$}, где $\varphi$ и $\psi$ -- любая пара утверждений таких, что $\varphi$ -- утверждение, получающееся из $\psi$ подстановкой выражения $Е$ вместо вхождения переменной $V.$ Например, справедливы свойства: $\{x+10 =30\} x:=x+10 \{x=30\},$$\{(x+10)* z > y \} x:=x+10\{x* z > y \}$.

Следующие два правила завершают построение исчисления свойств Zonnon-программ, использующих лишь уже рассмотренные конструкции языка; в дальнейшем они будут дополнены правилами и для других конструкций.

Правило вывода следствий формулируется следующим образом. Пусть для фрагмента программы $Р$ имеет место
{$\varphi\} P \{\psi$}, и пусть утверждение $\gamma$ сильнее $\varphi$, а утверждение $\delta$ слабее $\psi$. Тогда имеет место {$\gamma\} P\{\delta$}. Например, из рассмотренных выше свойств оператора присваивания $x:= x+10$ можно вывести свойства: $\{x=20,$$y=7\}$$x:= x+10$$\{x=30\}$, $\{(x+10)* z > y+5\} x:=x+10 \{x*z>y-3\}$.

Правило вывода свойств последовательности операторов имеет следующий вид. Пусть $Р$ и$Q$ -- последовательности операторов, обладающие соответственно свойствами {$\varphi\} P \{\gamma$} и {$\gamma\} Q \{\psi$}. Тогда для последовательности $R = P;Q$ имеет место свойство {$\varphi\} R \{\psi$}.

В качестве примера применения метода промежуточных утверждений покажем, что $\{x=A, y=B\} x := x+y; y :=x-y; x := x-y \{x=B, y=A\}$ для любых целых чисел A$А$ и B$В.$

По аксиоме оператора присваивания имеем следующие свойства операторов, составляющих анализируемую последовательность:
$\{x-y=B,y=A\} x := x-y \{x=B, y=A\},$

$\{x-(x-y)=B, x-y=A\} y := x-y \{x-y=B, y=A\},$

$\{(x+y)-((x+y)-y)=B, (x+y)-y=A\} x := x+y \{x-(x-y)=B, x-y=A\}$.

Применяя правило вывода следствий, из последнего свойства получаем

$\{x=A,y=B\} x := x+y \{x-(x-y)=B, x-y = A\}$.

Отсюда и из первых двух свойств по правилу вывода свойств последовательности операторов получаем: сначала --

$\{x=A,y=B\} x := x+y; y := x-y\{x-y=B, y=A\}$,

а затем --

$\{x=A, y=B\} x := x+y; y :=x-y; x := x-y \{x=B, y=A\}$.

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

В дальнейшем в тексты программ мы будем включать утверждения, размещая их в скобках комментариев. Такие формализованные комментарии называются аннотациями; они определяют те свойства состояний, которые справедливы в соответствующие моменты выполнения программы. Аннотированная программа может выступать в качестве доказательства своей правильности. Например, программу $Х10С$ возведения в десятую степень можно дополнить следующими аннотациями:

module X10D;
    var A,B : integer;
begin   (*$\{Input=X\}$ *)
    read(A);      (* {$A =X, \mid Input2 \mid = \mid Output \mid = 0$}*)
    B := A$*$A;  (* {$ B = Степ2(X,2), А=Х,\mid Input2 \mid = \mid Output \mid = 0$}*)
    B := B$*$B;  (*{$B = Степ2(X,4), A=X,\mid Input2 \mid = \mid Output \mid =0$}*)
    B := B$*$A;  (* {$B = Степ2(Х,5), А=Х,\mid Input2 \mid = \mid Output \mid =0$}*)
    B := B$*$B;  (*{$B = Степ2(Х,10),A=X,\mid Input2 \mid = \mid Output \mid= 0$}*)
    write(B) (* {$Output = Степ2(X,10)$}*)
end X10D.

Нетрудно убедиться, что программа удовлетворяет спецификации "Быстрое возведение в десятую степень", просто показав для каждой тройки (аннотация1, оператор, аннотация2) справедливость свойства {утверждение1} оператор {утверждение2} и соответствующего свойства завершаемости. Вместе с тем следует отметить, что программа X$Х10D$ перегружена утверждениями и часть ее аннотаций очевидна и легко восстановима из текста программы. Это говорит о том, что не обязательно включать в текст программы все известные вам утверждения о программе; нужно вставлять достаточно утверждений, чтобы программа стала понимаемой, однако не так много, чтобы она затерялась в них.

Следующий пример показывает, что иногда при описании свойств программ удобно использовать дополнительные ("внепрограммные") переменные. Рассмотрим следующую старинную задачу о переправе на другой берег волка, козы и капусты. На левом берегу реки находятся лодочник с лодкой, волк, коза и капуста. Их нужно переправить на правый берег. Лодка, помимо лодочника, вмещает лишь одного из троих (волка, козу или капусту). При этом нельзя оставлять наедине волка с козой, а также козу с капустой. Правильность следующего решения этой задачи очевидна из аннотаций, использующих две дополнительные переменные ЛевыйБерег и ПравыйБерег:

module ПЕРЕПРАВА;
begin

(*{ЛевыйБерег=(лодочник, волк, коза, капуста), ПравыйБерег=()}*)
writeln('Перевезти козу.');
(*{ЛевыйБерег=(волк, капуста), ПравыйБерег=(лодочник, коза)}*)
writeln('Переправиться без груза.');
(*{ЛевыйБерег=(лодочник, волк, капуста), ПравыйБерег=(коза)}*)
writeln('Перевезти волка.');
(*{ЛевыйБерег=(капуста), ПравыйБерег=(лодочник, волк, коза)}*)
writeln('Перевезти козу.');
(*{ЛевыйБерег=(лодочник, коза, капуста), ПравыйБерег=(волк)}*)
writeln('Перевезти капусту.');
(*{ЛевыйБерег=(коза), ПравыйБерег=(лодочник, волк, капуста)}*)
writeln('Переправиться без груза.');
(*{ЛевыйБерег=(лодочник, коза), ПравыйБерег=(волк, капуста)}*)
writeln('Перевезти козу.')
(*{ЛевыйБерег=(), ПравыйБерег=(лодочник, волк, коза, капуста)}*)
end ПЕРЕПРАВА.

Next:2.3.5 Упражнения Up:2.3 Доказательство свойств программ
Previous:2.3.3 Утверждения как множества

© В.Н. Касьянов, Е.В.Касьянова, 2004