Инвариант цикла - это предикат, который выполняется на каждой итерации цикла.
Вот, например, возьмем такой цикл:
Код:
q = 0;
while (a >= b)
{
a = a - b;
q++;
}
Инвариантом будет
![$P(a,b,q) \equiv (a + qb = a_0)$ $P(a,b,q) \equiv (a + qb = a_0)$](https://dxdy-03.korotkov.co.uk/f/6/7/7/677f9deea9ade85db877dc1e0c7a4d2b82.png)
(
![$a_0$ $a_0$](https://dxdy-01.korotkov.co.uk/f/0/0/7/007094eee0f16d09ce121fc2ba8e710782.png)
- начальное значение переменной
![$a$ $a$](https://dxdy-01.korotkov.co.uk/f/4/4/b/44bc9d542a92714cac84e01cbbb7fd6182.png)
)
Инварианты используются для доказательства того, что программа действительно делает то, что надо. В нашем случае поскольку инвариант выполняется на каждой итерации цикла, то после выхода из цикла будет
![$a + qb = a_0$ $a + qb = a_0$](https://dxdy-04.korotkov.co.uk/f/b/0/1/b01548866fbef3e358aed760a402421f82.png)
(инвариант) и
![$a<b$ $a<b$](https://dxdy-01.korotkov.co.uk/f/4/e/2/4e2392553d1d1035505840cbf0f5a45182.png)
(условие выхода из цикла), т.е.
![$q$ $q$](https://dxdy-02.korotkov.co.uk/f/d/5/c/d5c18a8ca1894fd3a7d25f242cbe889082.png)
- неполное частное и
![$a$ $a$](https://dxdy-01.korotkov.co.uk/f/4/4/b/44bc9d542a92714cac84e01cbbb7fd6182.png)
- остаток от деления
![$a_0$ $a_0$](https://dxdy-01.korotkov.co.uk/f/0/0/7/007094eee0f16d09ce121fc2ba8e710782.png)
на
![$b$ $b$](https://dxdy-01.korotkov.co.uk/f/4/b/d/4bdc8d9bcfb35e1c9bfb51fc69687dfc82.png)
.
До полного доказательства не хватает утверждения о том, что цикл обязательно завершится. В нашем случае если
![$a_0>0$ $a_0>0$](https://dxdy-04.korotkov.co.uk/f/f/5/0/f509d006c21ad280c929b2fe8a835d8482.png)
,
![$b>0$ $b>0$](https://dxdy-03.korotkov.co.uk/f/a/2/2/a22dca7a3838034445d5ed9038d9963182.png)
, то цикл завершится, так как на каждой итерации значение
![$a$ $a$](https://dxdy-01.korotkov.co.uk/f/4/4/b/44bc9d542a92714cac84e01cbbb7fd6182.png)
уменьшается.