Discussion :

[KiLVaiDeN]

Oui mais il y a alors une chose que je ne comprend pas, quand le programme doit interagir avec des données externes, il ne peut pas savoir "lors de la compilation" quelles valeurs il va recevoir en entrée. Par exemple, on fait x/y, pour tout y des lignes d'une table dans une base de données quelconque, il va bien falloir faire des tests non ?

Et une autre question que je me pose : un programme qui prend en compte tous les cas possibles, en traitant les problèmes par des tests, n'est-il pas en fin de compte lui-même "prouvé" ? Si on est sûr que tous les cas posant problème sont contournés, ce module peut être réputé sûr tout du moins, même si il ne s'agit pas de la notion de preuve.

Quand je disais que Math.divide(x,y) était plus précis que x/y, je parle surtout de l'analyse syntaxique, comme tu dis il est plus compliqué de traiter des expressions algébriques que de gérer des variables en paramètres dans une méthode, mais c'est encore une preuve de mon inexperience des compilateurs et des analyseurs syntaxiques, je trouve le problème infiniement complexe, par exemple :

x/(y/(z(1+x))) < comment traiter cette expression ?
Il est plus simple dans mon esprit de traiter :
Math.divide(x, Math.divide(y, Math.multiply(z, Math.add(1,x))));

Lorsque que tu dis que le constructeur doit se préoccuper de faire des freins qui ne lacheront pas, je dirais qu'on parle d'un domaine un peu différent, en mécanique il est vrai qu'on doit se soucier de fournir des éléments fiables, quitte à payer le prix fort pour les matériaux, car un défaut peut couter la vie. Et on ne peut pas mettre des capteurs partout pour détecter toutes les failles qui pourraient survenir. Ce serait impossible, car les paramètres ne sont pas tous connus.

C'est la différence entre le monde réel, constitué d'infines possibilités, et du monde informatique tel que je le vois, où le problème est différent, car le défaut est toujours de nature logicielle ( bien que le matériel peut aussi être responsable dans quelques cas, mais nous parlons du coté logiciel de la chose ) et donc pour contrer ce défaut il y a deux moyens pour rendre le logiciel sûr, les tests en temps réels, ou la fiabilité du "composant" logiciel utilisé. La deuxième solution, reviendrait à celle employée donc pour le cas de l'auto, une pièce fiable, mais cher ( ici en conception et en analyse ). Mais on a encore le cas peu couteux des tests, l'informatique offre l'avantage de fournir un moyen automatique de traiter les mêmes evenements, alors pourquoi ne pas appliquer ce principe à l'execution même d'un programme et à sa gestion d'erreur, en déployant une panoplie de tests, qui rendraient le code blindé de toute part ?

J'admire en tout cas le travail des gens comme toi, qui sont allés aussi loin dans l'abstraction, je propose une solution qui correspond à mes connaissances et à ce que je serais capable de produire, je ne dois sûrement pas encore réaliser la puissance de l'outil de preuve et le bienfait qu'il apporterait à l'informatique.. Dans le principe, un compilateur qui apporterait cette dimension de preuves, permettrait au developpeur de coder beaucoup de lignes de codes, en étant sûr que si la compilation a fonctionné, le programme sera garanti sans faille ? Ca me parrait inimaginable comme entreprise, mais je vois que tu es parmi ceux qui sont prêt à relever le défi et qui le prouvent par l'action, et encore une fois tu as toute mon admiration pour cette initiative

[DrTopos]

Il y a deux catégories de questions dans ton dernier post. Celles ayant trait aux preuves et celle ayant trait à l'analyse syntaxique. Je vais commencer par ces dernières.

Une expression comme x/y/z est analysée par un compilateur C ANSI comme (x/y)/z. Cela tient au fait qu'il a été décidé par les concepteurs que l'opérateur binaire infixe / s'associe de gauche à droite (on dit aussi s'associe à gauche). Il y a donc une règle que le programmeur C doit connaitre. S'il veut obtenir l'effet "inverse" il devra écrire x/(y/z), et là les parenthèses sont obligatoires. Parmi toutes ces règles, la plus connue est la précédence de * sur +, qui fait que x+y*z est lu comme x+(y*z). En C, le nombre de règles de précédences et d'association est tel que je mets au défi n'importe quel programmeur de les citer par coeur sans se tromper. Ceci peut être à l'origine de bugs bien subtils. J'en ai fait l'expérience à mes dépends. J'avais écrit un truc du genre:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
x == y&z

avec dans l'idée que c'était x == (y&z). Or, en C, == a une précédence plus élevée que &. J'ai débogué pendant trois jours avant de trouver la faute. Depuis cette époque, je suis devenu paranoiaque en matière de règles de précédence et d'association. Je mets toutes les parenthèses qu'il faut, même dans x + (y*z). Au moins, comme ça, c'est clair.

Une notation comme Math.divide(x,y), etc... est totalement non ambigüe, même sans règle d'association/précédence. Mais je trouve que c'est un peu abusif. Je crois que tout langage moderne doit être capable de supporter la surdéfinition (alias surcharge) pour alléger l'écriture. Mais évidemment, il doit aussi exiger de tout comprendre. Rien ne doit rester ambigü à la fin de la compilation. Lisp est un cas intéressant et tout à fait à part. L'expression (x/y)/z serait écrite (/ (/ x y) z), avec les deux paires de parenthèses obligatoires. Evidemment c'est totalement non ambigu.

Tout cela soulève un autre problème: même si ce qui est écrit est formellement correct (x == (y&z) et (x == y)&z sont tous deux formellement corrects en C), comment être sûr que le programmeur et le compilateur se sont compris. C'est typiquement un mal entendu. J'appelle ce genre de bug un bug d'intention par opposition au bug formel qu'un compilatur doit être capable de détecter.

J'ai peut-être en fait répondu complètement à coté de la question, car je viens de remarquer que tu avais écrit l'expression x/(y/(z(1+x))) avec toutes les parenthèses qu'il faut pour que ce soit non ambigü. Le traitement ne pose aucun problème. Quand on écrit un compilateur en s'aidant de YACC, on peut remettre les sous-expressions dans l'ordre qu'on veut avant de les traiter.

Revenons-en au sujet des preuves. Je suis d'accord que le monde réel (des voitures en particulier) n'est pas celui des maths, et d'ailleurs, je répète souvent à mes étudiants que les preuves mathématiques ne peuvent apporter de certitudes que sur les mathématiques elles-mêmes, tant qu'on introduit pas d'hypothèses extra-mathématiques. Dans le cas de l'informatique, notre hypothèse extra-mathématique est que le hardware fonctionne correctement, ce qui est je crois une hypothèse raisonable. Si le Pentium chauffe trop, évidemment il va faire n'importe quoi, mais c'est un autre problème. Par contre, le fait que le fichier qu'on veut ouvrir n'existe pas sur le disque dur nous concerne. Le fait que (toujours en C)

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
fopen("tagada","rt")

renvoie le pointeur nul, ne constitue pas une faute. C'est un comportement normal. On doit tester le retour de fopen et le traiter en conséquence. Le pistolet ici, c'est que le C nous laisse faire ce qu'on veut. En Anubis, le terme équivalent est 'file("tagada",read)', qui renvoie non pas un pointeur mais une donnée de type 'Maybe(RWAddr(Int8))', ce qui signifie textuellement peut-être une adresse à laquelle on peut lire et écrire des octets. Pour obtenir le fichier ouvert, on est obligé de détruire le résultat avec une conditionnelle qui ne peut être que de la forme suivante:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
6
if file("tagada",read) is 
   {
     failure then ...,
     success(f) then ...
   }

puisque le schéma de type 'Maybe' a deux alternatives de nom 'failure' et 'success'. On est donc obligé de traiter le cas où le fichier ne peut pas être ouvert, et de plus on n'a syntaxiquement accès au fichier ouvert ('f' ci-dessus) que dans le cas où le fichier a effectivement été ouvert. Donc, pas de pistolet, pas d'exception non plus.

Ne pas pouvoir ouvrir un fichier parce qu'il n'existe pas ou a été effacé n'est pas une erreur, alors que diviser par 0 est toujours une erreur. Les preuves ne prétendent éliminer que les erreur.

Prouver un programme ne consiste pas à savoir à la compilation tout ce qui va se passer. Ca consiste à s'assurer que quel que soit le scénario, le programme saura toujours quoi faire. Bien entendu, des tests peuvent être faits à l'exécution (sinon il n'y aurait pas de conditionnelles dans les langages), mais tous les cas doivent être prévus. L'exemple du fichier ci-dessus illustre bien ce phénomène. Je crois que cela répond à la question du premier paragraphe de ton post.

Par ailleurs, la notion de preuve se manipule comme celle de programme. On peut très bien avoir des bibliothèques de preuves comme on a des bibliothèques de programmes, qu'on utiliserait par une sorte d'#include. Il n'est pas nécessaire de tout redémontrer tout le temps. C'est d'ailleurs ce que les matheux ont fait de tout temps. On utilise des théories (des groupes, des espaces vectoriels, etc...) qui ne sont jamais que des bibliothèques de théorèmes.

Dans le principe, un compilateur qui apporterait cette dimension de preuves, permettrait au developpeur de coder beaucoup de lignes de codes, en étant sûr que si la compilation a fonctionné, le programme sera garanti sans faille ? Ca me parrait inimaginable comme entreprise...

Le logiciel de la ligne de métro 14 est constitué de 115000 lignes de B, qui sont garanties sans faute. Evidemment, ça demande un effort particulier, car plus de la moitié de ces lignes sont des preuves mathématiques qui ne produisent aucun code exécutable. J'ai beaucoup d'admiration pour le système B et pour son auteur Jean-René Abrial. Malgré tout, mes recherches m'ayant orienté sur une autre voie (surtout sur le pan du modèle mathématique), je continue à développer le successeur d'Anubis qui aura beaucoup de différences avec le B.

[KiLVaiDeN]

Merci beaucoup pour ces précisions, les choses sont plus claires, je prendrais le temps de répondre un peu plus longuement tout à l'heure quand j'aurais une petite pause café

[DrTopos]

Je pars ce matin en voyage pour quelques jours. je ne sais pas exactement de quoi je vais disposer comme accès Internet. Prière de m'excuser si les réponses tardent un peu.

[DrTopos]

Je colle ici ce mp que je viens de recevoir d'un futur membre qui ne peut pas poster sur ce fil.

Bonjour, je trouve ce débat très intéressant et j'aurais quelques remarques/questions que je ne peux malheureusement pas poster.

J'aimerais tout d'abord aborder le sujet de la division par zero et de l'ouverture d'un fichier inexistant. J'ai l'impression que lorsque fopen renvoie un pointeur nul, ce n'est qu'une extrapolation du comportement, la plus logique, et c'est aussi le cas d'erreur le plus fréquent. Dans la meme veine, serait-il vraiment impossible d'extrapoler la division de la meme manière, par exemple en introduisant une valeur "infini" dans les entiers, avec toute la gestion de résultat que cela implique, commme dans le cas de fopen.Je crois, et arretez moi si je me trompe, que les mathématiques ayant trait au calcul "infini" sont assez abouties.

Ensuite, à partir de quand un résultat statistique peut-il tenir lieu de preuve?
Je me rappelle avoir vu un algorithme non prouvé, qui pourtant terminait correctement dans 100% des cas testés : (il a peut-être été prouvé entre-temps) :

entrer n>0
tant que n!=1
si n est pair
n <- n / 2
sinon
n <- 3 * n + 1
fin tq
retourner n



Si une étude statistique montre qu'un diviseur n'est pas nul, peut-on dire que cette partie du code n'est pas buguée?

(merci de poster ça si ça vaut le coup)

[KiLVaiDeN]

Salut DrTopos, welcome back,

uzak: Il est vrai qu'en ce qui concerne la division par zero, il y a des choses qui ont été crées, par exemple "NaN" ( not a number ) ou "undefined" ou encore "infinite", et je pense que ta reflexion est liée un peu à celle que j'ai faite, à savoir qu'un programme pourrait être testé dans tous les cas possibles et fournir des résultats correctes si tous les cas posant problèmes ont étés pris en compte, mais ça n'empêche que ce n'est pas pareil que la notion de preuve.

DrTopos j'ai une question pour toi : en somme, si on utilise un langage dont les composants de base ont étés prouvés, est-ce qu'on est sûr que notre programme le sera aussi ? Je demande ça, car dans le cas de la division par 0, si j'ai bien compris, l'opération de division prouvée te fournirait un résultat cohérent quelque soit les paramètres en entrée, ce résultat pouvant être une erreur ?

Je me suis renseigné sur la notion de "Categories", et même un peu sur les topos (sur mathworld, un site en anglais vraiment bien fait) : bien que je n'ai pas compris grand chose, car les notions de maths évoquées sont hors de portée pour moi (pour l'instant tout du moins ) j'ai quand même remarqué une ressemblance frappante entre cette notion et la notion d'objets, présente dans les langages orientés objets. Est-ce que je me trompe ?

[KiLVaiDeN]

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
3
4
5
if file("tagada",read) is
   {
     failure then ...,
     success(f) then ...
   }

J'ai une question ici.. Je sais j'ai pleins de questions, mais faut pas m'en vouloir

Donc si j'ai bien compris, en Anubis, file("tagada",read) retourne un résultat de type Maybe. Il faut casser cette enveloppe pour pouvoir utiliser le contenu.

Pour la casser, tu testes la valeur du Maybe. Mais cette valeur que le Maybe renvoie ( soit failure, soit success ) est forcément un test d'écriture à l'adresse donnée, non ? si on peut écrire, on passe dans la branche success, sinon, on va dans failure. J'ai peut-être rien compris encore une fois

[DrTopos]

Au risque de me répéter, je réaffirme que le problème de la division par 0 et celui du fichier qu'on ne peut pas ouvrir sont de nature différente. Le premier est une erreur, le deuxième relève d'un comportement normal. Diviser par 0 ne doit jamais se produire, alors que ne pas trouver un fichier n'a rien d'anormal.

En ce qui concerne le calcul de l'infini, il faut distinguer deux choses: la théorie des ordinaux et cardinaux, qui est je crois tout à fait aboutie, et le fait d'introduire des éléments infinis dans la structure de corps qui à mon avis n'a pas grand sens si on le fait d'une manière naïve. Introduire l'infini dans les calculs ne peut se justifier que si on peut donner un sens précis à cet infini (comme on le fait en analyse non standard par exemple). Si c'est seulement une commodité pour permettre la division par 0, ce sera l'echec à coup sûr. De toute façon, même l'analyse non standard ne permet pas d'inverser 0, elle introduit seulement des infiniment petits et des infiniment grands (qui sont les inverses des infiniment petits, mais pas de 0).

Le problème principal est celui du sens qu'il faut donner à tout cela. On constate facilement en programmant que chaque fois qu'on écrit une division, elle n'aurait tout simplement pas de sens (au regard du but poursuivi par le programme) si on divisait par 0. La seule solution raisonnable est donc de s'assurer qu'on ne va jamais diviser par 0.

Il y a plusieurs façons de traiter ce problème. On peut l'ignorer complètement (langage C), on peut mettre un garde fou à l'exécution (exception dans le style Java), on peut intégrer le problème dans le typage du résultat (méthode employée par Anubis version 1), et enfin on peut éviter le problème dès la compilation, mais le seul moyen d'y parvenir est de prouver que quelque soit la façon dont le calcul se déroule (et en particulier, quelles que soient les données arrivant dans les entrées du programme) la division par 0 ne se produira jamais. Je répondrai plus longement plus tard sur cette histoire de division, car cela mérite encore des explications.

Par ailleurs, une statistique même positive à 100% ne constitue pas une preuve (pour un mathématicien du moins). L'algorithme dont tu parles (uzak, je précise, car les questions arrivent à une telle vitesse sur ce fil...) est connu sous le nom de problème de Syracuse. C'est un problème extrèmement difficile, sur lequel de nombreux mathématiciens ont travaillé. J'ai moi-même consacré plusieurs mois (il y a quelques années) à ce problème. J'avais espéré trouver quelque chose par des méthodes de théorie de la réécriture. Mais ça n'a pas marché. C'est réellement un problème diabolique. Je ne sais plus quel mathématicien (je crois que c'est Erdös) a dit que les mathématiques contemporaines n'étaient pas mûres pour ce genre de problème. On est bien obligés de rester modestes.

Ceci dit, même si les statistiques ne constituent pas une preuve, on est bien obligé de s'en contenter parfois. C'est ce que je fais moi-même quand je trouve surhumain de démontrer.

[DrTopos]

DrTopos j'ai une question pour toi : en somme, si on utilise un langage dont les composants de base ont étés prouvés, est-ce qu'on est sûr que notre programme le sera aussi ? Je demande ça, car dans le cas de la division par 0, si j'ai bien compris, l'opération de division prouvée te fournirait un résultat cohérent quelque soit les paramètres en entrée, ce résultat pouvant être une erreur ?

Si tu as un théorème dont l'énoncé commence par des quantificateiurs universels (quelque soit ...), tu peux particulariser ce théorème en instanciant les symboles universellement quantifiés. Tu obtiens un nouveau théorème que tu peux utiliser directement dans ton travail. Ce principe de démonstration fait partie de la définition même du sens du quantificateur universel. En fait le procédé est analogue à celui qui consiste à utiliser une fonction très générale dans une bibliothèque de programmes en l'appliquant seulement à des arguments particuliers. Si la fonction est correcte dans la bibliothèque, le cas particulier sera lui aussi correct. Conclusion, quand on particularise des composants prouvés on obtient des choses moins générales, mais tout aussi bien prouvées. Pour la question portant plus spécialement sur la division, je vais répondre plus tard dans un post consacré à la division.

Je me suis renseigné sur la notion de "Categories", et même un peu sur les topos (sur mathworld, un site en anglais vraiment bien fait) : bien que je n'ai pas compris grand chose, car les notions de maths évoquées sont hors de portée pour moi (pour l'instant tout du moins ) j'ai quand même remarqué une ressemblance frappante entre cette notion et la notion d'objets, présente dans les langages orientés objets. Est-ce que je me trompe ?

La théorie des Topos est une branche de la théorie des Catégories. Ce n'est pas très facile à aborder, et ça fait même peur à beaucoup de mathématiciens. La meilleure référence que je connaisse pour aborder cette théorie quand on est novice dans le sujet (mais je ne prétends pas connaitre toute la littérature sur le sujet) est le livre de Robert Goldblatt: Topoï édité chez North-Holland. Il fait plus de 500 pages, mais c'est un bouquin très pédagogique et très progressif, que l'auteur avoue avoir écrit précisément pour apprendre lui-même la théorie. Ceci dit, il doit exister des choses plus récentes et peut-être même meilleures.

Pour ce qui est des objets (de la POO), je ne vois pas de rapport direct, même s'il y a des gens, comme Gogen, qui ont beaucoup disserté sur le rapport entre objets au sens POO et catégories de faisceaux (des topos particuliers). J'avoue ne pas être convaincu par leurs arguments.

[KiLVaiDeN]

Un dernier post, un peu en rapport avec les choses évoquées, mais plutot pour évoquer une autre piste ( qui m'interesse énormément ) et qui n'a pas encore été prise en compte : il s'agit de l'orientation que l'informatique prendra, quand le fonctionnement du cerveau sera totalement démystifié.

Je me suis pas mal renseigné sur le sujet, et dans mes lectures j'ai apprit que :

l'architecture actuelle des ordinateurs, basée sur la théorie von neumann, ne correspond pas du tout à l'architecture du cerveau humain. Donc, en résumé, un ordinateur ne pourra _jamais_ égaler le cerveau, car il fonctionne tout simplement différement.

le cerveau introduit la notion du "peut-être" dans son raisonnement ( j'ai vu là un rapprochement avec le "Maybe" évoqué plus haut ) mais d'une façon "chaotique". Le cerveau est un organe, mélange de produits chimiques et d'impulsions nerveuses et neuronales, ce qui a pour conséquence que lorsqu'un choix est prit, imaginons en situation de problème, un autre aurait également pu être choisi. Une personne "pulsionnelle", agit donc différement d'une personne "réfléchie", bien que nous ayons tous des pulsions. Donc la notion la plus importante ici, est que le cerveau _peut produire des raisonnements faux_. Ce qui n'est pas le cas d'un programme informatique

fort de tout ça, le cerveau peut également "apprendre". Cet apprentissage se traduit (grossièrement) par une trace marquée plus fortement, lors de la stimulation d'un réseau de neurones. Par exemple, on apprend à jouer de la guitare, en s'entrainant. Cet entrainement a pour effet de "renforcer" les réseaux de neurones utilisés lorsque nous jouons de la guitare. Ce renforcement, par la suite, accélère le traitement de l'information, et donc nous permet de devenir plus performants. Ce phénomène est surtout chimique, lié aux neurotransmetteurs. Je ne suis pas un expert, donc je décris la chose très grossièrement.

Donc un système informatique futuriste, ne serait-il pas la représentation d'un cerveau, dont la notion de "chaos" serait retirée ?

[KiLVaiDeN]

En relisant mon post, je me rend compte qu'il n'est pas évident de faire le rapprochement avec le sujet de ce thread.

En fait "mon interrogation" serait : un système de preuve, ou un système de test, c'est très interessant, mais le cerveau possède un système "d'apprentissage", qui lui permet de mettre en rapport les choses, et donc de proposer une solution basée sur "l'experience", donc à terme, j'imagine bien un environnement de developpement, qui connaitrait le principe, les erreurs et les algorithmes de la plupart des programmes déjà écrits, qui en tirerait "une experience" et qui pourrait l'utiliser afin d'aider le programmeur a faire son propre programme, en fonction de ses objectifs, et en "prevoyant" les problèmes qui pourraient se poser.

Je dis tout ça en essayant d'imaginer ce que l'informatique pourrait devenir peut-être notre petit cerveau d'informaticien sera un jour cloné electroniquement

J'aimerais avoir l'avis de gens qui ont également creusé cette piste, même des suppositions ( comme les miennes ) sont les bienvenues..

[Manopower]

Pour en revenir au sujet du début, si je puis me permettre, il est parfois moins couteux de "laisser une part de mystère" dans son programme, de l'envoyer à tester et de traiter les retours.

car un développeur qui passe 3 fois plus de temps pour s'assurer que son programme est parfait, économisera certes 1 semaine ou 2 à son ami le testeur, mais s'il a pris 2 mois pour arriver à ce résultat...

Tant que le programme n'est pas livré à l'utilisateur final, je pense que le fait qu'il reste des bugs n'est pas génant. les services tests sont là pour faire gagner du temps au programmeur non ?

[gangsoleil]

Bonjour,

Je ne suis pas pécialement d'accord avec ce que tu dis : si tu fais ton programme correctement dès le début, tu auras beaucoup moins de soucis, ne serait-ce que parce qu'un bug peut en cacher un autre, et qe donc le nombre d'aller-retour entre le développeur et le testeur dans ce cas risque d'être assez exponentiel...

Ensuite, la preuve de programme n'est pas forcément utile dans tous les cas, mais dans tout ce qui est "life-critical", je pense que c'est une bonne idée de prouver les programmes...

Enfin, s'il existait un langage simple et pratique intégrant le système de preuve, je pense que les développeurs gagneraient beaucoup de temps, et passeraien donc encore moins de temps sur les projets (un peu plus de temps puisqu'il faut construire la preuve, mais quel gain de temps sur le debuggage !!!!!)

[DrTopos]

Un dernier post, un peu en rapport avec les choses évoquées, mais plutot pour évoquer une autre piste ( qui m'interesse énormément ) et qui n'a pas encore été prise en compte : il s'agit de l'orientation que l'informatique prendra, quand le fonctionnement du cerveau sera totalement démystifié.

Je trouve très intéressant de parler du cerveau et de ses rapports avec les ordinateurs, mais je crois indispensable de créer un autre fil sur ce sujet. On a déjà beaucoup de questions sur ce fil et cela risque de devenir incompréhensible.

Je te suggère donc de créer ce nouveau fil toi-même. N'oublie pas de mettre assez de tags devant le titre pour qu'on voit tout de suite de quoi il retourne.

[DrTopos]

Pour en revenir au sujet du début, si je puis me permettre, il est parfois moins couteux de "laisser une part de mystère" dans son programme, de l'envoyer à tester et de traiter les retours.

car un développeur qui passe 3 fois plus de temps pour s'assurer que son programme est parfait, économisera certes 1 semaine ou 2 à son ami le testeur, mais s'il a pris 2 mois pour arriver à ce résultat...

Tant que le programme n'est pas livré à l'utilisateur final, je pense que le fait qu'il reste des bugs n'est pas génant. les services tests sont là pour faire gagner du temps au programmeur non ?

C'est tout à fait le genre d'assertions qu'on ne peut pas prouver mathématiquement, et pour lesquelles les statistiques constituent l'outil adéquat.

Pour ma part, je pense qu'en prouvant les programmes on économise du temps, de l'énergie, de l'argent et on évite les risques (cf. ce que j'ai raconté dans un post précédent sur le travail de mon ami Olivier Duvernois). Mais il faudra encore beaucoup de temps et surtout d'expérimentations pour que la majorité des développeurs en soient convaincus.

[Manopower]

dans mon dernier post je n'ai pas voulu dire qu'il fallait volontairement laisser des bugs au testeur ! On est bien d'accord qu'il faut arriver à un maximum de qualité, mais il faut savoir aussi ne pas "gaspiller" du temps à faire le programme parfait, temps qui serait plus utile à allouer à un autre projet. Mais c'est certains qu'un bon test par le développeur est nécessaire avant d'envoyer au test. Si tout ce premier test est concluant, alors je pense qu'il est plus rapide d'envoyer au testeur plutot que de refaire X fois le tour de son appli dans l'hypothétique but de trouver une faille. ça c'est le boulot du testeur, à mon sens. La preuve ne devrait elle pas être un travail d'une personne tierce, dans la mesure ou il n'existe pas encore de code avec la preuve incluse ?

[KiLVaiDeN]

En fait, quand dans une chaine de developpement on se rend compte qu'il y a un bug, c'est rarement la personne qui a detecté le bug qui le répare ( elle n'est d'ailleurs pas habilité à le faire, même si elle savait le faire ). La seule chose que cette personne fait, c'est établir un cahier de tests, et déployer un à un les scénarios.

Après la réparation de l'erreur retombe quand même sur le coin de la figure du developpeur !

Je pense que le but de prouver le programme est interessant dans l'hypothèse que le temps de programmation reste le même, si le langage se porte bien à cela.

[DrTopos]

dans mon dernier post je n'ai pas voulu dire qu'il fallait volontairement laisser des bugs au testeur ! On est bien d'accord qu'il faut arriver à un maximum de qualité, mais il faut savoir aussi ne pas "gaspiller" du temps à faire le programme parfait, temps qui serait plus utile à allouer à un autre projet.

Tout à fait d'accord. Le mieux est l'ennemi du bien. Je suis moi-même un abominable perfectionniste, et ça m'a joué plus d'un tour.

La preuve ne devrait elle pas être un travail d'une personne tierce, dans la mesure ou il n'existe pas encore de code avec la preuve incluse ?

Si on fait un programme dans un langage sans formalisation des preuves, il vaut mieux prouver (dans les commentaires ou dans un document annexe) en programmant. Je souhaite beaucoup de courage à celui qui aura à prouver les programmes faits par d'autres. En fait, je pense que la meilleure méthode, tant qu'on n'utilise pas de langage incluant les preuves, est de faire d'abord un cahier des charges très précis et contenant une description précise du programme avec les preuves que les spécifications sont respectées par ces descriptions. Une fois que c'est fait, le travail de programmation est grandement simplifié et sécurisé.

[DrTopos]

Pour la casser, tu testes la valeur du Maybe. Mais cette valeur que le Maybe renvoie ( soit failure, soit success ) est forcément un test d'écriture à l'adresse donnée, non ? si on peut écrire, on passe dans la branche success, sinon, on va dans failure.

Je ne comprends pas ce que tu entends précisément par test décriture. En tout cas, le bout de programme que j'ai donné n'essaye pas d'écrire dans le fichier pour savoir s'il est ouvert. La primitive 'file' fait un appel à 'fopen' (la machine virtuelle d'Anubis étant écrite en C), et teste si le retour de fopen est NULL. Si c'est le cas le résultat est 'failure' sinon c'est 'success(f)', où 'f' est le 'handle' (donc forcément valide) du fichier. Maintenant, comment le compilateur Anubis implémente le type 'Maybe(RWAddr(Int8))' est une autre affaire. En fait une donnée de ce type est de longeur variable (en nombre de bits). 'failure' est représenté par un bit unique (qui vaut 0) et 'success(f)' est représenté par un mot de 32 bits, qui se décompose en un bit (le même que pour 'failure', mais qui cette fois vaut 1, et qui veut dire 'success') et un pointeur (représentant 'f') sur un record contenant tout ce qu'il faut pour se servir du fichier ouvert.

Le mot casser employé ci-dessus est adéquat. Effectivement, la conditionnelle 'casse' la donnée renvoyée par 'file' en testant le bit dont j'ai parlé, ce qui permet de se brancher sur le bon corps de cas. En théorie des types, et dans le folklore informatico-catégorique, chaque type a ses constructeurs et ses destructeurs (ces mots n'ayant pas le même sens qu'en C++). Donc on détruit ou on casse. Par exemple, dans le cas des types fonctionels, on construit les fonctions avec lambda en Lisp, function en CAML ou avec |-> en Anubis, et on les détruit en les appliquant à des arguments.

[DrTopos]

Je reviens donc comme je l'ai promis sur la question de la division par zéro. IL s'agit de traiter le problème non pas tellement du point de vue du programmeur, mais plutôt du point de vue du concepteur de langage. Par la même occasion, je considère le problème du dépassement de buffer qui est de la même nature.

Comme je l'ai suggéré dans un post pécédent, je vois 4 façons de traiter le problème que je vais appeler solutions 1, 2, 2bis et 3. (2/2bis à cause de la ressemblance entre ces deux méthodes).

Méthode 1: On ne fait rien de spécial, c'est à dire qu'on laisse au programmeur l'entière responsabilité de ce problème. Il doit faire attention de ne pas diviser par zéro et de ne pas faire de dépassement de buffer. C'est ce que fait le langage C (et de nombreux autres langages). Le compilateur C se moque pas mal qu'on divise par zéro. Ca ne le regarde pas.

Bien entendu, si j'ai un tableau t de 3 cases et si j'écris t[0], ou si j'écris la division x/2, je ne prends pas un grand risque. Le problème arrive quand on écrit t[ i ] ou x/i, et que i est le résultat d'un calcul dont on a du mal à maîtriser le résultat.

Méthode 2/2bis: on met un garde fou à l'exécution. Autement-dit, au run-time, juste avant de diviser, on teste si le dénominateur est nul, ou on teste si l'indice est dans les limites du tableau. Evidemment à ce stade on peut le faire facilement car i est calculé, ce qui n'était pas le cas à la compilation. C'est ce que fait Java avec son système d'exception (méthode 2), et c'est ce que fait Anubis 1 en prenant en compte la possibilité d'erreur dans le typage du résultat de la division ou de la lecture/affectation pour un tableau (méthode 2bis).

Cette méthode est bâtarde, d'abord parce qu'elle n'intervient que quand le mal est fait (l'opération de division est impossible ou la lecture/affectation dans le tableau est impossible) et c'est au programmeur de se débrouiller pour capturer l'exception (méthode 2) ou traiter le cas d'erreur (méthode 2bis). Dans un cas comme dans l'autre, il s'agit d'un rattrapage, un pis-aller, pour une erreur qui en bonne logique n'aurait jamais dû se produire, ce qui montre bien que ce n'est pas la solution idéale.

Malgré cela, cette solution 2/2bis est préférable à la méthode 1 dans le cas de programmes non fiables (en particulier sur le plan des mauvaises intentions, surtout lorsqu'ils sont récupérés sur le web), alors que la, méthode 1 est acceptable pour les logiciels qui sont distribués en confiance. D'ailleurs, ce qui justifie le fait qu'on continue à utiliser la méthode 1 quand c'est possible est le fait que la méthode 2/2bis, en introduisant un test à l'exécution provoque une perte sensible de performances.

Méthode 3: prouver à la compilation que la division par zéro ou le dépassement de buffer ne peut pas se produire, avec vérification de cette preuve par le compilateur. On voit bien que c'est la méthode idéale, car d'une part on n'aura pas à se soucier de traiter un cas d'erreur (qui ne peut pas se produire), et d'autre part comme on ne fait pas de test (qui devient inutile car une fois de plus l'erreur ne peut pas se produire), on ne diminue pas les performances.

Vous me direz qu'on aboutit au même résultat avec la méthode 1, si le programmeur est assez bon pour être certain qu'il n'a pas fait de faute. En fait, la seule différence entre la méthode 1 et la méthode 3, et le transfert de responsabilité du programmeur au compilateur. Je crois que c'est une différence suffisamment significative pour qu'on s'y intéresse.

Donc la question est maintenant de savoir comment y parvenir. D'abord il est bien clair qu'il faut impérativement que la syntaxe même du langage autorise l'écriture d'énoncés mathématiques et de preuves. Ce n'est pas très difficile. Les énoncés sont faciles à formaliser, puisqu'ils sont construits à partir des égalités et inégalités (et un certain nombre d'autres énoncés qu'on appelle atomiques) et d'autre part à l'aide des connecteurs logiques (vrai, faux, et, ou, implique, non, quelque soit, il existe) qui permettent de construire des énoncés non atomiques. La sémantique de ces énoncés peut s'exprimer formellement de plusieurs façons (qui ne sont pas complètement équivalentes d'ailleurs, mais cela n'a pas d'importance tant qu'on reste avec un système robuste, c'est à dire dans lequel tout énoncé prouvé est vrai) à l'aide soit de règles de déduction naturelle (à la Gentzen; c'est ce que fait le langage B), soit des adjonctions de foncteurs, etc..., mais certainement pas des tables de vérité, qui sont totalement impuissantes pour traiter ce genre de question.

Il se trouve que si la recherche de preuve est un problème très difficile, menant dans presque tous les cas à une explosion combinatoire, le problème de la vérification du caractère correct d'une preuve est au contraire facile, et essentiellement linéaire en complexité.

Maintenant, il reste la question de l'intégration de ces concepts parmi les concepts plus classiques de la programmation, c'est à dire par exemple la déclaration des types des fonctions. Reprenons l'exemple de la division. Dans les langages utilisant les méthodes 1 et 2, le typage de la division est int*int -> int, c'est à dire que la division (des entiers) prend deux entiers quelconques et renvoie un entier. Dans le cas de la méthode 2bis le typage est (en Anubis 1): (Int32,Int32) -> Maybe(Int32), la présence de Maybe obligeant le programmeur à prévoir quelquechose pour le cas où le dénominateur serait nul. Enfin, dans le cas de la méthode 3, le typage de la division serait quelque chose comme ceci (où Nat représente un type de vrais entiers naturels, sans limitation de taille comme en Lisp):

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
Nat * {n:Nat | n!= 0} -> Nat

Autement-dit, la condition que le dénominateur ne doit pas être nul est intégrée au type de départ, ce qui est tout à fait différent du Maybe qui porte sur le type d'arrivée, c'est à dire qui intervient après la division (éventuellement ratée), ou lieu d'intervenir avant. Dans le cas du buffer t, le typage de t[ ] (contenant 3 cases) serait quelquechose comme:

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
&#123;n&#58;Nat | n < 3&#125; -> T

où T est le type de ce qu'on met dans le tableau. (En théorie les tableaux (non mutables du moins) ne sont rien d'autre que des fonctions qui sont implémentées d'une façon particulière).

La question est maitenant de savoir comment le compilateur peut parvenir à faire le type-checking. Dans le cas d'une division, disons x/y, il vérifie que x est de type Nat, puis que y appartient à {n:Nat | n != 0}. Pour cela, il vérife d'abord que y est de type Nat, puis il cherche dans l'environnement s'il trouve une preuve de l'énoncé y != 0. A cette fin, il applique éventuellement des méthodes de recherche de preuve bridées (pour éviter l'explosion combinatoire), et de toute façon réclame la preuve au programmeur s'il ne la trouve pas lui-même. Dans le cas du buffer, c'est pareil sauf que l'énoncé à démontrer pour le terme t[ i ] est i < 3.

Prouver n'est pas plus difficile que programmer, pour la raison que c'est presque la même chose avec un vocabulaire différent (on pourrait faire un tableau comparatif pour mettre ceci en évidence). Toutefois, il y a une différence essentielle entre les types de données et les types de preuves (i.e. les énoncés), c'est qu'un type de donnés peut contenir des données distinctes, alors que deux preuves du même énoncé ont toujours la même sémantique. Quand on cherche une preuve d'un énoncé, peu importe celle qu'on obtient, pourvu qu'on en ait une. D'une certaine façon, ceci rend la recherche automatique de preuve plus facile que la recherche automatique de programme, et surtout, il est plus facile de spécifier une preuve (l'énoncé démontré par cette preuve suffit) que de spécifier un programme (le type de ce programme, qui est une fonction par exemple, ne suffit pas).

Moralité: il ne faut pas avoir peur des preuves.