3.1.4 Доказательство свойств ветвящихся программ

Семантика условного оператора позволяет сформулировать следующее правило вывода свойств условного оператора.

Пусть для операторов $Р$ и $Q$ и утверждений $\varphi$ , $\gamma$ и $\beta$ имеют место свойства { $\varphi, \beta$ } $P$ { $\gamma$ } и { $\varphi,\neg \beta$ } $Q$ { $\gamma$ }. Тогда имеет место свойство:

{ $\varphi$ } if$\beta$then P else Q end{ $\gamma$ }

В качестве примера рассмотрим применение этого правила для доказательства свойства

{ True } if X $>$ Y then Z := X else Z := Y end{ Z $\geq$ X, Z $\geq$ Y}

Исходя из семантики оператора присваивания имеем
 

$\{ X\geq X, X > Y \} Z := X \{ Z \geq X, Z > Y \}$ и
$\{ Y \geq X, Y \geq Y\} Z :=Y \{Z \geq X, Z \geq Y \}$,

которые по правилу следствий можно переписать следующим образом:

$\{ True, X > Y \} Z := X \{ Z \geq X, Z \geq Y \}$

и $\{ True, \neg (X > Y) \} Z := Y \{ Z \geq X, Z \geq Y \}$.

Отсюда, применяя правило условного оператора, получаем интересующее нас свойство. Используя известную связь условных и выбирающих операторов, можно сформулировать аналогичные правила вывода свойств для операторов выбора и условного оператора в сокращенной форме. Например, для оператора

case B of '=' : S1 |  '*', '+ ' :S2 |  '-': S3 end,

где $В$ -- некоторое выражение, вычисляющее литерное значение, а  S1, S2, S3 -- произвольные последовательности операторов, соответствующее правило имеет следующий вид.

Пусть для некоторых утверждений $\varphi$ и $\gamma$ справедливы три свойства$\{ \varphi, B = '='\} S1 \{ \gamma \},\{ \varphi, (B ='*') \vee (B = '+')\} S2 \{ \gamma \}$ и $\{ \varphi, B = '-' \} S3 \{ \gamma \}.$ Тогда имеет место следующее свойство:

{ $\varphi$ } case B of '=' : S1 |  '*', '+ ' :S2 |  '-': S3 end{ $\gamma$ }.
 

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