Invariant de boucle

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 so…