Правила корректности для условного оператора

Рассмотрим спецификацию условного оператора в виде тройки Хоара:

{P(x)} if ( C) A else B {Q(x, y)}. (2.13)

Предположим, что операторы A и B корректны. Их спецификации представлены тройками:

{P_A(x)} A {Q_A(x, y)}, {P_B(x)} B {Q_B(x, y)}.

Определим правила, гарантирующие корректность условного оператора (2.13).

Правило RC1. P(x) & C ├ P_A(x).

Правило RC2. P(x) & ØC ├ P_B(x).

Правило RC3. P(x) & C & Q_A(x, y) ├ Q(x, y).

Правило RC4. P(x) & ØC & Q_B(x, y) ├ Q(x, y).

Отметим, что условие C зависит от x.

Лемма 2.6. Пусть предусловие P(x) истинно. Допустим, операторы A и B корректны. Если правила RC1, RC2, RC3 и RC4 истинны, то условный оператор (2.13) является корректным.

Доказательство. Для оператора (2.13) необходимо доказать формулу (2.10). В ней дважды встречается подформула LS(if ( C) A else B)(x, y), определяемая согласно (3) в виде:

(C Þ LS(A)(x, y)) & (ØC Þ LS(B)(x, y)). (2.14)

В соответствии с формулой (2.10) достаточно доказать реализуемость формулы (2.14) и выводимость постусловия Q(x, y) из (2.14).

Допустим, что условие C истинно. Из истинности предусловия P(x) по правилу RC1 следует истинность P_A(x). По правилу E2 истинна формула $y. LS(A)(x, y). Далее будет истинной формула $y. (C Þ LS(A)(x, y)). Из истинности C следует истинность формулы ØC Þ LS(B)(x, y) и, следовательно, формулы $y. [(C Þ LS(A)(x, y)) & (ØC Þ LS(B)(x, y))]. Это обеспечивает реализуемость формулы (2.14) в случае истинности C. Реализуемость (2.14) в случае ложности C доказывается аналогичным образом.

Докажем выводимость постусловия Q(x, y) из формулы (2.14). Допустим, истинна формула (2.14). Пусть C истинно. Тогда истинно LS(A)(x, y). По правилу RC1 истинно P_A(x). По правилу E3 истинна формула LS(A)(x, y) Þ Q_A(x, y), а значит – и Q_A(x, y). Таким образом, истинна правая часть правила RC3. Тогда истинна левая часть правила, т. е. истинно постусловие Q(x, y). Доказательство истинности постусловия Q(x, y) для случая, когда C ложно, проводится аналогично с использованием правила RC4. □