Инвариант цикла
в программировании — логическое выражение, истинное после каждого прохода тела цикла / Материал из Википедии — свободной encyclopedia
У этого термина существуют и другие значения, см. Инвариант.
Инвариант цикла — в программировании — логическое выражение, истинное после каждого прохода тела цикла (после выполнения фиксированного оператора) и перед началом выполнения цикла, зависящее от переменных, изменяющихся в теле цикла.[1] Инварианты используются в теории верификации программ для доказательства правильности результата, полученного циклическим алгоритмом.