Инвариант цикла — в программировании — логическое выражение, истинное после каждого прохода тела цикла (после выполнения фиксированного оператора) и перед началом выполнения цикла, зависящее от переменных, изменяющихся в теле цикла.[1] Инварианты используются в теории верификации программ для доказательства правильности результата, полученного циклическим алгоритмом.
Инвариант цикла представляет собой математическое выражение (обычно — равенство), в которое неустранимым образом входят по крайней мере некоторые переменные, значения которых изменяются от одного прохода цикла до другого. Инвариант строится таким образом, чтобы быть истинным непосредственно перед началом выполнения цикла (перед входом в первую итерацию) и после каждой его итерации. Причём если в инвариант входят переменные, определённые только внутри цикла (например, счётчик цикла for
в Паскале или Аде), то для входа в цикл они учитываются с теми значениями, которые получат в момент инициализации.
Порядок доказательства работоспособности цикла с помощью инварианта сводится к следующему:
Также инварианты используют при проектировании и оптимизации циклических алгоритмов. Например, чтобы убедиться, что оптимизированный цикл остался корректным, достаточно доказать, что инвариант цикла не нарушен и условие завершения цикла достижимо.
Данная страница на сайте WikiSort.ru содержит текст со страницы сайта "Википедия".
Если Вы хотите её отредактировать, то можете сделать это на странице редактирования в Википедии.
Если сделанные Вами правки не будут кем-нибудь удалены, то через несколько дней они появятся на сайте WikiSort.ru .