Invariant de boucle

En programmation, une boucle est une instruction qui permet de répéter l'exécution d'une partie d'un programme. Un invariant de boucle est une propriété qui est vraie avant et après chaque répétition. C'est une propriété logique, qui permet d'étudier un programme ou un algorithme. En vérification formelle, en particulier en logique de Hoare, les invariants de boucles sont des prédicats logiques, qui servent à prouver les algorithmes qui les utilisent, en particulier la correction de ces algorithmes. Un invariant de boucle doit être vrai avant de commencer la boucle et il est garanti qu'il restera vrai après chaque itération de la boucle. En particulier, l'invariant sera toujours vrai à la fin de la boucle.Les boucles et la récursivité étant fondamentalement similaires, il y a peu de différence entre démontrer un invariant de boucles et prouver qu'un programme est correct en utilisant un raisonnement par récurrence. En pratique, l'invariant de boucle est souvent la propriété induction — l'hypothèse d'induction — qui sert à montrer qu'un programme récursif est équivalent à une boucle.