Теория и практика защиты программ

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


Правило вывода W1 - «Цикл с условием продолжения без инициализации»

If

{I and B} OP

{I}

then

{I} while В do S endwhile (I and not B} <

Если условие I

истинно непосредственно перед началом выполнения цикла с условием продолжения, то и I, и В будут истинными до первого выполнения тела цикла OP. Поскольку (I and В) является предусловием для I по отношению к OP, то I

будет истинным после первого выполнения OP. Поэтому и I, и В

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

Значение условия I

истинное, то есть константа, до и после каждого выполнения тела цикла OP. Поэтому условие I

называют инвариантом цикла. Инвариант цикла является ключевым понятием в разработке и понимании существа цикла.

При применении правила вывода W1

требуется, чтобы инвариант цикла I был истинным до выполнения цикла. Обычно инвариант I

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

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

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

Весьма часто желательно доказать корректность цикла совместно с его инициализацией. Для этого мы располагаем правилом вывода W2.



Содержание раздела