Q : Qu'est qu'un invariant de boucle ?

R : un invariant de boucle est une propriété qui reste vérifiée à n'importe quel itération de la boucle... ce qui permet de faire des preuves de correction et de terminaison

mais cela mérite sans doute un article complet...