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

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

{P(x)} A || B {Q(x, y, z)} [8]. (2.17)

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

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

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

Правило LP1. P(x) ├ P_A(x) & P_B(x).

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

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

Лемма 2.10. Допустим, спецификация параллельного оператора (2.17) реализуема, операторы A и B однозначны в области предусловий и корректны, а их спецификации - однозначны. Если правила LP1, LP2 и LP3 истинны (т. е. правая часть доказуема из левой части для каждого правила), то параллельный оператор (2.17) является корректным.

Доказательство. Поскольку операторы A и B однозначны, то и параллельный оператор (2.17) является однозначным. Поскольку спецификация оператора (2.17) реализуема, в соответствии с теоремой 2.1 для доказательства леммы достаточно доказать истинность формулы:

P(x) & Q(x, y, z) Þ LS(A || B)(x, y, z).

В соответствии с (2.2) формула LS(A || B)(x, y, z) эквивалентна LS(A)(x, y) & LS(B)(x, z).

Пусть истинны P(x) и Q(x, y, z). Докажем истинность LS(A)(x, y) и LS(B)(x, z). Из истинности предусловия P(x) по правилу LP1 следует истинность P_A(x) и P_B(x). По правилам LP2 и LP3 становятся истинными Q_A(x, y) и Q_B(x, z). Для предикатов A и B выполняются условия леммы 2.9. Поэтому истинны формулы:

P_A(x) & Q_A(x, y) Þ LS(A)(x, y);

P_B(x) & Q_B(x, z) Þ LS(B)(x, z).

Поскольку посылки этих формул истинны, то истинны LS(A)(x, y) и LS(B)(x, z). □