IdentifiantMot de passe
Loading...
Mot de passe oublié ?Je m'inscris ! (gratuit)
Navigation

Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter

Débats sur le développement - Le Best Of Discussion :

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


Sujet :

Débats sur le développement - Le Best Of

  1. #1
    Membre averti
    Profil pro
    Inscrit en
    Août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 73
    Localisation : France

    Informations forums :
    Inscription : Août 2005
    Messages : 417
    Points : 372
    Points
    372
    Par défaut [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.

  2. #2
    Modérateur
    Avatar de gangsoleil
    Homme Profil pro
    Manager / Cyber Sécurité
    Inscrit en
    Mai 2004
    Messages
    10 148
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Haute Savoie (Rhône Alpes)

    Informations professionnelles :
    Activité : Manager / Cyber Sécurité

    Informations forums :
    Inscription : Mai 2004
    Messages : 10 148
    Points : 28 113
    Points
    28 113
    Par défaut
    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
    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 ?
    "La route est longue, mais le chemin est libre" -- https://framasoft.org/
    Les règles du forum

  3. #3
    Membre régulier
    Profil pro
    Inscrit en
    Décembre 2002
    Messages
    89
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Décembre 2002
    Messages : 89
    Points : 114
    Points
    114
    Par défaut
    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.

  4. #4
    Membre averti
    Profil pro
    Inscrit en
    Août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 73
    Localisation : France

    Informations forums :
    Inscription : Août 2005
    Messages : 417
    Points : 372
    Points
    372
    Par défaut
    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
    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.

  5. #5
    Membre averti
    Profil pro
    Inscrit en
    Août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 73
    Localisation : France

    Informations forums :
    Inscription : Août 2005
    Messages : 417
    Points : 372
    Points
    372
    Par défaut
    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.

  6. #6
    Rédacteur

    Avatar de Matthieu Brucher
    Profil pro
    Développeur HPC
    Inscrit en
    Juillet 2005
    Messages
    9 810
    Détails du profil
    Informations personnelles :
    Âge : 42
    Localisation : France, Pyrénées Atlantiques (Aquitaine)

    Informations professionnelles :
    Activité : Développeur HPC
    Secteur : Industrie

    Informations forums :
    Inscription : Juillet 2005
    Messages : 9 810
    Points : 20 970
    Points
    20 970
    Par défaut
    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.

  7. #7
    Membre averti
    Profil pro
    Inscrit en
    Août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 73
    Localisation : France

    Informations forums :
    Inscription : Août 2005
    Messages : 417
    Points : 372
    Points
    372
    Par défaut
    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 ?

  8. #8
    Rédacteur

    Avatar de Matthieu Brucher
    Profil pro
    Développeur HPC
    Inscrit en
    Juillet 2005
    Messages
    9 810
    Détails du profil
    Informations personnelles :
    Âge : 42
    Localisation : France, Pyrénées Atlantiques (Aquitaine)

    Informations professionnelles :
    Activité : Développeur HPC
    Secteur : Industrie

    Informations forums :
    Inscription : Juillet 2005
    Messages : 9 810
    Points : 20 970
    Points
    20 970
    Par défaut
    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 -.

  9. #9
    Modérateur
    Avatar de gangsoleil
    Homme Profil pro
    Manager / Cyber Sécurité
    Inscrit en
    Mai 2004
    Messages
    10 148
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Haute Savoie (Rhône Alpes)

    Informations professionnelles :
    Activité : Manager / Cyber Sécurité

    Informations forums :
    Inscription : Mai 2004
    Messages : 10 148
    Points : 28 113
    Points
    28 113
    Par défaut
    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 route est longue, mais le chemin est libre" -- https://framasoft.org/
    Les règles du forum

  10. #10
    Membre expert
    Avatar de 2Eurocents
    Profil pro
    Inscrit en
    Septembre 2004
    Messages
    2 177
    Détails du profil
    Informations personnelles :
    Âge : 54
    Localisation : France

    Informations forums :
    Inscription : Septembre 2004
    Messages : 2 177
    Points : 3 166
    Points
    3 166
    Par défaut
    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 ...
    La FAQ Perl est par ici
    : La fonction "Rechercher", on aurait dû la nommer "Retrouver" - essayez et vous verrez pourquoi !

  11. #11
    Membre averti
    Profil pro
    Inscrit en
    Août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 73
    Localisation : France

    Informations forums :
    Inscription : Août 2005
    Messages : 417
    Points : 372
    Points
    372
    Par défaut
    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) ?

  12. #12
    Membre expert
    Avatar de 2Eurocents
    Profil pro
    Inscrit en
    Septembre 2004
    Messages
    2 177
    Détails du profil
    Informations personnelles :
    Âge : 54
    Localisation : France

    Informations forums :
    Inscription : Septembre 2004
    Messages : 2 177
    Points : 3 166
    Points
    3 166
    Par défaut
    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é.
    La FAQ Perl est par ici
    : La fonction "Rechercher", on aurait dû la nommer "Retrouver" - essayez et vous verrez pourquoi !

  13. #13
    Membre averti
    Profil pro
    Inscrit en
    Août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 73
    Localisation : France

    Informations forums :
    Inscription : Août 2005
    Messages : 417
    Points : 372
    Points
    372
    Par défaut
    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:
    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.

  14. #14
    Membre averti
    Profil pro
    Inscrit en
    Août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 73
    Localisation : France

    Informations forums :
    Inscription : Août 2005
    Messages : 417
    Points : 372
    Points
    372
    Par défaut
    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.

  15. #15
    Membre expert Avatar de KiLVaiDeN
    Profil pro
    Inscrit en
    Octobre 2003
    Messages
    2 851
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Octobre 2003
    Messages : 2 851
    Points : 3 481
    Points
    3 481
    Par défaut
    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 :

    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.

    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.

    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.

    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 )

    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é..

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

    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

    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 ?
    K

  16. #16
    Membre averti
    Profil pro
    Inscrit en
    Août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 73
    Localisation : France

    Informations forums :
    Inscription : Août 2005
    Messages : 417
    Points : 372
    Points
    372
    Par défaut
    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.

    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.

    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.

    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.

    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.

  17. #17
    Membre expert Avatar de KiLVaiDeN
    Profil pro
    Inscrit en
    Octobre 2003
    Messages
    2 851
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Octobre 2003
    Messages : 2 851
    Points : 3 481
    Points
    3 481
    Par défaut
    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

    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 !
    K

  18. #18
    Membre averti
    Profil pro
    Inscrit en
    Août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 73
    Localisation : France

    Informations forums :
    Inscription : Août 2005
    Messages : 417
    Points : 372
    Points
    372
    Par défaut
    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:
    (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:
    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 : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    enum E { a, b, c };
    Dans la suite du programme, on peut écrire (où e est supposé de type enum E):
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    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.

  19. #19
    Membre expert Avatar de KiLVaiDeN
    Profil pro
    Inscrit en
    Octobre 2003
    Messages
    2 851
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Octobre 2003
    Messages : 2 851
    Points : 3 481
    Points
    3 481
    Par défaut
    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 : Sélectionner tout - Visualiser dans une fenêtre à part
    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

    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 :

    on pourrait écrire :

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    Math.divide(x, y);
    Je vois bien les problèmes qui se posent par la suite..
    Par exemple :

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    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
    K

  20. #20
    Membre averti
    Profil pro
    Inscrit en
    Août 2005
    Messages
    417
    Détails du profil
    Informations personnelles :
    Âge : 73
    Localisation : France

    Informations forums :
    Inscription : Août 2005
    Messages : 417
    Points : 372
    Points
    372
    Par défaut
    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.

Discussions similaires

  1. Faut-il simplifier la programmation et revoir ses fondements ? Un journaliste s'essaye au développement
    Par Idelways dans le forum Débats sur le développement - Le Best Of
    Réponses: 383
    Dernier message: 24/02/2013, 01h16
  2. Preuve de programme en C
    Par boozook dans le forum C
    Réponses: 10
    Dernier message: 06/06/2012, 10h31
  3. Conception : réalité ou utopie
    Par grunk dans le forum ALM
    Réponses: 3
    Dernier message: 24/03/2011, 22h13
  4. Algorithme polynomial et preuve de programme
    Par yaya125 dans le forum Algorithmes et structures de données
    Réponses: 1
    Dernier message: 28/02/2011, 19h12
  5. Réponses: 13
    Dernier message: 09/08/2006, 23h25

Partager

Partager
  • Envoyer la discussion sur Viadeo
  • Envoyer la discussion sur Twitter
  • Envoyer la discussion sur Google
  • Envoyer la discussion sur Facebook
  • Envoyer la discussion sur Digg
  • Envoyer la discussion sur Delicious
  • Envoyer la discussion sur MySpace
  • Envoyer la discussion sur Yahoo