Construire des logiciels fiables

Les « bugs » informatiques, c’est-à-dire les erreurs involontaires de programmation, peuvent avoir des conséquences désastreuses, quand elles ont lieu dans un logiciel critique, comme dans un centre d’appel téléphonique d’urgence (cf. la panne des numéros d’urgence en France en juin 2021), ou pire dans le système de sécurité d’une centrale nucléaire. Nous allons voir comment la programmation défensive formellement vérifiée, en complément des méthodes traditionnelles du génie logiciel, permet de réduire significativement les risques de telles erreurs. En passant, nous discuterons de pensée floue, puis de formalisation mathématique en l’illustrant sur des problèmes proches des « sudokus » (en fait les problèmes SAT booléens).

À première vue, les erreurs involontaires de programmation logicielle, plus ordinairement appelées « bugs », ont des causes multiples : erreurs d’étourderie ou d’inattention (par exemple, interversion des noms « i » et « j ») ; contresens sur la signification d’un morceau de programme ou du cahier des charges (censé donné la description du comportement attendu du logiciel) ; sur-interprétation d’un cahier des charges ambigu, incomplet ou contenant du non-dit ; vraie erreur de raisonnement (par exemple mauvaise compréhension d’un concept, utilisation d’une hypothèse implicite fausse) ; etc. Pour empêcher ou détecter de telles erreurs lors du développement logiciel, l’état de l’art recommande de combiner un ensemble de « bonnes pratiques ». En pratique, il reste cependant toujours des bugs qui sont détectés bien trop tard, une fois que le logiciel est déjà entré en service.

Erreurs et pensée floue

Les sciences cognitives apportent un éclairage sur cette difficulté à construire des logiciels sans bug. Par exemple, considérons le problème suivant :

« Une balle et une batte coûtent au total \(1,10\) $. La batte coûte \(1\) $ de plus que la balle. Combien coûte la balle ? »

Selon le psychologue et économiste américano-israélien Daniel Kahneman, prix Nobel d’économie en 2002 pour ses travaux sur les biais cognitifs, la plupart d’entre nous (d’après les résultats de sondages réalisés sur les campus américains) répondent incorrectement « la balle coûte \(10\) cents », surtout si la réponse doit être donnée rapidement sans avoir le temps de réfléchir. Autrement dit, nous calculons intuitivement \(1,10 − 1 = 0,10\) sans nous rendre compte que le prix de la batte serait alors lui-même de \(1,10\) $ et donc que le coût total serait de \(1,20\) $. Le calcul correct est en fait légèrement plus compliqué : \(10\) cents, c’est ce qui reste à payer quand on a donné le dollar supplémentaire pour la batte, il reste à partager ce prix équitablement entre la balle et la batte. Le calcul correct est donc \((1,10 − 1) ÷ 2.\)

L’origine de telles erreurs s’explique par le fait que nous pensons principalement et préférentiellement de façon « floue ». Par exemple, considérons le concept familier de canard. Scientifiquement, ce concept n’est pas un taxon bien défini de la classification systématique des espèces vivantes : il est considéré comme ambigu. L’intérêt de ce concept flou, c’est que tout en s’appliquant à un grand nombre d’individus différents, il nous permet de distinguer instantanément et sans effort un canard d’un lapin, ce qui s’avère par exemple très utile pour anticiper les mouvements possibles de l’animal. Mais, comme le montre le dessin ci-dessous, ce flou est déformable jusqu’à l’absurde. Un tel flou entoure en fait la plupart de nos concepts (un autre exemple : combien de cheveux doit porter une tête pour cesser d’être « chauve » ?), et plus généralement de nos pensées, même verbalisées.

Artiste inconnu, Public domain, via Wikimedia Commons.

Regardons à nouveau le dessin ci-contre. Parmi les deux phrases entre guillemets suivantes, quelle est celle qui vous semble la plus appropriée pour caractériser ce que vous voyez ?

« je vois une tête de canard ou je vois une tête de lapin »

ou  bien « je vois une tête de canard et je vois une tête de lapin » ?

Étonnamment, le « ou » et le « et » semblent ici relativement similaires à quelques nuances près : le « ou » permet de suggérer le caractère non simultané des deux actions « je vois » ; tandis que le « et » permet d’en souligner le caractère contradictoire. Ailleurs, au restaurant par exemple, si le menu propose « fromage ou dessert », il faut choisir entre les deux. Au contraire, chez des proches, une proposition identique en fin de repas n’interdirait pas forcément de prendre les deux. Les mots « ou » et « et » semblent donc s’exclure ou pas en fonction du contexte. Pour éviter cette ambiguïté, les mathématiciens et mathématiciennes en restreignent l’usage en leur donnant un sens très précis. Nous allons y revenir.

Mais donner un sens univoque aux mots ne suffit pas à rendre les phrases non ambiguës. Par exemple, dans la phrase « le tribunal juge l’enfant sauvage », qui juge que l’enfant est sauvage ? Soit c’est le tribunal, si l’adjectif « sauvage » est considéré comme un complément du verbe « juge ». Soit c’est le locuteur ou la locutrice, si cet adjectif est considéré comme un complément du nom « enfant ». Bien sûr une telle ambiguïté grammaticale est évitable : il suffit ici de mettre la phrase sous la forme passive. La difficulté, c’est qu’au moment où nous énonçons ce genre de phrase, nous ne nous apercevons pas forcément de l’ambiguïté qu’elle recèle.

Essayer de penser moins flou est donc long et difficile : il faut beaucoup d’efforts, de la concentration, mais surtout de la méthode dirait Descartes. Car comme illustré ci-dessus, la pensée floue se niche au cœur même des langues humaines. En réaction, depuis plusieurs milliers d’années, les êtres humains construisent un langage dédié à la définition de concepts non flous et à la vérification que les raisonnements sur ces concepts sont corrects. Ce langage, c’est la mathématique.

Contrôler la pensée floue par la formalisation mathématique

La mathématique ne fait pas magiquement disparaître les difficultés, mais elle offre des outils. Notamment, le processus de vérification de la formalisation, qui, « idéalement » (cette vision un peu simpliste sera nuancée par la suite), ne suppose justement plus aucune forme de pensée et peut ainsi être complètement mécanisé. Cela n’interdit pas toute forme d’erreur, notamment des erreurs d’inattention. Mais ce risque est évitable en délégant cette vérification à un programme informatique, pour peu que celui-ci ait été lui-même bien vérifié.

Ainsi, la vérification du raisonnement mathématique est un processus mécanisable, exactement comme la vérification lexicographique — qui vérifie que nos textes n’utilisent que des mots du dictionnaire — ou comme la vérification de la cohérence des unités, méthode apprise au lycée pour vérifier ses solutions aux exercices de physique/chimie. Les langages de programmation s’étant déjà inspirés de tels procédés pour détecter certaines erreurs dans les programmes, via la « vérification des types », une façon de détecter plus d’erreurs de programmation est d’étendre la vérification des types à la vérification des raisonnements justifiant la correction de ces programmes informatiques. Dans les langages de programmation, la « vérification statique des types » généralise la vérification de la cohérence des unités physiques. D’un certain de point de vue, appelé isomorphisme de Curry-Howard, la vérification des preuves mathématiques s’apparente aussi à de la vérification des types.

Heuristique versus vérification

Au contraire du processus de vérification, le processus de formalisation lui-même est extrêmement difficile : c’est là que réside l’art mathématique (pour découvrir comment pense un mathématicien, lire le magnifique « Mathematica » de David Bessis). Aussi, généralement, les mathématiciens et mathématiciennes ne cherchent pas à formaliser comment ils ou elles inventent des mathématiques. Ils se contentent simplement de formaliser pourquoi leurs énoncés sont corrects.

Tout un chacun peut appréhender cette dichotomie entre heuristique et vérification sur des casse-têtes comme les sudokus : il est beaucoup plus rapide et facile de vérifier qu’un candidat de solution à un tel problème est correct, plutôt que d’inventer cette solution.

Vérifier une solution aux \(n\)-reines

Illustrons cela sur les casse-têtes, un peu plus simples, de \(n\)-reines. Dans la version « de base », il s’agit de placer \(n\) reines sur un échiquier de taille \(n × n\) de façon qu’aucune d’elles ne puisse en prendre une autre avec un seul mouvement (pour un mouvement d’une reine aux échecs : vertical, horizontal, ou diagonal). Trouver une solution pour \(n = 4\) demande un peu de réflexion. Mais vérifier que la figure 1 ci-dessus donne une solution est immédiat. Dans une variante, comme sur la figure 2 ci-dessus, l’échiquier peut initialement contenir des cases avec des reines déjà posées, et des cases où il est interdit de poser une reine (mais n’interdisant pas aux reines de « passer » pour en prendre une autre).

À vous d’essayer :

Le problème des \(3\)-reines a-t-il une solution ? Et la variante du problème des \(8\)-reines dessinée sur la figure 2, où une reine est déjà posée en ligne 1 et colonne 1, case notée plus simplement \(11\), et où il est de plus interdit de poser une reine aux cases \(83\) (ligne \(8\), colonne \(3\)) et \(64\) (ligne \(6\), colonne \(4\)) ?

Preuve visuelle de l’absence d’une solution aux \(n\)-reines

Considérons maintenant le problème des \(4\)-reines avec une reine déjà posée en case \(11\). Ce casse-tête n’a pas de solution. La preuve « visuelle » (voir la figure 3 ci-dessus) permet de le vérifier très simplement. Dans celle-ci, le caractère « ? » représente une case pouvant éventuellement contenir une reine sans être prise ; au contraire, les cases avec un numéro \(k\) sont atteignables par la reine éventuelle de la ligne \(k\). L’absence de solution se déduit de l’impossibilité de placer une reine à la ligne \(4\), celle-ci n’ayant pas de « ? ». Les cases laissées vides peuvent être ignorées dans la preuve d’absence de solution.

Preuve verbalisée de l’absence d’une solution aux \(n\)-reines

Pour expliciter davantage le raisonnement, rédigeons maintenant cette preuve dans un style mathématique plus classique. Utilisons une preuve par l’absurde : en supposant l’existence d’une solution satisfaisant les contraintes, on déduit une contradiction. Cela garantit qu’une telle solution est impossible.

Théorème Il n’y a pas de solution au problème des \(4\)-reines avec une reine en case \(11\).

Preuve

Supposons qu’une telle solution existe.

• Montrons d’abord que la case \(32\) (ligne \(3\), colonne \(2\)) contient une reine : en effet, comme \(21\) et \(22\) sont atteignables depuis \(11\), la reine de la ligne \(2\) est en \(23\) ou \(24\) et elle peut donc atteindre \(34\) ; comme par ailleurs \(31\) et \(33\) sont atteignables depuis \(11\), la reine de la ligne \(3\) est nécessairement en \(32\).
• Montrons ensuite qu’il est impossible de placer une reine en ligne \(4\) : en effet, \(41\) et \(44\) sont atteignables depuis \(11\) ; de même, \(42\) et \(43\) sont atteignables depuis \(32\).
• Absurde : dans toute solution, il doit y avoir une reine en ligne \(4\).

Remarquons que cette preuve s’arrange pour propager des contraintes ligne à ligne, en réduisant le nombre de possibilités de placer une reine à la ligne suivante. Elle reste ainsi concise, en évitant soigneusement une approche naïve par « essai-échec », énumérant tous les placements possibles.

De façon plus générale, les preuves mathématiques évitent d’avoir à tester un nombre élevé, voire infini de cas. Par exemple, nous allons définir dans la suite du procédé de vérification qu’un problème de \(n\)-reines donné a ou n’a pas de solution. Et nous allons prouver mathématiquement que les réponses données par ce procédé sont correctes. Cette preuve le garantira quel que soit le problème de \(n\)-reines, en particulier, quel que soit le \(n\) (il y en a une infinité possible).

Mécaniser la vérification des mathématiques

Pour vérifier de façon vraiment mécanique (notamment à l’aide d’un logiciel) les raisonnements ou les théories mathématiques, il faut développer une théorie mathématique du langage mathématique : c’est ce qu’on appelle une logique formelle. Cela permet de comprendre de façon non floue ce que doit faire le vérificateur et éventuellement de vérifier que ce vérificateur est correct. Comme formaliser « l’ensemble » du langage mathématique serait trop ambitieux, ce document en illustre la méthode sur un minuscule fragment, appelé logique des propositions conjonctives de booléens, tout juste suffisant pour formaliser les problèmes de \(n\)-reines (et de sudokus). Toutefois, cela donne déjà un bon aperçu de comment formaliser la mathématique.

Propositions et variables logiques

Toute logique formelle repose sur un langage de propositions. Une telle proposition représente un énoncé, qui peut valoir soit « vrai », soit « faux », en fonction de l’interprétation des variables apparaissant dans cet énoncé. Dans le cadre de notre logique, les variables sont simplement des entiers naturels non nuls qui sont eux-mêmes interprétés uniquement comme valant soit vrai, soit faux.

Typiquement, pour définir les problèmes de \(n\)-reines dans notre logique, nous représenterons chaque case de l’échiquier par une variable distincte, avec la convention que sa valeur « vrai » signifie « il y a une reine sur cette case ». Dans le cas des \(4\)-reines, nommons chacune des \(16\) variables directement par l’entier qui représente la position de la case dans l’échiquier : \(11\), \(12\),…, \(14\), \(21\), …

Pour définir mathématiquement le langage des propositions, nous aurons éventuellement besoin de nommer des (noms de) variables. Nous utiliserons alors \(x\), \(x\)₁, \(x\)₂… Autrement dit, chacun de ces \(x\) représentera un entier qui est lui-même une variable logique. C’est un exemple de ce que nous appelons dans la suite des méta-variables : des noms désignant certains fragments des propositions logiques.

Notre langage est bâti sur une hiérarchie de \(3\) catégories de propositions, incluses les unes dans les autres. Ainsi, une théorie sera représentée par une conjonction (c’est-à-dire un « et logique ») de clauses, ces dernières étant alors considérées comme des axiomes de ladite théorie. Les clauses sont elles-mêmes des propositions plus simples que ces propositions conjonctives. Mais commençons par le commencement…

Littéraux

Au niveau le plus élémentaire, les propositions s’appellent des littéraux et sont uniquement soit de la forme « \(−x\) » dont la valeur de vérité est l’opposée de celle de \(x\), soit de la forme « \(x\) » (de valeur de vérité \(x\)). Par exemple, dans la théorie des \(4\)-reines, le littéral « \(34\) » exprime qu’il y a une reine en case \(34\). Le littéral « \(−34\) » exprime qu’il y n’a pas de reine en case \(34\).

Nous utilisons \(ℓ\), \(ℓ\)₁, \(ℓ\)₂, … comme méta-variables de littéraux. L’opération involutive « \(−ℓ\) » est alors définie comme retournant le littéral de valeur opposée à \(ℓ\) (en ajoutant/supprimant le symbole « \(−\) » devant la variable).

Clauses

Au niveau intermédiaire, les propositions s’appellent des clauses et sont des ensembles finis de littéraux. Nous écrirons ces ensembles sous la forme de liste de littéraux séparés par des espaces. Par définition, une telle clause vaut vrai si et seulement si au moins un de ses littéraux vaut vrai. La clause vide sera écrite « F » et a pour valeur faux.

Par exemple, dans la théorie des \(4\)-reines, l’énoncé « la ligne \(2\) doit contenir au moins une reine » peut s’écrire comme la clause « \(21\) \(22\) \(23\) \(24\) ». Autrement dit, chaque espace représente un « ou » logique. Autre exemple, l’énoncé « les cases \(21\) et \(43\) ne peuvent pas contenir toutes les deux une reine » peut s’écrire comme la clause « \(−21\) \(−43\) ». Un dernier exemple, l’énoncé « si la case \(11\) contient une reine, alors la \(34\) aussi » s’écrit comme la clause « \(−11\) \(34\) ». En effet, « \(−11\) \(34\) » vaut vrai si et seulement si « \(11\) vaut faux ou \(34\) vaut vrai », ce qui est logiquement équivalent à « si \(11\) vaut vrai alors \(34\) vaut vrai » (énoncé en particulier vrai quand \(11\) vaut faux).

Les méta-variables de clauses sont notées \(c\), \(c\)₁, \(c\)₂, … Nous noterons aussi « \(c\)₁ \(c\)₂ » la clause résultant de l’union des deux clauses \(c\)₁ et \(c\)₂ (formée des littéraux étant dans \(c\)₁ ou dans \(c\)₂). Pour éviter les ambiguïtés en cas d’absence de parenthèses, nous considérons que l’espace est prioritaire sur tous les autres opérateurs binaires introduits par la suite (mais pas le « moins unaire », précédemment introduit). Lorsque nous souhaiterons commencer le calcul par une opération moins prioritaire que l’espace, par exemple « \ », nous utiliserons des parenthèses, comme usuellement en arithmétique ou en algèbre, par exemple dans « \(c\)₁ (\(c\)₂ \ \(c\)₃) ». Cette expression calcule ainsi l’union de \(c\)₁ et « \(c\)₂\ \(c\)₃ », alors que, d’après nos règles de priorités :

• « \(c\)₁ \(c\)₂ \ \(c\)₃ » est identique à « (\(c\)₁ \(c\)₂) \ \(c\)₃ »
• « \(c\)₁ \ \(c\)₂ \(c\)₃ » est identique à « \(c\)₁ \ (\(c\)₂ \(c\)₃) »

Conjonctions

Enfin, dans le cas général, nos propositions conjonctives sont des ensembles finis de clauses, écrits sous la forme de liste de clauses séparées par le symbole « \(∧\) ». Par définition, une telle conjonction vaut vrai si et seulement si toutes ses clauses valent vrai. La conjonction vide est écrite « T » et a pour valeur vrai. Autrement dit, chaque « \(∧\) » représente un « et » logique. Par exemple, dans la théorie des \(4\)-reines, l’énoncé « la diagonale de \(21\) à \(43\) doit contenir au plus une reine » peut s’écrire comme la conjonction

Celle-ci exprime en effet que toutes les paires de cases de la diagonale sont mutuellement exclusives : au moins une case de chacune de ces paires ne contient pas une reine. Comme vu précédemment, « \(−21\) \(−32\) » peut s’interpréter comme l’énoncé « si \(21\) vaut vrai alors \(32\) vaut faux » ce qui est aussi équivalent à dire « si \(32\) vaut vrai alors \(21\) vaut faux ». Les méta-variables de conjonctions sont notées \(p\), \(p\)₁, \(p\)₂, …

Au final, la théorie des \(4\)-reines s’exprime sous la forme d’une conjonction de \(80\) clauses : \(4\) clauses de \(4\) littéraux exprimant qu’il doit y avoir au moins une reine sur chacune des lignes et \(76\) clauses de \(2\) littéraux exprimant toutes les paires de cases mutuellement exclusives. La théorie des \(4\)-reines avec une reine en \(11\) s’exprime sous la forme d’une conjonction de \(81\) clauses : les \(80\) clauses précédentes et la clause réduite au littéral « \(11\) ».

Propositions satisfaisables

Une proposition est satisfaisable si et seulement si elle vaut vrai pour au moins une interprétation des variables. Rappelons que, pour notre logique, une interprétation associe à chaque variable, une valeur vrai ou faux fixée. Dans le cas de la théorie des \(n\)-reines, la satisfaisabilité exprime l’existence d’une solution. Pour garantir qu’une proposition est satisfaisable, il suffit d’exhiber une interprétation des variables et de vérifier que dans toutes les clauses de la proposition, il y a au moins un littéral qui vaut vrai pour cette interprétation. Ici, nous écrirons une telle interprétation sous la forme de l’ensemble de toutes les variables qui valent vrai (dans cette interprétation). Par exemple, la théorie des \(4\)-reines est satisfaisable avec l’interprétation « {\(12\), \(24\), \(31\), \(43\)} » : c’est la solution dessinée sur la figure 1. Sur le même principe, la théorie des \(8\)-reines avec une reine en \(11\) et les cases \(83\) et \(64\) interdites (incluant donc dans la théorie les deux clauses « \(−83\) » et « \(−64\) ») est satisfaisable avec l’interprétation « {\(11\), \(25\), \(38\), \(46\), \(53\), \(67\), \(72\), \(84\)} » dessinée sur la figure 5 (voir plus haut).

Propositions insatisfaisables

Une proposition est insatisfaisable si et seulement si elle vaut faux pour toute interprétation. Dans le cas de la théorie des \(n\)-reines, l’insatisfaisabilité exprime l’absence de solution. Pour la vérifier, il va falloir introduire un langage de preuves formelles.

Nous commençons par définir un calcul sur les clauses qui, étant donné une proposition \(p\) et une clause \(c\), garantit que pour toute interprétation, si \(p\) est vrai pour cette interprétation, alors \(c\) aussi. Autrement dit, ce calcul assurera que \(c\) est bien une conséquence logique de \(p\). Pour garantir que \(p\) est insatisfaisable, il suffira alors de montrer que F est une conséquence logique de \(p\).

Différence de clauses

Soient \(c\)₁ et \(c\)₂ deux clauses. Notons \(c\)₁ \ \(c\)₂ la clause obtenue à partir de \(c\)₁ en supprimant ses littéraux qui se trouvent aussi dans \(c\)₂. Par exemple,

Remarquons que \(c\)₁ \ \(c\)₂ \(=\) F revient à dire que tous les littéraux de \(c\)₁ sont dans \(c\)₂. Ce que nous notons \(c\)₂ \(⊇\) \(c\)₁. Dans ce cas, \(c\)₂ est une conséquence logique de \(c\)₁ (car tout littéral valant vrai dans \(c\)₁ se trouve aussi dans \(c\)₂). Remarquons aussi que si \(c\)₁ \ \(c\)₂ \(=\) \(c\)₃ alors \(c\)₂ \(⊇\) (\(c\)₁ \ \(c\)₃) et \(c\)₁ = \(c\)₃ (\(c\)₁ \ \(c\)₃). Nous allons utiliser ces propriétés ci-dessous.

Résolution arrière

Notons maintenant \(c\)₂ \(⊖\) \(c\)₁ la clause égale à « \(c\)₂ −(\(c\)₁ \ \(c\)₂) » si \(c\)₁ \ \(c\)₂ est réduite à un unique littéral. Par exemple,

                       \(−1\) \(2\) \(3\) \(⊖\) \(4\) \(2\) \(=\) \(−1\) \(2\) \(3\) \(−4\)         et          \(−1\) \(2\) \(3\) \(⊖\) \(−5\) \(−1\) \(3\) \(=\) \(−1\) \(2\) \(3\) \(5\)

Cette opération n’est pas définie si la clause \(c\)₁\ \(c\)₂ n’est pas réduite à un unique littéral. Par convention, l’opération \(c\)₂ \(⊖\) \(c\)₁ n’est utilisée que lorsqu’elle est bien définie. Pour faciliter la lecture, le littéral de différence est généralement écrit en tête de \(c\)₁, et son opposé sera alors écrit en queue dans le résultat.

Supposons \(c\)₂ \(⊖\) \(c\)₁ bien définie. Soit \(ℓ\) le littéral valant \(c\)₁ \ \(c\)₂. Et soit \(c\) \(=\) \(c\)₁ \ \(ℓ\). D’après les propriétés de la différence de clauses, \(c\)₂ \(⊇\) \(c\) et \(c\)₁ \(=\) \(ℓ\) \(c\). De plus, par définition, \(c\)₂ \(⊖\) \(c\)₁ \(=\) \(c\)₂ \(−ℓ\). On en déduit que la conjonction (\(c\)₂ \(⊖\) \(c\)₁) \(∧\) \(c\)₁ est égale à (\(c\)₂ \(−ℓ\)) \(∧\) (\(ℓ\) \(c\)). Lorsque cette dernière vaut vrai, on en déduit que « si \(ℓ\) vaut vrai alors \(c\)₂ vaut vrai sinon \(c\) vaut vrai ». On en conclut que \(c\)₂ est une conséquence logique de (\(c\)₂ \(⊖\) \(c\)₁) \(∧\) \(c\)₁. En effet, comme \(c\)₂ \(⊇\) \(c\), la clause \(c\)₂ est une conséquence logique de \(c\), donc si (\(c\)₂ \(⊖\) \(c\)₁) \(∧\) \(c\)₁ vaut vrai, quelle que soit la valeur de vérité de \(ℓ\), la clause \(c\)₂ vaut vrai.

Autrement dit, nous avons montré que « sachant \(c\)₁, pour montrer \(c\)₂, il suffit de montrer \(c\)₂ \(⊖\) \(c\)₁ ». C’est une forme de raisonnement dit en arrière, car on part de la conclusion à prouver pour en calculer une cause possible. L’opération \(c\)₂ \(⊖\) \(c\)₁ effectue ce que nous appelons la « résolution en arrière de \(c\)₂ sachant \(c\)₁ ». En combinant \(⊖\) et \(⊇\), écrivons maintenant nos premières preuves formelles de théorèmes.

Preuves formelles par chaînes de résolutions

Avec la convention \(c\)₃ \(⊖\) \(c\)₂ \(⊖\) \(c\)₁ \(=\) (\(c\)₃ \(⊖\) \(c\)₂) \(⊖\) \(c\)₁, si la relation « \(c\)_\(n+1\) \(⊖\) \(c\)_\(n\) \(⊖\) … \(⊖\) \(c\)₂ \(⊇\) \(c\)₁ » est satisfaite, et que toutes les résolutions intermédiaires sont bien définies, alors \(c\)_\(n+1\) est une conséquence logique de la conjonction « \(c\)₁ \(∧\) \(c\)₂ \(∧\) … \(∧\) \(c\)_\(n\) ». Peu importe l’ordre des clauses dans cette conjonction. Par contre, l’ordre importe dans la chaîne de résolutions. Si \(c\)₁, \(c\)₂, …, \(c\)_\(n\) sont elles-mêmes des clauses d’une conjonction \(p\), nous dirons alors que \(c\)_\(n+1\) est un théorème de la théorie \(p\).

Par exemple, on peut exprimer que l’énoncé informel « s’il y a une reine en \(11\), alors il y a au moins une reine en \(42\) ou \(43\) » est un théorème de la théorie des \(4\)-reines. Cet énoncé s’écrit sous la forme « \(-11\) \(42\) \(43\) ». Et sa preuve formelle est donnée par

Elle prouve le théorème en combinant \(3\) clauses de la théorie des \(4\)-reines : la clause exprimant qu’il y a au moins une reine sur la ligne \(4\) et les deux clauses exprimant que s’il y a une reine en \(11\) alors il n’y a pas de reine ni en \(41\) ni en \(44\).

En s’inspirant de la preuve visuelle de la figure 4, on peut prouver l’énoncé informel « il n’y a pas de reine en \(22\) » (pour le problème des \(4\)-reines de base). C’est le théorème formel « \(-22\) » dont la preuve formelle est :

La chaîne de résolutions produit ici la clause « \(-22\) \(11\) \(12\) \(13\) \(-14\) \(31\) \(32\) \(33\) \(34\) ».

L’intérêt de ce format de preuve, c’est qu’il n’exige pas d’écrire le résultat des résolutions intermédiaires : celles-ci sont directement calculées par le vérificateur de preuve. En même temps, les calculs du vérificateur sont très faciles et très rapides à effectuer.

Preuves formelles par suites de théorèmes

Soit \(p\) une théorie. Si \(c\) est un théorème prouvé dans cette théorie, alors la conjonction \(p\) \(∧\) \(c\) est elle-même une conséquence logique de cette théorie. Nous généralisons maintenant cette notion de théorème en autorisant les chaînes de résolutions à utiliser un théorème précédemment prouvé à partir de la théorie. Concrètement, nous écrirons une telle preuve de théorème comme une séquence de chaînes de résolutions séparées par un point-virgule. Par exemple, considérons la théorie suivante :

Dans cette théorie, le théorème « \(2\) » est démontré par la preuve formelle suivante, qui commence par prouver le théorème intermédiaire « \(2\) \(3\) ».

Là encore, la vérification est très facile et très rapide. Il existe d’autres formats de preuves formelles, encore plus compacts, mais plus complexes à vérifier. Notamment, le format RUP qui est produit très facilement par les solveurs-SAT de l’état de l’art. Ce format consiste à donner uniquement la liste des théorèmes, sans leur preuve sous forme de chaînes de résolution. Celles-ci se retrouvent par un algorithme appelé propagation unitaire (RUP est l’acronyme de Reverse Unit Propagation), qui, pour être au niveau d’efficacité de l’état de l’art, nécessite une représentation des données très astucieuse, dont la formalisation mathématique est complexe (les solveur-SATs modernes étant en effet capables de résoudre en moins d’une heure certains problèmes avec des millions de clauses et de variables). 

Méta-théorème (preuves formelles d’insatisfaisabilité)

Soit \(p\) une théorie dont F est un théorème. Alors \(p\) est insatisfaisable.

Preuve

Nous avons déjà justifié dans les paragraphes précédents que tout théorème \(c\) de \(p\) est une conséquence logique de \(p\). Donc F est une conséquence logique de \(p\). Si \(p\) était satisfaisable, alors F le serait aussi. F est insatisfaisable, donc \(p\) aussi.

Il se trouve que la réciproque de ce méta-théorème est aussi démontrable : cela nous garantit que pour toute proposition \(p\) insatisfaisable, il existe une preuve formelle de F. Mais, si nous sommes seulement intéressés à garantir la correction de notre procédé de vérification, cette garantie n’est pas strictement nécessaire. Pour des logiques plus complexes, permettant par exemple de formaliser les entiers naturels, la réciproque du méta-théorème de correction des preuves formelles est même nécessairement fausse. Dans ce cas, la logique est dite incomplète. C’est le fameux premier (méta-méta)théorème d’incomplétude de Gödel. 

Preuve formelle de l’absence de solution au problème des \(4\)-reines avec une reine en case \(11\) :

\(-11\) \(32\) \(⊖\) \(-31\) \(-11\) \(⊖\) \(-33\) \(-11\) \(⊖\) \(34\) \(32\) \(31\) \(33\)

\(⊖\) \(-21\) \(-11\) \(⊖\) \(-22\) \(-11\) \(⊖\) \(-23\) \(-34\) \(⊖\) \(-24\) \(-34\) \(⊇\) \(21\) \(22\) \(23\) \(24\) ;

F \(⊖\) \(11\) \(⊖\) \(-41\) \(-11\) \(⊖\) \(32\) \(-11\) \(⊖\) \(-42\) \(-32\) \(⊖\) \(-43\) \(-32\) \(⊖\) \(-44\) \(-11\) \(⊇\) \(41\) \(42\) \(43\) \(44\)

Cette preuve formelle est proche de la preuve par l’absurde donnée en début d’article, même si elles ont un style très différent (la preuve formelle utilisant des raisonnements « en arrière » alors que la preuve verbalisée est rédigée dans un style « en avant »). En particulier, cette preuve formelle est concise : chaque clause de la théorie n’est utilisée qu’au plus une fois. Et, son théorème intermédiaire, de la forme « s’il y a une reine en \(11\) alors il y a une reine en \(32\) », correspond à celui introduit dans la preuve verbalisée.

Preuve formelle de l’unicité de la solution au problème de la figure 2 :

Notre logique permet de montrer que le problème de la figure 2 (voir plus haut) n’a pas d’autre solution que celle donnée à la figure 5 (voir plus haut). Il suffit de prouver l’insatisfaisabilité de la théorie qui ajoute à la théorie initiale une clause interdisant cette solution, comme « \(-25\) \(-38\) \(-46\) \(-53\) \(-67\) \(-72\) \(-84\) » : cette clause exprime qu’il faut trouver un placement des reines qui diffère de celui en figure 5 sur au moins une case. N’importe quel solveur-SAT récent en trouve une preuve formelle en quelques millisecondes.

La figure 6 dans l’encart ci-dessous donne une telle preuve formelle, en utilisant une légère généralisation du format précédent, qui permet de rendre la preuve un peu plus courte. Cette généralisation consiste à autoriser à donner un nom optionnel aux théorèmes. Pour ne pas être confondu avec une variable, un tel nom de théorème doit commencer par une lettre. Il est associé à un théorème via un symbole « : » (voir la syntaxe utilisée par la figure 6, voir encart ci-dessous). Cela autorise les résolutions à utiliser le nom à la place de l’énoncé de son théorème associé. Pour être correcte, une preuve doit seulement contenir des noms de théorème qui sont associés à un théorème et un seul.

Heuristique versus vérification des problèmes SAT

En résumé, nous avons défini ci-dessus un procédé automatisable de vérification des solutions (ou d’absence de solution) aux problèmes encodables en logique des propositions à variables booléennes ; ce qui inclut les \(n\)-reines, les sudokus et bien d’autres choses. Ce procédé a l’avantage d’être beaucoup plus simple que les heuristiques de résolution dans cette logique, appelées communément solveurs-SAT.

Programmation défensive formellement vérifiée

Le constat que « la vérification est généralement nettement plus facile que la recherche » inspire un paradigme de conception de logiciels par programmation défensive, où la recherche de solution est effectuée par un oracle basé sur des heuristiques efficaces, mais jugé potentiellement non fiable, et où un vérificateur rigoureux se charge de valider la correction des résultats, en signalant les résultats non validés quand il y en a. Ce paradigme est notamment très utile dans les outils de développement des logiciels, comme les compilateurs qui traduisent un programme « source » écrit dans un langage de haut niveau, en code machine optimisé pour un processeur donné. En effet, un bug dans le compilateur pourrait introduire un bug dans le code machine généré, à l’insu des développeurs et développeuses. Dans ce contexte, la programmation défensive cherche à vérifier que le code machine est conforme au programme source. Quand ce n’est pas le cas, la compilation échoue, ce qui est beaucoup moins problématique que de produire silencieusement un code machine incorrect. Ainsi, en pratique, la programmation défensive est appliquée sur des problèmes SAT, mais aussi sur des problèmes très différents. Pour chaque famille de problèmes, il faut donc inventer des techniques de vérification adaptées, qui peuvent se révéler très différentes du cas des problèmes SAT. Par exemple, la vérification de compilateur s’appuie (entre autres) sur des techniques d’exécution symbolique.

 Vérification formelle

Lorsque la correction des résultats est vraiment critique (notamment si les « résultats » sont eux-mêmes des logiciels critiques), vérifier formellement le vérificateur lui-même apporte une sécurité supplémentaire. C’est ce qui s’appelle la programmation défensive formellement vérifiée, de l’acronyme PDFV. Concrètement, il s’agit de prouver formellement que l’implémentation du vérificateur est correcte. Cela nécessite aussi de formaliser sa métathéorie (par exemple, la métathéorie de la vérification en logique propositionnelle exposée à la section précédente). Le tout dans une logique formelle vérifiée par ordinateur. Ce serait de toute façon trop laborieux (et par conséquent pas réellement convaincant) à vérifier en mode « papier/crayon ». Des assistants à la preuve formelle tels que Coq ou Isabelle ont permis d’appliquer la PDFV à des logiciels « complexes », comme des solveurs-SAT de l’état de l’art. En particulier, ces assistants de preuve ont permis d’appliquer la PDFV à des logiciels avec des spécifications complexes (la spécification d’un logiciel décrit ce que doit faire le logiciel : c’est en quelque sorte un « mode d’emploi » complètement détaillé), comme le compilateur optimisant CompCert (formalisé en Coq) ou le système d’exploitation sécurisé seL4 (formalisé en Isabelle).

Assistants de preuve

En fait, les logiciels Coq et Isabelle sont eux-mêmes réalisés en programmation défensive. Ils offrent tous les deux des heuristiques puissantes pour construire des preuves formelles, mais utilisent un vérificateur assez réduit pour garantir que ces heuristiques ne permettent pas de prouver des théorèmes faux. Certains prototypes expérimentaux de ces logiciels ont même pu partiellement s’autovérifier (ce qui bien sûr n’offre pas une garantie absolue). C’est donc une forme de PDFV réflexive. Depuis plusieurs dizaines d’années que ces deux logiciels existent, nous avons maintenant un certain recul sur la quantité de bugs critiques (c’est-à-dire qui permettent potentiellement de prouver des théorèmes faux) découverts dans ces logiciels. Il est extrêmement faible : pour Coq, de l’ordre de un par an en moyenne. Dans ces conditions, étant donné de plus le caractère interactif des preuves formelles dans ces assistants de preuve, il est extrêmement peu probable qu’un de leurs bugs critiques permette aux utilisateurs et utilisatrices de prouver un théorème faux sans que ces derniers ne s’en aperçoivent.

Base informatique de confiance (Trusted Computing Base)

Par construction, les bugs de correction d’un logiciel en PDFV ne peuvent que se trouver dans un sous-ensemble très réduit du logiciel qui s’appelle la base informatique de confiance (TCB pour Trusted Computing Base en anglais). Celle-ci comprend surtout la formalisation des spécifications (par exemple, dans le cas de CompCert, les langages de programmation d’entrée et de sortie du compilateur), et éventuellement les composants du logiciel non couverts par la PDFV.

Dans le cas de CompCert, les spécifications formelles sont complexes : elles nécessitent plusieurs milliers de lignes de code Coq. Mais beaucoup moins que le reste du logiciel qui comprend des centaines de milliers de lignes de code. Depuis plus de quinze ans d’existence, ses bugs critiques — rappelons que dans le cas de CompCert, ils correspondent à des bugs introduits silencieusement par le compilateur dans le programme compilé, à partir d’un programme source sans bug —  sont exclusivement apparus dans sa TCB, et jamais dans une partie couverte par la PDFV. Et c’est une très bonne nouvelle, car la TCB est non seulement moins complexe que le reste du logiciel, mais elle évolue aussi beaucoup plus lentement (par exemple, la définition d’un langage de programmation évolue beaucoup plus lentement que l’implémentation de son compilateur). Finalement, le nombre de bugs critiques dans CompCert est lui-même très faible : moins d’une dizaine par an (très rapidement corrigés) contre plusieurs centaines (qui restent la plupart du temps non corrigés pendant plusieurs mois — les optimisations responsables étant par exemple simplement désactivées) pour des compilateurs traditionnels comme GCC ou LLVM.

Note de l’auteur : D’après l’étude « An empirical study of optimization bugs in GCC and LLVM » de Zhide Zhou et ses coauteurs en 2020, les développeurs et développeuses de GCC et LLVM prennent plus d’un an en moyenne pour corriger un bug critique d’optimisation. Dans mon expérience, une correction de bug critique dans la TCB de CompCert ne prend généralement que quelques jours.

En conclusion, la PDFV est une méthode effective pour rendre les logiciels beaucoup plus fiables, en complément des méthodes traditionnelles du génie logiciel. Pour la généraliser, il faut inventer les techniques de vérification défensive adaptées aux heuristiques de l’état de l’art dans chaque domaine d’application.