Bonjour.
Ma question est simple : j'ai lu quelque part qu'il était impossible de prouver un programme trop gros avec les outils actuels.
En effet, j'ai déjà lu cet argument comme quoi les programmes assez petits pouvaient être testés, mais pas les gros.
Pourquoi cette impossibilité ?
Qu'est-ce que tu entends par gros programme ? En terme de fonctionnalités ? De taille en Mo (voire Go maintenant) ? En terme de nombre de lignes de code ? De complexité du code ? De complexité des tâches effectuées ? etc..?
Bonjour,
Tu as toi-même donné la réponse.
Il me semble que c'est en terme de capacité mémoire, mais je ne suis sur de rien...Envoyé par bzh_nicolas
En fait, j'ai lu cette affirmation plusieurs fois sur des sites du style pcinpact, clubic, dans des dossiers assez spécialisée, sur windows, ou singularity.
Il disaient notamment qu'un noyau de système d'exploitation était suffisamment petit pour pouvoir être prouvé en théorie. Je suppose que ca doit être en terme de quantité de mémoire occupée à l'éxécution ou de nombre d'instructions.
Bonjour,
Il doit y avoir un lien avec l'explosion combinatoire comme au échec ou pire au jeux de go.
Il y a même des économiste qui trouvant que les bugs dans la technologie en général coute trop cher on demandé à des mathématiciens si on pouvait corriger tout les bug une bonne fois pour toute avant livraison à l'utilisateur.
Leur réponse est non et ils y a des bug qu'on ne trouvera pas avant 1 millions d'année et même plus.
La conséquence c'est que pour trouver les bug il faut des testeurs que l'on nomme consommateurs et que l'on attrape avec de la pub qui cré des besoins.
Plus le système est complexe et plus il y a de bug don plus il faut de testeurs pour les trouver et le corriger.
être consommateur est donc une activité utile mais quelquefois dangereuse et même mortelle.
Bonjour.
Les seuls test que l'on peut faire sont triviaux: on ne peut tester que ce que l'on connaît.
On peut pallier dans une toute petite mesure à cette limite par l' imagination; mais elle aussi est limitée.
Alors?.... A mes yeux (de plus en plus limités eux aussi), comme la perfection est utopique ,la seule solution qui existe est(hélas) la réalité, le test en vraie grandeur, en sachant qu' on risque de se casser la g....
Professionnellement, j'ai eu l' occasion d'avoir à traiter les conséquences d'un bug pourtant trivial: le programmeur avait fait une division sans tester si le diviseur était zéro.... Je ne sais s'il avait jugé que ce cas ne pouvait se produire;cependant il s'est produit après deux ans de fonctionnement jusque là sans problème...
Et les failles dites de sécurité, qui causent tant de mises à jour quelque soit le système d'exploitation... Certaines proviennent du mauvais emploi d'instructions dangereuses (ex: printf en C, sans en limiter la portée).
Concernant la limitation de la portée des tests, il me vient toujours à l'esprit la cause du crash du premier vol d'Ariane 5: encore une erreur de programmation! Et pourtant, on n'envoie pas en l'air quelques milliards sans 'tests'.....
A+
Il n'y a que dans le dictionnaire où 'réussite' vient avant 'travail'.
Je ne parles pas de tests, mais de preuve formelle de programme, qui permet de démontrer mathématiquement la viabilité et fiabilité d'un programme.
Dernière modification par Philou67 ; 31/01/2011 à 10h26. Motif: Citation inutile
Si ça existait, ça se saurait depuis longtemps....
Il n'y a que dans le dictionnaire où 'réussite' vient avant 'travail'.
Bonjour,
Je ne sais pas s'il y a rapport :
Alt-Ergo, preuve automatique pour la certification de code critique
Alt-Ergo est un logiciel pour la démonstration automatique de théorèmes. Il est dédié à la preuve déductive de programmes, qui réduit la correction d'un programme par rapport à sa spécification à la validité d'une formule logique. En particulier, Alt-ergo est situé en bout de chaîne de plate-formes de preuve utilisées dans l'avionique. Selon la complexité des codes analysés, ce sont des milliers de formules qu'il faut prouver. Parce qu'il n'est pas envisageable de faire toutes ces preuves à la main, l'utilisation d'un outil comme Alt-Ergo est cruciale pour le passage à l'échelle de cette approche.
http://www.inria.fr/innovation/aeron...-code-critique
Bonjour,
J'ai entendu parlé d'un compilateur C (donc un truc assez gros), prouvé mathématiquement, mais je n'ai plus le nom en tête.
Cordialement,
ProgVal
