Invariant de boucle

Un invariant de boucle est une propriété liée aux variables du programme qui est vraie chaque fois que l'exécution du programme atteint l'invariant.

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.

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

•  Initialisation: l'invariant de boucle doit être vrai avant la première exécution de la boucle.
•  Maintenance: si l'invariant est vrai avant une itération de la boucle, il devrait l'être également après l'itération.
•  Terminaison: Lorsque la boucle est terminée, l'invariant doit nous dire quelque chose d'utile, quelque chose qui nous aide à comprendre l'algorithme.

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 \(s=\sum_{k=0}^{i-1} k\), pourquoi?

•  L'invariant de boucle tient initialement puisque \(s = 0\) et \(i = 1\) à ce point.
•  En supposant que l'invariant est valable avant la ième itération, il en sera de même après cette itération puisque la boucle ajoute i à la somme et incrémente i d'une unité.
•  Lorsque la boucle est sur le point de se terminer, l'invariant indique que \(s = 0 + 1 + 2 +… + n\), exactement ce qui est nécessaire pour que l'algorithme soit correct.

En fait, les trois étapes ci-dessus constituent une preuve par induction, qui montre que \(s = 1 + 2 +… + n\) lorsque le programme quitte la boucle.

Exemple 

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

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

Pour le programme ci-dessus, l'invariant de boucle est max \(= max(tab[0], tab[1],…, tab[i-1])\), et il semble bien choisi:

•  L'invariant de boucle est initialement vrai puisque \(max = tab[0]\) et \(i = 1\) à ce stade.
•  il satisfait la propriété de terminaison puisque la variable max \(= max (max(tab[0], tab[1], …, tab[n-1]))\) lorsque la boucle se termine.
•  La propriété de maintenance indique: si l'invariant est vrai avant une itération de la boucle, il doit l'être également après cette itération.