[Fondements] Preuve de programme: utopie ou réalité ?

Bonjour à tous.

Au jour où les industries de pointe (et en particulier celles qui font du lociciel critique, mais pas seulement celles-là) s'interrogent de plus en plus sur la nécessité d'éradiquer les bugs, il serait intéressant de connaitre les (bonnes, voire très bonnes) habitudes des uns et des autres pour lutter contre ce fléau.

Le sujet étant très vaste, et recoupant la POO, l'extrème programming, et bien d'autres méthodologies (ces aspects étant d'ailleurs traités dans d'autres fils de ces forums), j'aimerai qu'on s'en tienne à l'aspect preuve de programme (automatique, assitée ou complètement manuelle, un commentaire dans le source pouvant avoir valeur de preuve), qui est déjà bien assez vaste.

En fait, la question (naïve) au centre de ce débat pourrait être: Quelles méthodes préventives utilisez-vous pour éviter d'avoir à déboguer ?

Faites nous part de vos expériences, de vos doutes, de vos espoirs, et de votre pratique quotidienne. Interrogez-vous sur les fondements de votre activité, et sur les rapports qu'elle entretient avec la logique mathématique.

A vos plumes.

Bonjour,

Je pense que les preuves formelles des programmes (c'est à dire la preuve mathématique d'un programme informatique) est quelque chose de très couteux et de très complexe, et qui demande que le programme ait été prévu pour cela.

Ceci dit, ce genre de preuve, qui devrait normalement être appliquée sur les logiciels critiques, ne l'est pas assez, voir très rarement (que ce soit dans l'avionique, l'automobile, ...), pour de fallacieuses raisons de coût...

Sinon, je ne vois pas bien ce vous entendez par

Citation:

---

preuve de programme automatique, assitée ou complètement manuelle, un commentaire dans le source pouvant avoir valeur de preuve

---

.

Est-ce que le fait d'écrire un test pour un bout de code donné est considéré comme une preuve ?

Je pense qu'il entendait par là la démonstration mathématique que le code (ou le bout de code en question) fonctionne, mise en commentaire.
Ou bien une simple annotation "prouvé", qui renverrait à la démonstration dans une documentation à part.

Citation:

---

Envoyé par gangsoleil

Bonjour,

Je pense que les preuves formelles des programmes (c'est à dire la preuve mathématique d'un programme informatique) est quelque chose de très couteux et de très complexe, et qui demande que le programme ait été prévu pour cela.

Ceci dit, ce genre de preuve, qui devrait normalement être appliquée sur les logiciels critiques, ne l'est pas assez, voir très rarement (que ce soit dans l'avionique, l'automobile, ...), pour de fallacieuses raisons de coût...

---

Je crois qu'il y a essentiellement deux façons de ``prouver des programmes''. On peut soit essayer de prouver des programmes écrits dans des langages n'ayant pas de notion de preuve (comme le C par exemple), et alors on s'embarque dans un processus incertain, car il s'agit de corriger et enrichir un texte dans lequel beaucoup d'informations sont manquantes. C'est ce que fait le logiciel CAVEAT développé au CEA et utilisé par Airbus (entre autres). Et effectivement c'est très couteux. Mais on peut aussi utiliser des langages et des outils qui maintiennent la cohérence logique tout au long du developpement. Dans ce cas, bien sûr, il faut faire des efforts pour écrire des preuves, qui sont une sorte de code qui ne produit pas de programme. Mais il y a une contre-partie car on économise beaucoup de debogage, ce qui fait que le coût est à mon avis moins élévé qu'avec les méthodes traditionnelles. Ces méthodes sont appliquées depuis pas mal d'années chez Alsthom, en particulier dans le train. Tout cela pour dire que je ne crois pas à l'argument ``coût''.

Citation:

---

Envoyé par gangsoleil

Sinon, je ne vois pas bien ce vous entendez par

Citation:

---

preuve de programme automatique, assitée ou complètement manuelle, un commentaire dans le source pouvant avoir valeur de preuve

---

.

Est-ce que le fait d'écrire un test pour un bout de code donné est considéré comme une preuve ?

---

Les mathématiciens écrivent bien des preuves qui ne sont que du texte sur du papier et qui ne sont jamais vérifiées par des machines. Aussi, je pense que des sources bien commentés peuvent contenir de telles preuves. Maintenant, un test ne constitue pas une preuve (de même qu'une expérience de physique ne saurait se substituer à une preuve mathématique), sauf peut-être dans les rares cas où il peut être complètement exhaustif (model checking).

En ce qui concerne les logiciels critiques, effectivement, les méthodes de preuves sont plus ou moins appliquées (plutôt moins que plus). Par exemple, des logiciels développés chez Sagem pour les drones (en langage C) ont demandé des milliers d'heures de débogage. Mais même quand elle sont utilisées, elles ne sont parfois que des preuves partielles. Les ingénieurs en avionique utilisent beaucoup le compilateur LUSTRE pour écrire des systèmes réactifs. Or ce compilateur fait surtout des vérifications de cohérence temporelle (absence de paradoxe temporel), mais ne prouve pas les automates stricto sensu.

Pour la suite de ce débat:

Il faut comprendre que même si la plupart d'entre nous n'utilisent pas de méthodes formelles strictes, elles sont quand même sous-jacentes dans tous les programmes bien écrits. Si un source est bien écrit, un lecteur humain peut, en raisonnant dans sa tête, s'assurer (c'est à dire prouver) qu'il est correct. C'est surtout de ce genre de preuve que j'aimerai qu'on débatte, l'heure n'étant sans doute pas encore venue de l'utilisation des langages à preuves dans les projets de développements non critiques. Ceci dit, la notion même de preuve de programme (formelle ou non) a plusieurs sens, et de celà aussi on peut débattre.

Citation:

---

Envoyé par naholyr

Je pense qu'il entendait par là la démonstration mathématique que le code (ou le bout de code en question) fonctionne, mise en commentaire.

---

C'est bien ce que j'entendais effectivement.

Ca ne m'arrive quasiment jamais de prouver un programme, même si j'ai effleuré ce thème dans ma formation - en prépa -. J'apprend à utiliser une approche de l'eXtreme Programming qui consiste à commencer par écrire des tests puis programmer, et toujours tester et retester ce que j'ai fait. Le test doit être le plus explicite possible et tester un maximum de possibilité, mais c'est difficile quand on a pas l'habitude, donc faire la preuve d'un programme, c'est encore plus difficile.
Je pense aussi que pour réussir à prouver un programme, il faut avoir de bonnes habitudes de programmation, c'est-à-dire mettre des noms de fonctions et de variables bien explicites, cela permettant de bien "voir" la démo.
Mais ce n'est que mon avis.

L'eXtreme Programming est une approche intéressante, et qui semble se généraliser. J'essaye d'ailleurs moi aussi de la mettre en application dans mon travail. Mais c'est plus une méthodologie ``sociale'' que ``fondationnelle''. D'une certaine façon c'est orthogonal à la preuve de programme, sauf peut-être en ce qui concerne les tests, ce qui ne veut pas dire que les preuves peuvent supprimer tous les tests, mais une partie d'entre eux seulement, car il y a clairement deux sortes de bugs: les bugs de nature formelle, que les preuves peuvent éviter, et les bugs sur l'intention du commanditaire qui necessiteront toujours du feed-back et des itérations.

En fait, il semble que la différence fondamentale en matière de difficulté entre les maths ``pures'' et la preuve de programmes, est qu'en math il est difficile de trouver les preuves (Fermat-Wiles étant un exemple extrème) et en info il est difficile de trouver les énoncés qu'on doit prouver (comme le montre le désaroi aussi bien des matheux que des ingénieurs dès qu'il s'agit de ``prouver'' un processus industriel). En tout cas, c'est ce que j'ai pu constater jusqu'à maintenant.

Citation:

---

Envoyé par Miles

Ca ne m'arrive quasiment jamais de prouver un programme, même si j'ai effleuré ce thème dans ma formation - en prépa -....

---

Ce qui m'intrigue dans ce que tu dis c'est le mot quasiment. Cela veut-il dire que ça t'arrive quand même, ou que cela t'est déjà arrivé ? Pourrais-tu développer un peu ?

En fait, j'ai dû en faire en cours, maintenant une fois que j'ai l'algorithme qui me fait ce que je veux - j'ai fait qqs démonstrations par exemple pour des matrices de Houseolder dans une algèbre non commutative ou même chose pour des matrices de Givens dans un cadre non commutatif -, je programme. Ce ne sont pas des preuves des programmes - dans le sens où le programme n'est pas démontrer, j'ai toujours encore à tester le fait que le programme fait bien ce que je voulais -.

Pour ma part, j'avoue que je ne prouve pas mes programmes (développement système en C).

En revanche, je les tests (relativement) beaucoup, et utilise des outils (comme 'purify') afin de trouver les bugs.

Pour ce qui est des algorithmes, j'avoue que le côté preuve me fait défaut, et qu'il faudrait que je fasse quelque chose un jour de ce côté là.

La démarche de "preuve" est, à mon avis, trop contraignante pour de nombreux développement. La plupart du temps, le risque de bug est admis : on en a trop fourni auparavant, donc l'idée qu'un programme puisse être parfait relève à présent - à tort - de l'utopie.

Cependant, à défaut de preuve, je crois que la recherche de la couverture maximale d'un programme est un indicateur de qualité et de la maturité du processus de développement.

Pour ceux qui ne savent pas (encore) de quoi il s'agit, une étude de couverture d'un programme vise à vérifier que toutes les alternatives sont prises en compte, que pour chaque Si, il y a bien un Sinon associé, ou à défaut d'autres Si qui vont vérifier toutes les autres valeurs.

Ainsi, l'étude de couverture permet de découvrir le code mort (où l'on ne passera jamais), de repérer le code critique (où l'on passe le plus fréquemment), de construire le meilleur jeu de test (celui qui activera tous les sous-programmes, qui passera dans tout le code actif), et de s'assurer qu'aucun cas n'a été oublié ...

Dans la démarche qualité, ce que l'on fait à parfois moins d'importance que de savoir pourquoi on le fait (ou pourquoi on ne le fait pas). La couverture permet de savoir ce que l'on fait, ou pas, et nécessite donc une justification de ce qui n'est pas couvert.

Je sais qu'il existe des outils réaliser ce traitement automatiquement ...

En perl, notamment, certains modules du CPAN sont dédiés à cette tache : Test::Strict, Devel::Cover, Devel::Coverage, ... Certains sont toujours dans des versions Alpha, ce qui démontre aussi la complexité de la tache, mais le processus qualité est en route ;)

En espérant faire avancer le débat ...

Citation:

---

Envoyé par 2Eurocents

Pour ceux qui ne savent pas (encore) de quoi il s'agit, une étude de couverture d'un programme vise à vérifier que toutes les alternatives sont prises en compte, que pour chaque Si, il y a bien un Sinon associé, ou à défaut d'autres Si qui vont vérifier toutes les autres valeurs.

---

Merci pour ta contribution. Il est clair qu'elle fait avancer le débat.

Pourrais-tu donner une référence à propos de cette notion de couverture (document théorique ou doc de logiciel) ?

Il faut bien voir que la couverture pourrait être analysée dès la phase algorithmique. Rien ne s'y oppose, en effet. Et les analyses manuelles sont souvent faites à ce niveau, avant que la complexité des traitements n'apparaisse, suite à l'assemblage des modules.

Cependant, la couverture doit de nouveau être vérifiée sur la version finale et définitive d'un programme.

C'est pour cela que l'analyse (automatique) de couverture est réalisée à l'aide d'outils spécifiques aux langages utilisés.

Citation:

---

Envoyé par DrTopos

Pourrais-tu donner une référence à propos de cette notion de couverture (document théorique ou doc de logiciel) ?

---

Il y a donc les modules Perl CPAN que j'ai déjà cité et que j'ai eu (un peu) l'occasion d'utiliser. Leur documentation n'est cependant pas toujours très explicite, ou très détaillée sur le concept

Sinon, je vais ajouter des outils que je connais de nom pour réaliser des traitements de ce type, mais que je n'ai jamais eu l'occasion d'utiliser. Leurs pages respectives indiquent assez bien ce qu'ils font :
- CTC++, pour le C et le C++.
- JCover pour le développement Java.

Sinon, il y a une page relativement détaillée sur Les Tests à l'Institut National des Télécommunications à Evry.

C'est tout ce que j'ai en boutique ... désolé.

Merci pour les références:

Citation:

---

Envoyé par 2Eurocents

- CTC++, pour le C et le C++.
- JCover pour le développement Java.

Sinon, il y a une page relativement détaillée sur Les Tests à l'Institut National des Télécommunications à Evry.

---

J'ai consulté CTC++ et la page relative aux tests.

En ce qui concerne CTC++ il me semble que ce système ne fasse que des test et statistiques à l'exécution. Il n'y a pas de ce que certains appellent une ``analyse statique'', c'est à dire ne demandant pas d'exécution du programme. (Je peux me tromper, mais c'est ce que je crois avoir compris).

Maintenant sur la page de tests de l'Institut des Télécoms, je cite le préambule:

Citation:

---

Le test est une approche dynamique de la vérification par laquelle le logiciel est exécuté avec des données de test pour vérifier la présence de caractéristiques prévues.

---

Ici encore, il ne s'agit que de tests à l'exécution.

Bien sûr, tous ces tests ont leur intérêt. Par exemple, la méthode McCabe permet d'améliorer la modularité du programme. De nombreux tests permettent d'améliorer les performances (profiling, bottlenecks,...).

Toutefois, aucun de ces tests ne peut être assimilé à une preuve, je dirai par définition. Une preuve est un processus formel qui permet de s'assurer que certaines conditions (spécifications) sont satisfaites, quelle que soit l'exécution particulière du programme. Aucune batterie de tests par exécution du programme ne peut avoir la valeur d'une preuve. Bien sûr, j'entends le mot ``preuve'' comme un mathématicien.

A un moment j'ai cru qu'il pouvait y avoir dans ce que tu as proposé une méthode s'apparentant aux preuves:

Citation:

---

Envoyé par 2Eurocents

Pour ceux qui ne savent pas (encore) de quoi il s'agit, une étude de couverture d'un programme vise à vérifier que toutes les alternatives sont prises en compte, que pour chaque Si, il y a bien un Sinon associé, ou à défaut d'autres Si qui vont vérifier toutes les autres valeurs.

---

car le fait de vérifier qu'on oublie pas de cas peut être fait statiquement (je connais au moins un compilateur qui le fait). Mais ce n'est pas ce que font les systèmes que tu as proposés.

Citation:

---

Envoyé par Miles

... une fois que j'ai l'algorithme qui me fait ce que je veux - ... , je programme.

---

Ici tu sous-entends en fait que l'algorithme est déjà prouvé (pas nécessairement par toi), et tu te contentes de le ``traduire'' dans ton langage de programmation. Dans ce cas, je crois qu'on peut parler de programme prouvé (mais bien entendu, avec la nuance, que l'erreur étant humaine, on n'a pas le même degré de fiabilité qu'avec une preuve vérifiée par un compilateur).

Citation:

---

Envoyé par Miles

Ce ne sont pas des preuves des programmes - dans le sens où le programme n'est pas démontrer,

---

Un programme peut être partiellement prouvé. Si on sait quelles sont les parties prouvées, on peut limiter le débogage au reste du programme.

Citation:

---

Envoyé par Miles

j'ai toujours encore à tester le fait que le programme fait bien ce que je voulais -.

---

Sans doute parce que l'algorithme en question ne constitue pas tout le programme. Mais aussi peut-être parce qu'une preuve ne peut finalement prouver que des spécifications formalisées. Tout ce qui est sous-entendu, dit oralement, frappé au coin du bon sens, etc... mais non formalisé, ne peut être formellement prouvé. C'est d'ailleurs sans doute cet aspect des choses qui rend l'introduction des preuves si difficile en programmation.

Pour ma part, sans avoir la prétention de faire avancer le débat, mes précautions prises pour avoir le moins de bugs possibles sont :

:arrow: Un bon environnement de developpement qui m'élimine tous les risques de fautes de frappes ou de paramètres manquants ou de type non cohérent. Eclipse pour Java est un exemple d'IDE idéalement bati pour cette prévention.

:arrow: Une utilisation systèmatique de modèles de code. Par exemple les design patterns, ou tout simplement un format de code classique pour gérer les exceptions, ou les autres structures qui sont récurrentes. J'essaie de n'écrire que les changements de codes, et pas de refaire des lignes que j'ai déjà faite ailleurs, surtout en matière de structure. Dans la plupart des IDE, il y a la notion de "template", qui permet de coller une structure de code.

:arrow: Une bonne gestion des exceptions. D'ailleurs je trouve qu'un langage permettant cela permet d'eliminer enormement de bugs en comparaison à un langage qui ne les gère pas.

:arrow: Une gestion personnelle des commentaires, surtout pour les accolades fermantes ( je place systèmatiquement le nom de l'élément fermant l'accolade, par exemple : } // end if )

:arrow: L'affichage de "log" pendant les phases critiques du code, pour tracer les valeurs de variables critiques, un bon outil de log est très utile, je n'utilise pas les debuggeurs car personnellement je trouve que c'est une mine d'informations _trop riche_ lorsqu'on souhaite une information précise. Et j'estime que si on ne sait pas ce qu'on souhaite, c'est soit qu'on débarque au milieu d'un code étranger ( auquel car l'utilisation du debuggeur est justifiée ) soit qu'on a fait une très mauvaise analyse, et que le code qu'on a produit est mal ficelé..

:arrow: Une utilisation intensive de la programmation orientée objet. L'encapsulation des traitements permet d'encapsuler également les bugs.

:arrow: Dernière chose qui me vient à l'esprit : le nom des variables et des méthodes. Plus on tend vers l'explicite, plus on va vite pour comprendre les erreurs de logique.

Je pense personnellement que pour l'informatique, il est de plus en plus important d'utiliser des modèles de code. Ce sont ces modèles qui devraient être "démontrés". Ensuite, nous pourrions les utiliser comme "théorèmes" dans nos propres programmes :wink:

PS : DrTopos, hier soir je me suis interessé au langage anubis, je n'ai pas encore eu le temps d'approfondir la question, mais les chiffres en pourcentages annoncés sont impressionnant, la démarche utilisée pour développer en anubis n'est-elle pas plus "contraignante" pour arriver à un tel résultat ? Est-elle plus intuitive ?

Merci KiLVaiDeN pour ta contribution détaillée.

Je crois que les méthodes 'anti-bugs' que tu proposes devraient être appliqués par tous. De toute façon j'imagine que comme professionnel de la programmation, ignorer de telles méthodes reviendrait à se faire harakiri.

Je ne vais pas les commenter, mais seulement ajouter les quelques principes que je mets moi-même en application dans mon developpement. Je ne développe pas en Java, mais seulement en C et en Anubis ces dernières années, ce qui entraine des différences méthodologiques assez importantes.

:arrow: Une chose qui peut paraître triviale, mais qui est très utile en C, est d'utiliser systématiquement la macro 'assert'. Pour moi c'est la première chose qu'on devrait apprendre en C. Si on utilise bien cette macro (en fait à chaque fois qu'une chose peut être 'assertée'), on diminue considérablement les temps de débogage. La raison en est simple: on sait tout de suite où il faut agir.

:arrow: Toujours pour le C, chaque 'switch' qui ne contient pas de cas 'default', doit systématiquement être complété par le cas 'default: assert(0);' J'ai fait cela de manière systématique dans le compilateur Anubis (550 pages de C quand même) et grand bien m'en a pris. J'ai certainement économisé des mois de débogage.

:arrow: Et puis évidemment, et on ne le répetera jamais assez: se méfier des effets de bord comme de la peste. Si on peut programmer déterministe (c'est à dire sans effet de bord) faisons-le, même si on perd un peu en performance. Là aussi on économise énormément de débogage.

:arrow: J'ai un certain nombre d'autres principes concernant le C (mais qui peuvent comme les précédents s'appliquer à C++ et Java aussi bien), comme par exemple de ne jamais faire d'effet de bord dans les arguments d'une fonction, car on ne sait pas dans quel ordre ils vont s'exécuter, etc...

En Anubis, c'est très différent, car le compilateur est beaucoup plus contraignant qu'un compilateur C C++ ou Java. Ceci dit, il n'est pas parfait non plus, et en particulier n'impose aucune contrainte sur les effets de bord. Donc là aussi on doit faire attention.

Les modèles de code sont bien sûr très intéressants. En Anubis on a une notion de 'schéma' qui ressemble aux templates du C++. J'utilise beaucoup de schémas. Par exemple, je suis en train d'écrire (en Anubis) un éditeur graphique qui est un schéma à lui tout seul, car il ignore tout du type des donnés à éditer (ce type étant un paramètre). Cette notion de schéma/template est sans aucun doute l'un des meilleurs outils pour la réutilisabilité du code (donc aussi pour la sûreté).

Un mot sur les exceptions. Quand j'ai fait le design d'Anubis, j'ai décidé qu'il n'y aurait pas de notion d'exception. Les exceptions sont traitées par la façon de typer les résulats des fonctions qui seraient susceptibles d'en lancer. Le résultat est que les situations exceptionnelles doivent être traitées immédiatement et explicitement dans le code qui exploite le résultat de l'appel. Même si ça introduit une certaine lourdeur (très relative), il est certain que cela rend le texte plus facile à relire, car le problème est traité là où il apparaît. La sûreté est également plus grande qu'avec un système de capture d'exception laissé à la responsabilité du programmeur.

Pour terminer je vais répondre aux deux autres questions de ton post scriptum. Les pourcentages annoncés ne sont pas des inventions, mais bel et bien le résultat des expériences menées par Olivier Duvernois et moi-même. Je pense qu'on peut en comprendre assez facilement la raison après un peu d'usage du compilateur Anubis. Il maintient un très haut niveau de cohérence du code. Par exemple, Olivier maintient seul un programme d'un million de lignes. Il lui arrive d'entreprendre des modifications de structure touchant une cinquantaine de modules, et en général c'est réglé en une demi-journée, sans mauvaise surprise (en particulier sans régression). C'est vrai que le compilateur Anubis est très très contraignant, mais on s'y fait, et en fin de compte, on est content qu'il le soit, parce que ça signifie tout simplement qu'il libère le programmeur d'un grand nombre de responsabilités.

Enfin, Anubis est-il intuitif ? J'ai constaté sur quelques cobayes qu'il est très facile à apprendre pour tous ceux qui ont fait du Lisp ou du CAML, mais qu'il peut être très difficile pour ceux qui n'ont fait que de l'impératif (C, C++, Java, assembleur, ...). La question est certainement d'être capable de remettre en cause sa façon de penser la programmation, car les gens qui n'ont jamais programmé s'y mettent facilement.

Merci pour ta réponse DrTopos, je compte passer du temps ce week-end pour comprendre comment fonctionne Anubis, car je suis intrigué par cette "nouvelle façon de programmer" qui a l'air prometeuse, je te ferais part de mon expérience :) Et il se peut même que je réalise un projet avec Anubis si je le trouve prometteur, car il n'y a pas de meilleur moyen d'apprendre un langage que de réaliser un projet avec.

Je me suis souvent posé des questions sur les manières d'optimiser la manière de programmer, sans réduire le champs des possibilités. Je parle du champs de possibilités, car il est facile de réduire considérablement la difficulté de programmer en offrant moins de "pistolets" pour se tirer dans le pied :wink:

Comme exemple on peut prendre un langage comme Coldfusion pour le developpement web, réputé pour être très simple d'utilisation et rapide à mettre en oeuvre, soit disant permettant de traiter n'importe quel problème lié aux applications web; oui c'est vrai il est très efficace dans la plupart des situations, mais ils oublient de préciser que le langage permet en effet de gérer 90% des demandes les plus courantes, mais les 10% restants non implémentées de base peuvent ralentir un projet au point de le rendre aussi long qu'un projet fait sous une plateforme J2EE ( Java ) qui bien que plus lourd et compliqué à mettre en oeuvre, propose la puissance du langage de programmation Java. Sans oublier que ces 10% ( obligatoirement traité dans un autre langage de coldfusion ) sont beaucoup plus sujets aux bugs que les autres 90% !

Il y a un autre aspect des choses : le langage est souvent adapté à résoudre une partie du problème, mais totalement inadapté pour une autre partie ! Par exemple, Perl, est réputé pour son efficacité dans le traitement des chaines de caractères, et C est réputé pour son efficacité dans la programmation système. Mais que se passe-t-il lorsque le programme qu'on souhaite réaliser doit pouvoir faire les deux ? On se retrouve embêté, on choisit le langage qui est le plus "généraliste" et qu'on connait le mieux, et en général on se rend compte que ce n'est pas le domaine de prédilection du langage qui est propice aux bugs et qui pose des difficultés, mais plutot celui qu'il ne gère pas de la manière la plus efficace !

Citation:

---

Envoyé par KiLVaiDeN

Je me suis souvent posé des questions sur les manières d'optimiser la manière de programmer, sans réduire le champs des possibilités. Je parle du champs de possibilités, car il est facile de réduire considérablement la difficulté de programmer en offrant moins de "pistolets" pour se tirer dans le pied

---

La réponse à cette question est indubitablement dans la logique mathématique. Il s'agit clairement de laisser au programmeur le maximum d'expressivité, tout en l'empêchant de faire des bêtises. On voit rapidement que ceci n'est réalisable que si le compilateur a une bonne comprehension du texte source.

Maintenant, qu'est-ce que ça veut dire comprendre le texte source ? Je crois que ça veut dire être capable d'associer un sens formel à chaque terme. Il faut donc que l'analyse du texte aboutisse à un modèle sémantique. Seulement voilà, ce n'est pas toujours facile pour une raison de non algébricité. Je vais donner un exemple très simple. Quand on écrit dans un programme C:

Code:

---

1 2

x == y

---

(où x et y sont de type 'int'), on n'a pas de soucis, car le résultat (un 'int' à interpréter comme un booléen) est toujours bien défini quelles que soient les valeurs de x et y. Par contre, si on écrit:

Code:

---

1 2

x/y

---

on doit faire attention de ne pas diviser par 0. La division n'est pas une opération algébrique, simplement parce qu'il y a cette restriction sur son usage. (Les gens qui font de l'algèbre universelle, théorie introduite par Garrett Birkhoff vers 1935, savent que la structure de corps, dans laquelle on peut diviser, n'est pas algébrique, alors que celle d'anneau, dans laquelle toutes les opérations sont définies pour toutes les valeurs possibles, est algébrique).

La vérification du fait que y n'est pas nul et donc qu'on peut diviser par y, n'est pas faisable par algorithme, car elle peut dépendre de la preuve d'un théorème. Or la recherche de preuve de théorème est un problème semi-décidable, mais pas décidable. On peut chercher indéfiniement sans trouver de preuve.

Un compilateur ne peut donc pas faire une telle vérification. La division est donc typiquement l'un des pistolets dont tu as parlé. Alors, doit-on supprimer la division, sous prétexte qu'elle présente un danger ? La réponse n'est pas forcément non, ça dépend de ce à quoi le langage va être utile. Mais bien entendu, pour un langage de programmation généraliste, il faut une division. La division est un cas particulièrement difficile à résoudre, mais voici un autre exemple pour lequel la solution est plus facile à obtenir. Toujours en C, imaginons qu'on ait défini un type énuméré:

Code:

---

1 2	enum E { a, b, c };

---

Dans la suite du programme, on peut écrire (où e est supposé de type enum E):

Code:

---

1 2 3 4 5 6

switch (e) { case a: ... case b: ... }

---

c'est à dire en omettant le case c:, ce qui fait que le switch n'est pas bien défini pour toutes les valeurs possibles de e. Ici c'est tout à fait différent du cas de la division. L'opération switch a été rendue délibérément non algébrique, et je considère personnellement que c'est une erreur de design. Il suffirait d'imposer que le switch doive traiter tous les cas et une seule fois chaque cas, pour que le switch ne soit plus un pistolet, tout en gardant toute son expressivité.

Il est clair que C, C++, Pascal, Java, JavaScript, PHP ... sont pleins de pistolets. Il en va de même de CAML, Lisp, Haskell,... et des autres langages fonctionnels, avec juste un peu moins de pistolets. La notion d'exception est un remède de fortune, car il faut attendre que le mal soit fait pour que l'exception soit levée. Dans un langage sans aucun pistolet, il est clair qu'il ne peut pas y avoir d'exception.

Un tel langage sans aucun pistolet est-il possible, avec une expressivité au moins aussi grande que C, C++, Java, Lisp ou CAML ? La réponse est oui, mais à la condition que le langage contienne ce qu'il faut pour écrire les énoncés mathématiques (en toute généralité, y compris les énoncés universellement et existentiellement quantifiés), et ce qu'il faut pour écrire des preuves mathématiques. S'il en est ainsi, on peut éviter la division par 0 statiquement, c'est à dire au moment de la compilation. Il suffit d'imposer au source de contenir la preuve que le diviseur ne peut pas être nul.

De tels langages existent: HOL, LEGO, B (pas le prédécesseur du C, mais le langage créé par J-R Abrial), nuprl, COQ (INRIA), PVS, etc... Pourquoi ces langages ne sont-ils pas plus utilisés ? Je crois qu'il y a deux raisons principales. La première est qu'ils ont en général une syntaxe et une interface affreusement difficile à utiliser. Un coup d'oeil sur un source en COQ suffit à te dégoûter à tout jamais. Ils ne sont pas naturels, même pour un mathématicien. La deuxième est de nature socio-culturelle. Les mathématiques sont mal enseignées, elles découragent beaucoup de jeunes, et parmi eux beaucoup de futurs développeurs. Je suis persuadé que si on était capable de surmonter ces deux problèmes, les informaticiens ne se tireraient plus de balle dans le pied. Toutefois, le problème de ces langages à preuve n'est pas seulement leur syntaxe ou leur interface. Ils modélisent souvent des mathématiques exotiques. Et ça c'est un problème profond de logique mathématique. Pour moi la seule solution valable est la théorie des topos, mais aujoud'hui aucun langage (à ma connaissance) n'est fondé dessus.

Je suis d'un niveau terminale S en maths, et encore, j'ai oublié beaucoup de choses, et je suis d'accord avec toi sur le fait qu'un informaticien devrait se reconcilier avec les mathématiques pour faire des algorithmes et des programmes toujours plus performants.

Maintenant, il y a aussi quand même des choses qui me trainent dans la tête : prouver constamment les choses admises, n'est-ce pas de la redondance ? J'ai l'impression que quand quelque chose est admis, il suffirait plutôt juste de tester le cas qui ne va pas, et envoyer une erreur. Un peu à la façon d'une base de données, qui recenserait tous les cas possibles, et ceux qui ne le sont pas, sans chercher à savoir ce que la requête veut dire.

Par exemple, voila comment je vois la chose :

On entre x/y dans une ligne de code. Sachant que j'aime beaucoup l'approche Objet ( car je la trouve pratique pour pleins de choses ), dans mon esprit, le fait de faire cette ligne de code dans un bloc ( par exemple une méthode ), implique qu'un attribut de l'objet y soit positionner à true pour ce bloc, par exemple :

Code:

---

1 2 3 4 5

/* ceci serait effectué lors de la compilation, pour le bloc concerné */ y.setIsZeroAllowed(false); /* le bloc étant aussi un objet dans ma vision des choses, il faudrait aussi rajouter */ thisbloc.addTestIfZero(y);

---

Ensuite, lors de chaque attribution de valeur au runtime pour y, il y aurait le test supplémentaire en début de bloc qui serait bloquant en cas de valeur 0, et donc une erreur serait envoyé, sans que la division ait eut lieu. C'est la façon que je trouve la plus logique d'éviter le cas qui pose problème, ou bien peut-être que je perd de vue des milliers de paramètres, il ne faut pas m'en vouloir, je n'ai jamais conçu de compilateur :wink:

Par contre il est vrai que le compilateur a donc beaucoup de travail, et pour simplifier ce travail, il faut avoir une syntaxe très rigoureuse, par exemple au lieu d'écrire :

Code:

---

x/y

---

on pourrait écrire :

Code:

---

Math.divide(x, y);

---

Je vois bien les problèmes qui se posent par la suite..
Par exemple :

Code:

---

Math.divide(x, (ici une expression complexe) );

---

Là ça se corse, mais si chaque expression ( même simple, si elle ne contient qu'une variable ) était un objet, j'attribuerais l'attribut isZeroAllowed(false) à l'expression entière, qui elle se chargerait de répercuter au niveau de son propre bloc evaluate()..

Pas taper si je dis des bêtises :wink:

Citation:

---

Envoyé par KiLVaiDeN

Pas taper si je dis des bêtises

---

Il n'est pas question que je tape, je suis trop heureux d'avoir des interlocuteurs. Je crois que tout le monde peut s'exprimer librement sur ce fil, et si des "bêtises" sont dites au sens mathématique, je le ferai remarquer bien sûr, mais j'espère être capable de le faire sans blesser personne.

Ce que tu proposes s'apparente à la notion de test, pas de preuve. Car c'est seulement à l'exécution qu'on va savoir que y est nul, pas à la compilation. Ce n'est pas le même genre de prévention. Je fais une comparaison extrème (et un peu caricaturale, j'en conviens) avec l'automobile. Est-ce que le constructeur doit se préoccuper de faire des freins qui ne lacheront pas, ou est-ce qu'il peut se contenter de donner un numéro de téléphone auquel lancer une exception après que les freins auront laché ? C'est là toute la différence.

Je ne vois pas en quoi Math.divide(x,y) est plus précis que x/y. La division a seulement un nom différent. C'est tout. Evidemment, si le symbole / est surchargé, le compilateur doit être capable de résoudre l'ambigüité, mais ça ne pose pas de problème, c'est une technique connue.

Le problème pour 'y', ne vient pas de la complexité syntaxique de l'expression, mais de la façon dont le compilateur peut l'évaluer. Si c'est une expression compliquée, mais si le compilateur peut calculer qu'elle vaut (disons) toujours 2, il n'y a pas de problème. Ceci vaudra pour la preuve que 'y' ne peut pas être nul. Malheureusement, c'est une situation idéale et rare.

Ta dernière proposition d'attacher l'attribut isZeroAllowed(false) à l'objet 'y' reste aussi du domaine du test, car encore une fois le fait que 'y' soit nul ne sera connu qu'à l'exécution.

Je crois (je devrais dire 'je sais') que le seul moyen de faire passer la décision de la nullité de 'y' du moment de l'exécution au moment de la compilation est de prouver. On n'y coupera pas.

Tu as bien fait de faire ces remarques, car je crois que cette discussion va aider les lecteurs de ce fil à faire la différence entre test et preuve.