Identifier une propriété I qui est (1) vraie avant la boucle, (2) conservée à chaque itération, (3) qui, combinée à la condition de sortie, donne le résultat souhaité.
Quand utiliser
Pour prouver la correction partielle d'un algorithme itératif.
Exemple
Pour le tri par insertion : l'invariant est « L[0:i] est trié ». Au début i=1 (trivial), à chaque itération on insère L[i] à sa place, et à la fin L[0:n] est trié.