Составители:
1) Правило оператора await. Поскольку де йстви е оп ератора
await похоже на действие оператора if, то правило вывода анало-
гично:
{P ∧ B} S {Q}
{P } < await(B)S; > {Q}
.
Предпосылка: “если P ∧ B истинны, то если S завершается, то Q
будет истинным”; вывод: “из состояния P оператор await приводит
к Q” (если await завершается).
Замечание. Правила вывода ничего не говорят о задержках
выполнения (задержки выполнения влияют на свойство живучести
и на свойство безопасности).
2) Правило оператора co. Рассмотрим выражение
co S
1
; //S
2
; // . . . //S
n
; oc.
Говорят, что процессы S
i
не влияют друг на друга, если ни один
процесс не совершает операции, нарушающие условия выполнения
другого процесса.
Предполож им, что выражения
{P
i
} S
i
{Q
i
}
свободны от взаимного вмешательства (т.е. процессы S
i
не влияют
друг на друга) и истинны. Тогда истинно выражение
{P
1
∧ . . . ∧ P
n
} co S
1
; // . . . //S
n
; oc {Q
1
∧ . . . ∧ Q
n
}.
Это правило можно записать следующим образом
{P
i
} S
i
{Q
i
} [свободны от взаимного вмешательства]
{P
1
∧ . . . ∧ P
n
} co S
1
; // . . . //S
n
; oc {Q
1
∧ . . . ∧ Q
n
}
.
Рассм отрим программу
{x == 0}
co < x = x + 1; > // < x = x + 2; > oc
{x == 3}
Истинна ли эта тройка? Если выполнение программы начина-
ется при x = 0, то нет возможности сказать, какое x поступит в
32
Страницы
- « первая
- ‹ предыдущая
- …
- 29
- 30
- 31
- 32
- 33
- …
- следующая ›
- последняя »
