Інваріант циклу являє собою математичний вираз (зазвичай - рівність), в яке непереборним чином входять принаймні деякі змінні, значення яких змінюються від одного проходу циклу до іншого. Інваріант будується таким чином, щоб бути істинним безпосередньо перед початком виконання циклу (перед входом в першу ітерацію) і після кожної його ітерації. Причому якщо в інваріант входять змінні, певні тільки всередині циклу (наприклад, лічильник циклу for в Паскалі або Аді), то для входу в цикл вони враховуються з тими значеннями, які отримають в момент ініціалізації.
Доведення коректності циклу із застосуванням інваріанта
Порядок докази працездатності циклу за допомогою інваріанта зводиться до наступного:
- Доводиться, що вираз інваріанта істинно перед початком циклу.
- Доводиться, що вираз інваріанта зберігає свою істинність після виконання тіла циклу; таким чином, по індукції, доводиться, що після закінчення всього циклу інваріант буде виконуватися.
- Доводиться, що при істинності інваріанту після завершення циклу змінні приймуть саме ті значення, які потрібно отримати (це елементарно визначається з виразу інваріанта і відомих кінцевих значеннях змінних, на яких ґрунтується умова завершення циклу).
- Доводиться (можливо - без застосування інваріанта), що цикл завершиться, тобто умова завершення рано чи пізно буде виконано.
- Істинність тверджень, доведених на попередніх етапах, однозначно свідчить про те, що цикл виконається за кінцевий час і дасть бажаний результат.
Також інваріанти використовують при проектуванні і оптимізації циклічних алгоритмів. Наприклад, щоб переконатися, що оптимізований цикл залишився коректним, досить довести, що інваріант циклу не порушений і умова завершення циклу досяжно.