Инвариант цикла - это предикат, который выполняется на каждой итерации цикла.
Вот, например, возьмем такой цикл:
Код:
q = 0;
while (a >= b)
{
a = a - b;
q++;
}
Инвариантом будет

(

- начальное значение переменной

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

(инвариант) и

(условие выхода из цикла), т.е.

- неполное частное и

- остаток от деления

на

.
До полного доказательства не хватает утверждения о том, что цикл обязательно завершится. В нашем случае если

,

, то цикл завершится, так как на каждой итерации значение

уменьшается.