Discussion :

[Luc Orient]

Faut voir...
Ce n'est faux que si sa phrase signifie "il n'existe pas de ..." mais elle est incontestable, sauf par quelqu'un qui connaît son entreprise, si elle signifie "nous ne possédons pas de ...".
Je t'accorde qu'il faut probablement comprendre le premier sens mais... qui sait ?

... c) Relis mon post et tu comprendras que nous n'avons pas de débogueur en gros système. Si tu ne me crois pas renseigne toi. Tu verras !

Voilà ... je me suis renseigné et j'ai vu ...

[gorgonite]

C'est assez triste de voir un tel mépris pour le monde académique :-\ Tu suggères donc de rejeter tout ce qui vient de ce monde, sous prétexte que ce n'est forcément que pompeux ? Ce n'est pas un peu réducteur tu penses ? Et peut être que ce n'est pas parce qu'une méthode ne garantie pas 100% de sécurité qu'elle est forcément à jeter, non ? Et à quel point es-tu au fait de ces méthodes ? De coq à frama-C, en passant par la méthode B, lesquelles as-tu regardé ?

heureusement que tous les industriels ne sont pas comme cela... aussi bien des grands comptes que des petites PME sont au courant (ou s'informent dans la mesure de leurs moyens) des innovations théoriques et pratiques faites dans les labos de recherche... et les mettent en oeuvre dans leurs produits (que ce soit un sous-ensemble bien choisi/maitrisé en interne, des thèses CIFRE, des postes de docteur-ingénieurs, etc)

clairement après si l'on reproche au monde académique l'impossibilité d'appliquer comme une boîte noire un algo pour exhiber n'importe quel bug sur n'importe quel langage... ben allez engueuler Mr. Gödel pour l'indécidabilité (ou Mrs Turing et Rice pour les problèmes d'arrêt ^^)

[super_bus]

Faut voir...
Ce n'est faux que si sa phrase signifie "il n'existe pas de ..." mais elle est incontestable, sauf par quelqu'un qui connaît son entreprise, si elle signifie "nous ne possédons pas de ...".
Je t'accorde qu'il faut probablement comprendre le premier sens mais... qui sait ?

Voilà ... je me suis renseigné et j'ai vu ...

Je parlais de ce qui existe dans les entreprises. Ou si tu préfères : dans notre entreprise nous ne possédons pas de débogueur. Ou si tu préfère encore, nous n'avons pas à notre disposition un débogueur dans notre entreprise. Et donc, je te mettais au défit de te renseigner auprès de quelqu'un qui travaille en gros système pour lui demander s'il connaissait un débogueur dans SON ENTREPRISE et s'il avait l'habitude de l'utiliser. Je ne parlais pas de l'existence d'un débogueur dont on trouve les renseignement sur INTERNET. Je fais mon mea culpa. Je n'ai pas été assez précis dans mes affirmations.

Et puis, croix-tu qu'une entreprise va investir dans un utilitaire qui ne sera presque jamais utilisé ? Les débogueurs ne font pas parties de la politique des grands chantiers dans les entreprises où nous utilisons du gros système.

Et même s'il en existait un, je n'ai jamais été au courant de son existence. Ni mes collègues de boulots car j'ai posé la question !

[Luc Orient]

... Et donc, je te mettais au défit de te renseigner auprès de quelqu'un qui travaille en gros système pour lui demander s'il connaissait un débogueur dans SON ENTREPRISE et s'il avait l'habitude de l'utiliser. Je ne parlais pas de l'existence d'un débogueur dont on trouve les renseignement sur INTERNET. Je fais mon mea culpa. Je n'ai pas été assez précis dans mes affirmations.

Je travaille dans une entreprise avec des ordinateurs Mainframe IBM et Xpediter est utilisé sur notre site de développement ...

CQFD.

[super_bus]

Merci LUC ORIENT, je ne savais pas cela pouvait exister en entreprise ! Encore Merci de me l'avoir confirmer. A vrai dire, je n'ai jamais creuser la question, car cela ne m'a jamais intéresser.

N'empêche que mon propos reste le même : on peut très bien s'en passer ! ! !

Et pas uniquement sur le gros système mais dans tout les cas. Je n'ai pas fait que du COBOL, mais aussi du C (sur mini et micro), C++ (sur micro), pour les langages les plus récent, prolog, lisp, ada, et d'autres plus anciens comme PL1, Fortran, basic ...

Non, je n'en ai jamais eu besoin. Sauf en assembleur, mais là c'est un autre cas de figure (Vidage mémoire = DUMP).

[B.AF]

C'est assez triste de voir un tel mépris pour le monde académique :-\ Tu suggères donc de rejeter tout ce qui vient de ce monde, sous prétexte que ce n'est forcément que pompeux ? Ce n'est pas un peu réducteur tu penses ? Et peut être que ce n'est pas parce qu'une méthode ne garantie pas 100% de sécurité qu'elle est forcément à jeter, non ? Et à quel point es-tu au fait de ces méthodes ? De coq à frama-C, en passant par la méthode B, lesquelles as-tu regardé ?

Quand on te lit, effectivement, tu es tellement méprisant de la réalité que vivent les autres dans leur quotidien de développeur - que tu taxes quasiment d'incompétence - que ce n'est pas surprenant qu'une fois de plus tu n'as pas compris.

Je ne méprise pas le monde académique, en revanche les donneurs de leçons théoriques oui.

D'ailleurs ta réaction prouve qu'au dessus du sujet, c'est surtout la propre importance et le propre crédit que tu veux t'accorder qui t'importe.

Et que tu ferais mieux d'arrêter l'interprétation et la présomption, faire ton/tes applis, les vendre, monter une boite, en mesurer toute la dimension économique, et y appliquer tes leçons de production en maintenant une grille de salaire et une rentabilité ainsi que la satisfaction du client. Et essayer là dedans de dégager les moyens nécessaires à faire de la recherche.
Ce jour là, tu mesureras peut être que les conseilleurs ne sont jamais les payeurs, ni les responsables.

Et homme de science que je suis, évite les raccourcis, couper les cheveux et expliquer aux autres qu'ils sont idiots sous prétexte que leur quotidien ne leur permet pas d'exploiter des théories académiques, ca n'a rien à voir avec de la recherche. C'est de la vanité.

Quand à l'explication que j'ai donné que tu t'es joyeusement permise de généraliser est la démonstration brillante effectuée par un chercheur brillant(Nassim Taleb) de son ouvrage "The Black Swan: The Impact of the Highly Improbable".
Cette démonstration a largement servi à démontrer l'inefficience de la loi normale à distribuer correctement les risques.
Donc le poujadisme, sans moi et surtout pas avec le détournement de mes mots.

Voilà, tu peux étaler tranquillement tout ce que tu as appris sur les bancs de l'école et si tu as une méthodologie de test révolutionnaire qui me permet de garder un coût de développement constant versus une qualité totale grace à un simple debugger, laisses moi un mp, je suis prêt à faire un chéque pour la r&d dans ce domaine.

[TropMDR]

Quand on te lit, effectivement, tu es tellement méprisant de la réalité que vivent les autres dans leur quotidien de développeur - que tu taxes quasiment d'incompétence - que ce n'est pas surprenant qu'une fois de plus tu n'as pas compris.

Ces méthodes permettent effectivement d'éviter très largement de recourir à un débogueur, puisqu'elles assurent statiquement (sans avoir à lancer le programme) qu'on s'est débarrassé de toute une classe de bugs (par exemple dépassement de bornes dans un tableau), voir même plus précisément dans certain cas, que le programme satisfait ses spécification à 100%. Donc elles permettent aussi de trouver des bugs dans les programmes *avant* de les exécuter.

Mais, comme le dit wikipedia,

Cependant, elles sont généralement coûteuses en ressources (humaines et matérielles) et actuellement réservées aux logiciels les plus critiques.

Il est donc effectivement peu probable qu'on les retrouve d'ici peu dans l'informatique de gestion. Mais ce n'est pas une séparation intrinsèque.

Et moi je prouve mes programmes en Coq. J'ai zéro bug. Mathématiquement prouvé. En revanche, je ne viens pas expliquer aux gens qui ont des bugs que ce sont des débiles. Parce que je n'écris pas de serveur web répondant à des milliers de connexion par secondes, on des navigateurs réagissant au clic en moins d'un quart de seconde.

[super_bus]

Je continue d'halluciner ! ! !

Je croyais que c'était un forum de professionnels ? Et donc je pensais avoir affaire à des gens ayant une certaine ouverture d'esprit. Non, il n'y a que la critique et rien que ca. Essayez tout de même d'évoluer un tout petit peu.

Certains ont comme seules connaissances WIKIPEDIA. Ce qui prouve que le niveau vol très bas.

Bon je n'insiste plus. Je vois que cela ne sert à rien de discuter.

BYE BYE.

[TropMDR]

Je croyais que c'était un forum de professionnels ? Et donc je pensais avoir affaire à des gens ayant une certaine ouverture d'esprit. Non, il n'y a que la critique et rien que ca. Essayez tout de même d'évoluer un tout petit peu.

Non mais sérieusement, il faut arrêter mon bon monsieur ! Au delà d'un certain niveau, toute crédibilité disparait hein. Par exemple, quand on est celui qui dit

Un débogueur est valable pour les débutants, pour se former à la compréhension du langage. Il vous fait perdre du temps mais cela est nécessaire pour votre formation. Par la suite, le débogueur, ce sera vous. Mais si après 10 ans d'expérience professionnelle, vous avez recourt à un débogueur, alors je vous le dit "changé de boulot". Car après tout ce temps, vous ne connaissez toujours pas ni le langage, ni des méthodologies de développement et donc vous êtes totalement incompétent.

c'est quand même pas hyper crédible de venir harceler les gens sur l'ouverture d'esprit.

Certains ont comme seules connaissances WIKIPEDIA. Ce qui prouve que le niveau vol très bas.

Après, d'aucun pourrait penser qu'entre la définition wikipedia et

Les méthodes formelles appartiennent à la logique formelle et ce traite dans des problèmes d'intelligence artificielle. Tu trouves ca dans les chapitres consacrés au calcul des prédicats. Par simplification, il s'agit de la résolution par réfutation de la décomposition de problème mathématique.

il est peut être plus raisonnable de se tourner vers la première !

Et puis pour finir, à 15h40, vous aviez voté pour 781 messages. Maintenant, à minuit 24, vous avez voté pour 1475 messages. Vous ne pensez pas qu'à 51 ans, c'est un petit peu dommage de passer des heures à voter au hasard pour gagner des points (et si vous avez écrit un script pour le faire à votre place, c'est tout aussi malheureux) ?

[B.AF]

Et toi tu ne te dis pas qu'à ton age s'acharner de façon aussi thérapeutique sur une personne ne fait pas de toi le meilleur juge de la nature humaine ?

'On est d'ordinaire plus médisant par vanité que par malice.' - La Rochefoucauld
En tous les cas, magnifique démonstration !

[zaventem]

N'empêche que mon propos reste le même : on peut très bien s'en passer ! ! !

On peut également enfoncer un clou avec une clé à molette mais quand j'ai un marteau dans ma boite à outils, je préfère l'employer

[chaplin]

Et moi je prouve mes programmes en Coq. J'ai zéro bug. Mathématiquement prouvé.

Peut-on voir un exemple, ça m'intéresse, après chacun fait ce qu'il veut, avec ou sans débogueur.

[souviron34]

C'est assez triste de voir un tel mépris pour le monde académique :-\ Tu suggères donc de rejeter tout ce qui vient de ce monde, sous prétexte que ce n'est forcément que pompeux ? Ce n'est pas un peu réducteur tu penses ? Et peut être que ce n'est pas parce qu'une méthode ne garantie pas 100% de sécurité qu'elle est forcément à jeter, non ? Et à quel point es-tu au fait de ces méthodes ? De coq à frama-C, en passant par la méthode B, lesquelles as-tu regardé ?

tu m'as l'air assez adepte du Noir et Blanc.... (et ce n'est pas la première fois que je le note)..

Il serait grand temps de mûrir un peu et d'accepter que le monde, et en particulier le développement informatique, est plutôt un ensemble de nuances de gris...



Que ce soit B.A.F. ou moi ou d'autres, personne ne rejette "tout ce qui vient du monde académique"...

Nous rejetoins des théories qui disent que "ça c'est LA méthode", "ça c'est LE processus", "ça c'est LE langage", "ça c'est LE paradigme", "le zero bug C'EST possible, "ce qui est prouvé mathématiquemnt est correct", etc etc...


Il n'est pas du tout curieux que les personnes qui soutiennent ça aient un tantinet d'expérience...

Le fait de se cogner le nez à la réalité, industrielle et/ou de recherche, sur des choses différentes et sur une (assez) longue durée relativise simplement beaucoup les affirmations....




Ce qui vient de la recherche, qu'elle soit académique pure ou de R&D, est, dans beaucoup de cas, utile...

ça ne contredit en rien le fait qu'elle ne soit pas parfaite, et qu'en particulier les affirmations qu'elle produise ou sur lesquelles elle se base soient (partiellement) fausses...

C'est tout ce qu'on dit...

Et effectivement, il est assez triste de ne pas arriver à comprendre la différence entre la théorie et la pratique, et même entre la pratique dans un environnement cadré, contrôlé, à la limite du "mono-thread", avec la pratique réelle dans le monde réel, où rien n'est pardait, ni les specs, ni la doc, ni la plateforme, ni le processus de développement, ni la mise en oeuvre, ni la maintenance, ni la direction, ni......



Et je préfère de très loin avoir affaire en développeent à un auto-didacte qu'à un académique pétri de certitudes...

La science est basée sur le doute... Il semble que désormais on ne vous enseigne plus le doute comme base fondamentale.. C'est bien dommage...



La signature d'un membre éminent de ce forum est limpide :

"Algorithme : méthode complexe de résolution d'un problème simple"

[TropMDR]

Peut-on voir un exemple, ça m'intéresse, après chacun fait ce qu'il veut, avec ou sans débogueur.

Si tu veux voir des exemples de taille raisonnable, tu peux regarder la formalisation des arbres rouges noirs par Jean-Christophe Filliâtre:
http://www.lri.fr/~filliatr/fsets/

En plus gros et moins simple à suivre, tu as toute la librairie standard de coq sur les ensembles et les maps fonctionnels, dont par exemple les AVL "à la caml"
http://coq.inria.fr/stdlib/Coq.MSets.MSetAVL.html#
La partie intéressante commence là
http://coq.inria.fr/stdlib/Coq.MSets...VL.html#lab512

Tu as par exemple un prédicat d'appartenance InT qui te dit ce que veut dire "un élément est dans mon ensemble", puis des preuves des différentes oppérations, par exemple l'insertion

Code :

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

1
2
Lemma add_spec : forall s x y `{Ok s},
 InT y (add x s) <-> X.eq y x \/ InT y s.

Il faut lire ce lemme comme disant "j'ai une preuve que pour tout ensemble s et élément x et y, si y appartient à add x s (c'est à dire à l'ajout de x dans s), alors soit y est égal à x, soit y était déjà dans s, et la réciproque est vraie". C'est exactement la spécification que l'on attend pour l'ajout d'un élément à une collection.

On a donc une preuve formelle (vérifiée par coq, et coq est trèèèèèèès pointilleux sur la vérification des preuves), que la librairies des FSets se comporte parfaitement. Il n'y aura donc jamais à utiliser un débogueur à cet endroit. (elle est complètement spécifié, même pour le maintient de l'équilibrage des arbres)

Ca c'est pour les librairies. Maintenant, il y a des projets nettement plus gros. Par exemple, il y a CompCert, un compilo C écrit en Coq, avec une preuve de préservation sémantique. Cette preuve dit "si j'arrive à compiler un programme du C vers l'assembleur, alors on a l'assurance que le programme final se comporte exactement comme le programme initial".

Alors pour ne pas faire complètement hors sujet, est ce que cela signifie forcément que toute méthode de débug est définitivement inutile. Tristement, la réponse est non :-\ Juste qu'il n'y aura jamais (dans le cas de compcert) de programme produit avec une sémantique différente.

En revanche, il se peut parfaitement qu'il échoue à compiler un programme alors qu'il aurait du (le compilo est une fonction partielle).

Mais aussi pour les optimisations par exemple, ce qui est spécifié, c'est qu'elles doivent produire un code qui "fait la même chose". Il n'est pas spécifié qu'elles doivent optimiser. Donc on peut très bien écrire une grosse optimisation, qui au final ne change en gros pas le code, et ce pour des raisons complexe à détecter.

Donc dans ces cas là, ou la spécification est finalement partielle (on spécifie que le compilateur ne doit pas pouvoir changer la sémantique, on ne spécifie pas qu'il doit améliorer les performances), il peut en fait rester utile de mettre les mains dans le cambouis pour trouver où s'est glissé l'erreur.

[chaplin]

C'est si difficile de se dire qu'il existe des gens avec une façon de penser différente de la notre, qu'un outil adapté à l'un ne l'est pas forcément à l'autre ? Et on pourrait pas élever le débat un peu plus haut que "avec mon éditeur à moi, j'appuie sur deux touches seulement pou faire ça, alors que toi c'est trois, t'es trop nul mec" ?

Surtout qu'en informatique, il y a quand même pléthore de question technique où l'on peut avoir un véritable débat (parfois même constructif , avec de vrais arguments techniques. Venez, on se concentre un peu là dessus ?

Peut-on continuer dans ce sens, SVP ?

Edit: A une minute près je viens de voir le post, merci TropMDR.
Quand on décide d'écouter un intervenant, c'est le respecter.

[Guardian]

Et même s'il en existait un, je n'ai jamais été au courant de son existence. Ni mes collègues de boulots car j'ai posé la question !

Je continue d'halluciner ! ! !

Je croyais que c'était un forum de professionnels ? Et donc je pensais avoir affaire à des gens ayant une certaine ouverture d'esprit. Non, il n'y a que la critique et rien que ca. Essayez tout de même d'évoluer un tout petit peu.

Certains ont comme seules connaissances WIKIPEDIA. Ce qui prouve que le niveau vol très bas.

Bon je n'insiste plus. Je vois que cela ne sert à rien de discuter.

BYE BYE.

Et c'est lui qui allucine, j'le crois pas
C'est l'hôpital qui se fout de la charité !

[TropMDR]

Il semble que mon point de vue se soit noyé dans les différents messages et ait été interprété plutôt à mon désavantage. Je vais donc essayer de le résumer :

J'utilise des méthodes formelles (en l'occurrence Coq) pour prouver mes programmes. Ces méthodes apportent une certitude proche de 100% que les programmes n'ont pas de bug. Ce que j'entends par là: déjà, ils n'ont pas de dépassement de tampon, pas d'overflow, pas de déréférencement de pointeurs nuls, pas de double free, etc. Là c'est plus le langage qui l'assure que vraiment la preuve. Ensuite, on sait qu'ils satisfont leur spécification (j'insiste sur le fait qu'on ne prouve pas un algorithme qu'on implémente ensuite. On prouve directement le programme).

Néanmoins, il reste toujours un risque d'erreur : une spécification erronée ou incomplète. Dans l'exemple que je donnais plus haut sur les optimisations, c'est une spécification incomplète (on demande à l'optimisation de ne pas altérer la sémantique du programme, mais on ne s'assure pas qu'elle optimise effectivement). Mais les spécifications sont écrite en langage mathématique, sans ambiguité, et sont (du moins dans l'idéeal) nettement plus concise que le programme les implémentant (voir la spécification de add sur un AVL, comparée à son implémentation).
Il est enfin possible que l'outil lui même soit bogué, mais là, la probabilité est *vraiment* faible (la TCB (trusted computing base) est vraiment réduite)

Donc non, on n'est pas à 0% de chance d'avoir un bug, on est tout de même à beaucoup, beaucoup, beaucoup moins qu'avec des programmes non prouvés.

Néanmoins, ces méthodes sont extrêmement lourde à mettre en place. Il est par exemple très compliqué de prouver un programme impératif (surtout un programme C...). Rien que spécifier un algo de tri (je ne parle même pas de le prouver), est une opération complexe (je parie mon poids en choucroute que la moitié des programmeurs sont incapable de donner une spécification correcte du premier coup). Alors prouver un quick-sort en place, boarf. Et en plus, ce n'est qu'une sous sous sous partie d'un vrai programme. Il y a donc encore un travail de titan à faire avant que ces méthodes soient accessibles au plus grand nombre.

D'ici là, je suis comme tout le monde, je veux continuer à voir l'informatique progresser et de nouveaux programmes arriver. Et dans ces programmes, il y aura toujours des bugs (puisqu'on n'a pas encore trouvé de programmeurs infaillible. La plupart reste humains...). Et donc oui, il faudra des outils pour aider à débuguer ! Bien sûr, le "good ol'" printf fonctionne dans plein de cas. Il me parait quand même bizarre de rejeter pour autant des outils un brin plus "moderne", comme un débogueur, surtout qu'ils ont quand même fait des progrès, principalement en terme d'interface !

Et puis il y a aussi une percolation progressive des différentes méthodes. Par exemple, le compilo C d'Apple incorpore un analyseur statique pour aider à trouver des causes classique d'erreurs. Tous ces outils permettent de limiter les cas où un déboguer est utile. Mais on est encore bien loin de le rendre inutile dans tous les cas.

[Guardian]

Il me parait quand même bizarre de rejeter pour autant des outils un brin plus "moderne", comme un débogueur, surtout qu'ils ont quand même fait des progrès, principalement en terme d'interface !

C'eest effectivement le principal problème mis en évidence par cette discussion : le rejet des méthodes.
Il semble pourtant évident que plus on a d'outils, meilleures sont les chances d'avoir un bon résultat. J'utilise principalement un EDI avec débogeur intégré et donc, forcément, j'utilise celui-ci. Cela ne m'empêche pas d'utiliser d'autres méthodes selon le problème à résoudre et ce que j'estime le plus efficace pour le résoudre.
Que chacun ait ses préférences est normal. Que d'aucun dénigrent les méthodes des autres me semble absurde.

[el_slapper]

(.../...)J'utilise des méthodes formelles (en l'occurrence Coq) pour prouver mes programmes. Ces méthodes apportent une certitude proche de 100% que les programmes n'ont pas de bug. Ce que j'entends par là: déjà, ils n'ont pas de dépassement de tampon, pas d'overflow, pas de déréférencement de pointeurs nuls, pas de double free, etc. Là c'est plus le langage qui l'assure que vraiment la preuve. Ensuite, on sait qu'ils satisfont leur spécification (j'insiste sur le fait qu'on ne prouve pas un algorithme qu'on implémente ensuite. On prouve directement le programme).

Néanmoins, il reste toujours un risque d'erreur : une spécification erronée ou incomplète. Dans l'exemple que je donnais plus haut sur les optimisations, c'est une spécification incomplète (on demande à l'optimisation de ne pas altérer la sémantique du programme, mais on ne s'assure pas qu'elle optimise effectivement). Mais les spécifications sont écrite en langage mathématique, sans ambiguité, et sont (du moins dans l'idéeal) nettement plus concise que le programme les implémentant (voir la spécification de add sur un AVL, comparée à son implémentation).
Il est enfin possible que l'outil lui même soit bogué, mais là, la probabilité est *vraiment* faible (la TCB (trusted computing base) est vraiment réduite)

Donc non, on n'est pas à 0% de chance d'avoir un bug, on est tout de même à beaucoup, beaucoup, beaucoup moins qu'avec des programmes non prouvés.

Néanmoins, ces méthodes sont extrêmement lourde à mettre en place. Il est par exemple très compliqué de prouver un programme impératif (surtout un programme C...). Rien que spécifier un algo de tri (je ne parle même pas de le prouver), est une opération complexe (je parie mon poids en choucroute que la moitié des programmeurs sont incapable de donner une spécification correcte du premier coup). Alors prouver un quick-sort en place, boarf. Et en plus, ce n'est qu'une sous sous sous partie d'un vrai programme. Il y a donc encore un travail de titan à faire avant que ces méthodes soient accessibles au plus grand nombre.(.../...)

En d'autres termes, ce sont des méthodes hors de portée du commun des mortels. Il est bien possible qu'elles rendent le débugging obsolète. Mais le prix me parait prohibitif, en termes de main-d'oeuvre, de délais, sans même parler de l'outillage et de la formation.

Sur le sujet de XPEDiter sous cobol, j'ai vu(chez un autre client), j'ai abandonné. Alors que j'utilise régulièrement le débugger de VBA/EXCEL, XPED est lourdingue, et ne propose pas vraiment de valeur ajoutée par rapport à un display(printf pour les non-cobolistes) pour du batch. Et il avait tendance à avoir des comportements intrusifs en transactionnel, suffisement pour fausser le débogage..... Peut-être à cause d'une mauvaise installation. En tous cas, je passe mon chemin - alors même qu'à l'occasion, un débuggeur facile d'utilisation pourrait me rendre service.

Enfin, sur le sujet général des méthodes, la plupart des méthodes que j'ai vu appliquées en servaient qu'à masquer l'incompétence des intervenants. Or, aucune méthode ne permet de pallier l'incompétence. Evidemment, appliquées par des gens au niveau, et dans un périmètre approprié, les méthodes marchent. Mais certains s'en méfien,t autant que moi, c'est qu'il a sans doute, lui aussi, trop vu de blabla méthodologique noyer le coeur du projet. Imposée à tort et à travers(ce qui est vrai le plus souvent), une méthode fait plus de mal que de bien. Donc, quand arrive une nouvelle méfiance, les "anciens" ont plus que tendance à s'en méfier. Non pas qu'elle soit mauvaise en soit(c'est rarement le cas), simplement qu'elle arrive comme un cheveu sur la soupe.

[TropMDR]

En d'autres termes, ce sont des méthodes hors de portée du commun des mortels. Il est bien possible qu'elles rendent le débugging obsolète. Mais le prix me parait prohibitif, en termes de main-d'oeuvre, de délais, sans même parler de l'outillage et de la formation.

En gros il y a de ça, oui. Mais bon, des dizaines de milliers de personnes comptent chaque jours sur un outil développé avec de telles méthodes pour aller au boulot: toute l'informatique de la ligne 14 a été développé en utilisant la méthode B.

En gros, ça coute très cher d'appliquer de telles méthodes, il faut donc être dans un domaine où il y a un retour sur investissement, par exemple en gagnant une forte assurance sur le fait qu'on ne tuera personne ! C'est aussi utilisé par exemple pour les carte à puce, pour s'assurer que la machine virtuelle java embarquée se comporte correctement.

Et peut être qu'à moyen terme on peut espérer voir de plus en plus de programme annoté par des spécifications en JML ou ACSL par exemple, ce qui aide à la fois pour la documentation (c'est beaucoup moins ambigüe qu'une spécification en anglais !), les tests (pour un framework de test, les spécifications sont des assertions qui peuvent être mise à l'épreuve), voir même progressivement pour la preuve (on pourrait imaginer que la fonction apparait en vert dans l'IDE si l'outil a réussi à prouver la spécification et en rouge s'il a trouvé un contre exemple).

Il est permis de rêver