Правило цикла с условием продолжения без инициализации

Листинг 6.10. Правило вывода W1 — «Цикл с условием продолжения без инициализации».

Если условие / истинно непосредственно перед началом выполнения цикла с условием продолжения, то и I, и В будут истинными до первого выполнения тела цикла ОР. Поскольку (1 and В) является предусловием для I по отношению к ОР, то / будет истинным после первого выполнения ОР. Поэтому и I, и В будут истинными до второго выполнения тела цикла ОР и т. д. Условие I будет истинным после каждого выполнения ОР. Если когда-то наступит такой момент, что выполнение цикла закончится, то условие I будет истинным, а условие В ложным. То есть условие (I and not В) будет истинным при завершении цикла (если завершится его выполнение).

Значение условия I истинное, т. е. константа, до и после каждого выполнения тела цикла ОР. Поэтому условие / называют инвариантом цикла. Инвариант цикла является ключевым понятием в разработке и понимании существа цикла.

При применении правила вывода W1 требуется, чтобы инвариант цикла I был истинным до выполнения цикла. Обычно инвариант I изначально истинен тривиальным образом. Другими словами, начальное состояние представляет особый случай инварианта цикла. При завершении выполнения цикла условие (I and not В) истинно. То есть конечное состояние также представляет особый случай инварианта I. Рассматривая инвариант цикла I с общих позиций, его можно считать результатом обобщения начального и конечного состояний. Из последнего вытекает следующее правило.

Эмпирическое правило определения инварианта цикла формулируется так: следует обобщить (ослабить) начальное и конечное состояния (предусловие и постусловие) для того, чтобы найти подходящий инвариант цикла.

Практически любому (за некоторым исключением) циклу предшествует его инициализация — выполнение сегмента программы, единственным назначением которого является установка исходной истинности инварианта цикла.