Ce qu’il faut savoir

• on appelle “invariant de boucle” une propriété qui est vraie avant et après chaque itération (boucle)

• un invariant de boucle peut permettre de prouver la correction d’un algorithme

• il est nécessaire de démontrer que l’on a bien un invariant de boucle, cette démonstration doit se faire en 3 étapes :

  • INITIALISATION : on doit montrer que l'invariant de boucle est vrai avant la première itération de la boucle

  • CONSERVATION : on doit montrer que si l'invariant de boucle est vrai avant une itération de la boucle, il le reste avant l'itération suivante.

  • TERMINAISON : une fois la boucle terminée, l'invariant fournit une propriété utile qui aide à montrer la correction de l'algorithme.

Ce qu’il faut savoir faire

• vous devez être capable de trouver un invariant de boucle dans un algorithme

• vous devez être capable de prouver que c’est bien un invariant de boucle

• d’utiliser cet invariant de boucle pour démontrer la correction d’un algorithme (notamment les algorithmes de tri par insertion et de tri par sélection)