Составители:
Перечислим наиболее важные правила вывода.
Правило композиции
{P } S
1
{Q}, {Q} S
2
{R}
{P } S
1
; S
2
{R}
.
Правило оператора if
{P ∧ B} S {Q}, {P ∧ ¬B} ⇒ Q
{P } if (B)S; {Q}
.
Правило оператора while
{I ∧ B} S {I}
{I} while(B)S; {I ∧ ¬B}
.
Правило следования
{P
0
⇒ P }, {P } S {Q}, Q ⇒ Q
0
{P
0
} S {Q
0
}
.
Для правила оператора while используется инвариант цикла
I; этот предикат, значение которого истинно перед каждым повто-
рением цикла и после н его. Если инвариант I и условие B истинны
до S, то I истинно и после S; на этом обстоятельстве и зиждется
выполнение цикла. Как только B становится ложным, цикл пр екр а-
щается (а I остается истинным), состояние принимает вид I ∧ ¬B.
Пример. (программа просмотра массива и поиска первого
вхождения з начения x).
i = 1;
{i == 1 ∧ (∀j : 1 <= j < i : a[j]! = x)}
while (a[i]! = x)
i = i + 1;
{(∀j : 1 <= j < i : a[j]! = x) ∧ a[i] == x}
§10 Логика программирования при
параллельном выполнении
Оператор параллел ьного выполнения co является управляющим
оператором. Процессы состоят из последовательных операторов и
операторов синхронизации (например, await): < await (B) S; >.
31
Страницы
- « первая
- ‹ предыдущая
- …
- 28
- 29
- 30
- 31
- 32
- …
- следующая ›
- последняя »
