Un invariant de
boucle est une propriété portant sur le programme et ses
variables qui
doit être vraie avant
l'exécution de la boucle et après chaque
itération. L'invariant aide souvent à
comprendre le fonctionnement
d'un algorithme (algorithmes de tri, ...)
Une fonction variante
aide à prouver ou à se convaincre que l'itération se
termine dans tous les cas (pas de boucle infinie).