Terminaison et invariant de boucle

Vidéo de Cédric Gerland (8:48)

Variants, invariants de boucle, terminaison et correction des algorithmes⚓︎

I. Introduction⚓︎

Ce cours aborde des concepts fondamentaux pour la vérification et la correction des algorithmes, en particulier ceux liés aux boucles. On parlera des invariants de boucle, des variants de boucle, de la terminaison des algorithmes et de la correction formelle avec des exemples d'illustration.

II. Invariants de boucle⚓︎

Définition : un invariant de boucle est une propriété ou une condition qui reste vraie avant et après chaque itération d'une boucle.

Utilité : les invariants de boucle sont utilisés pour prouver la correction des boucles, en garantissant qu'une certaine propriété est maintenue tout au long de l'exécution de la boucle.

Exemple : soit une boucle qui calcule la somme des premiers n entiers naturels :

🐍 Editeur

def somme_n_entiers(n):
    somme = 0
    i = 1
    while i <= n:
        somme += i
        i += 1
    return somme

Invariant de boucle : cela peut être ici : « à chaque début d'itération, somme est égale à la somme des entiers de 1 à i-1 ».

Preuve :

Initialisation : avant la première itération, i = 1 et somme = 0, ce qui est la somme des entiers de 1 à 0.

Conservation : si, avant une itération, somme est la somme des entiers de 1 à i-1, après l'ajout de i à somme et l'incrémentation de i, somme devient la somme des entiers de 1 à i.

Terminaison : la boucle termine quand i > n, donc à la fin somme est la somme des entiers de 1 à n.

III. Variants de boucle⚓︎

Définition : un variant de boucle est une expression qui décroît à chaque itération de la boucle et est utilisée pour prouver la terminaison de la boucle.

Utilité : les variants de boucle assurent que la boucle ne s'exécutera pas indéfiniment.

Exemple : d'après l'exemple précédent :

🐍 Editeur

def somme_n_entiers(n):
    somme = 0
    i = 1
    while i <= n:
        somme += i
        i += 1
    return somme

Variant de boucle : un variant de boucle pourrait être « n - i + 1 », qui représente le nombre d'itérations restantes.

Preuve :

Initialisation : au début, i = 1 donc le variant est n - 1 + 1 = n.

Conservation : à chaque itération, i augmente de 1, donc n - i + 1 décroît de 1.

Terminaison : La boucle se termine lorsque i > n, et à ce moment-là, le variant est 0 ou négatif.

IV. Terminaison⚓︎

Définition : un algorithme est termine si, pour toute entrée donnée, il finit par s'arrêter après un nombre fini d'étapes.

Exemple : considérons une boucle infinie comme contre-exemple :

🐍 Editeur

while True:
    pass

Ce code ne se termine jamais. Pour prouver la terminaison d'une boucle, on doit montrer qu'un variant de boucle décroît vers une borne inférieure (typiquement 0) avec chaque itération.

V. Correction des algorithmes⚓︎

Définition : un algorithme est correct s'il produit le résultat attendu pour toute entrée valide.

Méthodes de preuve :

La correction d'un algorithme peut être prouvée par:

Invariant de boucle : prouver qu'une propriété reste vraie à chaque itération.

Preuve de terminaison : montrer qu'une boucle se termine.

Preuve de post-condition : assurer que, à la fin de l'algorithme, la condition de sortie est satisfaite.

Exemple : exemple de somme

🐍 Editeur

def somme_n_entiers(n):
    somme = 0
    i = 1
    while i <= n:
        somme += i
        i += 1
    return somme

Preuve de correction

Invariant de boucle : à chaque début d'itération, \(somme\) est la somme des entiers de \(1\) à \(i-1\).

Terminaison : le variant \(n - i + 1\) décroît vers \(0\).

Post-condition : quand la boucle se termine, \(i = n + 1\), donc somme est la somme des entiers de \(1\) à \(n\).

Exercice n°1 : Factorielle⚓︎

Soit l'algorithme suivant :

🐍 Editeur

def factorielle(n):
    resultat = 1
    i = 1
    while i <= n:
        resultat *= i
        i += 1
    return resultat

Q1. Trouvez un invariant pour la boucle qui calcule la factorielle de \(n\).

Un invariant de boucle est une propriété qui reste vraie avant et après chaque itération de la boucle. Pour cet algorithme, l'invariant de boucle peut être formulé comme suit :

Invariant : à chaque début d'itération de la boucle while, resultat est égal à la factorielle de \(i-1\).

Formellement, avant chaque itération, on a : \(resultat = (i−1)!\)

Preuve de l'invariant de boucle :

Initialisation : Avant la première itération, \(i = 1\) et \(resultat = 1\). La factorielle de \(0\) est \(1\), donc l'invariant est vrai au début.

Conservation : Supposons que l'invariant est vrai au début de l'itération pour un certain \(i\), c'est-à-dire que \(resultat = (i-1)!\). Lors de cette itération, \(resultat\) est multiplié par \(i\) : \(resultat *= i\). Après cette multiplication, \(resultat = (i-1)! * i = i!\). Puis, \(i\) est incrémenté de \(1\), donc à la fin de l'itération, resultat est égal à \(i!\) et \(i\) est égal à \(i+1\). Ainsi, avant l'itération suivante, l'invariant est maintenu.

Terminaison : La boucle se termine lorsque \(i > n\). À ce stade, \(i = n+1\) et selon l'invariant, \(resultat = n!\). Donc, l'algorithme retourne \(resultat\) qui est la factorielle de \(n\).

Q2. Proposez un variant de boucle pour le calcul de la factorielle.

Un variant de boucle est une expression qui décroît strictement avec chaque itération de la boucle et est utilisée pour prouver que la boucle se termine. Pour cet algorithme, un variant de boucle pourrait être :

Variant : \(n - i + 1\)

Ce variant décroît de \(1\) à chaque itération puisque \(i\) est incrémenté de \(1\) à chaque itération.

Preuve de terminaison :

Initialisation : Au début, \(i = 1\) donc le variant est \(n - 1 + 1 = n\).

Maintien : A chaque itération, \(i\) est incrémenté de \(1\), donc le variant \(n - i + 1\) décroît de \(1\).

Borne Inférieure : La boucle se termine lorsque \(i > n\), donc le variant atteint 0 ou une valeur négative.

Q3. Prouvez la correction de l'algorithme.

Pour prouver la correction de l'algorithme, on doit montrer que pour toute entrée valide \(n\) (c'est-à-dire un entier non négatif), l'algorithme renvoie la valeur correcte de \(n!\).

Invariant de boucle : à chaque début d'itération, resultat = (i-1)!.

Preuve de terminaison : le variant \(n - i + 1\) décroît et atteint \(0\) ou une valeur négative, assurant que la boucle se termine.

Post-condition : à la fin de l'algorithme, lorsque \(i > n\), resultat contient \(n!\).

Ainsi, l'algorithme calcule correctement la factorielle de \(n\) et se termine pour toute entrée valide.

Q4. Conclure.

En utilisant l'invariant de boucle et le variant, on a prouvé la correction de l'algorithme \(factorielle\).

L'invariant montre que, tout au long de l'exécution, on a correctement calculé la factorielle des valeurs intermédiaires jusqu'à \(n\).

Le variant assure que la boucle se termine.

Par conséquent, l'algorithme est correct et renvoie bien la factorielle de \(n\).

Exercice n°2 : Nombres premiers⚓︎

Soit l'algorithme suivant :

🐍 Editeur

def est_premier(n):
    if n <= 1:
        return False
    i = 2
    while i * i <= n:
        if n % i == 0:
            return False
        i += 1
    return True

Q1. Trouvez un invariant pour la boucle qui calcule le prédicat est_premier(n).

Un invariant de boucle est une propriété qui reste vraie avant et après chaque itération de la boucle. Pour cet algorithme, l'invariant de boucle peut être formulé comme suit :

Invariant : à chaque début d'itération de la boucle while, pour tous les entiers \(k\) tels que \(2 \le k < i\), \(n \% k \neq 0\) et \(i * i \le n\).

En d'autres termes, avant chaque itération de la boucle, on a vérifié que \(n\) n'est divisible par aucun nombre entre \(2\) et \(i-1\), et que \(i * i\) est toujours inférieur ou égal à \(n\).

Q2. Proposez un variant de boucle.

Un variant de boucle est une expression qui décroît strictement avec chaque itération de la boucle et est utilisée pour prouver que la boucle se termine. Pour cet algorithme, un variant de boucle pourrait être :

Variant : \(n - i * i\)

Ce variant diminue à chaque itération, car \(i\) augmente de \(1\) à chaque itération, et donc \(i * i\) augmente. Lorsque \(i * i\) devient plus grand que \(n\), la boucle s'arrête.

Q3. Prouvez la correction de l'algorithme.

Initialisation :

Avant la première itération de la boucle, \(i\) est initialisé à \(2\). À ce point, aucun entier \(k\) ne satisfait \(2 \le k < i\), donc l'invariant est trivialement vrai.

Conservation :

Supposons que l'invariant est vrai au début d'une itération pour un certain \(i\). Si \(n % i = 0\), l'algorithme retourne False, ce qui est correct car \(n\) n'est pas premier. Sinon, \(i\) est incrémenté de \(1\). Pour le nouvel \(i\), tous les entiers \(k\) tels que \(2 \le k < i\) ont été vérifiés, et \(n \% k \neq 0\). De plus, \(i * i <= n\) est toujours vérifié à l'entrée de la boucle.

Terminaison :

La boucle se termine lorsque \(i * i > n\). A ce stade, tous les entiers \(k\) tels que \(2 \le k \le \sqrt{n}\) ont été vérifiés. Si aucune division exacte n'a été trouvée, \(n\) est premier et l'algorithme retourne True.

Q4. Conclure.

En utilisant l'invariant de boucle et le variant, on peut prouver la correction de l'algorithme.

L'invariant montre que, tout au long de l'exécution, on a correctement vérifié que \(n\) n'est divisible par aucun nombre dans la plage spécifiée.

Le variant assure que la boucle se termine. Par conséquent, l'algorithme est correct : il retourne True si et seulement si \(n\) est un nombre premier.

why3, un outil pour découvrir expérimentalement les variants et invariants

Logiciel why3 pour automatiser la « preuve » des programmes (en ligne)