Интернет магазин китайских планшетных компьютеров

Компьютеры - Инвариант (программирование)

Инвариантом в программировании называется логическое выражение, истинное после каждого прохода тела цикла и перед началом выполнения цикла, зависящее от переменных, изменяющихся в теле цикла.

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

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

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

Понятие инварианта также используется в объектно-ориентированном программировании для обозначения непротиворечивого состояния объекта. Подразумевается, что вызов любого метода оставляет объект в состоянии инварианта.