Page 72 - 6571

ся в стані, що задовольняє кон’юнкції предикатів P . Якщо всі
i
процеси завершуються, кінцевий стан задовольнятиме кон’юнкції
предикатів Q . Таким чином, отримаємо наступне правило виве-
i
дення.

{ }P S i { }Q вільні від взаємного впливу
i
i

{P Ù ... PÙ n }
1
coS ; / /.../ / S oc
1 n
{Q Ù ... QÙ } .
1 n
При цьому, щоб висновок був істинним, процеси та їх обґру-

нтування не повинні впливати один на одного.
Один процес втручається в інший (впливає на інший), якщо
він виконує присвоєння, що порушує твердження в іншому про-
цесі. Твердження характеризують, що в процесі передбачається

істинним до і після виконання кожного оператора. Таким чином,
якщо один процес присвоює значення спільній змінній і тим са-
мим робить недійсним припущення іншого процесу, то обґрунту-

вання іншого процесу стає помилковим.
Як приклад розглянемо наступну програму:

{x == 0}
co <x = x+1; > // <x = x+2; >oc
{x == 3}

Якщо виконання програми починається з стану, в якому зна-
чення x рівне 0, то при завершенні програми значення x буде рів-

ним 3. Але що ж буде істинним для кожного процесу? Припу-
щення, що значення x буде рівним 0 на початку виконання кож-
ного з них є невірним, оскільки порядок виконання операторів не

є детермінованим. Зокрема, на припущення, що на початку вико-
нання процесу змінна x має значення 0, впливає інший процес,
який може бути виконаним першим.
Взаємне невтручання. Нехай a – дія присвоєння в деякому

процесі, а pre ( )a – його передумова. Нехай C – критичне твер-

дження в іншому процесі. Якщо необхідно, перейменуємо лока-
льні змінні в процесітак, щоб їхні імена відрізнялися від імен ло-
кальних змінних в дії a і передумові pre ( )a . Тоді дія не втруча-

ється в (не впливає на) C , якщо наступне твердження є теоремою
логіки програмування:

71