Page 73 - 6571

{C Ù pre ( )} { }a a C . (1)

Таким чином, критичне твердження C є інваріантним щодо
дії присвоєння a.

Як приклад розглянемо останню з наведених вище програм.
Передумова першого процесу є критичним твердженням. На ньо-
го не впливає оператор присвоєння в другому процесі, оскільки

істинна наступна трійка:

{(x == 0 Úx == 2) Ù (x == 0 Úx == 1)}
x = x+2;
{x == 0 Úx == 2}

Перший предикат спрощується до x == 0, тому після дода-

вання 2 до змінної x значення змінної x буде або 0, або 2. Дана
трійка висловлює наступний факт: якщо другий процес викону-
ється перед першим, то на початку виконання першого процесу

змінна x буде мати значення 2. У даній програмі є ще три крити-
чних твердження: постумова першого процесу та перед- і посту-
мова другого процесу. Усі інші докази взаємного невтручання
аналогічні наведеному.

Запитання для самоперевірки

1. Що розуміють під терміном «логіка програмування»?

2. Із яких правил складається будь-яка формальна логічна си-
стема?
3. Коли логіка програмування є несуперечливою щодо інтер-

претації?
4. Коли логіка програмування є повною щодо інтерпретації?
5. Як називаються формули у логіці програмування?

6. З чого складається «трійка» у логіці програмування?
7. Які чотири найбільш важливих правила виведення у логіці
програмування Ви знаєте?
8. Що таке інваріант циклу у паралельній програмі?

9. У якому випадку говорять, що один процес втручається в
(впливає на) інший?
10. В чому полягає принцип взаємного невтручання?

72