Exemple

On divise deux entiers strictement positifs $a$ et $b$ en déterminant deux entiers $q$ et $r$ tels que $a = bq + r$ avec $0 \leq r < b$. Voici un algorithme déterminant $q$ et $r$ :

On choisit comme invariant de boucle la propriété $a = bq + r$.

• Comme $q$ est initialisé à $0$ et $r$ à $a$, alors la propriété $a = bq + r = b.0 + a$ est vérifiée avant le premier passage dans la boucle.
• Avant une itération arbitraire, supposons que l'on ait $a = bq + r$, montrons que cette propriété est conservée par cette itération. Soient $q^\prime$ la valeur de $q$ à la fin de l'itération et $r^\prime$ la valeur de $r$ à la fin de l'itération. Nous devons montrer que $a = bq^\prime + r^\prime$. On a $q^\prime = q + 1$ et $r^\prime = r - b$, alors $bq^\prime + r^\prime = b(q + 1) + (r - b) = bq + r = a$. La propriété est bien conservée.