Page 59 - 4868

57 Ошибка! Стиль не определен.

co S ; // S ; // ... // S ; oc;
1 2 n
Припустимо, що для кожного оператора наступний вираз є істинним:

{ }P S { }Q
i i i
У відповідності з інтерпретацією трійок це означає, що якщо S
i
починається в стані, що задовольняє P та S , і завершується, то стан
i i
задовольняєQ .Для того щоб ця інтерпретація залишалася вірною при
i
паралельному виконанні, процеси повинні починатися в стані, що
задовольняє кон’юнкції предикатів P .Якщо всі процеси завершуються,
i
кінцевий стан задовольнятиме кон’юнкції предикатів Q .Таким чином,
i
отримаємо наступне правило виведення.
{ }P S { }Q вільні від взаємного впливу
i i i
{P  ... P }
1 n
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, якщо наступне твердження є теоремою
логіки програмування:
{C  pre ( )} { }a a C (1)