инвариант цикла

EN: loop invariant

Свойство, истинное перед каждой итерацией цикла и сохраняемое каждой итерацией. Используется в доказательствах корректности: если инвариант выполняется при инициализации, сохраняется на каждом шаге и влечёт желаемый результат при завершении, алгоритм корректен. Пример: в сортировке вставками инвариант — префикс до текущего индекса всегда отсортирован.