Технология программирования. - 46 стр.

UptoLike

Рубрика:

- 48 -

P => I, (I,¬Q) => R и пусть обобщённый оператор S обладает следующим свой-

ством {I} S {I}.

Тогда для оператора цикла

ПОКА Q ДЕЛАТЬ S ВСЁ ПОКА

справедливо следующее свойство:

{P} ПОКА Q ДЕЛАТЬ S ВСЁ ПОКА {R}.

Предикат I называют инвариантом оператора цикла. Инвариант цикла – это

неизменные отношения, являющиеся истинными независимо от того, сколько раз

выполнился цикл [1].

Доказательство:

Для этого достаточно доказать следующее свойство:

{I}

ПОКА Q ДЕЛАТЬ S ВСЁ ПОКА {I, ¬Q}

(в соответствии с теоремой 5 на основании имеющихся в условиях данной теоремы

импликаций).

Пусть перед выполнением оператора цикла для некоторого состояния ИС ис-

тинен предикат I. Если при этом предикат Q ложен, то оператор цикла по семанти-

ке будет эквивалентен пустому оператору. В силу теоремы 1 о свойствах пустого

оператора

цикла справедливо утверждение {I, ¬Q}. Если же перед выполнением

оператора цикла предикат Q будет истинен, то оператор цикла по своей семантике пре-

вращается в составной оператор следующего вида:

S; ПОКА Q ДЕЛАТЬ S ВСЁ ПОКА

В силу свойства оператора S после его выполнения повторяется исходная ситуация:

предикат I – истинен перед выполнением оператора цикла, но для другого уже изме-

нённого состояния ИС (для которого предикат Q может быть либо истинен, либо ло-

жен). Применяя математическую индукцию, можно за конечное число шагов достичь

или прийти к ситуации, когда перед выполнением оператора цикла будет справедли-

во утверждение {I, ¬Q}. А в этом случае, как было показано выше, это утверждение

будет справедливо и после выполнения оператора

цикла. Теорема доказана.

Завершимость выполнения программы. Другими словами, под завершимо-

стью понимают отсутствие в ПС зацикливаний при тех или иных исходных дан-