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