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 jardiland . Évalué à 5.
[^] # Re: Se passer des tests ...
Posté par ɹǝıʌıʃO . Évalué à 3.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 4.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
Mais lors d'une recherche de meilleur qualité, il n'y a pas d'autres solutions non ?
"La première sécurité est la liberté"
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 3.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 2.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 3.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
Ensuite, il faut aussi prouver le prouver, ce qui n'est pas gagné.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Ontologia (site web personnel) . Évalué à 5.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Se passer des tests ...
Posté par auve . Évalué à 1.
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 benoar . Évalué à 4.
[^] # Re: Se passer des tests ...
Posté par MrLapinot (site web personnel) . Évalué à 2.
[^] # Re: Se passer des tests ...
Posté par Axioplase ıɥs∀ (site web personnel) . Évalué à 2.
[^] # Re: Se passer des tests ...
Posté par Ontologia (site web personnel) . Évalué à 3.
- 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...
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 2.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 2.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Se passer des tests ...
Posté par ɹǝıʌıʃO . Évalué à 1.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 1.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Se passer des tests ...
Posté par TImaniac (site web personnel) . Évalué à 3.
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 Ontologia (site web personnel) . Évalué à 2.
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.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Se passer des tests ...
Posté par auve . Évalué à 6.
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 TImaniac (site web personnel) . Évalué à 0.
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.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 2.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Se passer des tests ...
Posté par TImaniac (site web personnel) . Évalué à 4.
Sinon joli le dérapage sur la forme.
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Axioplase ıɥs∀ (site web personnel) . Évalué à 3.
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 2PetitsVerres . Évalué à 2.
Tous les nombres premiers sont impairs, sauf un. Tous les nombres premiers sont impairs, sauf deux.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 2.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 4.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Se passer des tests ...
Posté par TImaniac (site web personnel) . Évalué à 2.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par TImaniac (site web personnel) . É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.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par TImaniac (site web personnel) . É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é.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par TImaniac (site web personnel) . Évalué à 2.
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 Nicolas Boulay (site web personnel) . Évalué à 1.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par TImaniac (site web personnel) . Évalué à 2.
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par TImaniac (site web personnel) . Évalué à 2.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Ontologia (site web personnel) . Évalué à 2.
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.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par TImaniac (site web personnel) . Évalué à 2.
Comme qui dirait, en théorie c'est faisable, mais ça marchera jamais en pratique.
[^] # Re: Se passer des tests ...
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par outs . Évalué à 1.
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 outs . Évalué à 1.
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 ɹǝıʌıʃO . Évalué à 2.
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.[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 1.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Se passer des tests ...
Posté par ɹǝıʌıʃO . É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.
[^] # Commentaire supprimé
Posté par Anonyme . Évalué à 1.
Ce commentaire a été supprimé par l’équipe de modération.
[^] # Re: Se passer des tests ...
Posté par ɹǝıʌıʃO . Évalué à 1.
Je dis simplement que la vérification est supérieure aux testsPour enchaîner surpour 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 Nicolas Boulay (site web personnel) . Évalué à 1.
"La première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par ɹǝıʌıʃO . Évalué à 3.
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 Nicolas Boulay (site web personnel) . Évalué à 1.
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 première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par ɹǝıʌıʃO . Évalué à 3.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par ɹǝıʌıʃO . É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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par ɹǝıʌıʃO . Évalué à 1.
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 Nicolas Boulay (site web personnel) . Évalué à 3.
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 première sécurité est la liberté"
[^] # Re: Se passer des tests ...
Posté par Ontologia (site web personnel) . Évalué à 2.
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.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Se passer des tests ...
Posté par TImaniac (site web personnel) . Évalué à 2.
[^] # Re: Se passer des tests ...
Posté par Antoine . Évalué à 2.
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 outs . Évalué à 2.
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 auve . Évalué à 5.
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 TImaniac (site web personnel) . Évalué à 10.
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 -mat . Évalué à 1.
[^] # Re: mouais
Posté par outs . Évalué à 2.
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 Nicolas Boulay (site web personnel) . Évalué à 4.
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 première sécurité est la liberté"
[^] # Re: mouais
Posté par allcolor (site web personnel) . Évalué à 1.
D'une manière général, la preuve, c'est génialDis par quelqu'un pour qui les démonstrations sont quelque-choses de surnaturelles, ça fait sourire ===========>[_o/]
[^] # Re: mouais
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: mouais
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Re: mouais
Posté par EzDaYo . Évalué à 7.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: mouais
Posté par EzDaYo . Évalué à 3.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: mouais
Posté par totof2000 . Évalué à 3.
Si, certains l'ont dit ou le pensent très fort ...
# prouveur automatique/assistant de preuve
Posté par fmaz fmaz . Évalué à 2.
- 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 Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Re: prouveur automatique/assistant de preuve
Posté par psychoslave__ (site web personnel) . Évalué à 1.
Cela dit, ce serait peut être prendre le canon pour dégommer la mouche.
[^] # Re: prouveur automatique/assistant de preuve
Posté par Yusei (Mastodon) . Évalué à 6.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
- 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 première sécurité est la liberté"
[^] # Re: prouveur automatique/assistant de preuve
Posté par 태 (site web personnel) . Évalué à 5.
>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 Nicolas Boulay (site web personnel) . É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 première sécurité est la liberté"
[^] # Re: prouveur automatique/assistant de preuve
Posté par 태 (site web personnel) . Évalué à 2.
> 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 smc . Évalué à 6.
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 smc . Évalué à 1.
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 psychoslave__ (site web personnel) . Évalué à 1.
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 outs . Évalué à 1.
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 Yusei (Mastodon) . Évalué à 3.
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 psychoslave__ (site web personnel) . Évalué à 1.
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 Yusei (Mastodon) . Évalué à 3.
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 Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: prouveur automatique/assistant de preuve
Posté par Ontologia (site web personnel) . Évalué à 2.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: prouveur automatique/assistant de preuve
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
"La première sécurité est la liberté"
[^] # Re: prouveur automatique/assistant de preuve
Posté par Thomas Douillard . Évalué à 2.
[^] # Re: prouveur automatique/assistant de preuve
Posté par allcolor (site web personnel) . Évalué à 2.
[^] # Re: prouveur automatique/assistant de preuve
Posté par Yusei (Mastodon) . Évalué à 3.
[^] # Re: prouveur automatique/assistant de preuve
Posté par Ontologia (site web personnel) . Évalué à 2.
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 :)
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: prouveur automatique/assistant de preuve
Posté par outs . Évalué à 3.
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 Ontologia (site web personnel) . Évalué à 1.
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.
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: prouveur automatique/assistant de preuve
Posté par Nicolas Boulay (site web personnel) . Évalué à 2.
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 première sécurité est la liberté"
[^] # Re: prouveur automatique/assistant de preuve
Posté par Yusei (Mastodon) . Évalué à 3.
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 Kerro . Évalué à 4.
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 Yusei (Mastodon) . Évalué à 2.
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 Kerro . Évalué à 2.
on peut facilement écrire un programme qui exécute tous les programmes possiblesEmuler 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 Yusei (Mastodon) . Évalué à 2.
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 Yusei (Mastodon) . Évalué à 2.
[^] # Re: prouveur automatique/assistant de preuve
Posté par Thomas Douillard . Évalué à 2.
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 Yusei (Mastodon) . Évalué à 3.
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 psychoslave__ (site web personnel) . Évalué à 2.
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 Dr BG . Évalué à 2.
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 Axioplase ıɥs∀ (site web personnel) . Évalué à 3.
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 Ontologia (site web personnel) . Évalué à 2.
Ben oui, mais j'aie bien vous faire discuter pendant des heures, ça compense les cours de fac que j'ai jamais eu ;-)
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.