Citation:
Envoyé par ArielD
Voilà ... je me suis renseigné et j'ai vu ...Citation:
Envoyé par super_bus
Version imprimable
Citation:
Envoyé par ArielD
Voilà ... je me suis renseigné et j'ai vu ...Citation:
Envoyé par super_bus
Citation:
Envoyé par TropMDR
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é :aie: (ou Mrs Turing et Rice pour les problèmes d'arrêt ^^)
Citation:
Envoyé par ArielD
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.Citation:
Envoyé par Luc Orient
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 !
Je travaille dans une entreprise avec des ordinateurs Mainframe IBM et Xpediter est utilisé sur notre site de développement ...Citation:
Envoyé par super_bus
CQFD.
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).
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.Citation:
Envoyé par TropMDR
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.
Citation:
Envoyé par B.AF
Citation:
Envoyé par TropMDR
Citation:
Envoyé par TropMDR
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.
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 ditCitation:
Envoyé par super_bus
c'est quand même pas hyper crédible de venir harceler les gens sur l'ouverture d'esprit.Citation:
Envoyé par super_bus
Après, d'aucun pourrait penser qu'entre la définition wikipedia etCitation:
Envoyé par super_bus
il est peut être plus raisonnable de se tourner vers la première !Citation:
Envoyé par super_bus
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) ?
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 !:roll:
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 ;)Citation:
Envoyé par super_bus
Peut-on voir un exemple, ça m'intéresse, après chacun fait ce qu'il veut, avec ou sans débogueur.Citation:
Envoyé par TropMDR
tu m'as l'air assez adepte du Noir et Blanc.... (et ce n'est pas la première fois que je le note)..Citation:
Envoyé par TropMDR
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"
Si tu veux voir des exemples de taille raisonnable, tu peux regarder la formalisation des arbres rouges noirs par Jean-Christophe Filliâtre:Citation:
Envoyé par chaplin
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
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.Code:
2Lemma add_spec : forall s x y `{Ok s}, InT y (add x s) <-> X.eq y x \/ InT y s.
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.
Peut-on continuer dans ce sens, SVP ?Citation:
Envoyé par TropMDR
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.
Citation:
Envoyé par super_bus
Et c'est lui qui allucine, j'le crois pas 8OCitation:
Envoyé par super_bus
C'est l'hôpital qui se fout de la charité ! :ptdr:
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.
C'eest effectivement le principal problème mis en évidence par cette discussion : le rejet des méthodes.Citation:
Envoyé par TropMDR
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.
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.Citation:
Envoyé par TropMDR
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.
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.Citation:
Envoyé par el_slapper
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 ;)