Инвариант цикла

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

Порядок доказательства работоспособности цикла с помощью инварианта сводится к следующему:

1. Доказывается, что выражение инварианта истинно перед началом цикла.
2. Доказывается, что выражение инварианта сохраняет свою истинность после выполнения тела цикла; таким образом, по индукции, доказывается, что по завершении всего цикла инвариант будет выполняться.
3. Доказывается, что при истинности инварианта после завершения цикла переменные примут именно те значения, которые требуется получить (это элементарно определяется из выражения инварианта и известных конечных значениях переменных, на которых основывается условие завершения цикла).
4. Доказывается (возможно — без применения инварианта), что цикл завершится, то есть условие завершения рано или поздно будет выполнено.
5. Истинность утверждений, доказанных на предыдущих этапах, однозначно свидетельствует о том, что цикл выполнится за конечное время и даст желаемый результат.

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