On prouve la validité d'un algorithme itératif à l'aide de la méthode des invariants de boucle.
On raisonne par récurrence pour montrer qu'une telle propriété est préservée à chaque itération de la boucle. Elle suffit à prouver la validité de l'algorithme si elle est trivialement vraie à la première itération et qu'à la dernière itération, sa véracité entraîne celle de l'algorithme. Voyons cela sur un exemple.