Составители:
{C ∧ pre(a)} a {C}, т.е. если истинны C ∧ pre(a) перед применением
a, то истинно C после применения a.
Иначе говоря, критическое утверждение C инвариантно отно-
сительно действия a.
Рассмотрим пример, вытекающий из приведенной выше про-
граммы: предусловие первого процесса является критическим
утверждением (поскольку оно находится вн е оператора await).
Однако на него не влияет оператор присваивания во втором про-
цессе, ибо истинна такая тройка:
{(x == 0 ∨ x == 2) ∧ (x == 0 ∨ x == 1)}
x = x + 2
{x == 0 ∨ x == 2}
В рассматриваемой программе имеется еще три критических
утверждения: постусловие пер вого процесса, предусловие и посту-
словие второго процесса. Аналогично проверяется взаимные невме-
шательства и в этих сдучаях.
§11 Устранение взаимного вмешательства:
непересекающиеся множества переменных
Имеется четыре основных метода устранения взаимного вмеша-
тельства:
1) использование непересекающихся множеств переменных;
2) применение ослабленных утверждений;
3) отслеживание глобальных инвариантов;
4) синхронизация.
Остановимся более подробно на первом методе.
Множество записи процесса — множество переменных, кото-
рым он присваивает значения.
Множество чтения — это множество переменных, которые он
читает, но не изменяет.
Множество ссылок процесса — множество переменных, кото-
рые встречаются в утверждениях доказательства правильности
процесса.
34
Страницы
- « первая
- ‹ предыдущая
- …
- 31
- 32
- 33
- 34
- 35
- …
- следующая ›
- последняя »
