Prouver au lieu de tester

Ce que veut dire « démontrer qu'un programme est correct », et pourquoi c'est possible

Le problème, en une phrase

Un test exécute un programme sur un cas et regarde si le résultat est bon. Une preuve établit que le résultat est bon sur tous les cas, sans les exécuter.

Tout le reste de ce dossier découle de cet écart. Il est plus grand qu'il n'en a l'air.

Prenons une fonction qui additionne deux entiers 32 bits. Le nombre de couples possibles est 2⁶⁴, soit environ 18 milliards de milliards. À un milliard de tests par seconde, les essayer tous demanderait près de six cents ans. Pour une fonction de trois arguments, l'univers n'est plus assez vieux.

Un test ne peut donc jamais être exhaustif. C'est la formulation qu'en a donnée Edsger Dijkstra en 1969, et qui est restée :

Le test d'un programme peut servir à montrer la présence de bugs, jamais leur absence.

Cette phrase est souvent citée comme un mot d'esprit. Ce n'en est pas un : c'est une observation de dénombrement. Tester, c'est échantillonner. On peut échantillonner intelligemment — aux bornes, sur les cas dégénérés, au hasard — on échantillonne quand même.

Une histoire vraie : la recherche dichotomique

La recherche dichotomique cherche une valeur dans un tableau trié en coupant l'intervalle en deux à chaque étape. C'est l'algorithme le plus enseigné qui soit. Sa version canonique contient cette ligne :

milieu = (bas + haut) / 2

Elle est fausse.

Si bas et haut sont des entiers 32 bits et que leur somme dépasse 2³¹, l'addition déborde et produit un nombre négatif. milieu devient négatif, l'accès au tableau sort de ses bornes, le programme s'effondre. Il faut écrire :

milieu = bas + (haut - bas) / 2

Cette ligne figurait dans un livre de référence publié en 1986. Elle a été recopiée pendant vingt ans. Elle se trouvait dans la bibliothèque standard de Java, utilisée quotidiennement par des millions de programmes. Joshua Bloch l'y a découverte en 2006.

Elle avait été testée d'innombrables fois. Tous les tests passaient. Il aurait fallu un tableau de plus d'un milliard d'éléments pour la déclencher — ce que personne n'avait dans les mains en 1986, et que personne n'avait pensé à écrire en test ensuite.

Une preuve, elle, aurait buté immédiatement. Le raisonnement qui établit la correction de la dichotomie suppose que milieu est compris entre bas et haut. Il faut démontrer cette hypothèse. Sur des entiers mathématiques, elle est vraie. Sur des entiers 32 bits, la démonstration échoue — et l'endroit exact où elle échoue est exactement l'endroit du bug.

C'est le motif général. Une preuve ne trouve pas les bugs : elle échoue à l'endroit du bug. La différence est qu'elle ne peut pas passer à côté.

Pourquoi c'est possible

Objection immédiate : si les cas sont en nombre astronomique, comment peut-on affirmer quelque chose sur tous ?

Parce que le programme, lui, est fini. Il tient sur quelques pages. Et le raisonnement suit la structure du texte, pas celle des données.

Prenons la valeur absolue :

fonction abs(x) :
    si x < 0 alors renvoyer -x
    sinon renvoyer x

Combien de valeurs possibles pour x ? Quatre milliards. Combien de cas à examiner pour démontrer que abs(x) est toujours positif ? Deux.

Si x < 0, on renvoie -x. Or l'opposé d'un nombre négatif est positif. Correct.
Si x ≥ 0, on renvoie x, qui est positif par hypothèse. Correct.

Ces deux cas couvrent tout. Non par échantillonnage, mais parce que le si du programme découpe lui-même l'espace en deux morceaux, et que dans chaque morceau on peut raisonner sur une propriété partagée plutôt que sur des valeurs individuelles.

C'est le principe central, et il n'y en a pas d'autre : le raisonnement suit la forme du programme. Un si donne deux cas. Une séquence d'instructions se traite instruction par instruction. Une boucle se traite par récurrence — c'est le point difficile, et l'article suivant y revient en détail. Un programme de cent lignes demande de l'ordre de cent petits raisonnements, pas 2¹⁰⁰⁰ vérifications.

(Cet exemple a d'ailleurs un piège, et il est instructif : sur des entiers 32 bits, abs du plus petit entier négatif, −2 147 483 648, vaut… lui-même. Son opposé n'est pas représentable. La ligne « l'opposé d'un nombre négatif est positif » est fausse dans ce cas précis. Une preuve menée sérieusement s'arrête là et exige qu'on traite le cas. Le lecteur constatera qu'il n'y a pas d'exemple si petit qu'il soit à l'abri.)

Ce qu'est une spécification

Avant de démontrer qu'un programme est correct, il faut dire ce que « correct » signifie. C'est un énoncé séparé du programme, et cette séparation est la moitié du travail.

La spécification décrit quoi, le programme décrit comment. Pour une fonction de tri :

Spécification. Étant donné un tableau t, la fonction renvoie un tableau r tel que :

r est trié par ordre croissant ;

r contient exactement les mêmes éléments que t, avec les mêmes multiplicités.

Deux remarques sur cet énoncé.

La condition 2 n'est pas décorative. Sans elle, la fonction qui renvoie un tableau vide satisfait la spécification. Celle qui renvoie mille zéros aussi. Une spécification incomplète est satisfaite par des programmes absurdes, et c'est le mode de défaillance le plus courant de toute la discipline — l'article IV y revient.

La spécification ne dit rien du comment. Tri fusion, tri rapide, tri à bulles : elle les accepte tous. Elle ne dit rien non plus de la vitesse, de la mémoire, ni du fait que le tri soit stable. Ce qui n'est pas écrit n'est pas garanti. Une preuve est un contrat, et un contrat ne couvre que ses clauses.

L'objet mathématique

Reste à justifier le mot « mathématique », qui peut sembler emprunté.

Il ne l'est pas, et c'est même une particularité du logiciel. Un pont est un objet physique : l'acier a des défauts, le sol tasse, le vent souffle. Aucun calcul ne dit tout de lui, et l'ingénieur applique des coefficients de sécurité — c'est-à-dire qu'il compense l'ignorance par de la marge.

Un programme n'a pas cette matérialité. C'est un texte fini, dans un langage aux règles définies, exécuté par une machine dont le comportement est spécifié. Il n'y a rien à mesurer : tout est déjà écrit. Un programme est plus proche d'une démonstration que d'un pont, et la question « ce programme est-il correct ? » est de même nature que « cette démonstration est-elle juste ? ».

Cette parenté est plus profonde qu'une analogie. Elle porte un nom — la correspondance de Curry-Howard — et l'article suivant montre qu'un simple vérificateur de types en est déjà une exploitation quotidienne, y compris chez ceux qui n'ont jamais entendu le terme.

Deux réserves, importantes, pour ne pas laisser croire que la matière a disparu.

D'abord, la machine réelle n'est pas exactement la machine idéalisée. Les entiers débordent — on vient d'en voir deux exemples. La mémoire est finie. Les flottants ne sont pas les réels. Une preuve menée sur des entiers mathématiques alors que le code tourne sur des entiers 32 bits démontre quelque chose de vrai à propos d'un programme qui n'existe pas. Les outils sérieux modélisent l'arithmétique machine, exactement.

Ensuite, la machine physique peut trahir : un rayon cosmique retourne un bit, un processeur a un défaut de conception. Ces choses arrivent et aucune preuve ne les couvre. La correction démontrée d'un programme est une correction sous hypothèse que la machine respecte sa spécification. C'est une hypothèse excellente, ce n'est pas une certitude.

Les trois niveaux

Entre « aucune garantie » et « tout démontré » il n'y a pas un fossé mais une pente. Trois repères suffisent à s'orienter.

Les tests échantillonnent. Coût faible, garantie faible, valeur réelle : ils attrapent les fautes grossières, qui sont la majorité. On ne les abandonne pas parce qu'on prouve.

Les propriétés vérifiées automatiquement sont l'étage intermédiaire, et le meilleur rapport entre effort et garantie. Un vérificateur de types démontre à chaque compilation qu'aucune exécution ne confondra un texte et un nombre : une preuve sur une infinité de cas, gratuite, que tout le monde utilise sans y penser. Une contrainte UNIQUE en base de données garantit qu'aucune insertion, jamais, ne créera de doublon. Un test de propriété tire mille cas au hasard plutôt qu'un seul choisi à la main.

La preuve complète établit la conformité entière à une spécification. Coût élevé, garantie maximale. On la réserve à ce dont la défaillance est intolérable : commandes de vol, signalisation ferroviaire, cryptographie, noyaux de systèmes, compilateurs.

Le reste de ce dossier décrit comment fonctionne le troisième niveau — l'article II pour le code, l'article III pour les bases de données — puis, dans l'article IV, ce que ce troisième niveau ne donne pas, même quand il réussit.