Journal La preuve de programme : où en est-on ?

Posté par (page perso) .
3
3
mar.
2009
Je suis en train (d'essayer) de lire la thèse de J-C Filliâtre http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz intitulée Preuve de programmes impératifs en théorie des types
L'objectif est simple : on pose des contrat pre et post sur un morceaux de code, on peut aussi poser des invariants au sein d'une boucle, et le logiciel ( http://why.lri.fr/index.fr.html ) qui est tiré de cette thèse :
  • Prouve la complétude et l'adéquation des contrats au code
  • Prouve que le code respecte les contrats

Plus fort que du test unitaire, de la preuve de contrat, c'est tout simplement impressionnant !*
Je ne vais pas décrire le principe ici, j'ai trop peur d'avoir mal compris.
En gros, le code impératif est traduit dans un code fonctionnel très propre et d'une sémantique très petite , la couverture et la complétude des contrats est ensuite vérifiée pour enfin générer une obligation de preuve qui peut être donnée à Coq (Logiciel d'assistance de preuve) ou un démonstrateur automatique comme Alt-ergo.
(En passant quelqu'un dans la salle saurait-il m'expliquer la différence entre assistant et démonstrateur automatique ?)

Ca faisait longtemps que je connaissais ce travail, mais je pensais bêtement que ça ne faisait que de la vérification de cohérence de contrats, je crois que je vais vite tester ça...
J'imagine que d'autres outils existent, mais je me demande s'ils ont une telle maturité..

Bref à quand des outils intégrés aux applications Java/J2EE ?
ie. la complétude des contrats à poser est-elle véritablement problématique dans une utilisation courante en informatique de gestion ?
La taille des programme à prouver est-elle limitée ?
Les informations de sorties sont-elles exploitables ?

Tout cela pour dire, que même si des outils comme Coq resteront incompréhensible pour le grand public, je pense que des outils comme caduceus ou Krakatoa (respectivement l'adaptation de why à C et Java) ont un grand avenir devant eux, il manque peut être des les packager, des les intégrer à des outils de développement industrialisé comme Maven, mais qu'ils pourraient avoir un impact énorme sur le développement logiciel en général.

* J'en avais discuté avec Pierre Weiss au SL 2006, et il était lui même très impressionné par ce travail (et par IsaacOs/Lisaac aussi ;-)
  • # Se passer des tests ...

    Posté par . Évalué à  5 .

    En même temps, si tu trouve un manager / décideur pressé qui est capable de comprendre quand on lui dis : « on n'a pas besoin de faire des tests, on a une démonstration rigoureuse à la place et c'est beaucoup mieux », alors justement je cherche du boulot en ce moment (crise + période d'essai = chômage).
    • [^] # Re: Se passer des tests ...

      Posté par (page perso) . Évalué à  3 .

      Prouver un programme ne dispense pas de le tester (souvenir de mon module de tests en M2 : Intel avait une preuve de correction pour l'instruction FDIV du Pentium 1...). Les tests seront toujours là pour ce que les preuves ne peuvent pas prévoir. Évidemment, il y a une énorme marge pour remplacer des tests par des preuves là où c'est approprié.
      • [^] # Re: Se passer des tests ...

        Posté par (page perso) . Évalué à  4 .

        La vérification évite bien de devoir tester.

        Lors de tests, on teste qu'une petite partie de l'espace d'état mais tout ce qui est fait par tests peut également être fait par vérification (avec une petite aide humaine). En effet, les tests ne sont que la vérification d'un certain nombre chemins dans l'application et la vérif. permet également de faire cela (mais pour tous les chemins pour tous les états d'entrée ce qui est plus général).

        La vérification a cependant aussi ses limitations. La vérification s'applique uniquement sur les propriétés que l'utilisateur a défini. Ces propriétés sont une abstraction du programme. Par exemple, la propriété que 2 trains ne soient jamais dans des directions opposées sur la même voie. Si on veut vérifier l'entièreté d'un programme, le seul moyen est de réécrire le programme en spécification formelle c'est-à-dire avoir une propriété complète qui est le comportement du programme. Cela revient à écrire 2 fois le même programme dans des paradigmes différents et de vérifier qu'ils produisent les mêmes résultats...

        Ecrire 2 fois le même programme n'est pas du tout pratique et cela n'est (quasi) jamais fait, donc, on se satisfait d'une abstraction, d'une approximation du comportement. Ce qui n'est jamais parfait mais généralement plus efficace que des tests qui ont tendance à louper des cas particuliers (car on prouve que c'est juste pour toutes les inputs pas juste un chemin dans l'application).
        • [^] # Re: Se passer des tests ...

          Posté par . Évalué à  2 .

          Cela revient à écrire 2 fois le même programme dans des paradigmes différents et de vérifier qu'ils produisent les mêmes résultats...

          Mais lors d'une recherche de meilleur qualité, il n'y a pas d'autres solutions non ?

          "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

          • [^] # Re: Se passer des tests ...

            Posté par (page perso) . Évalué à  3 .

            Je ne suis pas sur de bien comprendre la question ? Pourrais-tu clarifier ?

            Mais j'essaie quand même de répondre en clarifiant mes propos.

            Ce que je disais c'est que le but de la vérification c'est de garantir certaines propriétés.

            Si la propriété est une spécification (totale) alors spec est déjà en quelque sorte le programme en lui-même. Si cette spec était "exécutée", par une machine, son comportement serait le même que celui du programme à vérifier.
            • [^] # Re: Se passer des tests ...

              Posté par . Évalué à  2 .

              Si la propriété est une spécification (totale) alors spec est déjà en quelque sorte le programme en lui-même. Si cette spec était "exécutée", par une machine, son comportement serait le même que celui du programme à vérifier.

              Je comprends bien. D'où la recherche de l'écriture de spec exécutable (est ce que tu connais Scade ? c'est l'argument des LLR executable pour le vendre).

              Mais il existe toujours un moment il faut spécifier ce que tu mets dans la spec. Il y a toujours une spec de spec en cascade.

              Donc, il y a toujours à un moment l'écriture de quelques choses de non ambigüe et l'écriture du code final. Ce qui revient à avoir 2 "modèles", non ?

              "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

              • [^] # Re: Se passer des tests ...

                Posté par (page perso) . Évalué à  2 .

                C'est effectivement ce que je disais : tout vérifier revient à écrire la même chose 2 fois.

                Un programme et une spec complète possèdent exactement la même sémantique. Pour un observateur externe, il n'y a pas moyen de les distinguer en pbservant les comportements.

                On peut voir le truc, donc, comme 2 modèles ou 2 programmes ou (1 programme, 1 modèle). Cela n'a pas d'importance car ils ne sont pas distinguable.

                PS: Je simplifie un peu, ils sont généralement distinguable du point de vue de l'efficacité.
                • [^] # Re: Se passer des tests ...

                  Posté par . Évalué à  2 .

                  Ma question était de savoir si il existait d'autres méthodes.

                  J'imagine que écrire le code puis écrire sa preuve devrait aussi suffire.

                  Mais d'après les exemples de "Why" pour un code de 20 lignes, il y en a 1000 de preuves. On est loin d'être utilisable.

                  "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                  • [^] # Re: Se passer des tests ...

                    Posté par (page perso) . Évalué à  3 .

                    De mon expérience, les spécifications sont plus ou moins de la taille du programme. Pour ce qui est de la preuve, elle peut être grande (si on fait de preuve symbolique) mais cela n'a pas d'importance c'est généré automatiquement. De plus, la seule chose qui compte ce n'est pas la grandeur preuve fournie mais que c'est prouvé ;-)

                    Le système avec des pré/post.conditions/invariants ne donnent pas de mauvais résultat et cela n'est pas si complexe que cela. L'humain aidant pas mal...
                    • [^] # Re: Se passer des tests ...

                      Posté par . Évalué à  2 .

                      J'ai du me tromper alors. Je parles évidement de la taille de ce que fournis l'humain pour faire la preuve.

                      Ensuite, il faut aussi prouver le prouver, ce qui n'est pas gagné.

                      "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                      • [^] # Re: Se passer des tests ...

                        Posté par (page perso) . Évalué à  5 .

                        Coq a été prouvé, ils ont sacrifié un thésard pour ça....

                        Un pays bien organisé est celui où le petit nombre fait travailler le grand nombre, est nourri par lui, et le gouverne - Voltaire

                        • [^] # Re: Se passer des tests ...

                          Posté par . Évalué à  1 .

                          Oui, enfin rappelons avec monsieur Gödel que la preuve se base forcément sur quelque-chose de « plus fort » que la théorie de Coq elle-même. Il n'y a pas de preuve de cohérence de Coq en Coq, sans ajouter d'axiome supplémentaire, et (autre façon de voir les choses) il est impossible pour la même raison de coder l'algorithme de réduction du calcul des constructions inductives, la base formelle de Coq, en Coq.

                          Pour reprendre une image de Jean-Yves Girard, les preuves de cohérences sont des assurances contre l'explosion de la Terre (même si elle peuvent avoir des retombées pratiques et nous apprendre des choses).
                          • [^] # Re: Se passer des tests ...

                            Posté par . Évalué à  4 .

                            Il me semble que pour Coq, il ont essayé de réduire au maximum l'ensemble représentant les axiomes de base afin de les prouver "à la main", et de faire prouver le reste de Coq à partir de ça. Bon, c'est assez approximatif, si quelqu'un avait une explication plus clair, je suis pour.
                          • [^] # Re: Se passer des tests ...

                            Posté par (page perso) . Évalué à  2 .

                            Et pourtant, je n'y connais pas grand'chose, mais il y a dans le bureau à côté du mien, quelqu'un qui travaille sur Coq-en-Coq. Et les première tentatives remontent à 1989 ! Lire l'introduction de son article aux JFLA par exemple, disponible sur sa page web : http://stephane.glondu.net
                          • [^] # Re: Se passer des tests ...

                            Posté par (page perso) . Évalué à  2 .

                            Hum, sans aller jusqu'à mon pote Gödel, COQ est pas turing complet, c'est justement ce qui permet d'avoir des propriétés décidables si t'as réussi à coder ton programme en COQ.
                  • [^] # Re: Se passer des tests ...

                    Posté par (page perso) . Évalué à  3 .

                    Dans le cas de code non critique (ie. informatique de gestion), si le logiciel est capable de dire, au choix :
                    - Couverture des contrats insuffisante
                    - Code valide pour ses contrats
                    - Code invalide pour ses contrats

                    c'est déjà énorme.

                    Si en plus, il sort un contre exemple, alors là c'est génial.

                    J'imagine qu'en aéronautique, ou en hardware, on se doit de vérifier la preuve généré... Dans l'informatique de gestion on veut qq chose de plus rapide et plus fiable que l'écriture de tests unitaires à la mano...

                    Un pays bien organisé est celui où le petit nombre fait travailler le grand nombre, est nourri par lui, et le gouverne - Voltaire

                    • [^] # Re: Se passer des tests ...

                      Posté par (page perso) . Évalué à  2 .

                      Exactement. Vérifier quelques propriétés (ou contrats comme tu dis) est amplement suffisant pour la plupart des projets.
                      • [^] # Re: Se passer des tests ...

                        Posté par . Évalué à  2 .

                        Je rajouterai l'équivalence des programmes, c'est énorme pour l'optimisation.

                        Je ne pense pas que l'on est besoin que toutes assertions soit prouvable, j'ai peur que cela sois compliqué. Je préfère que des assertions simples (division par zéro) puisse être traité sur le programme en entier. Générer un contre exemple, c'est indispensable tellement, c'est utile.

                        La génération automatique de pattern de teste pour passer les assertion en dynamique pour faire la couverture de code est très utile (pour avoir le pire cas en timing aussi). Les stratégies de tests pour trouver les vecteurs sont parfaitement automatisable (gestion des classes d'équivalence, branches, valeur singulière, etc..)

                        "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                        • [^] # Re: Se passer des tests ...

                          Posté par (page perso) . Évalué à  2 .

                          Oui c'est utile d'avoir une trace mais en version symbolique c'est parfois, pour le moins, ardu à lire ;-)

                          Pour ma part, j'ai plus pratiqué le model checking et l'exploration des états/traces de programmes distribués avec des logiques temporelles pour spécifier les propriétés. On obtient en cas de réfutation une trace (suite d'états) qui est fort utile.
        • [^] # Re: Se passer des tests ...

          Posté par (page perso) . Évalué à  1 .

          Tu dis une chose et son contraire dans le même texte. Avec des méthodes de vérification, on arrive actuellement à prouver un petit nombre de propriétés d'un programme, voire la correction d'un petit programme, mais guère plus. C'est insuffisant dès lors que le programme va être utilisé pour des applications importantes, en particulier si un bug peut avoir des effets désastreux (pas forcément en vies humaines : le bug du Pentium a coûté cher à Intel en relations publiques). C'est aussi insuffisant dès lors que le milieu dans lequel on va utiliser le programme est difficile à simuler.
          • [^] # Re: Se passer des tests ...

            Posté par (page perso) . Évalué à  1 .

            Je ne dis pas une chose et son contraire. Je dis simplement que la vérification est supérieure aux tests (ceux-ci n'étant pas exhaustifs même sur une propriété précise à vérifier contrairement à la vérification).

            Mais je suis réaliste en disant que la vérification a aussi des limites. Mais ces limites sont beaucoup plus loin que celles du testing.
            • [^] # Re: Se passer des tests ...

              Posté par (page perso) . Évalué à  3 .

              Pour moi la vérification n'est pas supérieur aux tests. Il y a des spécifications que tu seras bien en peine de valider avec un vérificateur.
              Exemple de spécification :
              - le temps de réponse moyen est de 300ms.
              - la charge nominale sur un serveur de type TrucMuche est de 5000 requêtes simultanées avec un temps de réponse acceptable.
              - l'interface graphique doit respecter les HIG Gnome.
              - l'utilisateur ne doit jamais attendre plus d'1 seconde entre 2 écrans successifs.
              - l'application doit utiliser la police de caractère par défaut de l'environnement.
              Bon courage pour spécifier tout ca en pre-post conditions :)
              Par contre ca s'écrit très bien en tests. Voir ca s'automatise.
              Bref, les vérificateurs c'est très bien si tu te cantonnes au périmètre purement mathématique d'un programme.
              Mais dans la vraie vie, un logiciel est rarement limité à ca... quelques briques tout au plus...
              • [^] # Re: Se passer des tests ...

                Posté par (page perso) . Évalué à  2 .

                Dans la boite où je bosse, les spécifications dont tu donnes l'exemple relève plus des tests fonctionnels ou de performances.
                On utilise des logiciels spécifiques pour cela, qui vont automatiser l'expérience utilisateur dans le clickodrome, etc...

                Là ou la preuve de code est intéressante, c'est en complément des tests unitaires (avec junit) qui font parti intégrantes de la procédure de compilation qu'on automatise avec maven (le make amélioré de java).

                Effectivement l'intérêt de ce genre de logiciel est limité à une petite partie du processus de fabriquation du logiciel, mais ça peut avoir un intérêt en terme de coût non négligeable.

                Un pays bien organisé est celui où le petit nombre fait travailler le grand nombre, est nourri par lui, et le gouverne - Voltaire

              • [^] # Re: Se passer des tests ...

                Posté par . Évalué à  6 .

                Manque de bol, sur tes cinq examples, les trois traitants de temps de réponse sont tout à fait dans le colimateur des méthodes formelles via par exemple automates temporisés*, et du fameux problème de calcul du temps d'exécution pire cas**. En particulier, ton premier exemple est un grand classique de la vérification de système temps-réel, domaine qui me semble particulièrement bien étudié !

                Pour les problèmes d'interface graphique, effectivement c'est plus difficile, et je ne pense pas que les méthodes formelles aient un quelconque intérêt.

                * : http://mpri.master.univ-paris7.fr/attached-documents/C-2-8/m(...)

                ** : http://en.wikipedia.org/wiki/Worst-case_execution_time
                • [^] # Re: Se passer des tests ...

                  Posté par (page perso) . Évalué à  0 .

                  En particulier, ton premier exemple est un grand classique de la vérification de système temps-réel, domaine qui me semble particulièrement bien étudié !

                  Eh ben rajoute à mes specifications que c'est censé marché sous Windows XP. Voilà hop, t'as un système non temps-réel, accroche toi pour la vérification.
                  • [^] # Re: Se passer des tests ...

                    Posté par (page perso) . Évalué à  2 .

                    >Eh ben rajoute à mes specifications que c'est censé marché sous Windows XP. Voilà hop,
                    >t'as un système non temps-réel, accroche toi pour la vérification.

                    Et avec tes tests dans ce ca précis, peux-tu garantir quelque chose ? Si non, tu n'a toujours rien démontré à part ta maitrise des sophismes.
                    • [^] # Re: Se passer des tests ...

                      Posté par (page perso) . Évalué à  4 .

                      Bah les tests ne prouvent jamais rien : ils n'offrent donc pas de garantie mais un degré de confiance. A l'instant où tu déroule le test, le comportement du programme est conforme à ce qui était attendu. Ca veut évidemment pas dire que ca sera toujours le cas. Mais tu peux faire des tests d'endurance qui te donneront un bon degré de confiance.
                      Sinon joli le dérapage sur la forme.
                      • [^] # Re: Se passer des tests ...

                        Posté par . Évalué à  2 .

                        Un outil formel pour le faire permettrait de te trouver le ou les vecteurs d'entrées correspondant à ton pire cas et mesurer ensuite le temps d'exécution. Tout cela pourrait être automatique.

                        "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                      • [^] # Re: Se passer des tests ...

                        Posté par (page perso) . Évalué à  3 .

                        Oh que si ça prouve.
                        Quand un programme buggue suite à un test, ça prouve qu'il y a un bug. C'est pas une information inutile ça !!!
                • [^] # Re: Se passer des tests ...

                  Posté par . Évalué à  2 .

                  Je ne suis pas d'accord. Demander un temps moyen de 300ms ce n'est pas du temps réel. Un temps maximum de 300ms, oui, mais un temps moyen non. Et ça ne peut pas être résolu par le calcul du pire cas.

                  Tous les nombres premiers sont impairs, sauf un. Tous les nombres premiers sont impairs, sauf deux.

                  • [^] # Re: Se passer des tests ...

                    Posté par (page perso) . Évalué à  2 .

                    Cela peut être considéré comme du temps réel avec des deadlines soft. Mais la plupart du temps, on veut un temps maximum c'est vraim.

                    Il est possible même d'associer un distribution de probabilité aux événements et de s'assurer que le système répond selon cette loi. Un peut à la mode des SLA, il faut un temps de réponse dans 90% des cas de un 1j, pas plus 10% au-dela de cette limite.

                    Mais bon, pour ce genre de système c'est beaucoup plus simple d'avoir des deadlines hard.
              • [^] # Re: Se passer des tests ...

                Posté par (page perso) . Évalué à  4 .

                >Exemple de spécification :
                >- le temps de réponse moyen est de 300ms.

                >- la charge nominale sur un serveur de type TrucMuche est de 5000 requêtes simultanées
                >avec un temps de réponse acceptable.


                >- l'utilisateur ne doit jamais attendre plus d'1 seconde entre 2 écrans successifs.

                Garanti par la théorie du temps réel (hard deadline) [1] :
                http://en.wikipedia.org/wiki/Real-time_computing

                Nullement garanti par des tests.

                >- l'interface graphique doit respecter les HIG Gnome.

                Fallacieux car Il n'y pas de specification formelle (juste une informelle pour ça).

                >- l'application doit utiliser la police de caractère par défaut de l'environnement.

                Vérifiable avec la bonne propriété. Il n'y pas de différence avec une propriété du genre : la barrière du passage à niveau doit être fermé quand le train passe. La propriété à vérifier est : Pour tout état du programme, la police affiché (l'affichage fait partie de l'état) est celle de l'environement.

                >Bon courage pour spécifier tout ca en pre-post conditions :)

                La vérification ce n'est pas seulement des pre/postconditions et des invariants. Notament, le model-checking [2][3] n'est pas fait pour les chiens.

                [1] http://www.google.com/search?hl=en&q=formal+verification(...) au choix
                [2] http://en.wikipedia.org/wiki/Model_checking
                [3] https://linuxfr.org//2008/02/05/23656.html
                • [^] # Re: Se passer des tests ...

                  Posté par (page perso) . Évalué à  2 .

                  Garanti par la théorie du temps réel
                  Si t'as pas d'OS temps réel, t'as perdu.

                  Nullement garanti par des tests.
                  Personne n'a dit que les tests offraient de garanties.

                  Fallacieux car Il n'y pas de specification formelle (juste une informelle pour ça).
                  Bienvenu dans la vraie vie ! Je dirais que la grande majorité des spécifications logicielles telles qu'exprimées par le client sont informelles, incomplètes ou insuffisantes, et c'est ma principale remarque initiale. Toutes les tentatives de formalisation à partir de ces specs (specs détaillées, specs formelles puis pre-post conditions) passent par une interprétation humaine de specs informelle, et c'est là que le test reste utile. Tu es obligé de rédiger un cahier de tests, tu peux le faire valider par le client pour voir s'il est conforme à ses attentes, tu le soumets aux équipes de validation qui vont y jeter un regard humain et y déceler des erreurs d'interprétation, y ajouter leur interprétation, etc.
                  Un valideur formelle ne valide pas les specs, d'où l'intérêt de mon exemple qui n'a strictement rien de fallacieux, et qui au contraire me paraît très réaliste.

                  Pour tout état du programme, la police affiché (l'affichage fait partie de l'état) est celle de l'environement.
                  Je te pari que t'es incapable de prouver une telle propriété.
                  • [^] # Re: Se passer des tests ...

                    Posté par . Évalué à  2 .

                    Si t'as pas d'OS temps réel, t'as perdu.

                    Tu as perdu quoi ? Dire que tu compares une méthode formelle (style celle de absint qui utilise un modèle cpu+mémoire) avec la simple mesure de quelques vecteur d'entrés !

                    Personne n'a dit que les tests offraient de garanties.

                    Pourquoi tu sous entends que la solution formelle serait moins bonne alors ?

                    Un valideur formelle ne valide pas les specs, d'où l'intérêt de mon exemple qui n'a strictement rien de fallacieux, et qui au contraire me paraît très réaliste.

                    Bien sur qu'elle valide les specs ! En rédigeant la spec formelle tu identifies immédiatement tous les manques et précision à demander à ton client !

                    "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                    • [^] # Re: Se passer des tests ...

                      Posté par (page perso) . Évalué à  2 .

                      Tu as perdu quoi ?
                      Tu as perdu la possibilité de prouver quoique ce soit, puisque sur un OS non temps-réel tu n'as strictement aucune garantie sur la disponibilité des ressources.

                      Pourquoi tu sous entends que la solution formelle serait moins bonne alors ?
                      J'ai jamais dis ca, je dis juste que la solution formelle a trop de contraintes fortes et qu'elle n'est pas applicable dans certains cas, auquel cas il faut bien faire une autre forme de test.

                      Bien sur qu'elle valide les specs !
                      Si la spec contient une erreur, le fait de formaliser la spec va peut être t'aider à trouver l'erreur, mais en aucun cas la méthode formelle en soit ne garantie que tu vas trouver ces erreurs.
                      C'est pas parcque tu as réussi à formaliser les specs que les specs sont valides. Ca veut juste dire que l'humain qui les as interprétés n'a pas trouver de problème lors de la formalisation. Si ca se trouve le client c'est mal exprimé et ton logiciel vas pas faire ce qui est prévu, va savoir !

                      En rédigeant la spec formelle tu identifies immédiatement tous les manques et précision à demander à ton client !
                      N'importe quoi. Tu peux identifier certains manques et certaines imprécisions, mais tu ne peux pas identifier toutes les erreurs dans les specs. Si la spec dit que le volant doit être dans le coffre de la voiture, c'est peut être tout à fait valide techniquement mais totalement abhérent du point de vue utilisateur. Et là si tu fais pas des tests d'ergonomie...

                      Quand à demander au client, c'est un doux rêve, souvent le client il veut pas tout formaliser, parcque ca supposerait qu'il réfléchisse sur ses besoins... hors il a en parti fait appel à tes services pour que tu l'aide dans cette tâche de formalisation. C'est con mais c'est comme ca dans la vraie vie, souvent tu te buttes face à un client qui ne veut pas répondre (pas le temps ou ne sais pas trancher) et tu dois faire des choix.
                      • [^] # Re: Se passer des tests ...

                        Posté par . Évalué à  2 .

                        Tu as perdu la possibilité de prouver quoique ce soit, puisque sur un OS non temps-réel tu n'as strictement aucune garantie sur la disponibilité des ressources.

                        Quelle différence entre une vérification formelle et un test, ici ?

                        C'est pas parcque tu as réussi à formaliser les specs que les specs sont valides.

                        C'est évident ça. mais dans ce cas, on parle de valider la spec par celle au dessus. Au moins on peut trouver les incohérences.

                        Et là si tu fais pas des tests d'ergonomie...

                        Cela veut dire que tu codes en suivant une spec mais que tu tests en suivant autre choses ? Je te souhaite bien du courage pour expliquer d'où vient le problème à ton client ! (sa spec et pas ton code)

                        'est con mais c'est comme ca dans la vraie vie, souvent tu te buttes face à un client qui ne veut pas répondre (pas le temps ou ne sais pas trancher) et tu dois faire des choix.

                        Je commençais à comprendre que ton client ne faisait pas des avions :)

                        "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                        • [^] # Re: Se passer des tests ...

                          Posté par (page perso) . Évalué à  2 .

                          Quelle différence entre une vérification formelle et un test, ici ?
                          Les tests de performance et d'endurance vont te permettre d'obtenir un degré de confiance en mesurant le temps de réponse.
                          Si tu joues le jeu de la vérification formelle, tu démonteras juste que ce n'est pas prouvable. T'es bien avancé.

                          Je te souhaite bien du courage pour expliquer d'où vient le problème à ton client ! (sa spec et pas ton code)
                          C'est tout le problème des clients qui ne savent pas ce qu'ils veulent :)

                          Je commençais à comprendre que ton client ne faisait pas des avions :)
                          Oué bah on en revient toujours à la base : en dehors des domaines où la sécurité est primordiale, en général personne se fait chier à atteindre le niveau de spécification formelle nécessaire à l'utilisation de ces méthodes de vérification.
                          • [^] # Re: Se passer des tests ...

                            Posté par . Évalué à  2 .

                            Les tests de performance et d'endurance vont te permettre d'obtenir un degré de confiance en mesurant le temps de réponse.
                            Si tu joues le jeu de la vérification formelle, tu démonteras juste que ce n'est pas prouvable. T'es bien avancé.


                            Renseignes toi mieux. Ce genre d'outil existe déjà et fonctionne.

                            par exemple : http://www.absint.com/ait/

                            "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                            • [^] # Re: Se passer des tests ...

                              Posté par (page perso) . Évalué à  2 .

                              "aiT WCET Analyzers statically compute tight bounds for the worst-case execution time (WCET) of tasks in real-time systems"
                              C'est bien ce que je dis, si t'as pas la contrainte OS temps réel, t'es bien avancé.
                              • [^] # Re: Se passer des tests ...

                                Posté par . Évalué à  1 .

                                Pas plus pas moins qu'avec un test...

                                "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                                • [^] # Re: Se passer des tests ...

                                  Posté par (page perso) . Évalué à  2 .

                                  J'ai pourtant cru être clair : les tests "non formels" apporteront un degré de confiance dans ce cas précis, là où la méthode formelle ne te donnera aucun degré. C'est ON/Off : prouvé/pas prouvé. Ca marche tout le temps, ou pas. Y'a pas de milieu. Ben dès fois la spec elle dit qu'il faut que ca marche 95% du temps dans des conditions normales d'utilisation. Ben ca la méthode formelle peut pas m'aider.
                                  • [^] # Re: Se passer des tests ...

                                    Posté par . Évalué à  2 .

                                    C'est ON/Off : prouvé/pas prouvé.

                                    Ben non. Cela ne marche pas que comme ça.

                                    Si c'est pas prouvé, il te donne un contre exemple immédiatement, donc tu corriges très rapidement ton appli pas besoin de la suite de non régression "overnight". C'est sans doute la partie la plus utile.

                                    Si c'est prouvé bingo. Si l'assertion est correctement exprimé. C'est en fait moins utile que le cas précédent.

                                    Si il n'y arrive pas, le prouveur d'Esterel te donne une profondeur temporel genre 10 coups d'horloges, si on connait la structure de son code (pas de mémoire à plus de 10 coups en arrière), on peut être confiant.

                                    Dans la vérification formel, j'inclus aussi la génération automatique de vecteurs d'entrée pour augmenter le taux de couverture. Il n'y a plus qu'à avoir des sorties de références ou des assertions à vérifier.

                                    Le static timing analyser de temps en pire cas permet de te trouver ton pire cas en timing. (il faut par contre un beau modèle de ton systèm)

                                    J'ai dû oublier d'autres types de vérification.

                                    "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                                    • [^] # Re: Se passer des tests ...

                                      Posté par (page perso) . Évalué à  2 .

                                      il te donne un contre exemple immédiatement, donc tu corriges très rapidement ton appli pas besoin de la suite de non régression "overnight". C'est sans doute la partie la plus utile.
                                      Ah oué, je vois bien le prouver me dire : "ah regardes quand je lance firefox et le plugin flash, il bouffe les 3/4 de la RAM et 100% du CPU, pendant ce temps là l'application que je valide ne répond plus dans les temps moyens acceptables".
                                      Pourtant c'est un peu tout le problème des OS non temps-réel, et je vois mal ton prouveur être capable d'apréhender tout la complexité des comportements possibles d'une machine qui exécute un environnement qui n'offre pas de garanties temps-réel...

                                      Dans la vérification formel, j'inclus aussi la génération automatique de vecteurs d'entrée pour augmenter le taux de couverture.
                                      Ca me paraît borderline et plus du domaine de la vérification mathématique, on se rapproche du test traditionnel. On arrive également à produire des tests de couverture de code automatiquement sans passer par un vérificateur formel.

                                      (il faut par contre un beau modèle de ton systèm
                                      Oué donc arrache toi pour ton application qui tourne sous Windows ou Ubuntu.
                                      • [^] # Re: Se passer des tests ...

                                        Posté par . Évalué à  2 .

                                        Ca me paraît borderline et plus du domaine de la vérification mathématique, on se rapproche du test traditionnel. On arrive également à produire des tests de couverture de code automatiquement sans passer par un vérificateur formel.

                                        Tu fais une différence entre formelle et mathématique ?

                                        Sinon, pour l'augmentation de taux de couverture, il y a aussi des système utilisant de l'aléatoire, mais la plus part sont des systèmes formels.

                                        Oué donc arrache toi pour ton application qui tourne sous Windows ou Ubuntu.

                                        Par system, je parlais de HW.

                                        "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                                      • [^] # Re: Se passer des tests ...

                                        Posté par (page perso) . Évalué à  2 .

                                        Il te parle d'Esterel là. Esterel permet de faire du dev pour du hardware, monde où les entrées/sorties sont assez normés.

                                        Effectivement sur un OS desktop, on est pas dans le même monde, donc votre débat n'a pas lieu d'être en ces termes.

                                        Un pays bien organisé est celui où le petit nombre fait travailler le grand nombre, est nourri par lui, et le gouverne - Voltaire

                                        • [^] # Re: Se passer des tests ...

                                          Posté par . Évalué à  2 .

                                          Même avec un OS, je ne vois pas ce qui empêche de définir des contraintes temps réel mou.

                                          Tu dois pouvoir écrire un modèle d'OS du style, tu as 90 % de chance de te prendre une IT qui dure 10 us, 9% quel dure 100us, 1% 800 µs. Idem pour bon nombre des appels systèmes.

                                          Tu perds beaucoup en précision mais cela reste utile. On peut faire plein de choses avec des probabilités.

                                          "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                                          • [^] # Re: Se passer des tests ...

                                            Posté par (page perso) . Évalué à  2 .

                                            Le problème est qu'il est vraiment trop compliqué d'avoir des stats fiables, y'a tellement de configuration matérielles et logiciels que ca devient totalement irréaliste.
                                            Comme qui dirait, en théorie c'est faisable, mais ça marchera jamais en pratique.
                                            • [^] # Re: Se passer des tests ...

                                              Posté par . Évalué à  2 .

                                              On est purement dans la théorie pour l'instant :)

                                              "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                                            • [^] # Re: Se passer des tests ...

                                              Posté par . Évalué à  1 .

                                              Dans la pratique les processeurs grand public sont bourré de caches prédictif et de pipeline ce qui rend la détermination du temps d'exécution au pire des cas très pessimiste par rapport au cas moyen.
                                              De plus effectivement les OS normaux n'ont pas de garantie de schéduling temps-réel. D'ailleur linux sans patch n'est pas très bon a ce jeu là.

                                              Après effectivement en théorique tu peut quand même faire une analyse formelle des prop temps-réel mais elle sera très pessimiste pour être utilisable en pratique (c'est a dire qu'on sous utilisera la puissance du processeur). Mais en pratique on met des logiciels temps-réel sur les OS et du matos adapté donc y'a pas trop lieu de polémiquer sans fin.

                                              Ben ce qui est du temps réel mou (soft realtime) ben par définition c'est pas grave si on loupe des deadline, donc l'intéret de faire une preuve formelle est moins évidente.
                          • [^] # Re: Se passer des tests ...

                            Posté par . Évalué à  1 .

                            Oué bah on en revient toujours à la base : en dehors des domaines où la sécurité est primordiale, en général personne se fait chier à atteindre le niveau de spécification formelle nécessaire à l'utilisation de ces méthodes de vérification.

                            On peut trouver des compromis, des lightweight formal method, par exemple on fait des modèles formel mais pas exhaustif et on s'en sert pour générer des jeux de test. Après on peut en rester là ou aller plus loin dans la preuve sur le modèle si il y a un intéret/budget.
                            Il y a pas mal de projet comme çà, c'est intéressant je pense.
            • [^] # Re: Se passer des tests ...

              Posté par (page perso) . Évalué à  2 .

              La vérification consiste à construire (ou obtenir) une spécification et prouver qu'un code source s'y conforme. Le test consiste à placer le programme exécutable dans les conditions - à trouver, ce qui n'a rien d'évident - dans lesquelles il est susceptible d'être utilisé et... voir ce qui se produit. Ce sont deux choses différentes, orthogonales, toutes deux indispensables dans un projet où la sûreté est importante.
              Je dis simplement que la vérification est supérieure aux testsCeci a à peu près autant de sens qu'affirmer que C++ est supérieur à XML.
              • [^] # Re: Se passer des tests ...

                Posté par (page perso) . Évalué à  1 .

                Un test tests c'est

                A partir d'un état de départ, on vérifie une propriété sur l'état d'arrivée en exécutant une partie de code

                1 état ---execution--> 1 état

                La vérif (et notament le model checking), on part de tous les états possibles et on vérifie que pour tous les états de destination, la propriété est vérifiée

                Tous les états d'entrée ---Vérification---> Tous les états de sortie

                Trivialement, le testing est un cas particulier de la vérification. Donc, la vérification fait tout ce que le testing fait mais plus encore.
                • [^] # Re: Se passer des tests ...

                  Posté par (page perso) . Évalué à  2 .

                  1 état ---execution--> 1 état
                  Ça, c'est un test. Ce qu'on appelle tester, c'est trouver et appliquer un jeu de tests, càd une collection de tests satisfaisant des critères bien définis, notamment de couverture.

                  Je ne vais pas répéter encore une fois ce que j'ai déjà dit deux fois, j'ai bien compris que tu tiens à faire profiter tout le monde de ton ignorance de ces deux domaines bien distincts et, par ailleurs, fort intéressants tous les deux. J'ai baigné dans les deux milieux quand j'étais moi-même doctorant au LRI. J'y ai travaillé avec les membres de l'équipe parall, entre autres ceux qui font du model-checking. J'y ai aussi rencontré par exemple Marie-Claude Gaudel et des membres de son équipe de génie logiciel, où l'on fait notamment de la recherche sur le test de programmes. J'y ai aussi rencontré des membres de l'équipe de démonstration et programmation, dont entre autres Jean-Christophe Filliâtre, et je serais très étonné, pour employer une litote, qu'il considère ses travaux comme "supérieurs" à ceux de Marie-Claude.

                  Au passage, puisque tu es tellement plus fort que tous ces incompétents de chercheurs, tu pourrais aller dire au CEA que les recherches sur le test de logiciels de contrôle-commande que l'on y conduit sont inutiles. Ça va sûrement beaucoup les intéresser.
                  • [^] # Re: Se passer des tests ...

                    Posté par (page perso) . Évalué à  1 .

                    Pourquoi as-tu besoin d'étaler ton CV ? Un argument d'autorité ? Très bien, et bien, j'ai également été doctorant et j'ai cotoyé un certain temps le labo d'un turing award. Maintenant, peut-on, cessez ce genre d'enfantillage et parler avec de réels arguments ?

                    >Ça, c'est un test.

                    J'ai dit exactement cela, je n'ai jamais prétendu le contraire. La couverture n'est pas exhaustive car c'est un ensemble de tests qui n'ont pas le but d'être axhaustifs.

                    Maintenant, pour ce qui est de la supériorité c'est une interprêtation abusive de ta part du mot. Je l'ai exprimé comme un surensemble.

                    Il y a évidement des cas où des tests sont suffisants et que la vérification serait une totale perte de temps. Rien n'empêche de faire de la recherche dans le domaine du testing puisque que c'est un domaine intéressant autant que la vérification.

                    N'empêche que je considére la vérification comme beaucoup plus générale que le testing. Le testing peut être vu comme un cas particulier de la vérification.

                    >Au passage, puisque tu es tellement plus fort que tous ces incompétents de chercheurs,

                    J'ai été chercheur... Donc, mon petit gars, je trouve ton commentaire complètement stupide et les propos que tu essaies de m'assigner pas très digne de quelques u qui devrait avoir un esprit scientifique.
                    • [^] # Re: Se passer des tests ...

                      Posté par (page perso) . Évalué à  1 .

                      Dire
                      Je dis simplement que la vérification est supérieure aux testsPour enchaîner sur
                      pour ce qui est de la supériorité c'est une interprêtation abusive de ta part du mot. Je l'ai exprimé comme un surensemble.C'est au minimum minimorum une formulation vraiment très maladroite. Plus vraisemblablement, de la grosse mauvaise foi.

                      Pourquoi as-tu besoin d'étaler ton CV ? Un argument d'autorité ?Voilà qui est, pour le coup, une interprétation (très) abusive. J'indique que j'ai rencontré des personnes qui travaillent sur les sujets évoqués, ce qui ne peut de toute évidence pas être ton cas.

                      N'empêche que je considére la vérification comme beaucoup plus générale que le testing. Le testing peut être vu comme un cas particulier de la vérification.Bravo : après je ne sais plus combien d'explications, tu persistes encore et toujours. Mais bien sûr, c'est toi qui as raison et les spécialistes de ces domaines qui ont tort.

                      Quant au reste, même si j'admets que ton attitude bornée consistant à répéter ad nauseam les mêmes assertions toujours aussi fausses est passablement irritante, je te signale que je ne t'ai jamais insulté et t'invite à en faire de même.
                      • [^] # Re: Se passer des tests ...

                        Posté par . Évalué à  1 .

                        tu ne démontres ni n'explique rien en l'occurrence.

                        "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                        • [^] # Re: Se passer des tests ...

                          Posté par (page perso) . Évalué à  3 .

                          J'ai donné les deux définitions, qui sont clairement différentes. Pour ceux qui dorment au fond [,qui écrivent sans avoir lu et qui moinssent à la vue du nom de l'auteur], voici un exemple très simple. Le bug de l'instruction FDIV du Pentium 1, pourtant réalisée par un algorithme pour lequel il existe une preuve de correction, était dû à l'absence de certaines entrées dans une table de valeurs précalculées.

                          Pour la preuve, ceci n'existe pas. Lorsqu'il y a une table de valeurs précalculées dans une preuve, cette table est une constante. Vérifier que toutes les valeurs y sont n'a guère de sens puisque ça revient à écrire l'assertion selon laquelle une constante est égale à elle-même.

                          Du point de vue des tests (après coup, bien sûr, c'est toujours plus facile), il aurait fallu un test par entrée de la table. Comme le test porte sur la table produite et non sa spécification, ce n'est plus équivalent à une opération nulle.

                          C'est un exemple-jouet, bien sûr, mais c'est déjà suffisant pour montrer que la preuve de programmes et le test sont deux disciplines différentes qui s'intéressent à deux choses différentes. Il n'y a clairement pas d'inclusion de l'une dans l'autre. Après, on peut remarquer tant qu'on veut qu'elles utilisent des méthodes similaires : on utilise des automates aussi en traitement automatique des langues, pourtant je n'ai entendu personne déclarer que le TAL est inclus dans la preuve de programmes. Pas encore, du moins.
                          • [^] # Re: Se passer des tests ...

                            Posté par . Évalué à  1 .

                            En général, tu fais un test pour couvrir un point de spécification. Donc, tu trouves à la main des vecteurs d'entrée, tu évalue ce que doivent être tes sorties et tu compares avec la sortie de ton code.

                            Dans la preuve formel, tu ajoutes une assertion qui correspond à un point de spécification. La vérification formel balaye toutes les possibilités d'entrée à la recherche d'un contre exemple.

                            Dans le cas du test, tu es limité par les vecteurs d'entrée que tu trouves à la main alors qu'avec un moteur de preuve, tu as l'exhaustivité.

                            "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                            • [^] # Re: Se passer des tests ...

                              Posté par (page perso) . Évalué à  3 .

                              Ça peut continuer longtemps comme ça...

                              tu trouves à la main des vecteurs d'entrée, tu évalue ce que doivent être tes sorties et tu compares avec la sortie de ton code.Tu vis en 1970 ?

                              Dans le cas du test, tu es limité par les vecteurs d'entrée que tu trouves à la main alors qu'avec un moteur de preuve, tu as l'exhaustivité.Pour écrire ça, il faut :
                              * soit ne pas avoir lu ce que j'ai écrit juste avant ;
                              * soit choisir délibérément de n'en tenir aucun compte.

                              Bref, je laisse tomber. Comme dirait l'autre, ma patience a des limites, mais faut pas exagérer.
                              • [^] # Re: Se passer des tests ...

                                Posté par . Évalué à  2 .

                                Tu vis en 1970 ?

                                Et toi sur quelle planète ?

                                J'ai l'impression qu'il y une différence entre les pratiques habituelles pour le développement live critical et ce que tu crois l'être... vu depuis un labo.

                                "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                                • [^] # Re: Se passer des tests ...

                                  Posté par (page perso) . Évalué à  0 .

                                  J'ai l'impression qu'il y une différence entre les pratiques habituelles pour le développement live critical et ce que tu crois l'être...Les applications live critical (je suppose que tu entends par là life critical, dans la grande tradition francophone de l'emprunt inutile de mots anglais avec autant de fautes que de mots) incluent le contrôle de réacteurs nucléaires, la spécialités de mes formateurs en test de logiciels. C'est un domaine dans lequel on ne se contente pas d'écrire des papiers, et pour avoir habité près de ce genre d'installations, je n'en suis pas fâché.
                                  • [^] # Re: Se passer des tests ...

                                    Posté par . Évalué à  2 .

                                    life critical en effet :)

                                    Et bossant pour une boite qui vend un "langage formel" pour ce genre d'application, je peux te dire que tout ce qui est vérification formel est loin d'être la règle, et est encore moins reconnu (sauf peut-être dans le ferroviaire et encore).

                                    "La spécialités de mes formateurs en test de logiciels" et ils forment à quel genre de technique ?

                                    "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                                    • [^] # Re: Se passer des tests ...

                                      Posté par (page perso) . Évalué à  1 .

                                      Lorsque le cours portait sur de la technique, c'était du contrôle-commande et les programmes étaient écrits en Lustre. L'objectif était de voir comment on peut produire un jeu de tests et en valider un (qui peut avoir été préparé par quelqu'un d'autre).

                                      Quant à la vraie vie, j'ai eu vent que d'une façon très générale, les trains, les avions et les fusées sont à la pointe (pas forcément très aiguisée) en matière de vérification et de test, avec aussi les télécom. J'ai aussi vu passer des papiers industriels montrant que certains fabricants de matériels informatiques censés être sûrs utilisent des méthodes de test automatisé assez poussées depuis qu'ils se sont rendus compte que l'investissement est rentable sur le plan purement financier.
                                      • [^] # Re: Se passer des tests ...

                                        Posté par . Évalué à  3 .

                                        Un futur codeur Scade ;) Je peux te dire que la verif formel de scade débute.

                                        Et je peux te dire que dans la vrai vie, j'ai pas eu vent de comment cela passe; je le fais tous les jours. Je dois respecté la DO178B (celle d'aujourd'hui, en 1970, elle n'existait pas).

                                        Dans ce que tu décris, je ne vois rien de différent avec un test utilisant un "golden model", que l'on utilise en ce moment.

                                        Si tu as une autre méthode moins chiante, je suis preneur.

                                        "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                              • [^] # Re: Se passer des tests ...

                                Posté par (page perso) . Évalué à  2 .

                                Tu vis en 1970 ?
                                Tu sais l'informatique d'entreprise a à peu près 30 à 40 ans de retard sur ce qui est au point en labo...
                                Regarde Java : ça a 42 ans de retard si tu regardes Simula 67 (sorti en 67 comme son nom l'indique) qui possède une très grande partie des fonctionalitées offertes par Java.

                                Surtout en France ou les théoriens sont perçu par mes collègues comme une bande de professeur nimbus incapable de proposer qq chose d'utile.

                                Un pays bien organisé est celui où le petit nombre fait travailler le grand nombre, est nourri par lui, et le gouverne - Voltaire

                • [^] # Re: Se passer des tests ...

                  Posté par (page perso) . Évalué à  2 .

                  C'est sûr si c'est toi qui défini ce qu'es un test, on peut pas te contredire.
    • [^] # Re: Se passer des tests ...

      Posté par . Évalué à  2 .

      « on n'a pas besoin de faire des tests, on a une démonstration rigoureuse à la place et c'est beaucoup mieux », alors justement je cherche du boulot en ce moment (crise + période d'essai = chômage)

      Si c'est vraiment ta façon de coder, il vaudrait peut-être mieux que tu restes au chômage.
      Je n'aimerais pas monter dans une voiture qui n'a jamais été testée en grandeur nature sous prétexte qu'on a une « démonstration rigoureuse à la place » (sic).
      • [^] # Re: Se passer des tests ...

        Posté par . Évalué à  2 .

        Ben en fait dans l'ingénierie classique les méthodes formelles sont déjà la norme suffit de remplacer le terme «méthode formelle» par «résistance des matériaux» ou «thermodynamique» etc...
        Par exemple quand on construit un pont, on sait déjà (avant de le construire) que le pont va résister si on met des camions de 33t dessus, cela n'empêche pas d'essayer effectivement de mettre des camions dessus quand on a fini de le construire, comme tu l'à fait remarqué.

        Après le problème de l'informatique c'est qu'actuellement on ne fournit pas (usuellement) de garantie sur la qualité des logiciels. Si les freins de ma voiture lâchent, je peux attaquer le constructeur de la voiture. Mais si un logiciel m'a fait perdre ma compta la clause de non-responsabilité du fournisseur de logiciel empêche de demander de réparations.

        De plus il faut bien distinguer deux types de tests : les tests type unitaires et les tests d'intégrations. Je t'assure que la preuve formelle fournit une garantie bien plus forte que que les tests unitaires sur l'absence de bug. Mais même avec des preuves formelles il faut toujours faire des tests d'intégration car il faut *valider* la spécification formelle. C'est à dire est ce que c'est la bonne spec ? et est-ce qu'on a pas oublié des propriétés importantes ? La preuve ne fait que *vérifier* la spec, des propriétés ou le code produit
      • [^] # Re: Se passer des tests ...

        Posté par . Évalué à  5 .

        Je n'aimerais pas monter dans une voiture qui n'a jamais été testée en grandeur nature sous prétexte qu'on a une « démonstration rigoureuse à la place » (sic).

        Tu peux dormir sur tes deux oreilles : l'électronique embarquée dans les bagnoles n'a à ma connaissance en général pour elle ni « démonstration rigoureuse », ni politique de test sérieuse. Ouf !

        J'ajoute également qu'en ce qui me concerne, il me déplairait au plus haut point de prendre un avion, de me voir poser un pacemaker* ou d'être opéré par un robot chirurgical dont les logiciels de commande ont uniquement été testés et non pas soumis à des méthodes formelles.

        * Rappel : http://news.cnet.com/8301-13739_3-9883822-46.html Étonnant, non ?
  • # mouais

    Posté par (page perso) . Évalué à  10 .

    oué c'est utile, mais ca validera jamais tes spécifications. Et ca ne te les inventera pas non plus.
    Pour avoir fait mumuse avec ce genre d'outil (méthode B à l'époque), t'en arrives à trouver les bugs dans les spec détaillées du programme : manque de précision voir absence, incohérence voir contradiction, etc.
    Et comme d'hab, les specs sont sujettes à interprétations, sont elles-mêmes tirées de specs plus générales voir d'un cahier des charges.
    Dans la vraie vie, on obtient trop rarement le niveau de spécification détaillé suffisant pour pondre les fameuses pre-post conditions indispensables pour ce genre d'outil de preuve, bref c'est rarement utilisable.
    Y'a à mon avis encore beaucoup de boulot pour les analystes, architectes et testeurs et les outils de preuve resteront quelque chose de coûteux à mettre en oeuvre et sera donc limité aux projets "critiques" (là où la sécurité est en jeu).
    • [^] # Re: mouais

      Posté par . Évalué à  1 .

      À ce sujet, s'il y en a que ça intéresse, on (http://www.systerel.fr) propose régulièrement des stages autour de B (http://www.eventb.org)... Et parfois des offres d'emploi aussi...
      • [^] # Re: mouais

        Posté par . Évalué à  2 .

        En passant le logiciel pour faire de la méthode B évènementielle, développé lors du projet de recherche européen Rodin (c'est aussi le nom du logiciel), est un logiciel libre :
        http://sourceforge.net/projects/rodin-b-sharp/
        il y a un prouveur dedans qui est libre aussi, par contre ceux qu'on installe avec le plugin proviennent de l'atelierB de clearsy ( http://www.clearsy.com/ )
    • [^] # Re: mouais

      Posté par . Évalué à  4 .

      Ce que tu dis, c'est justement que c'est très précieux, car cela trouve jusqu'au manquement de la spec. Cela repousse le travail idiot du test systématique par une recherche d'une meilleur cohérence de spec et d'un test de haut niveau.

      Personne n'a jamais dit qu'un ordinateur ferait tout le boulot à ta place.

      Sinon dans les prouveurs "100% automatique", il recherche si il existe les conditions de plantage du code C, comme les "array out of bound", les division par zéro. Le but est ici de prouver que le code ne plante pas, pas qu'il correspond à la spec. C'est déjà pas mal car on ne demande rien aux codeurs "en plus".

      D'une manière général, la preuve, c'est génial, sauf que cela passe rarement à l'échelle (pb numero 1) et "les gens" ne font pas confiance à un "toujours vrai" rendu par un outil, par contre, ils aiment bien qu'on trouve leur bug.

      "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

      • [^] # Re: mouais

        Posté par (page perso) . Évalué à  1 .

        D'une manière général, la preuve, c'est génial

        Dis par quelqu'un pour qui les démonstrations sont quelque-choses de surnaturelles, ça fait sourire ===========>[_o/]
        • [^] # Re: mouais

          Posté par . Évalué à  2 .

          Dans ce cas là, c'est l'outil qui l'a fait à ta place /o\

          "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

        • [^] # Re: mouais

          Posté par . Évalué à  2 .

          D'ailleurs, y'a ESL Technology qui est à racheter (ex-Esterel EDA), la boite qui a repris le langage Esterel. 10 ans de R&D. Elle est en faillite suite à l'arrêt de la moitié des contrats de prestation du principale client TI.

          L'intégration de le preuve est assez sympa. Le langage lui-même fait passer le VHDL pour de l'assembleur par rapport à Java.

          "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

          • [^] # Re: mouais

            Posté par . Évalué à  7 .

            De mon point de vue, en tant qu'utilisateur quotidien d'Esterel, utilisateur avéré de son module de preuve formelle, utilisateur d'autres modules de preuve formelle et utilisateur de validation par stimuli pseudo-aléatoires sous force brute, la validation par preuve formelle est complémentaire à toute autre forme de validation. Aucune n'est à négliger. Un court retour d'expérience s'impose.

            Dans le projet dont je m'occupe, la preuve formelle a permis de trouver certains bugs fonctionnels bien avant tout autre forme de validation et a en outre le net avantage de proposer un contre exemple de taille minimale, ce qui facilite le travail des designers.

            La preuve formelle, telle qu'intégrée à Esterel permet aussi, avec peu d'effort, soit de trouver des contre-exemples pour les cas d'émission multiples de signaux, les cas de lecture avant écriture, les cas de dépassement... soit de prouver que l'implémentation est sure de ce point de vue - ce qui déjà n'est pas négligeable.

            Toujours dans ce projet, certains sous-modules qui s'y prêtaient ont été prouvés formellement. Comme souligné plus haut, cela signifie que selon les contraintes d'entrées qui ont été définies, le sous-module ne viole aucune des propriétés décrites. Donc, si l'algorithme de preuve est sur-contraint pour quelque raison que ce soit, certains bugs peuvent ne pas être détectés. C'est arrivé dans ce projet, même les modules prouvés formellement en aval de la validation fonctionnelle usuelle, se sont vu trouver des bugs par la validation par stimulus pseudo-aléatoire. Mais force est de constater que ces modules prouvés formellement ont eu proportionnellement moins de bugs trouvés par la validation fonctionnelle que les autres en regard de leur complexité.

            Enfin, de mon point de vue, l'atout maître de la preuve formelle, est la preuve d'équivalence lors de l'optimisation d'un module. Elle permet de prouver que deux implémentations sont formellement équivalentes, et donc de remplacer en confiance l'implémentation naïve initiale, qui a le mérite d'être claire et lisible, par la version optimisée.

            En conclusion, la preuve formelle c'est un nouvel outil pour la validation de code. C'est un outil puissant, complémentaire aux autres formes de validation, et, comme tout outil, il faut savoir l'utiliser à bon escient et en connaître les limites.
            • [^] # Re: mouais

              Posté par . Évalué à  2 .

              tu travaillais ou avec Esterel ? Chez TI ?

              "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

              • [^] # Re: mouais

                Posté par . Évalué à  3 .

                Oui, je travaille à TI.

                Pour en revenir au sujet initial, notre but a été d'utiliser Esterel comme spécification exécutable et donc d'utiliser le même formalisme dans toutes les étapes du projet, depuis la description fonctionnelle (spécification) jusqu'à la génération du RTL (en Verilog / VHDL), dans le but de minimiser les interventions humaines, sources d'interprétations et d'erreurs.
                • [^] # Re: mouais

                  Posté par . Évalué à  2 .

                  Et maintenant que la société est en faillite, vous allez faire comment ?

                  "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

      • [^] # Re: mouais

        Posté par . Évalué à  3 .

        Personne n'a jamais dit qu'un ordinateur ferait tout le boulot à ta place.
        Si, certains l'ont dit ou le pensent très fort ...
  • # prouveur automatique/assistant de preuve

    Posté par . Évalué à  2 .

    Il n'existe pas de vrai prouveur automatique utilisable. Donc si on veut prouver des choses à l'aide de logiciels, on a deux choix:
    - faire un prouveur automatique de trucs très simple ;
    - faire un logiciel intéractif qui permet, avec le cerveau de l'utilisateur, de prouver des trucs compliqués.

    Un assistant de preuve, c'est la seconde approche. Si tu veux montrer « A et B », il va te demander de prouver « A » puis de prouver « B ». Je connais des personnes qui font de la preuve d'algorithmes pour l'arithmétique flottante et avoir un logiciel qui « n'oublie pas » de cas, c'est précieux. Par ailleurs, un assistant de preuve permet de démontrer automatiquement des morceaux de preuves, ce qui rend la vie de l'utilisateur (un peu) plus facile.
    • [^] # Re: prouveur automatique/assistant de preuve

      Posté par . Évalué à  2 .

      Tu pourrais nous expliquer le genre de code qui est fournis à un assistant de preuve, par exemple, en utilisant du pseudo code ?

      Dans le milieu de l'aéronautique, il est souvent question de comparaison de modèles et de confrontation d'interprétation de spec entre 2 équipes utilisant des outils différents. Donc, on a une équipe qui développe le programme et l'autre un modèle sous une autre forme. On compare ensuite les résultats de tests définit par avance par l'équipe de test (mais qui pourrait être généré automatiquement par classe d'équivalence des entrées et couverture de code)

      Le but serait ici de facilité la vie de la deuxième équipe.

      "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

    • [^] # Re: prouveur automatique/assistant de preuve

      Posté par (page perso) . Évalué à  1 .

      Moi je dirais qu'il n'en existe pas encore, mais théoriquement, je vois pas ce qui l'empêche. Y a déjà des travaux qui sont fait pour virtualiser le réseau neuronale d'un cerveau humain, et donc, à priori, de faire penser ce cerveau comme celui d'un être humain. À partir de là, tu remplaces ton utilisateur physique par cet utilisateur virtuel, et hop…

      Cela dit, ce serait peut être prendre le canon pour dégommer la mouche.
      • [^] # Re: prouveur automatique/assistant de preuve

        Posté par . Évalué à  6 .

        Moi je dirais qu'il n'en existe pas encore, mais théoriquement, je vois pas ce qui l'empêche.
        Théoriquement, il est prouvé depuis longtemps qu'il n'existe pas d'algorithme permettant entre autres, et pour n'importe quel programme en entrée:
        - de déterminer si ce programme s'arrête
        - de déterminer si ce programme fait la même chose qu'un autre programme
        - et par extension de déterminer si ce programme est conforme à sa spécification

        Donc tous les prouveurs qu'on pourra écrire seront limités, non autonomes ou non déterministes.

        En poussant ton approche plus loin on peut même observer que si la conscience humaine est simulable sur ordinateur, alors un humain ne peut pas non plus prouver toutes ces choses.
        • [^] # Re: prouveur automatique/assistant de preuve

          Posté par . Évalué à  2 .

          Tu parles quand même dans un cadre très général bien loin des cas pratiques.

          - de déterminer si ce programme fait la même chose qu'un autre programme

          Dans le cas général.

          Parce que c'est justement dans ce domaine là que les prouveurs formelles sont utilisés industriellement à grande échelle. On appelle cela les "equivalence checker". C'est un outil du domaine de l'EDA qui permet de s'assurer qu'une mer de portes générées par un synthétiseur est équivalent au code source HDL.

          - et par extension de déterminer si ce programme est conforme à sa spécification

          Il faut encore savoir ce qu'est une spec. Souvent, c'est super flou et pas clair. Le client veut que le produit réponde à son problème et ne plante pas, par contre, il ne sait pas forcément bien le définir. C'est plus un problème d'ingénierie logiciel que de preuves mathématiques.

          "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

          • [^] # Re: prouveur automatique/assistant de preuve

            Posté par (page perso) . Évalué à  5 .

            >>et par extension de déterminer si ce programme est conforme à sa spécification
            >Il faut encore savoir ce qu'est une spec

            D'après le théorème de Kleene, il n'existe pas d'algorithme capable de prouver qu'un algorithme vérifie une propriété non triviale.

            Il n'y a pas à tortiller, si la "spec" est "le programme termine sur l'entrée 16 en temps 64", c'est trivial, si c'est "le programme calcule factorielle", c'est indécidable. Les specs que tu veux vérifier, c'est parce qu'elles sont non triviales, donc quoi qu'il arrive, tu auras des cas où ton programme se gourrera ou juste ne répondra pas, même si la spec est parfaitement claire.

            > Dans le cas général.

            Il y a heureusement des cas où un humain ou un programme est capable de prouver qu'un programme vérifie une propriété, mais ce sont juste des cas particuliers ;)
            • [^] # Re: prouveur automatique/assistant de preuve

              Posté par . Évalué à  1 .


              Il n'y a pas à tortiller, si la "spec" est "le programme termine sur l'entrée 16 en temps 64", c'est trivial, si c'est "le programme calcule factorielle", c'est indécidable. Les specs que tu veux vérifier, c'est parce qu'elles sont non triviales,


              Non, c'est aussi parce que le programme est gros.

              Tu veux vérifier que tu ne t'es pas planté dans la copie d'une équation, dans la recopie d'une constante, que tu n'as pas de cas ou tu core dump.

              "le programme calcule factorielle"

              Sauf que ta spec ne dira pas ça. Il dira factoriel selon l'algo bidule précis à 10^-14 en code double flottant. De toute façon, je vois mal factoriel comme étant une fonction de base de ton logiciel de preuve.

              La "preuve" sera l'équivalence à x^-14 prêt entre l'équation mathématique de la spec et ton code (souvent des développements limité).

              Mais pour le cas de factoriel, le test tel que définit par la DO-178B demande de couvrir les classes d'équivalences, ce qui va se réduire à tester un nombre négatif, zéro, un nombre positif, voir les nombres max et min du range spécifié, et le range+1 pour voir que cela ne plante pas. 7 tests en tout pour vérifier l'équivalence à 10^-14 prêt et pour avoir la certif de ton avion.

              Si tu fais quelques milliers de test en random() en plus, c'est encore mieux (mais la certif s'en fout). Les partitions par classe d'équivalence fonctionnent en test boite blanche quand tu connais la tête du code et que tu voix bien qu'il n'y a pas de branchement. De toute façon, à l'exécution du test, tu vérifies la couverture de code.

              Certe tu n'auras pas prouver l'équivalence entre spec et code mais tu auras une grande confiance, ce qui est le principale.

              "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

              • [^] # Re: prouveur automatique/assistant de preuve

                Posté par (page perso) . Évalué à  2 .

                > Sauf que ta spec ne dira pas ça. Il dira factoriel selon l'algo bidule précis à 10^-14 en code double flottant.
                > La "preuve" sera l'équivalence à x^-14 prêt entre l'équation mathématique de la spec et ton code (souvent des développements limité).

                Tu sais que factorielle est une fonction à valeurs entières ? Il n'y a même pas d'erreur sur les entiers... Alors faire des développements limités pour prouver sa validité...

                > Mais pour le cas de factoriel, le test tel que définit par la DO-178B demande de couvrir les classes d'équivalences, ce qui va se réduire à tester un nombre négatif, zéro, un nombre positif, voir les nombres max et min du range spécifié, et le range+1 pour voir que cela ne plante pas. 7 tests en tout pour vérifier l'équivalence à 10^-14 prêt et pour avoir la certif de ton avion.

                Si ton programme ne répond pas en 3 jours pour MAX_INT, tu en déduis qu'il ne calcule pas factorielle ? Parce que, seulement 7 tests, pourquoi pas, mais si tu ne prouves pas que chaque test termine, ça ne rend pas le problème suffisamment trivial pour être décidable.
      • [^] # Re: prouveur automatique/assistant de preuve

        Posté par . Évalué à  6 .

        A vrai dire, le théorème d'incomplétude de Gödel a prouvé en 1931 l'inexistence d'un système à la fois consistent et complet pour l'arithmétique. Alors si on ne peut pas prouver l'arithmétique, on ne risque pas de prouver des cas plus compliqués (comme les langages de programmation Turing-complets utilisés majoritairement, et même des langages plus simples).

        Les réseaux neuronaux ne vont pas aider. Ils pourraient se baser sur des heuristiques (ce que fait l'homme), mais comment distinguer ce qui est formellement prouvé par les règles d'inférence (réécriture) de ce qui est supposé par exploration?

        Ce que l'homme est capable de faire, et que l'ordinateur ne peut pas faire, c'est sortir du système de types (aller dans une couche "méta" sur demande). Il existe des classes computationnelles où les algorithmes de preuves sont tractables (voire simplement décidables) mais ce sont des cas restreints et peu pratiques pour l'informatique "réelle".

        Donc, effectivement, théoriquement, il y a quelque chose qui les empêche. Si on reste dans le cadre formel. Après, si on s'en fout que l'ordinateur dise n'importe quoi, oui on peut, mais autant faire une sortie aléatoire qui dit vrai ou faux.
        • [^] # Re: prouveur automatique/assistant de preuve

          Posté par . Évalué à  1 .

          "Il existe des classes computationnelles où les algorithmes de preuves sont tractables (voire simplement décidables) mais ce sont des cas restreints et peu pratiques pour l'informatique "réelle"."

          En refactorant cette phrase, problème de consistance :)....... je voulais dire :

          "Les preuves sur la majorité des classes computationnelles de l'informatique "réelle" sont intractables, voire indécidables."
        • [^] # Re: prouveur automatique/assistant de preuve

          Posté par (page perso) . Évalué à  1 .

          Je ne suis pas d'accord avec ton approche «Ce que l'homme est capable de faire, et que l'ordinateur ne peut pas faire». À partir du moment où je reproduit le shéma neuronale d'un cerveau humain dans un logiciel, je ne vois pas ce qui ferait que l'un soit incapable de faire virtuellement ce que l'autre fait physiquement.

          Ok, on a pas encore de machine capable de faire ça, mais à ne pas en douter, ça va venir. C'est même le genre de réflexion qui terrifie [[Bill Joy]] (et paf le cheminl'argument d'autorité).

          Bon, sinon, je vois plusieurs réflexions sur le fait que la preuve d'un programme ne peut être fait de manière générale, et alors ? Du moment qu'elle le fait au moins aussi bien que le ferait un humain et en plus rapide, ça vaut le coups non ? Qu'est-ce qu'on en à faire que notre programme ne réponds pas au contrat dans des cas ultra rares auquel on aurait pas pensé soit même ? Dans le pire des cas, le cas rare ce produira et le malchanceux fera un rapport de bogue. La majorité des logiciels ne sont pas destinés à lancer des fusés ou guider des avions hein.

          Cela dit, je comprends bien l'aspect branlette intellectuelle, la satisfaction que ce serait de ce dire que son logiciel est «parfait», qu'il tourne tip-top sur son OS micro-noyau écrit en ADA. Mais bon avoir un OS à noyau monolithique qui répond bien à mes besoins concrets, c'est déjà pas si mal.
          • [^] # Re: prouveur automatique/assistant de preuve

            Posté par . Évalué à  1 .

            Bon, sinon, je vois plusieurs réflexions sur le fait que la preuve d'un programme ne peut être fait de manière générale, et alors ? Du moment qu'elle le fait au moins aussi bien que le ferait un humain et en plus rapide, ça vaut le coups non ?

            En pratique ce n'est pas le cas, on passe beaucoup de temps à s'arracher les cheveux pour comprendre pourquoi le prouveur automatique n'ai pas capable de faire ce truc qui a l'air trivial...

            Après oui effectivement il y a des techniques «pousse-bouton» qui ne font que chercher a trouver des bug sans chercher l'exhaustivité et cela peut faire gagner pas mal de temps. Mais cela nécessite quand même d'écrire une spécification formelle et c'est souvent la dessus que les gens ont du mal.
          • [^] # Re: prouveur automatique/assistant de preuve

            Posté par . Évalué à  3 .

            À partir du moment où je reproduit le shéma neuronale d'un cerveau humain dans un logiciel, je ne vois pas ce qui ferait que l'un soit incapable de faire virtuellement ce que l'autre fait physiquement.

            On ne sait pas ce qu'est la conscience humaine. Si c'est seulement une propriété émergente de l'agencement des atomes du cerveau, alors je suis d'accord, mais il y a des gens sérieux qui contestent ça, par exemple Penrose.

            Qu'est-ce qu'on en à faire que notre programme ne réponds pas au contrat dans des cas ultra rares auquel on aurait pas pensé soit même ?

            Tu supposes que dans tous les cas utiles/pratiques on peut prouver des choses (manuellement ou automatiquement). Ça reste à voir.

            Après, réfléchir à ce qu'on peut prouver et ce qu'on ne peut pas prouver, ce n'est pas de la branlette intellectuelle, et ça ne sert pas seulement à dire "je ne peux pas, donc je n'essaye pas". Ça sert aussi à savoir quelles sont les choses auxquelles je dois renoncer si je veux avoir une preuve solide.
            • [^] # Re: prouveur automatique/assistant de preuve

              Posté par (page perso) . Évalué à  1 .

              Si c'est seulement une propriété émergente de l'agencement des atomes du cerveau, alors je suis d'accord, mais il y a des gens sérieux qui contestent ça, par exemple Penrose.

              Je veux bien lire l'argumentation de ce monsieur, parceque je suis curieux de savoir ce qui peu le pousser à penser autrement mis à part de l'anthropocentrisme, et encore plus intéressant, voir s'il arrive à s'en sortir sans s'en prendre à la théorie de l'évolution.

              Je lis rapidement sur wikipédia que :

              Même s'il refuse la possibilité d'une intelligence ou d'une conscience pour une machine de Turing (et donc pour un ordinateur traditionnel), Penrose n'exclut pas la possibilité d'une intelligence artificielle, qui serait fondée sur des processus quantiques. Car selon lui, ce sont des processus quantiques et notamment le processus de réduction du paquet d'onde (qui ne peut être modélisé par un système formel, car - entre autres - fondamentalement indéterministe) qui entrent en jeu dans le phénomène de la conscience.


              Bah c'est très bien, on utilisera des ordinateurs quantique alors, voilà tout. :)
              • [^] # Re: prouveur automatique/assistant de preuve

                Posté par . Évalué à  3 .

                je suis curieux de savoir ce qui peu le pousser à penser autrement mis à part de l'anthropocentrisme

                Probablement qu'il rejette certaines implications philosophiques du matérialisme. L'esprit humain a l'air non déterministe, et ça nous arrange bien de penser qu'on a du libre arbitre. Mais si on est simulables par un ordinateur déterministe, que devient notre libre arbitre ? Si on me simule plusieurs fois de suite dans les mêmes conditions, vais-je prendre à chaque fois les mêmes décisions ? Etc.
                • [^] # Re: prouveur automatique/assistant de preuve

                  Posté par . Évalué à  2 .

                  Et pourquoi pas ? Cela n'est jamais arrivé :/

                  "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                  • [^] # Re: prouveur automatique/assistant de preuve

                    Posté par (page perso) . Évalué à  2 .

                    Principe de sceptique : on en a pas la preuve, alors on en sais rien, inutile de platonifier :-)

                    Un pays bien organisé est celui où le petit nombre fait travailler le grand nombre, est nourri par lui, et le gouverne - Voltaire

                    • [^] # Re: prouveur automatique/assistant de preuve

                      Posté par . Évalué à  2 .

                      En science, tu n'auras jamais que des contres exemple de théorie, au mieux tu vérifies des prédictions, mais tu ne prouveras pas sa "vérité".

                      "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                      • [^] # Re: prouveur automatique/assistant de preuve

                        Posté par . Évalué à  2 .

                        Je dirai plutôt qu'un contre exemple à une théorie qui "marche" peut arriver à n'importe quel moment: ce n'est pas parce que je n'ai vu passer que des signes blancs que tous les signes sont blancs, c'est un exemple classique je crois.
                        • [^] # Re: prouveur automatique/assistant de preuve

                          Posté par (page perso) . Évalué à  2 .

                          Moi j'ai vu passer des signes de la main ainsi que des signes cabalistiques mais le vilain petit canard rejeton du cygne, ça... je l'ai écrasé. snif ====>[]
                        • [^] # Re: prouveur automatique/assistant de preuve

                          Posté par . Évalué à  3 .

                          C'est cohérent avec ce qu'il dit: la théorie "tous les cygnes sont blancs" peut seulement être réfutée par l'observation d'un contre exemple, mais ne pourra jamais être prouvée, quel que soit le nombre d'observations de cygnes blancs.
                          • [^] # Re: prouveur automatique/assistant de preuve

                            Posté par (page perso) . Évalué à  2 .

                            A ce propos, je vous conseille le "Cygne Noir" de Nassim Nicholas Taleb

                            Une review qui n'a pas l'air trop mal : http://www.bakchich.info/article2665.html
                            http://www.lesbelleslettres.com/livre/?GCOI=22510100957220
                            http://www.alternatives-economiques.fr/le-cygne-noir--la-pui(...)

                            Son site :
                            http://www.fooledbyrandomness.com/
                            Son itw sur France Culture (il est libano américain, mais il parle couramment français) :
                            http://www.fooledbyrandomness.com/franceculture.mp3

                            C'est le grand copain de Benoit Mandelbrot :)

                            Un pays bien organisé est celui où le petit nombre fait travailler le grand nombre, est nourri par lui, et le gouverne - Voltaire

                          • [^] # Re: prouveur automatique/assistant de preuve

                            Posté par . Évalué à  3 .

                            Non mais n'importe quoi :)
                            1) on n'observe pas les contre-exemple et 2) on ne prouve pas les cygnes...

                            Les cygnes font partit du monde réel, donc si on a une théorie (tous les cygnes sont blanc) on fait des expériences et des observations pour la vérifier (exemple: biologie, physique)

                            Maintenant si on en science hypothéco-déductive (mathématique, informatique) on pose des définitions (on appelle un cygne un oiseau aquatique de couleur blanche) et après on en déduit des propriétés avec des démonstrations et des contre-exemple.

                            Mais on mélange pas tout :)

                            De plus on peut manipuler des raisonnements à l'infini, ce n'est pas un problème.

                            Et pour les tests on cite toujours Dijkstra d'habitude:
                            "Program testing can be used to show the presence of bugs, but never to show their absence!"
                            http://en.wikiquote.org/wiki/Edsger_W._Dijkstra
                            • [^] # Re: prouveur automatique/assistant de preuve

                              Posté par (page perso) . Évalué à  1 .

                              Les cygnes font partit du monde réel, donc si on a une théorie (tous les cygnes sont blanc) on fait des expériences et des observations pour la vérifier (exemple: biologie, physique)
                              Tu raisonnes en médiocristan (de médio, milieu): le cygne a longtemps été perçu comme forcément de couleur blanche.
                              On en a donc établi une règle, par "expériences et observations".
                              Or un jour on a découvert l'existance de cygnes noirs (en 1790).

                              Moralité : faire attention au scientisme platonifiant, on effectue un peu trop vite de belle conclusions qui ont toutes le visage de la belle démonstration scientifique.

                              Un pays bien organisé est celui où le petit nombre fait travailler le grand nombre, est nourri par lui, et le gouverne - Voltaire

                              • [^] # Re: prouveur automatique/assistant de preuve

                                Posté par . Évalué à  2 .

                                Je ne décrit juste que la méthode expérimental [[Méthode_scientifique]]

                                wikipedia:

                                La méthode expérimentale est souvent constituée des 8 étapes suivantes :

                                1. Préciser la question
                                2. Recueillir des informations et des ressources (observer)
                                3. Forme des hypothèses
                                4. Effectuer l'expérience et de recueillir des données
                                5. Analyser les données
                                6. Interpréter les données et tirer des conclusions qui serviront pour valider ou infirmer les hypothèses et peut-être aussi comme de point de départ pour de nouvelles hypothèses
                                7. Publier les résultats
                                8. Reproduire les expériences (souvent fait par d'autres scientifiques)


                                Il s'agit évidement de théorie sur le monde réel, pas les mathématiques.

                                "La liberté de tout dire n'a d'ennemis que ceux qui veulent se réserver le droit de tout faire". "La question n'est pas de savoir si vous avez quelque chose à cacher. La question est de savoir si c'est nous qui contrôlons le gouvernement ou l'inverse

                            • [^] # Re: prouveur automatique/assistant de preuve

                              Posté par . Évalué à  3 .

                              1) on n'observe pas les contre-exemple

                              Un contre-exemple est un exemple qui contredit une hypothèse. Par conséquent, si j'émet l'hypothèse "tous les cygnes sont blancs", et que je croise un cygne noir, j'observe un contre-exemple.

                              2) on ne prouve pas les cygnes.

                              Et c'est pour ça que j'ai parlé de prouver la théorie "tous les cygnes sont blancs". On prouve (enfin, on conforte) des théories.

                              Ensuite, naturellement, Dijkstra est toujours pertinent, et ici si on veut se ramené à nos histoires de sciences expérimentales, avec les tests de programmes on teste l'hypothèse "ce programme n'a pas de bugs". Les tests peuvent la réfuter, mais jamais la prouver.
                • [^] # Re: prouveur automatique/assistant de preuve

                  Posté par . Évalué à  4 .

                  Je fais partie des personnes persuadées que notre cerveau n'est qu'un bête tas de particules comme n'importe quel autre tas de particules (un rocher, une étoile, un foie, une serviette éponge). Ce qui différencie les tas est l'arrangement des particules qui n'est pas le fruit du hasard mais celui de règles physiques (que nous ne connaissons pas totalement). Ca donne que notre cerveau n'a pas plus de "conscience-magique" qu'un fer à repasser. Une conscience certes (processus intellectuel), mais une "âme" et autres choses du même acabit, je rejette.

                  Cela fait qu'en gros, moyennant une machine suffisament puissante, on peut émuler un cerveau humain ou de flamand rose. Il faut bien entendu émuler les stimulis extérieurs. Ca ne garantie pas qu'à données d'entrées égales, la sortie soit égale. Pour la simple raison que certains processus sont basés sur des lois physiques qui donnent des résultats non déterministes. Le synapse 21575123021 caché dans un coin *pourrait* ne pas transmettre l'information de la même manière avec les mêmes données d'entrée.

                  Nous sommes là aux limites de nos connaissances actuelles: certains processus physiques donnent des résultats non déterministes pour l'éventuelle raison que nous ne connaissons pas les "vraies" lois. Nous connaissons des sortes de macro-lois, donc nous perdons de la précision, d'oû le non déterminisme.
                  Rien n'interdit que les "vraies" lois contiennent une bonne dose d'aléas. Cela ne nous donnera pas plus une âme, et dieu n'existera pas plus (je n'ai pas oublié la majuscule).
                  • [^] # Re: prouveur automatique/assistant de preuve

                    Posté par . Évalué à  2 .

                    Cela fait qu'en gros, moyennant une machine suffisament puissante, on peut émuler un cerveau humain

                    Ce qui a plein d'implications philosophiques rigolotes. Par exemple on peut facilement écrire un programme qui exécute tous les programmes possibles. Et donc, si on le laisse tourner suffisamment longtemps et avec suffisamment de mémoire, ce programme simulera toutes les consciences imaginables, y compris la mienne pendant que j'écris ça, mais aussi une version de moi où je n'écris pas ça.

                    On pourrait pousser encore plus loin et d'autres l'ont fait, voir entre autres les travaux de Bruno Marchal, ou bien le roman de Greg Egan, "permutation city".

                    Ca ne garantie pas qu'à données d'entrées égales, la sortie soit égale.

                    Si, parce qu'une machine de Turing est déterministe.

                    Nous connaissons des sortes de macro-lois, donc nous perdons de la précision, d'oû le non déterminisme.

                    Ça c'est la version du monde datant d'avant la découverte de la mécanique quantique: si on savait simuler avec assez de précision, alors le monde serait déterministe. La mécanique quantique affirme que le monde que nous observons est par nature non déterministe, et qu'il ne s'agit pas d'un problème de précision.

                    Ce qui ne veut pas dire que notre conscience est soumise à ça, car la mécanique quantique ne s'applique pas à notre niveau. Les histoires de Roger Penrose me semblent être une tentative de "sauver" le libre arbitre en ajoutant de l'aléa en ajoutant des "phénomènes quantiques" agissant sur nous. Ça me parait violer le principe d'Okham, mais pourquoi pas. Et Penrose est quelqu'un de fort respectable par ailleurs, donc ça mérite d'être considéré au moins un instant.
                    • [^] # Re: prouveur automatique/assistant de preuve

                      Posté par . Évalué à  2 .

                      on peut facilement écrire un programme qui exécute tous les programmes possibles
                      Emuler un cerveau nécessite certes un grosse puissance avec les moyens actuels, mais ça "loge" dans notre univers. Ca logera même très probablement dans une machine de bureau dans quelques années (10, 50, 200 ?).

                      En revanche exécuter tous les programmes possibles n'est pas faisable dans notre univers. Faute de temps (nombre de programmes infini, donc temps infini). Faute d'espace (taille infinie pour la plupart des programmes). C'est éventuellement faisable dans un univers englobant le nôtre. Tous les programmes possibles seront donc uniquement ceux concernant notre sous-univers.

                      Manara a illustré il y a bien longtemps une nouvelle (de lui peut-être) dans laquelle un être écrit tous les livres possibles. L'un d'eux est pile l'histoire qui est en train de se dérouler. Ca restait un pretexte pour dessiner des femmes nues, principale spécialité de ce dessinateur.
                      • [^] # Re: prouveur automatique/assistant de preuve

                        Posté par . Évalué à  2 .

                        J'aurais dû préciser que ce programme exécutant tous les programmes ne les exécutera pas jusqu'au bout pour la plupart. L'important est que si on lui offre suffisamment de ressources, il les exécute tous. C'est plus les implications philosophies qui sont intéressantes, et pas l'idée de le réaliser un jour :)

                        Pour faire cet énumérateur de programme, on ordonne les programmes par longueur, puis:
                        - x = 1
                        - t = 1
                        - on exécute t secondes de chaque programme de taille <= x
                        - on incrémente t et x
                        - on répète infiniment

                        À l'infini, on a exécuté tous les programmes. Évidemment c'est inatteignable par manque d'énergie pour faire tourner un ordinateur infiniment, mais par contre au bout de "longtemps" on aura probablement simulé toutes les consciences humaines vivantes aujourd'hui. Plus quelques autres.
                      • [^] # Re: prouveur automatique/assistant de preuve

                        Posté par . Évalué à  2 .

                        Pour la nouvelle illustrée par Manara, ça doit être au minimum inspiré de la nouvelle de Borges, "la bibliothèque de Babel", qui parle d'une bibliothèque contant tous les livres d'une certaine taille.
                  • [^] # Re: prouveur automatique/assistant de preuve

                    Posté par . Évalué à  2 .

                    certains processus physiques donnent des résultats non déterministes pour l'éventuelle raison que nous ne connaissons pas les "vraies" lois.

                    il a été prouvée que la physique quantique n'était pas une théorie de ce type, une théorie "à variable cachée" en terme physique (je donne les mots clés, je ne comprends pas la physique quantique en détail) ...

                    Ça veut dire que si la physique quantique est a peu prêt valable, elle est intrinsèquement non déterministe et pas la conséquence d'une théorie déterministe de plus bas niveau mais inconnue, de ce que j'en comprends.

                    Bon, je suis pas non plus sûr que ça implique qu'il n'existe pas une telle théorie dans l'absolu, mais c'est une pièce à verser au débat (et c'est vachement cool d'en débattre, surtout quand on y pige que dalle et qu'on écoute des gens qui maitrisent et qui savent en parler :) )
                    • [^] # Re: prouveur automatique/assistant de preuve

                      Posté par . Évalué à  3 .

                      Bon, je suis pas non plus sûr que ça implique qu'il n'existe pas une [théorie déterministe] dans l'absolu

                      En fait, si on prend l'interprétation "multivers" de la physique quantique, ça explique de manière élégante le non déterminisme que l'on observe. Mais je ne sais pas si j'arriverai à résumer ça clairement et succintement.

                      Dans cette interprétation, il existe une infinité d'univers parallèles. Par exemple, si je met un chat dans une boîte avec un dispositif qui peut le tuer ou pas aléatoirement, il existe plein d'univers parallèles dans lesquels j'ai fait ça. Tant que je n'ai pas ouvert la boîte, je ne sais pas si le chat est encore en vie. Au moment où j'ouvre, ces univers se répartissent en deux groupes: ceux dans lesquels le chat est mort, et ceux dans lesquels le chat est vivant. La proportion d'univers dans chaque groupe est ce que nous percevons comme la probabilité que l'évènement se produise.

                      Pourquoi ? Parce que le "moi" qui observe est dans un univers et un seul. Donc parmis tous ces univers, je suis dans un seul. La probabilité que le chat soit mort est égale à ma probabilité d'être dans un univers du groupe chat-mort, donc est égale à la proportion d'univers qui sont chat-mort.

                      Ça résoud le problème du non-déterminisme en ce sens que le multivers est déterministe, ce qui est assez satisfaisant du point de vue philosophique. Là où on voit du hasard, il ne s'agit en réalité que de proportion. Et on ne voit du hasard que parce que notre conscience n'observe qu'un univers à la fois.
                • [^] # Re: prouveur automatique/assistant de preuve

                  Posté par (page perso) . Évalué à  2 .

                  Je ne pense pas qu'on puisse avoir deux fois strictement la même situation, ça demanderais à ce que tout l'univers retrouve la même configuration identique, ce qui n'est pas à la porté de l'être humain. Le fait est que même en supposant l'esprit humain déterminable (déterministe?), les paramètres contextuels me paraissent trop vaste pour qu'on puisse déterminer précisément la moindre de tes réactions. Après pour faire de la manipulation des esprits, les super ordinateurs n'ont pas été attendu pour développer des méthodes qui rende des personnes enclines à croire/choisir certaines choses plutôt que d'autre.

                  Cela étant, avec un ordinateur quantique j'imagine qu'on doit pouvoir sortir du cadre déterministe, la physique quantique étant non-déterministe. Remarque qu'on peu tout à fait faire de même avec un ordinateur classique en insérant des données aléatoires; et non pseudo-aléatoire, par exemple random.org fournie des nombres aléatoires en utilisant les interférances atmosphérique il me semble).
          • [^] # Re: prouveur automatique/assistant de preuve

            Posté par (page perso) . Évalué à  2 .

            À partir du moment où je reproduit le shéma neuronale d'un cerveau humain dans un logiciel, je ne vois pas ce qui ferait que l'un soit incapable de faire virtuellement ce que l'autre fait physiquement

            Sauf qu'il y a plein de choses qui jouent, l'esprit étant lié au corps. Le système hormonal joue pour une grande part. Alors effectivement, on pourrait simuler tout ça en théorie, mais on est pas pour autant capable de trouver le programme qui permet de le simuler !

            Turing pensait que si nos pensées étaient des fonctions effectivement calculables, alors ont pourrait les calculer sur une machine de Turing. Il y a équivalence des fonctions, même si elles sont codées différemment. Mais avec ça on est bien avancé car même si c'est vrai, c'est trouver ce fameux programme qui paraît coton.

            Tout comme la conception de systèmes experts. On s'est rendu compte que l'humain utilise beaucoup de connaissances implicites qu'il n'arrive pas toujours à verbaliser. Partir sur un système de règles formelles est donc exclu car on arrive pas à produire toutes les règles. En marge du model cognitiviste, on a le model connexioniste qui essaye à partir de réseaux de neurones (ou autres models statistiques) de capturer les règles automatiquement. Mais cela nécessite un long apprentissage. De plus, il faut bien choisir une structure à ton réseau de neurones et ça va grandement influer sur tes résultats. Le cerveau a sélectionné des structures par évolution. Il faudrait donc un algo évolutionnaire pour construire des réseaux de neurones et les évaluer. Bon déjà, ça fait encore un algo à coder correctement pour y parvenir.

            Je ne sais pas où en sont les simulations artificielles de réseaux de neurones réels, mais ça m'étonnerait qu'ils prennent tout en compte. Le fonctionnement du cerveau est bien complexe (et pas totalement connu) et les interactions avec les autres parties du corps ne sont pas négligeables (rien que les entrées/sorties, déjà). Bref, y'a encore du boulot pour arriver à simuler l'intelligence humaine.
  • # Je te rassure

    Posté par (page perso) . Évalué à  3 .

    y'a encore des gens qui bossent sur la preuve de programme, et dans plein de domaines, comme les types linéaires, les bisimulations, l'interprétation abstraite, le model-checking…

    Je dirai même que ça se porte pas pire, comme domaine, mais que ça prend des bonnes brutes qui aiment l'alphabet grec en fin de DEA. C'est pas très sexe, c'est souvent contraire à l'image de l'informatique (comprendre "NTIC") que se font les gens, dans la mesure où les doctorants et chercheurs usent plus de papier brouillon que leur clavier…

    A part ça, tu peux éviter de faire des journaux intéressants où j'ai envie de répondre à tout le monde pendant des heures ?
    • [^] # Re: Je te rassure

      Posté par (page perso) . Évalué à  2 .

      A part ça, tu peux éviter de faire des journaux intéressants où j'ai envie de répondre à tout le monde pendant des heures ?
      Ben oui, mais j'aie bien vous faire discuter pendant des heures, ça compense les cours de fac que j'ai jamais eu ;-)

      Un pays bien organisé est celui où le petit nombre fait travailler le grand nombre, est nourri par lui, et le gouverne - Voltaire

Suivre le flux des commentaires

Note : les commentaires appartiennent à ceux qui les ont postés. Nous n'en sommes pas responsables.