Définition
Définition : Invariant de boucle (ou d'algorithme)
Un invariant est un propriété qui est toujours vrai en des points clefs de la boucle (de l'algorithme).
Fondamental : Invariant de boucle
L'invariant d'une boucle while est généralement la condition de celle-ci.
Le point clef où est valide l'invariant est alors au début du corps de la boucle.
Exemple : Exemple d'invariant
Un invariant peut-être :
La condition d'une boucle
whileUne condition sur la taille d'une liste