Invariant de boucle

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 il est garanti qu'il restera vrai 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 similaires, 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

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.

int max(int n, const int a[]) {
    int m = a[0];
    // m est égal à la valeur maximale de a[0...0]
    int i = 1;
    while (i != n) {
        // m est égal à la valeur maximale de a[0...i-1]
        if (m < a[i])
            m = a[i];
        // m est égal à la valeur maximale de a[0...i]
        ++i;
        // m est égal à la valeur maximale de a[0...i-1]
    }
    // m est égal à la valeur maximale de a[0...i-1], et i==n
    return m;
}

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

Eiffel

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

• Variant de boucle (en), une fonction mathématique associée à un algorithme, permettant par exemple de prouver la terminaison d'une boucle while.

Références

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

Bibliographie

• Thomas H. Cormen, Charles E. Leiserson, Ronald L. Rivest, and Clifford Stein. Introduction à l'algorithmique, Deuxième édition. Dunod 2004 (ISBN 2-1000-3922-9). Pages 16, section 2.1: Tri par insertion.
• David Gries, « A note on a standard strategy for developing loop invariants and loops », Science of Computer Programming, vol. 2, p. 207–214, 1984.
• Michael D. Ernst, Jake Cockrell, William G. Griswold, David Notkin. « Dynamically Discovering Likely Program Invariants to Support Program Evolution », International Conference on Software Engineering, p. 213–224, 1999.
• Robert Paige, « Programming with Invariants », IEEE Software, 3(1):56–69, janvier 1986.
• Yanhong A. Liu, Scott D. Stoller et Tim Teitelbaum, « Strengthening Invariants for Efficient Computation », Science of Computer Programming, 41(2):139–172, octobre 2001.
• Michael Huth, Mark Ryan, Logic in Computer Science, Second Edition.