Prouver un algorithme

Jusqu'ici, la façon de contrôler un algorithme a toujours été la même : le dérouler sur un jeu d'essai et comparer la sortie à ce qui était attendu. Cette méthode est indispensable, et elle a un défaut que rien ne corrigera jamais : elle ne parle que des données essayées. Un jeu d'essai qui échoue prouve qu'il y a une faute. Un jeu d'essai qui passe ne prouve rien.

La question posée ici est donc concrète, et elle se pose devant n'importe quelle boucle un peu longue : comment savoir qu'elle fait bien ce qu'on croit, alors qu'il est impossible d'essayer toutes les entrées possibles. La réponse tient en une phrase écrite au bon endroit.

Trois essais qui passent ne prouvent rien

Voici un algorithme qui cherche le plus petit élément d'un tableau. Il est presque juste, et c'est ce « presque » qui fait tout le chapitre.

Le résultat affiché est 2, et c'est bien le plus petit élément du tableau. Un deuxième essai sur [3, 1, 4] rendrait 1, un troisième sur [6, 6, 6] rendrait 6. Trois essais, trois succès : l'algorithme paraît correct, et il serait mis en production sans hésiter.

Il est faux. La même ligne, sur un autre tableau :

Le résultat affiché est 6, alors que le plus petit élément vaut 5. Une seule case a changé par rapport au tableau précédent, et la réponse est devenue fausse.

La faute, ici, est visible à l'œil une fois qu'elle est nommée : la comparaison porte sur t[i] < t[i - 1], c'est-à-dire sur l'élément précédent du tableau, alors qu'elle devrait porter sur le minimum retenu jusque-là. L'algorithme compare chaque valeur à sa voisine au lieu de la comparer au record en cours. Reste à savoir comment on trouve ce genre de faute sans avoir la chance de tomber sur le bon jeu d'essai.

L'invariant de boucle

L'idée est de renoncer à parler des données et de parler de la boucle elle-même. Plutôt que de demander « que vaut le résultat sur ce tableau », on énonce une propriété qui décrit ce que les variables contiennent à chaque tour, et on montre que la boucle la préserve.

Le cas le plus simple est celui d'une somme. La boucle ci-dessous additionne les cases d'un tableau, et la trace affiche à chaque tour la valeur de somme et celle de i.

L'invariant s'énonce ainsi : au moment de tester la condition, somme contient le total des cases t[1] à t[i - 1]. Il se lit directement dans la figure, parce que les deux variables qu'il met en relation sont justement celles que le moteur affiche. À dérouler la boucle pas à pas, la vérification se fait tour après tour :

La dernière ligne est celle qui conclut : à la sortie, i vaut 5, donc l'invariant affirme que somme contient le total des cases t[1] à t[4], c'est-à-dire de tout le tableau. Le résultat cherché tombe alors sans qu'il ait été nécessaire de connaître les valeurs du tableau.

Les trois obligations d'un invariant

Vérifier un invariant sur cinq lignes de trace est un bon exercice de lecture, mais ce n'est encore qu'un jeu d'essai déguisé. La preuve proprement dite tient en trois points, et il faut les trois.

1. L'initialisation. L'invariant est vrai avant d'entrer dans la boucle. Ici, somme vaut 0 et i vaut 1 : l'invariant réclame le total des cases t[1] à t[0], c'est-à-dire d'aucune case, et le total d'aucune case vaut bien 0.
2. La conservation. Si l'invariant est vrai au début d'un tour, il est encore vrai au début du tour suivant. En supposant somme égale au total de t[1] à t[i - 1], le corps ajoute t[i] puis augmente i de 1 : somme contient alors le total de t[1] à t[i], qui est bien le total de t[1] à t[i - 1] pour la nouvelle valeur de i.
3. La conclusion. Combiné à la raison qui fait sortir de la boucle, l'invariant donne le résultat voulu. On sort quand i > longueur(t), et comme i augmente de 1 par tour, on sort avec i = longueur(t) + 1 exactement : somme contient le total de tout le tableau.

Un invariant qui se casse, et le tour exact où il se casse

Retour à l'algorithme faux du début. L'invariant qu'il faudrait pour conclure est évident : min contient le plus petit des éléments t[1] à t[i]. Si cette propriété tient à chaque tour, alors au dernier tour min contient le plus petit de tout le tableau, et l'algorithme est juste.

La figure suivante vérifie cet invariant elle-même. Une variable reference suit le plus petit élément réellement rencontré, calculé correctement ; à chaque tour, la comparaison entre min et reference dit si l'invariant tient encore.

La sortie produite est sans ambiguïté :

tour 2 : min = 5 = plus petit de t[1..2] : invariant tenu
tour 3 : min = 5 = plus petit de t[1..3] : invariant tenu
tour 4 : min = 7 alors que le plus petit de t[1..4] vaut 5 : invariant rompu
tour 5 : min = 6 alors que le plus petit de t[1..5] vaut 5 : invariant rompu

L'invariant tient deux tours, et se rompt au tour 4. À dérouler la figure jusque-là, le moment se voit dans la colonne min : elle passe de 5 à 7. Une variable censée contenir un minimum vient d'augmenter, ce qui est absurde en soi, et la ligne responsable est celle qui vient d'être exécutée.

L'invariant fait alors office de cahier des charges pour la correction. Il faut que min soit comparé à ce qu'il contient, et non à la case précédente :

La conservation se démontre maintenant en une phrase. Si min est le plus petit de t[1] à t[i - 1] en entrant dans le tour, alors le plus petit de t[1] à t[i] est soit ce même min, soit t[i] : le test choisit exactement le bon des deux. L'initialisation est vraie parce que min ← t[1] fait de min le plus petit d'une portion d'un seul élément. La conclusion suit, et l'algorithme est correct pour tous les tableaux, pas seulement pour trois.

La terminaison se prouve à part : le variant

Tout ce qui précède établit une chose, et une seule : si la boucle s'arrête, le résultat est le bon. C'est ce que l'on appelle la correction partielle, et le « si » n'est pas une formalité.

La recherche dichotomique fournit le variant le plus lisible du parcours. La portion encore à explorer va de bas à haut ; sa taille, haut - bas + 1, est le variant. La figure la calcule à chaque tour, pour qu'elle se lise dans la trace au même titre que les autres variables.

La colonne variant prend successivement les valeurs 8, 3, 1 puis 0. Elle décroît strictement, elle ne descend jamais sous zéro, et la boucle s'arrête donc après quatre tours au plus sur ce tableau. Le raisonnement ne dépend pas des valeurs : chaque tour remplace bas par milieu + 1 ou haut par milieu - 1, et dans les deux cas la portion perd au moins la case milieu.

Il suffit de retirer un seul caractère pour que la garantie disparaisse. Dans la version suivante, l'auteur a écrit haut ← milieu au lieu de haut ← milieu - 1.

Le déroulement s'interrompt de lui-même : le moteur refuse d'aller au-delà de cinq cents pas et le signale. Les trois premiers tours sont irréprochables, haut descend de 8 à 4 puis à 3, et bas monte à 3. Puis bas et haut valent tous les deux 3, milieu vaut 3, la valeur cherchée est plus petite que t[3], donc haut ← milieu réaffecte 3 à une variable qui valait déjà 3. Le variant reste bloqué à 1, et rien ne le fera plus descendre.

Preuve complète d'une recherche dichotomique

Reste à mettre les deux moitiés bout à bout sur un algorithme utile. La recherche dichotomique, étudiée dans le chapitre diviser pour régner, cherche une valeur dans un tableau trié en coupant en deux à chaque tour.

L'invariant. Si x figure dans le tableau, alors son indice est compris entre bas et haut. La formulation compte : l'invariant ne promet pas que x est présent, il promet que la portion bas à haut est le seul endroit où il peut encore se trouver.

L'initialisation. Avant le premier tour, bas vaut 1 et haut vaut longueur(t) : la portion est le tableau entier, et l'invariant est vrai sans rien supposer.

La conservation. Le tableau étant trié, si t[milieu] < x, alors toutes les cases d'indice inférieur ou égal à milieu contiennent des valeurs inférieures à x, donc x ne peut pas s'y trouver, et bas ← milieu + 1 conserve l'invariant. Le cas symétrique se traite de la même façon. C'est ici, et nulle part ailleurs, que l'hypothèse « le tableau est trié » est utilisée : la preuve désigne elle-même la condition d'emploi de l'algorithme.

La conclusion. La boucle s'arrête pour deux raisons possibles. Soit trouve est devenu non nul, et t[trouve] = x a été testé directement. Soit bas > haut, la portion est vide, et l'invariant affirme que x ne pouvait être que là : x est donc absent du tableau.

La terminaison. Le variant est haut - bas + 1, déjà examiné plus haut. Sur ce déroulement, la trace montre bas passer de 1 à 5, puis milieu tomber sur 6 et trouve prendre la valeur 6 : la valeur 23 est bien en sixième position, et deux tours ont suffi là où un parcours case par case en aurait demandé six.

Vérification

Exercices type

Exercice 1 : énoncer l'invariant de la boucle extérieure du tri par insertion, et le vérifier sur la trace.

après le tour 2 : 3 7 9 1 5 2
après le tour 3 : 3 7 9 1 5 2
après le tour 4 : 1 3 7 9 5 2
après le tour 5 : 1 3 5 7 9 2
après le tour 6 : 1 2 3 5 7 9

Exercice 2 : l'algorithme suivant est censé compter les éléments strictement positifs d'un tableau. Énoncer son invariant et dire s'il tient.

compte ← 0
Pour i de 1 à longueur(t)
    Si t[i] > 0 Alors
        compte ← 1
    FinSi
FinPour

Exercice 3 : proposer un variant pour une boucle qui divise n par 2 tant que n est pair.

La méthode

1. Écrire l'invariant avant la boucle, pas après l'algorithme. Une boucle dont l'invariant ne s'énonce pas est une boucle dont l'intention n'est pas claire, et c'est le moment de la réécrire plutôt que de la prouver.
2. Le formuler sur les variables que la trace affiche. Un invariant qui parle d'une quantité invisible ne se vérifie pas pas à pas ; un invariant qui relie i et l'accumulateur se contrôle d'un coup d'œil sur chaque tour.
3. Vérifier les trois obligations dans l'ordre : vrai avant le premier tour, préservé par un tour quelconque, concluant une fois combiné à la condition de sortie.
4. Traiter la conclusion avec la valeur exacte de sortie. Sortir avec i = longueur(t) + 1 et sortir avec i = longueur(t) ne donnent pas le même résultat, et c'est là que se logent les erreurs d'un tour.
5. Poser le variant séparément : une quantité entière, positive ou nulle, que chaque tour fait décroître strictement. Vérifier que la décroissance est stricte dans tous les cas du corps, y compris les branches rares.
6. Faire dire à la figure si l'invariant tient. Ajouter le calcul de référence et un message par tour transforme une figure qui illustre en figure qui vérifie, et le tour de la rupture apparaît sans discussion.

Synthèse

• Un jeu d'essai qui échoue prouve la présence d'une faute ; un jeu d'essai qui passe ne prouve pas son absence.
• Un invariant de boucle est une propriété des variables, vraie avant le premier tour et préservée par chaque tour. Ses trois obligations sont l'initialisation, la conservation et la conclusion.
• Un invariant supposé qui se rompt désigne le tour exact de la faute, et la figure le montre quand elle calcule elle-même la valeur de référence.
• Un variant est une quantité entière positive qui décroît strictement à chaque tour ; son existence prouve la terminaison, et la décroissance doit être stricte.
• La correction d'un algorithme est la réunion de la correction partielle, donnée par l'invariant, et de la terminaison, donnée par le variant.

Le chapitre suivant, gloutons et programmation dynamique, met ces outils au travail sur une famille d'algorithmes où l'intuition se trompe souvent : ceux qui choisissent à chaque étape ce qui paraît le mieux sur le moment.