...vous pourriez me le prouver ?

Une statistique, dont j'ai oublié la source, indiquait que 80% des crashes aériens seraient, à l'heure actuelle (c'était il y a quelques années déjà !), imputables au logiciel. Et ce n'est pas faute de soigner la réalisation des logiciels de bord. Il devient alors urgent soit de mettre au point une méthode permettant de prouver qu'un programme est correct, soit de mettre au point une technique permettant de produire des programmes nécessairement corrects.

Un test ne prouve rien : les corbeaux noirs et les corbeaux roses.

Pendant longtemps notre seule possibilité a résidé dans la conduite de tests aussi poussés que possible. Malheureusement un test qui réussit ne prouve logiquement rien et les seuls tests probants sont ceux qui échouent [1]. Dans ce domaine, la logique et le bon sens ne font pas forcément bon ménage.

Le bon sens nous amène à considérer que plus une affirmation est confirmée par des expériences variées, plus elle est vraie. Malheureusement, les mêmes expériences permettent de renforcer des affirmations contradictoires.

Pour illustrer cette remarque, une petite histoire en deux volets permet de montrer qu'utilisée sans précaution, une apparence de logique permet de conclure exactement ce que l'on veut.

* on a longtemps cru que tous les cygnes étaient blancs... avant de découvrir les cygnes noirs d'Australie.
** le guide, en fin logicien, sait bien que la contraposition d'une proposition lui est équivalente.

Nous sentons bien que, dans ces conditions, il va nous falloir définir très précisément ce que veut dire prouver et ce qu'il est possible de prouver.

En fait, le guide ne pouvait pas utiliser la logique dans ce cadre comme nous le verrons au chapitre Le vrai et le prouvé.

Question : Qu'auriez-vous tenté de faire à la place du guide ? Son attitude est-elle logique et/ou raisonnable ? Quelles fautes a-t-il commises ?

De l'expression des besoins à la spécification

L'expression de besoin, rédigée par un client (potentiel) est nécessairement floue et ambiguë. Ce n'est ni le métier, ni la préoccupation du client de faciliter l'écriture d'un programme. A la limite, ce n'est pas sa préoccupation non plus de savoir si son besoin sera satisfait par un programme ou par n'importe quoi d'autre.

Question : Est-il possible de définir l'égalité de deux programmes ? A quelles difficultés se heurte-t-on ? Finalement à quoi revient l'introduction de l'équivalence opérationnelle ?

Le premier travail de l'informaticien est donc de traduire cette expression de besoin en une spécification formalisée. Le formalisme utilisé pour construire la spécification doit permettre la preuve de l'équivalence opérationnelle [2] entre cette spécification et le programme réalisé à partir de celle-ci.

De la spécification à la réalisation

La preuve d'une réalisation (un programme) a été abordée selon deux angles :

• comment prouver un programme existant et développé selon les méthodes traditionnelles.
• comment produire un programme nécessairement correct.

De ces deux méthodes c'est la deuxième qui s'est révélée la plus fructueuse et qui semble devoir s'imposer aujourd'hui.

Prouver l'existant

Le pionnier dans ce domaine est incontestablement E.W. Dijkstra. L'approche qu'il propose consiste :

• à trouver un invariant caractérisant le problème,
• à montrer, pas à pas, que cet invariant est conservé tout au long du programme.

Malheureusement cette méthode est beaucoup trop lourde pour pouvoir être appliquée à des programmes de taille raisonnable. De plus si elle permet de mettre les erreurs en évidence, elle ne donne aucun moyen de les corriger. Elle est donc tombée en désuétude en tant que telle. Par contre, l'utilisation d'invariants s'est révélé un outil puissant de conception de programmes.

Construire directement un programme correct

Les deux approches qui permettent de construire, si c'est possible, un programme correct correspondent aux deux formes que peut prendre la conjecture de Howard-Curry :

• un programme est une solution de ses équations de spécification. Cette approche correspond à la programmation fonctionnelle dont les langages de programmation suivants sont le support : Scheme, ML, Caml, Hope, Miranda, Haskell, etc. Elle découle directement des travaux sur le lambda-calcul de A.Church, H.Curry, S.Kleene, D.Scott et C.Strachey...
• les spécifications expriment un théorème dont le programme est une preuve. Cette approche correspond à la programmation logique dont le langage Prolog est le support le plus connu. Elle découle directement des travaux sur le calcul des prédicats, la logique d'ordre 1 et le principe de résolution de Aristote, T.A.Skolem, J.Herbrand, J.A.Robinson, R.Kowalski (école d'Edimbourg) et de A.Colmerauer (école de Marseille).

Ces deux approches n'ont pas été, à l'origine, introduites dans le cadre de l'informatique. La première concernait une théorie des fonctions calculables et la deuxième était une théorie de la logique mathématique. Les travaux initiaux datent du début du XXème siècle (vers 1920), leur application à l'informatique est assez récente (vers 1960-80).

Et la machine dans tout ça ?

Et bien, seule la structure de la machine peut être prouvée car cette structure peut être décrite par une sorte de programme (il existe depuis déjà une vingtaine d'années des langages de description de processeurs et les compilateurs de silicium associés). Les lois physiques sur lesquelles le fonctionnement du processeur est fondé ne peuvent être que réfutées.

Bibliographie

• Logik der Forschung
  Karl Popper - Julius Springer Verlag, Vienna, 1935.
• The Logic of Scientific Discovery
  Karl Popper - Hutchinson, London, 1959. — La traduction anglaise du précédent.

• A Discipline of Programming
  Edsger Wybe Dijkstra - New Jersey: Prentice Hall, 1976.

Notes

1. (retour) Les chercheurs ont bien compris cette difficulté et aujourd'hui, une théorie scientifique n'est considérée comme valable que tant qu'elle n'a pas été réfutée. Le travail du chercheur est donc de tenter de réfuter la théorie. Une théorie n'est acceptée comme scientifiquement bien fondée que si elle permet la réfutation. C'est l'absence de réfutabilité qui conduit à considérer comme non scientifiques des domaines comme l'astrologie, la numérologie, la psychomorphologie etc. Cependant, de nombreux domaines moins suspects (médecine, pharmacologie, sociologie, ...) sont considérés comme pas tout à fait scientifiques alors que nul ne songerait à douter de leur validité.
2. (retour) On dira que deux choses (programmes) sont opérationnellement équivalentes si on peut en avoir le même usage.
   If it quackles like a duck, waggles like a duck and splashes like a duck, give me a good reason for not saying it is a duck. — Lewis Caroll