Les variants et invariants de boucle

Les variants

Un variant de boucle est une variable dont la valeur se modifie à chaque itération de boucle, jusqu’à atteindre une valeur permettant l’arrêt :

p = 1
while p < 23 :
    p = 2*p

p est multiplié par 2 à chaque tour de boucle, on est sûr que la variable atteindra une valeur supérieure à 23.

En général, on utilise un listeleau pour le démontrer :

Nombre de tour	Valeur de p
1	2
2	4
3	8
4	16
5	32

👉 Aller à l'exercice ici 👈

Les invariants

Le variant de boucle est une variable dont la valeur est modifiée dans une boucle. Un invariant de boucle est une propriété qui est VRAIE avant ET après l’exécution d’une boucle. Concrètement, cela permet de vérifier que chaque tour de boucle effectue bien la propriété en elle-même.

La vérification de la propriété se fait en 3 étapes, de la même manière qu’un raisonnement par réccurence :

• Initialisation : Montrer que l’invariant de boucle est vrai avant l’exécution de la boucle;
• Maintenance : Montrer que si c’est vrai avant l’exécution, cela doit rester vrai durant toute l’exécution de la boucle;
• Terminaison : Quand la boucle termine, l’algorithme doit donner une propriété, un affichage, qui montre la correction de l’algorithme (c’est-à-dire que l’algorithme se finit sans problème, en ayant respecté la propriété initiale).

Exemple :
tri par insertion : propriété = trier un listeleau par ordre croissant

def insertion(liste):
    for i in range(len(liste)):
        elt = liste[i]
        j = i-1
        while j >= 0 and elt < liste[j]:
            liste[j+1] = liste[j]
            j -=1
        liste[j+1] = elt
    return liste

Visualisation de l'algorithme

Lien menant à une visualisation de l'algorithme

Tester l'algorithme avec la liste [6,4,5,1,9].

• Initialisation : i vaut 0. On a la liste [6], composée d’un seul élément. Une liste à un seul élément est triée par définition, donc la propriété est VRAIE.
• Maintenance : A chaque tour de boucle, liste[0:i-1] est trié :
  • On chercher à déplacer la valeur liste[i] le plus à gauche possible en comparant liste[i] aux valeurs précédentes;
  • Si la valeur à gauche est plus grande, on déplace liste[i] ;
  • À la fin du tour de boucle, liste[0:i] est trié, donc la propriété est VRAIE.
• Terminaison : Quand la boucle principale est finie, on sait que la propriété est VRAIE comme indiqué dans l’étape maintenance. Ici, on renvoie liste, et on peut l’afficher pour vérifier que la liste est bien triée.

👉 Aller à l'exercice ici 👈