Invariant de boucle

Les invariants de boucle

Qu'est-ce qu'un invariant de boucle ?

Un invariant de boucle bien choisi est utile à la fois lors de la conception, du test et de la modification du code. Il sert également de documentation et peut être le fondement d'une preuve d'exactitude d'un algorithme.

Propriétés d'un bon invariant

Un bon invariant de boucle doit satisfaire trois propriétés :

En fait, ces trois étapes constituent une preuve par induction, qui montre que la propriété souhaitée est vraie lorsque le programme quitte la boucle.

Exemple 1 : Calcul de la somme des n premiers entiers

Pour vous donner plus de sens sur cette méthode, nous prendrons l'exemple suivant :

def somme(n):
    s = 0
    for i in range(1, n+1):
        s += i
    return s

L'invariant de boucle pour ce programme est :

Pourquoi cet invariant ?

• Initialisation : L'invariant de boucle tient initialement puisque \(s = 0\) et \(i = 1\) à ce point. La somme de 1 à 0 est vide, donc égale à 0.
• Maintenance : En supposant que l'invariant est valable avant la i-ème itération (c'est-à-dire \(s = 1+2+\dots+(i-1)\)), alors pendant l'itération, la boucle ajoute \(i\) à la somme. Après l'itération, \(s\) devient \(1+2+\dots+(i-1)+i\) et \(i\) est incrémenté. Donc l'invariant \(s = 1+2+\dots+(i-1)\) reste vrai pour la prochaine itération.
• Terminaison : Lorsque la boucle se termine (après avoir traité \(i = n+1\)), l'invariant indique que \(s = 1 + 2 + \dots + n\), exactement ce qui est nécessaire pour que l'algorithme soit correct.

Exemple 2 : Recherche du maximum dans un tableau

Considérez le programme suivant qui calcule le maximum d'un tableau :

def max_tableau(tab):
    max_val = tab[0]
    for i in range(1, len(tab)):
        if tab[i] > max_val:
            max_val = tab[i]
    return max_val

Pour ce programme, l'invariant de boucle est :

Cet invariant semble bien choisi :

• Initialisation : L'invariant de boucle est initialement vrai puisque \(\text{max\_val} = tab[0]\) et \(i = 1\) à ce stade. Le maximum du premier élément est bien \(tab[0]\).
• Maintenance: Supposons que l'invariant est vrai avant une itération (\(\text{max\_val} = \max(tab[0], \dots, tab[i-1])\)). Pendant l'itération, on compare \(tab[i]\) avec \(\text{max\_val}\) :
  • Si \(tab[i] > \text{max\_val}\), on met à jour \(\text{max\_val}\) avec \(tab[i]\).
  • Sinon, \(\text{max\_val}\) reste inchangé.
  Dans les deux cas, après l'itération, \(\text{max\_val} = \max(tab[0], \dots, tab[i])\). Comme \(i\) est incrémenté, l'invariant reste vrai pour la prochaine itération.
• Terminaison : Lorsque la boucle se termine (\(i = \text{len}(tab)\)), l'invariant nous dit que \(\text{max\_val} = \max(tab[0], tab[1], \dots, tab[n-1])\), ce qui est exactement le résultat attendu.

Récapitulatif des invariants des exemples

Exercice d'application

Considérez l'algorithme de recherche dichotomique suivant :

def recherche_dichotomique(tab, x):
    debut = 0
    fin = len(tab) - 1
    
    while debut <= fin:
        milieu = (debut + fin) // 2
        if tab[milieu] == x:
            return milieu
        elif tab[milieu] < x:
            debut = milieu + 1
        else:
            fin = milieu - 1
    
    return -1

Question : Quel est l'invariant de boucle de cet algorithme ? Vérifiez les trois propriétés.