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

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

{P(x)} A; B {Q(x, y)}. (2.12)

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

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

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

Правило RS1. P(x) ├ P_A(x) & "z (Q_A(x, z) Þ P_B(z)).

Правило RS2. P(x) & $z (Q_A(x, z) & Q_B(z, y)) ├ Q(x, y).

Лемма 2.5. Пусть предусловие P(x) истинно. Допустим, операторы A и B корректны. Если правила RS1 и RS2 истинны, то оператор суперпозиции (2.12) является корректным.

Доказательство. В соответствии с формулой (2.10) достаточно доказать реализуемость LS(A; B)(x, y) и выводимость постусловия Q(x, y) из LS(A; B)(x, y). В соответствии с (2.1) формула LS(A; B)(x, y) определена как $z.(LS(A)(x, z) & LS(B)(z, y)).

Из истинности предусловия P(x) по правилу RS1 следует истинность формул P_A(x) и "z (Q_A(x, z) Þ P_B(z)). Из истинности P_A(x) и правила E2 следует истинность формулы $z. LS(A)(x, z). Допустим, для некоторого z₀ формула LS(A)(x, z₀) истинна. Из истинности P_A(x) и правила E3 следует истинность LS(A)(x, z₀) Þ Q_A(x, z₀). Как следствие, истинно Q_A(x, z₀). Далее, из истинности формулы "z (Q_A(x, z) Þ P_B(z)) следует истинность P_B(z₀). По правилу E2 истинна формула $y LS(B)(z₀, y). Далее, истинна конъюнкция LS(A)(x, z₀) & $y LS(B)(z₀, y), и затем – формула $y. $z. (LS(A)(x, z) & LS(B)(z, y)), т. е. доказана реализуемость LS(A; B)(x, y).

Докажем выводимость постусловия Q(x, y) из LS(A; B)(x, y). Пусть LS(A; B)(x, y) истинно, т. е. истинна формула $z.(LS(A)(x, z) & LS(B)(z, y)). Пусть формула истинна для некоторого z₁. По правилу E3 истинна формула LS(A)(x, z₁) Þ Q_A(x, z₁) и далее – Q_A(x, z₁). Истинность Q_A(x, z₁) и "z (Q_A(x, z) Þ P_B(z)) влечет истинность P_B(z₁). По правилу E3 истинно LS(B)(z₁, y) Þ Q_B(z₁, y). Поскольку LS(B)(z₁, y) истинно, то истинно Q_B(z₁, y). Таким образом, истинна правая часть правила RS2, а значит – и левая, т. е. истинно постусловие Q(x, y). □