Page 58 - 4868

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

входження значення x. За умови, що x зустрічається в a, цикл завершується

присвоєнням змінній i індексу першого входження.
i = 1;
{i == 1  ( j: 1 <= j <і:a[j] != x)}
while (a[і] != x)
і = і+1;
{(j:1 <= j < і:a[j] != x)  a[i] == x}
В даному прикладі інваріантом циклу виступає предикат з квантором.
Він істинний перед виконанням циклу, оскільки область визначення квантора
порожня. Він також істинний перед кожним виконанням тіла циклу і після
нього. Коли виконання оператора циклу завершується, a[1] рівно x, і

значення x раніше не зустрічалося в масиві a.
Правило слідування дозволяє посилювати передумови і послаблювати
постумови. В якості прикладу розглянемо наступну трійку:
{x == 0} x = x+1; {x == 1}

Згідно правила слідування істинною буде також наступна трійка:

{x == 0} x = x+1; {x> 0}
У другій трійці постумова слабша, ніж у першій, оскільки вона

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

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

Оператор паралельного виконання co виступає оператором керування.
Отже, його дія описується правилом виведення, що враховує вплив
паралельного виконання. Процеси у свою чергу складаються з послідовних
операторів і операторів синхронізації, таких як оператор await.
З погляду часткової коректності дія оператора
< await (B) S; >найбільш схожа на дію оператора іf, для якого умова B
істинна, коли починається виконанняS .Отже, правило висновку для
оператора await аналогічне правилу виведення для оператора іf.
{P  B } S { }Q
.
{ }P  await ( ) ; { }B S  Q

Дана гіпотеза говорить наступне: «якщо виконання S починається в
стані, коли P та B істинні, і завершується, то Q також буде істинним». Отже,
оператор await призводить до стану, що задовольняєQ , якщо починається в

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