Avez-vous jamais remarqué comment, quand le programme informatique que vous utilisez rencontre une difficulté, il s’arrange le plus souvent pour suggérer que c’est de votre faute ? L’exemple le plus irritant que je connaisse observe sur ces sites marchands qui sont très heureux de vous demander votre numéro de carte de crédit mais n’acceptent pas que vous l’écriviez tel qu’il apparaît sur votre carte, gentiment divisé en quatre groupes de quatre chiffres faciles à mémoriser et à recopier, ce qui serait bien naturel et leur coûterait une (je dis bien, une) ligne de code supplémentaire. Hélas, sauf exception louable, le site web vous enguirlande si vous avez le malheur d’insérer un espace, vous forçant ainsi à relire ad nauseam une longue séquence de seize chiffres pour repérer l’erreur qui n’aura pas manqué de s’y glisser.

C’est la première ligne de défense du logiciel fautif ou mal fichu : tout vous mettre sur le dos. Un utilisateur culpabilisé est un utilisateur qui ne se plaindra pas. Cependant, il arrive que le bug soit si profond dans le code, ou que toute action possible de votre part soit à l’évidence tellement inoffensive, que le logiciel devra se fendre d’un message moins agressif mais plus sibyllin du type “une erreur s’est produite, veuillez réessayer ultérieurement ou contacter votre administrateur”. S’ajoute éventuellement un intimidant et illisible diagnostic en anglais, rempli de détails techniques qui n’ont pour objectif que de vous rappeler à quel point vous n’y connaissez rien et seriez donc mal placé(e) pour critiquer. Notons au passage que le logiciel (et le développeur qui l’a commis) ne reconnaît toujours en rien que l’erreur soit la sienne ! C’est, a priori, la faute d’un autre – peut-être le réseau, votre ordinateur à vous, un hébergeur de sites web, voire la faute à pas de chance.

Il existe cependant des cas où le logiciel fautif se retrouve dans une situation telle qu’il doive abandonner toute ligne de défense de ce type, reconnaître son incapacité à continuer quoi que ce soit, et abandonner immédiatement la partie en faisant seppuku. C’est ce qui se passe quand ses instructions lui commandent de faire quelque chose d’impossible, par exemple de lire le contenu d’une case de mémoire qui n’existe pas.  Il se retrouve alors tellement mal en point qu’il ne peut même pas vous prévenir avant de s’arrêter. C’est un autre programme plus robuste, intégré au système d‘exploitation et chargé de surveiller ce qui se passe, qui se chargera de rassembler les restes du défunt et de prévenir les proches. Pour faciliter l’autopsie, il va en effet recopier quelque part dans un énorme fichier l’intégralité de la mémoire utilisée par votre logiciel au moment de son arrêt, ainsi que les instructions qu’il était en train d’exécuter : le développeur pourra ainsi (on l’espère du moins) reconstituer les derniers instants de la victime et identifier le bug assassin. Cette levée du corps virtuelle s’appelle en Anglais un core dump, et s’il en existe un équivalent officiel en français je ne l’ai pas trouvé.

Mon premier core dump fut le plus impressionnant, car il se produisit sur l’IBM 360 du Palais de la Découverte auprès duquel, adolescent, je m’étais introduit frauduleusement pour tester l’un de mes tout premiers programmes. En l’occurrence, ce core dump se traduisit par l’impression de la mémoire de l’ordinateur directement sur un nombre impressionnant de feuilles de papier listing qui s’échappaient à toute vitesse de l’imprimante, menaçant de m’étouffer sous leur nombre ; en m’enfuyant je me sentais exactement comme Mickey dans L’Apprenti sorcier (et me fis ultérieurement engueuler de la même manière).

Outre le fait que j’étais encore grand débutant, une raison fondamentale pour que ce programme plante de manière aussi spectaculaire tenait à sa nature : c’était ce que l’on appelle une procédure récursive, un bout de programme informatique qui fait dans certains cas appel à lui-même. Or, quand un programme informatique en appelle un autre cela coûte un peu de mémoire ; un programme récursif mal fichu qui s’appelle soi-même à l’infini – un peu comme fabriquer une infinité de reflets en utilisant deux miroirs face à face – finit par utiliser toute la mémoire disponible, et boum : core dump.

Passée l’anecdote, le concept de programme récursif (on parlera plus proprement de fonction récursive) est intimement lié à la notion de récurrence ou d’induction que nous avons commencé d’explorer la semaine dernière avec nos cocus de Bagdad ; il illustre aussi les rapports fascinants entre preuve et programme que continuent d’explorer les théoriciens de l’informatique.

Le problème que je cherchais à résoudre avant de planter ce vénérable ordinateur (aux lumières et cadrans dignes d’un film de SF, par ailleurs) est très connu et s’appelle le jeu des tours de Hanoï. Vous disposez de trois piquets alignés ; sur l’un d’entre eux sont disposés par taille décroissante un certain nombre de disques percés, disons sept, le plus grand en bas, le plus petit en haut, ce qui forme une pyramide conique. Il vous est demandé de déplacer votre pyramide entière sur un autre piquet choisi à l’avance en ne déplaçant d’un piquet à l’autre qu’un disque à la fois, pris aux sommet d’une pile, et ce sans jamais poser un disque sur un autre plus petit que lui.

Nous pouvons utiliser un argument similaire à celui de la semaine dernière pour prouver que c’est possible quel que soit le nombre de disques. En effet, si nous n’avons qu’un seul disque la solution est immédiate : enlevez votre disque du piquet où il se trouve et posez-le sur le piquet choisi. Supposons maintenant – c‘est notre hypothèse d’induction – que nous sachions résoudre le problème pour un certain nombre N, supérieur ou égal à 1, de disques et considérons une pyramide de N+1 disques. Nous pouvons alors procéder ainsi : d’abord, déplacer les N disques du haut – qui forment aussi une pyramide – sur le seul piquet libre qui n’a pas été choisi comme cible, en laissant à sa place le plus grand disque qui restera en bas. Par hypothèse d’induction nous pouvons faire cela. Ensuite nous déplaçons le grand disque sur le piquet choisi, jusqu’ici resté libre. Enfin, nous déplaçons à nouveau les N plus petits disques vers ce même piquet, qui contiendra à la fin la pyramide entière. Nous avons donc une solution pour N+1 disques. Puisque notre hypothèse d’induction est vraie pour un disque et que sa validité pour N disques entraîne sa validité pour N+1 disques, nous venons de prouver qu’il existe toujours une solution au problème des tours de Hanoï.

Il est à prévoir que le lecteur informaticien et féru d’économie conceptuelle trouvera cette démonstration un rien inélégante. J‘aurais en effet pu considérer le cas de zéro disques, pour lequel il n’y a strictement rien à faire, et obtenir une démonstration encore plus concise. Mais il me semble que pour l’immense majorité de nos congénères, l’idée de déplacer une pyramide de zéro disques sans faire un seul mouvement ressemble plus à un koan zen bizarre qu’à autre chose, sans garantie d’illumination qui plus est.

Quoi qu’il en soit, il reste à observer que cette preuve que nous venons d’établir possède une propriété géniale : elle ne nous dit pas seulement que l’on peut résoudre le problème, elle nous dit aussi comment. C’est ce qu’on appelle une preuve constructive. En suivant les étapes qu’elle décrit, un être humain – ou un programme informatique qui simule la situation – pourra effectivement déplacer la pyramide. Et l’on observe bien que la méthode, la procédure, l’algorithme utilisé, pour déplacer une pyramide de 7 disques, fera appel à lui-même à deux reprises pour déplacer une pyramide de 6 disques, chacune de ces opérations nécessitant à son tour deux déplacements de 5 disques, etc…

Quand une preuve mathématique peut être directement transposée en programme informatique, comme c’est le cas ici avec les langages informatiques modernes, le développeur est ravi : il obtient une garantie formelle, mathématique, que le programme obtenu est correct. Il sait (au lieu de simplement croire ou espérer) que son programme ne plantera pas, ne bouclera pas à l’infini, mais finira par donner un résultat, toujours le bon. C’est rare et c’est précieux. Dans des domaines tels que le nucléaire ou l’aéronautique, de telles propriétés peuvent signifier la différence entre la vie et la mort et sont recherchées à tous prix. Plus généralement, l’étude de ce que l’on appelle les méthodes formelles de certification des programmes informatiques est un champ de recherche très actif (et un domaine où, cocorico, la France est fort en pointe grâce à l’INRIA).

Le lecteur se demande peut-être, si tout cela est vrai, comment je me suis débrouillé pour planter l’ordinateur ? Ce qui me manquait, en l’occurrence, ce n’était pas une preuve mathématique : c’était un langage informatique suffisamment sympa pour que l’adaptation de cette preuve y soit simple. Le seul langage dont je disposais à l’époque – le seul compris par cet ordinateur-là – était assez rébarbatif quoique aussi puissant qu’un autre, et l’adaptation de ma preuve n’y allait pas de soi. Je me suis trompé quelque part et mes disques s’envolaient à l’infini, ou peut-être que je me retrouvais à déplacer un nombre négatif toujours plus grand de disques… je ne le saurai jamais, car je n’ai jamais eu le courage de revenir chercher mon core dump dans la corbeille à papier de la salle de calcul.

Yannick Cras
Le nombre imaginaire

PS – À l’attention du lecteur ou de la lectrice que ma petite énigme des crayons de couleur laisserait perplexe depuis une semaine : l’erreur (intentionnelle) du raisonnement réside dans mon affirmation que si tous les crayons de chaque paquet de N crayons ont la même couleur, alors tous les crayons du paquet total de N+1 crayons ont la même couleur. Ce n’est vrai que si ces paquets de N crayons ont au moins un crayon en commun, comme par exemple deux paquets différents de deux crayons pris dans un groupe de trois – qui ont bien toujours un crayon en commun. Or, pour N=2 crayons, chaque paquet de 1 crayon est bien d’une couleur homogène, mais ces paquets n’ont aucun crayon en commun, donc rien ne les oblige à partager cette couleur.

[print_link]