Un autre exemple

Déterminons un algorithme qui calcule le produit de deux entiers $a$ et $b$ avec $a$ positif ou nul sans effectuer de multiplication.

• Montrons que le programme se termine. La séquence formée par les valeurs prises par $m$ au fil des itérations est strictement croissante, il y a donc un moment où $m \geq a$. Donc l'algorithme se termine.
• Considérons comme invariant de boucle $p = m.b$, montrons par récurrence qu'il est vérifiée.
  • $m$ est $p$ sont initialisés à $0$, on a bien $0 = 0.b$.
  • montrons maintenant que la propriété est conservée. Supposons qu'au début d'une itération donnée, on ait $p = m.b$. Soient $p^\prime$ et $m^\prime$ les valeurs de ces variables à la fin de cette itération, montrons que l'on a $p^\prime = m^\prime .b$. On a les relations $p^\prime = p + b$ et $m^\prime = m + 1$. Donc $p^\prime = p + b = m.b + b = (m + 1).b = m^\prime .b$. La propriété est donc conservée par chaque itération de l'algorithme.
• La première de valeur de $m$ qui nous fera sortir de la boucle est $a$, donc après la dernière itération on aura $p = mb = ab$. Ce programme place donc dans $p$ le produit de $a$ par $b$.