Page 71 - 6571

У другій трійці постумова слабша, ніж у першій, оскільки
вона характеризує більше станів (значення x може як бути рівним
1, так і взагалі бути невід’ємним числом).

8.3 Семантика паралельного виконання

Оператор паралельного виконання co виступає оператором
керування. Отже, його дія описується правилом виведення, що

враховує вплив паралельного виконання. Процеси у свою чергу
складаються з послідовних операторів і операторів синхронізації,
таких як оператор await.
З погляду часткової коректності дія оператора < awa

t (B) S; > найбільш схожа на дію оператора іf, для якого
умова B істинна, коли починається виконання S . Отже, правило

висновку для оператора await аналогічне правилу виведення для
оператора іf.
{P Ù B } { }S Q
.
{ }P < await ( ) ; { }B S > Q

Дана гіпотеза говорить наступне: «якщо виконання S почи-
нається в стані, коли P та B істинні, і завершується, то Q також

буде істинним». Отже, оператор await призводить до стану, що
задовольняє Q , якщо починається в стані, що задовольняє P (за

умови, що виконання оператора await завершується). Правила
виведення нічого не говорять про можливі затримки виконання,
оскільки затримки впливають на властивість живучості, а не на
властивість безпеки.

Тепер розглянемо вплив паралельного виконання, заданого,
наприклад, наступним оператором:

co S ; // S ; // ... // S ; oc;
1 2 n

Припустимо, що для кожного оператора наступний вираз є
істинним:

{ }P S i { }Q
i
i
У відповідності з інтерпретацією трійок це означає, що якщо
S починається в стані, що задовольняє P та S , і завершується, то
i
i
i
стан задовольняє Q . Для того щоб ця інтерпретація залишалася
i
вірною при паралельному виконанні, процеси повинні починати-

70