Prouver un algorithme : invariant et terminaison

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, par exemple la température la plus basse d'un relevé. 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, comme le total des consommations relevées sur quatre jours. La boucle ci-dessous additionne les cases d'un tableau, et la trace affiche à chaque tour la valeur de somme et celle de i.

Voici ce que valent les deux variables au moment où la condition est testée, tour après tour, avec en dernière colonne le total des cases qui précèdent t[i] :

i et somme changent à chaque ligne, et pourtant une chose ne change jamais : somme est toujours égale à la dernière colonne. Une relation entre les variables qui tient d'un tour à l'autre porte un nom.

L'invariant de cette boucle 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.

La dernière ligne du tableau 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. La trace le montre sur le tour 3 : il commence avec i = 3 et somme = 11, le total de t[1] et t[2]. Le corps ajoute t[3], qui vaut 2, puis fait passer i à 4. Au test suivant, l'invariant réclame le total de t[1] à t[4 - 1], c'est-à-dire t[1] + t[2] + t[3], soit 13, et somme vaut bien 13. Le même raisonnement vaut pour un tour quelconque, sans connaître les valeurs : si somme contient le total jusqu'à t[i - 1], le corps lui ajoute t[i], et elle contient le total jusqu'à t[i] ; puis i augmente de 1, et « jusqu'à t[i] » avec l'ancienne valeur de i se lit « jusqu'à t[i - 1] » avec la nouvelle. Toute la difficulté tient dans cette dernière phrase : la même lettre désigne deux nombres, avant et après i ← i + 1, et l'invariant se relit toujours avec la valeur que i a au moment du test.
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.

Les deux premiers points sont un raisonnement par récurrence. L'initialisation est le cas de base, la conservation est l'hérédité, et la conclusion est ce qu'on en tire une fois la boucle terminée. C'est exactement le schéma employé sur les suites, décrit dans le chapitre sur les suites. Un invariant de boucle n'est rien d'autre qu'une récurrence appliquée au numéro du tour.

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 : après le tour i, min contient le plus petit des éléments t[1] à t[i]. Si cette propriété tient après chaque tour, alors après le dernier, où i vaut longueur(t), 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 ; à la fin de 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 valeur de min, affichée sous le listing : 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 chaque nouvelle valeur soit comparée à min, le record en cours, et non à la case précédente :

La conservation se démontre maintenant en une phrase. Si, après le tour i - 1, min est le plus petit de t[1] à t[i - 1], alors le plus petit de t[1] à t[i] est soit ce même min, soit t[i] : le test du tour i 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, ce qui est l'invariant pris juste avant le premier tour. La conclusion suit, et l'algorithme est correct pour tous les tableaux, pas seulement pour trois. L'invariant figure désormais en commentaire au-dessus du Pour, là où l'encadré sur la place de l'énoncé demande de l'écrire : le moteur ignore cette ligne, le lecteur non.

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é.

Une boucle Pour s'arrête d'elle-même, puisque son nombre de tours est fixé à l'entrée et que modifier son compteur dans le corps n'y change rien. La question se pose pour le TantQue, dont rien ne garantit a priori que la condition deviendra fausse.

La recherche dichotomique fournit le variant le plus lisible du parcours. Ici, elle cherche la valeur 7 dans un relevé de huit mesures rangées par ordre croissant. 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 variable variant, calculée pour être lue dans la trace mais absente de la condition, prend successivement les valeurs 8, 3, 1 puis 0. Elle décroît strictement et ne descend jamais sous zéro : partie de 8, elle garantit que la boucle s'arrête en huit tours au plus. 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. La dichotomie fait en réalité bien mieux, puisque chaque tour garde au plus la moitié de la portion, soit quatre tours au plus sur ce tableau de huit cases ; mais pour prouver l'arrêt, la décroissance stricte suffit.

Il suffit d'effacer le - 1 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.

Correction = correction partielle + terminaison. L'invariant établit que le résultat est bon si la boucle s'arrête. Le variant établit qu'elle s'arrête. Les deux ensemble, et seulement les deux ensemble, permettent de dire qu'un algorithme est correct.
Les deux moitiés se perdent séparément : une boucle qui ne termine pas peut avoir un invariant parfait, et une boucle qui termine toujours peut rendre n'importe quoi.

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. Son invariant est écrit en commentaire au-dessus du TantQue.

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. Et quand t[milieu] = x, ni bas ni haut ne changent : l'invariant reste vrai sans rien faire. 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. Un tour se termine de deux façons. Si t[milieu] = x, trouve devient non nul et la boucle s'arrête au test suivant : ce tour est le dernier, même si la portion n'a pas rétréci. Dans les deux autres branches, bas passe à milieu + 1 ou haut à milieu - 1, et la taille de la portion, haut - bas + 1, perd au moins la case milieu : elle décroît strictement sans jamais descendre sous zéro. La taille seule n'est donc pas un variant de cette boucle, puisqu'elle ne bouge pas dans la branche qui trouve. Les deux cas se réunissent en un seul variant : la taille de la portion, augmentée de 1 tant que trouve vaut 0. Dans la branche qui trouve, la taille reste la même mais le 1 ajouté disparaît ; dans les deux autres, la taille baisse d'au moins 1 et le 1 reste. Ce variant est entier, jamais négatif, et il baisse d'au moins 1 à chaque tour, quelle que soit la branche prise. C'est exactement la vérification que demande la méthode : la branche qui trouve est la branche rare, et c'est précisément celle où la taille seule ne bouge pas.

Le déroulement de la figure l'illustre, sans rien prouver de plus : ce variant vaut 9 avant le premier tour, puis 5 quand bas passe de 1 à 5, puis 4 quand milieu tombe sur 6 et que trouve prend 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.

Mettre en pratique

Un invariant donne la valeur d'une variable à un tour choisi sans dérouler la boucle, et un variant borne le nombre de tours avant toute exécution. L'un et l'autre se calculent.

La troisième réponse et la quatrième ne se contredisent pas : l'une est ce que la preuve de terminaison garantit, l'autre ce que la dichotomie fait vraiment.

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