Составители:
каждый из процессов (0, 2 в первый и 0, 1 во второй). От этого бу-
дет зависеть результат (на первый вз гляд кажется, что x может
быть 1, 2 или 3), ибо порядок выполнения недетерминирован.
Очевидно, достаточно проверить истинность программы с
предусловием x == 0 и с постусловием x == 3, а именно:
{x == 0}
co{x == 0 ∨ x == 2}
< x = x + 1; >
{x == 1 ∨ x == 3}
//{x == 0 ∨ x == 1}
< x = x + 2; >
{x == 2 ∨ x == 3}
oc
{x == 3}
Утверждения в каждом процессе учитывают оба порядка выполне-
ния, причем конъюнкция предусловий дает {x == 0}:
{x == 0 ∨ x == 2} ∧ {x == 0 ∨ x == 1} = {x == 0},
а конъюнкция постусловий дает {x == 3}:
{x == 1 ∨ x == 3} ∧ {x == 2 ∨ x == 3} = {x == 3}.
Вывод: Истинность рассматриваемой тройки доказана.
Замечание. Приведенный пример иллюстрирует схему доказа-
тельства программы (все три тройки оказались истинными).
Формальное определение невмешательства
Действие присваивания — это оператор присваивания или опе-
ратор await, содержащий одно или несколько присваиваний.
Критическое утверждение — это предусловие или постуловие
вне оператора await.
Если a — действие присваивания в некотором процессе, pre(a)
— его предусловие, C — критическое утверждение в другом про-
цессе, действие a не вмешивается в C, если истинна тройка
33
Страницы
- « первая
- ‹ предыдущая
- …
- 30
- 31
- 32
- 33
- 34
- …
- следующая ›
- последняя »
