Invariant de boucle

Un article de Wikipédia, l'encyclopédie libre.

En programmation, une boucle est une instruction qui permet de répéter l'exécution d'une partie d'un programme. Un invariant de boucle est une propriété qui est vraie avant et après chaque répétition. C'est une propriété logique, qui permet d'étudier un programme ou un algorithme.

En vérification formelle, en particulier en logique de Hoare, les invariants de boucles sont des prédicats logiques, qui servent à prouver les algorithmes qui les utilisent, en particulier la correction de ces algorithmes.

Un invariant de boucle doit être vrai avant de commencer la boucle et est alors garanti de rester correct après chaque itération de la boucle. En particulier, l'invariant sera toujours vrai à la fin de la boucle. Les boucles et la récursivité étant fondamentalement similaire, il y a peu de différence entre démontrer un invariant de boucles et prouver qu'un programme est correct en utilisant un raisonnement par récurrence. En pratique, l'invariant de boucle est souvent la propriété induction — l'hypothèse d'induction — qui sert à montrer qu'un programme récursif est équivalent à une boucle.

Exemple informel[modifier | modifier le code]

Le programme C max() retourne la valeur du plus grand élément de son argument, le tableau a[], si sa taille n est au moins 1.

Aux lignes 3, 6, 9, 11 et 13 du programme, un commentaire donne une propriété à cette étape de l’exécution du code. Les propriétés des lignes 6 et 11 sont littéralement les mêmes, c'est donc un invariant de la boucle entre les lignes 5 et 12. Quand la ligne 13 est atteinte, l'invariant tient toujours et on sait que la condition de continuation i!=n de la ligne 5 est fausse; ces deux propriétés impliquent que m est égal à la valeur maximale dans a[0...n-1], celle qui doit être calculée par la fonction, donc que la valeur correcte est retournée ligne 14.

 1 int max(int n, const int a[]) {
 2     int m = a[0];
 3     // m est égal à la valeur maximale de a[0...0]
 4     int i = 1;
 5     while (i != n) {
 6         // m est égal à la valeur maximale de a[0...i-1]
 7         if (m < a[i])
 8             m = a[i];
 9         // m est égal à la valeur maximale de a[0...i]
10         ++i;
11         // m est égal à la valeur maximale de a[0...i-1]
12     }
13     // m est égal à la valeur maximale de a[0...i-1], et i==n
14     return m;
15 }

Si le paradigme de programmation défensive était suivi, la condition de boucle i!=n de la ligne 5 devrait être i<n afin d'éviter les boucles infinies pour les valeurs négatives, théoriquement interdites, de n. Même si intuitivement cela ne devrait pas faire de différence, la preuve devient un peu plus complexe puisque seul i>=n est certain ligne 13. Afin d'obtenir i<=n cette condition doit être rajoutée dans l'invariant de boucle. Il reste simple de voir que i<=n est aussi un invariant de boucle puisque i<n ligne 6 peut être obtenu de la condition de boucle (modifiée) de la ligne 5, et donc que i<=n tient ligne 11 après que i ait été incrémenté ligne 10. Cependant, quand les invariants de boucles sont donnés formellement à des programmes de vérification, des propriétés aussi évidentes telles que i<=n ont souvent été ignorées.

Support dans les langages de programmation[modifier | modifier le code]

Eiffel[modifier | modifier le code]

Le langage Eiffel offre nativement un support pour les invariants de boucles[1]. Les invariants de boucles sont exprimés avec une syntaxe similaire à celle des invariants de classes. Dans l'exemple ci-dessous, l'expression d'invariant de boucle x <= 10 doit être vraie après l'initialisation puis après chaque exécution de la boucle, et c'est vérifié à l'exécution.

    from
        x := 0
    invariant
        x <= 10
    until
        x >= 10
    loop
        x := x + 1
    end

Lien interne[modifier | modifier le code]

Référence[modifier | modifier le code]

  1. Meyer, Bertrand, Eiffel: The Language, Prentice Hall, 1991, p. 129–131.

Bibliographie[modifier | modifier le code]