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

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

{P(x)} A || B {Q(x, y, z)}. (2.11)

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

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

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

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

Правило RP2. Q_A(x, y), Q_B(x, z) ├ Q(x, y, z).

Лемма 2.4. Пусть предусловие P(x) истинно. Допустим, операторы A и B корректны. Если правила RP1 и RP2 истинны (т. е. правая часть доказуема из левой части для каждого правила), то параллельный оператор (2.11) является корректным.

Доказательство. Для доказательства корректности оператора (2.11) в соответствии с формулой (2.10) достаточно доказать реализуемость LS(A || B)(x, y, z) и выводимость постусловия 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) по правилу RP1 следует истинность P_A(x) и P_B(x). Далее, по правилу E2 становятся истинными формулы $y. LS(A)(x, y) и $z. LS(B)(x, z). Их конъюнкция определяет реализуемость LS(A || B)(x, y, z).

Докажем выводимость постусловия Q(x, y, z) из LS(A)(x, y) & LS(B)(x, z). Допустим, истинна формула LS(A)(x, y) & LS(B)(x, z). Применим правило E3 для P_A(x) и P_B(x), истинность которых определена выше. Получаем истинность формул LS(A)(x, y) Þ Q_A(x, y) и LS(B)(x, z) Þ Q_B(x, z). Как следствие, будут истинны Q_A(x, y) и Q_B(x, z). Применяя правило RP2, получаем истинность постусловия Q(x, y, z). □