Задача (пример). Требуется по неотрицательному целому $a$ и целому положительному делителю $b$ вычислить целые частное $q$ и остаток $r$, такие что
$$a=q\cdot b+r\text{и}0\le r<b.$$
Программа (псевдокод):
q := $0$
r := $a$
while r $\ge$ $b$ do
r := r $-$ b
q := q $+$ $1$
end
Предусловие (безопасность входа): $P:a\ge 0\wedge b>0$.
Постусловие (цель): $Q:a=q\cdot b+r\wedge 0\le r<b$.
Инвариант цикла. Натуральный инвариант — сохранение разложения исходного $a$ через текущие $q,r$:
$$I(q,r):a=q\cdot b+r\wedge r\ge 0.$$
Построение инварианта (кратко). Идея: каждая итерация уменьшает $r$ на ровно $b$ и увеличивает $q$ на $1$, поэтому сумма $q\cdot b+r$ должна оставаться равной исходному $a$. Дополнительно требуется гарантия, что $r$ не уходит в отрицательное — это обеспечит корректность остатка и безопасность вычитания.
Доказательство корректности по инварианту (три шага).
1) Инициализация: до цикла $q=0$, $r=a$. Тогда
$$a=0\cdot b+a,$$ поэтому $I(q,r)$ выполняется при выполнении $P$ (также $r=a\ge 0$ из $P$).
2) Сохранение (индуктивный шаг): предположим $I(q,r)$ верно перед телом цикла и выполнен условный переход $r\ge b$. После телa: $r^{\prime }=r-b$, $q^{\prime }=q+1$. Тогда
$$q^{\prime }\cdot b+r^{\prime }=(q+1)\cdot b+(r-b)=q\cdot b+r=a,$$ и $r^{\prime }=r-b\ge 0$ (так как $r\ge b$ и $b>0$). Значит $I(q^{\prime },r^{\prime })$ верно — инвариант сохраняется.
3) Выход и постусловие: цикл останавливается при $\neg (r\ge b)$, т.е. при $r<b$. Выйдя из цикла, инвариант всё ещё верен, следовательно
$$a=q\cdot b+r\wedge r\ge 0.$$ Вместе с условием выхода даёт
$$a=q\cdot b+r\wedge 0\le r<b,$$ что равно $Q$.
Доказательство завершимости (терминирование). Введём функция меры (вариант) $V(r)=r$. При каждой итерации $V$ уменьшается на $b$ (по меньшей мере на $1$, так как $b>0$), и при этом всегда остаётся неотрицательной по инварианту. Следовательно число итераций конечно — цикл завершается.
Заключение. При предпосылке $P:a\ge 0\wedge b>0$ инвариант $I$ корректно инициализируется и сохраняется, при выходе обеспечивает требуемое постусловие $Q$. Таким образом программа корректна и безопасна.