le cas simple:
1. if (a == 0)
2. do_a();
3. else
4. do_b();
Dans ce cas, si je couvre les lignes 1, 2 et 4, j'ai couvert tout mon programme.
Un autre cas:
1. while( a < 15 )
2. do_something( a );
La, ca ne marche plus: si j'execute avec a = 14, j'aurai couvert tout mon programme (ligne 1 et 2) mais je pourrai toujours faire des bugs. On peut imaginer par exemple que la valeur a = -3 fasse literalement planter le bazar.:
int do_something( int a) {
return 15 / (a + 3);.
}
Donc en plus d'avoir une couverture de code, il faut encadrer les intervalles de valeur possibles de toutes les variables du programme. Et evidemment, il faut tester toutes les combinaisons possible. On peut imaginer:
int do_something( int a, int b) {
return 15 / (a + b);.
}
Il faut ici soit garantir que a sera toujours different de -b, soit tester conjointement toutes les valeurs de a et b.
Si on combine tout ca, on arrive a des tests exponentiels.
Conclusion 1 : meme avec la meilleure volonte du monde, il est difficile de tester completement un programme.
Cependant, les gars qui ont pense XP ne sont pas cons : ils mettent en avant le white box testing (transparent box serait plus approprie). Le developpeur titille son programme la ou il sait que celui-ci risque d'avoir mal. Couple avec une bonne couverture de test, on a qqch de tres fiable.
Finalement, le test et l'analyse des resultats reste un melange d'exhaustivite et d'appreciation personelle du developpeur.
Dommage, j'aimerai bien pouvoir apporter plus de preuves sur la fiabilite du code que j'ecris.
# Pas si simple...
Posté par Lucas . Évalué à 6.
Pour la vérification de la couverture, on ne regarde bien sûr pas que les lignes couvertures par les tests. On peut aussi chercher une couverture des chemins (où on regarde quels chemins d'execution ont été couverts dans le programme), ou une couverture des expressions (on peut vérifier que les 2 membres d'une expr booléenne ont été évalués au moins une fois à vrai et à faux, par exemple). Bref, il y a des tonnes de critères. Tu dois pouvoir trouver un cours sur le test sur le net.
Et puis, il ne faut pas oublier que la couverture n'est pas une fin en soi : elle doit être utilisée uniquement comme une mesure de la qualité du jeu de test.
L'utilisation à en faire est :
- écrire un jeu de test
- regarder sa couverture, analyser quels sont les points mal testés
- compléter le jeu de test en insistant sur les points mal testés, sans chercher de manière explicite à couvrir les lignes non couvertes jusqu'à maintenant
- regarder la couverture du jeu de test après modif
- ...
Il ne faut surtout pas chercher à obtenir 100% de couverture en regardant la couverture après chaque écriture de test !
Bon, c'est pas tout ça, mais j'ai cours.
[^] # Re: Pas si simple...
Posté par pifou . Évalué à 3.
Premièrement, avoir une couverture de test de 100% c'est super difficile, surtout avec un langage objet, puisqu'une méthode peut réagir de différentes manières selon l'état de l'objet. Essayer de couvrir tout le code d'une classe pour chaque état de l'objet reviendrait à explorer un arbre de possibilité infinie (ou du moins qui s'agrandit exponentiellement).
Deuxièmement, un test n'a selon moi un intêret que s'il est écrit avant le code qu'il doit tester cela afin d'éviter les biais logique du programmeur-testeur. Je trouve ça plus logique qu'on code une fonction à partir des spécifs (dont les tests peuvent faire partie) plutôt que l'inverse. C'est ce que préconise d'ailleurs la méthode XP.
Troisièmement, pour rejoindre ce qui est dit plus bas, si tu veux une preuve de la fiabilité de ton programme il faut utiliser des méthodes formelles. Personnelement je trouve les langages à spécifications formelles (Coq, PWS, B, Z ...) fastidieux et surtout très eloignées des connaissances actuelles des programmeurs (surtout niveau mathématique). Je suis plutôt partisant de l'ajout de formalisme simple dans les programmes, comme par exemple le propose Eiffel avec ses pre/postcondition et invariant (on trouve des équivalents dans les langages plus communs comme Java). Cela permet en deux mots de spécifier plus formellement ce qu'une méthode est censé faire (=~postcondition) d'après ce qu'on lui passe comme paramètres (=~precondition). On peut voir ça comme une signature sémantique de la méthode (à comparer à la signature syntaxique classique (type de retour, type des paramètres)).
En utilisant un système de test avec des contrats, on peut arriver à gagné un peu de confiance dans son application. Sauf que rien ne dit qu'on a bien écrit nos tests ou nos contrats (je ne parle même pas du code:). J'ai pu pendant mes études tester un outil assez sympas pour justement faire des "tests" de "robustesse" de tout cela. Il s'agit de générer des mutants (déformation de la sémantique du code, par exemple remplacer un + par un -) dans le code et de lancer les tests dessus. À l'execution, si tes tests et contrats sont bien écris ils devraients détecter les erreurs, dans le cas contraire c'est qu'ils sont mal définis. Pour en revenir à la couverture des tests, on se rends compte avec cette méthode qu'on détecte rapidement les endroits non testés : ce sont les endroits où le plus de mutants restent vivants (le programme continue de s'executer ou s'est planté).
Le problème, c'est que je ne suis pas sûr que les techniques d'analyse de code par mutation soient sortit des labos de recherche :/. J'avais personnelement essayé JMutator de l'équipe Triskell de l'IRISA à Rennes. C'est dommage, j'avais trouvé ça plutôt puissant même si c'était un peu long (pour avoir des données significatives il faut générer beaucoup de mutants, et dans JMutator chaque mutant correspond à une nouvelle compilation d'une classe Java).
Pour conclure, il n'existe pas de méthodes miracles, c'est à toi de trouver la solution correspond le mieux à tes besoins.
[^] # Re: Pas si simple...
Posté par Philippe F (site web personnel) . Évalué à 2.
Je ne suis pas d'accord. Le principe de la programmation objet est bien d'isoler les composants de facon a pouvoir les faire evoluer de facon autonome. Le corollaire, c'est que tu peux aussi les tester de facon autonome et donc de facon relativement finie.
S'il y a des conditions difficile a reproduire, c'est peut-etre aussi celle-la qui peuvent s'averer dangereuses. Par exemple, j'ai un protocole de communication sans-contact. C'est dur de simuler la perte de paquet dans le protocole, mais c'est hyper important de le faire, quitte a modifier un peu l'architecture de la gestion du protocole.
> Je trouve ça plus logique qu'on code une fonction à partir des spécifs
Dans le monde ideal, c'est comme ca. Dans le monde reel, il faut s'adapter. Moi je preconise deux approches:
- une approche black-box ou le testeur se base sur les specifs et test ce qui lui parait le plus important
- une approche transparent box ou le developpeur titille son programme la ou il sait que ca peut faire mal. Dans l'exemple que j'ai donne plus haut, un testeur ne pensera pas forcement a tester avec a = -b mais le developpeur lui saura que c'est une valeur cle a verifier.
Le plus proche d'un outil de couverture de code et couverture de chemin d'execution, c'est le cerveau du programmeur. Faire des tests uniquement en black-box (a partir des specifs), c'est se passer de cet outil.
> Il s'agit de générer des mutants
Super idee. Je vais chercher des references et voir si je peux mettre ca en pratique. En c, ca va etre un peu lourd...
[^] # Re: Pas si simple...
Posté par LeMagicien Garcimore . Évalué à 2.
Je ne suis pas (du tout) convaincu que l'ajout d'invariant et de post/preconditions constitu une preuve formelle. Elle est encore bien dépendante de ton banc de test. Ce n'est donc pas une preuve, au plus un outil de test avancé.
[^] # Re: Pas si simple...
Posté par Snark_Boojum . Évalué à 1.
Ils ne permettent pas de prouver a priori que le code n'a pas de bogue . Par contre ils augmentent largement l'efficacité des tests.
Snark
# pas une preuve
Posté par Lucas . Évalué à 4.
Et puis un test n'est pas une preuve que le programme est correct, juste un moyen de trouver des erreurs...
[^] # Re: pas une preuve
Posté par Olivier Grisel (site web personnel) . Évalué à 3.
Mais meme si un tel systeme te permet de prouver que ton programme suit exactement le specs, rien ne prouve que les specs ne comportent pas de 'bugs' (erreurs, comportement pas prévu), meme si en théorie les specs doivent etre plus simple à comprendre que le programme lui meme.
[^] # Re: pas une preuve
Posté par kolter (site web personnel, Mastodon) . Évalué à 2.
La méthode B : http://www.atelierb.societe.com/(...)
ça se fait avec un AGL qui tourne entre autre sous Linux mais qui coûte super cher ...
fonctionnement : en gros tu lui donne des spécifications (très mathématique : thérories des ensemble et relations, pas trop compliqué), l'AGL essaye de prouver qu'elles sont exactes, ensuite il faut rapprocher les specs de structure plus "informatiques" : c'est l'implémentation, et une fois que l'AGL
arrive à prouver que les specs et la pseudo implémentation sont prouvées, il te pisse le code en C/ADA/... avec makefile et tout le toutim et t'as du code prouvé ... (pas besoin de faire de test)
ça c'est la thérorie....
/!\ : rien que le fait d'évoquer cet méthode va faire frémir certains d'entre vous...
m'enfin ça me rapelle quelques souvenirs...
M.
[^] # Re: pas une preuve
Posté par Olivier Serve (site web personnel) . Évalué à 2.
Heureusement que l'examen ne portait pas dessus...
Je ne sais pas si ce sont les explications qu'on a reçu ou bien si on était trop peu habitué, mais je m'en souviens comme d'une usine à gaz qui accouche d'une souris (normalement ce sont les montagnes mais là non ;) ).
[^] # Re: pas une preuve
Posté par Yaourt . Évalué à 1.
Tes tests de couverture fonctionnelle permettent de s'assurrer que dans un scénario "normal", ton appli va faire ce qu'elle doit faire.
Ce scénario va aller + ou - loin dans les cas aux limites, mais ca restera des cas prévus.
Pour s'assurrer qu'un code fait ce qu'il doit faire dans le cadre général, je ne connais que la preuve formelle... mais ceci réveille en moi que de mauvais souvenirs ...
[^] # Re: pas une preuve
Posté par ckyl . Évalué à 3.
En montrant que ton test fonctionne, tu as prouvé que ton code fonctionnait pour *une* valeure. Wahou c'est super génial mais on va pas aller loin avec ca.
Il permet de detecter les erreurs, de plus en s'amusant a faire passer les tests par classes d'equivalence on obtient un peu plus de certitude.
Mais ca ne prouve rien du tout. Prend une methode qui calcul la racine carre d'un entier sur 32 bits. Pour *prouver* que ton code est bon par des tests il faut faire 2^32 tests... et qui verifie les resultats ?
Les tests permettent au mieux d'augmenté le niveau de confiance dans le code. Par ce qu'une division qui arrondie trop vite vers 0 & co c'est si vite arrivé...
[^] # Re: pas une preuve
Posté par iznogoud . Évalué à 2.
[^] # Re: pas une preuve
Posté par Philippe F (site web personnel) . Évalué à 3.
Moi j'interesse ici a la fiabilite (j'avais pas realise en ecrivant le journal, mais c'est vraiment le sujet). Comment prouver que l'appli ne fait jamais ce qu'elle ne doit pas faire. En gros, comment eviter a tout prix le segfault. Un utilisateur peut comprendre qu'une fonction ne fontionne pas bien. Mais un crash, ca reste incomprehensible et ca donne une tres tres mauvaise impression.
Apres, l'extension de "comment prouver que l'appli ne fait jamais ce qu'il faut pas meme quand on a la torture" peut etre vu comme "comment trouver le jeu de test qui torture l'appli suffisamment pour etre sur qu'elle resiste bien". On peut penser au cas simpliste du mec qui se code son strlen et qui est tout content parce que il marche. Sauf que quand tu lui passes un pointeur nul, paf, ca plante.
La preuve formelle, je ne connais que de nom mais apparemment, c'est tres difficile a conciler avec le travail quotidien du developpeur. Il faut y consacrer des resources et une intelligence non negligeable pour un resultat qui peut sembler minimal a cote de ce qu'on est capable de coder avec les memes resources.
Je developpe un OS pour carte a puce (proprietaire, mais aussi open source, cf jayacard.sf.net) et je voudrai etre sur qu'il est securise.
La technique de la mutation de code me parait une bonne approche. En plus de la couverture de code, ca permet de localiser des zones sombres. Je suis preneur d'autres trucs.
[^] # Re: pas une preuve
Posté par djano . Évalué à 1.
Il s'agit de polyspace:
http://www.polyspace.com(...)
J'en ai entendu parler lors d'un stage où la boite avait de grosse contrainte de fiabilité.
En gros d'après ce que j'en ai compris, ce logiciel vérifie le domaine des variables et s'assure qu'elles restent dans un certain intervalle, ainsi que le dereferencement de pointeur null, entre autres.
D'après la pub sur leur site, cela permet de vérifier statiquement des erreurs qui ne se voient normalement qu'à la compilation.
Il y a plus de détails sur leur site avec des livres blancs expliquant leur technique : http://www.polyspace.com/white_papers.htm(...)
Attention, il faut fournir quelques informations, mais tu peux mettre des informations bidons, cela marche aussi.
# Ca existe (enfin presque).
Posté par Anonyme . Évalué à 5.
http://www.cours.polymtl.ca/log2000/Intro_Z.pdf(...) http://www.ingenieurs-supelec.org/groupespro/automobile/MethodeB/sl(...) )
C'est dur, mais ca marche. En gros le principe est le suivant : tu spécifies tes opérations avec un langage formel (posé avec des définitions j'espère que tu est pas allergique aux maths) avec les pré et post conditions, invariants et compagnie.
En suite il y a des analyseurs qui te transforment ta spec en langage informatique - les transformations sont elles-même prouvées - , tu compile et tu a les parties de ton programme que tu voulais prouver.
Le hic, c'est qu'il faudrait que le compilateur et le système sur lequel ca tourne soient aussi prouvé, mais bon c'est déjà mieux qu'un truc écrit directement.
C'est pas fun, c'est pas facile, et en plus c'est pas optimisé du tout. Mais c'est la seule manière de faire du code prouvé.
En passant, n'oublie pas que les processeurs aussi ne sont pas complètement testés, et que l'on ne sait pas si 1 612 313 *3461 donne le bon résultat.
(en tout cas 1+1 chez moi ca marche)
# Un truc en C++ qui fait ca
Posté par Monsieur Flynn . Évalué à 1.
j'utilise déja CppUnit pour les tests unitaires ( d'ailleurs si quelqu'un utilise un truc mieux, je suis preneur ( et si quelqu'un utiliser Cppunit avec le runner Qt je suis preneur aussi, ca merde chez moi ;( )
mais j'aurais utilisé un truc de couverture de code pour avoir la totale
Cppunit/Valgrind/ couverture de code ...
j'avoue de pas encore avoir eu le courage de me bouger pour aller chercher sur google des lib de couverture de code en C++ ... alors si vous en utilisez :) ..
[^] # Re: Un truc en C++ qui fait ca
Posté par . Takhi . Évalué à 4.
phase 1: instrumenter le code pour qu'il fasse de l'analyse de coverage.
gcc ... -Wall -fprofile-arcs -ftest-coverage
phase 2:
utilise l'outil gcov fournit la plupart du temps avec le compilo.
trouvé vite fait:
http://www.network-theory.co.uk/docs/gccintro/gccintro_67.html(...)
NB: un autre outil est fournit avec gcc:
gprof qui est souvent utile pour faire du profiling de code .. et t'apercevoir que tu as encore omis un passage de std::string par reference ... ;)
[^] # Re: Un truc en C++ qui fait ca
Posté par Monsieur Flynn . Évalué à 1.
mais bon le problème c'est que la couverture de code en C++ ..
ca me sort les fonctions renommet à la sauce C ( donc un peu incompréhensible ) ...
et ca me trouvera pas si je fais des fonctions inline qui ne sont pas appelées ..
t'aurais pas un truc typiquement C++ ( je sais je sais je suis chiant )
[^] # Re: Un truc en C++ qui fait ca
Posté par . Takhi . Évalué à 1.
c'est vrai que c'est bete ce mangling..
gprof a comme option --demangle mais pas gcov..
il y a longtemps j'avais du utliser un trucoverage de chez numega mais j'etais plus accaparé par mes fuites mémoires que par ma couverture de code :-)
[^] # Re: Un truc en C++ qui fait ca
Posté par mdlh . Évalué à 2.
Dans un premier temps, n'utilise pas d'optimisations.
[^] # Re: Un truc en C++ qui fait ca
Posté par Philippe F (site web personnel) . Évalué à 2.
http://ltp.sourceforge.net/coverage/lcov.php(...)
http://www.semdesigns.com/Products/TestCoverage/CppTestCoverage.htm(...)
Bon, en fait, il n'y a pas grand chose.
J'ai decouvert au bout de 2 heures que ca fait partie de gcc, et ca me semble le plus robuste comme approche. Mais tu peux essayer les autres, ca peut etre interessant (enfin, ceux qui sont libres).
La methode bourrin ou tu pre-process tes sources et ou tu rajoutes des macros de couveture de code, tu peux aussi te la redevelopper a la main.
# exponentiel => indecidable
Posté par 태 (site web personnel) . Évalué à 3.
Apres, si tu veux aller plus loin, tu vas t'apercevoir que savoir si un programme fait bien ce que tu veux est indécidable, et là, ça devient vraiment embetant, mais encore une fois, il y a des gens que ca ne gene pas (les editeurs d'antivirus par exemple)
[^] # Re: exponentiel => indecidable
Posté par Matthieu Moy (site web personnel) . Évalué à 4.
Petit jeu: Calculer 2^64. (inspiré du célèbre problème de l'échiquier). En déduire le nombre d'opérations qu'il faut pour vérifier un programme a 64 variables si l'algo est en 2^nombre de variables. Convertir ce nombre d'opérations en temps (unité de temps laissée au choix du lecteur, entre la seconde et le million d'annéés).
Question 2: compter le nombre de variables dans un programme réél et refaire le calcul précédant.
Question 3: Programmer la suite de fibbonacci non optimisée, faire tourner le programme pour n = 1, n = 10, n = 100. Revenir poster un commentaire ici quand le dernier calcul sera terminé.
Conclusion: Revenir ici disserter sur le fait qu'un algo exponentiel, c'est pas grave, c'est juste inefficace.
En pratique, les algos de verif sont tous exponentiels dans le pire cas (et encore, la question est souvent indécidable), et la difficulté est de trouver le moyen de ne pas être dans le pire cas. Avec du model checking symbolique par exemple, des problèmes qui auraient mis des milliards d'années de calcul en model checking enumératif peuvent être résolu en une fraction de seconde (cf. le fameux papier 10^20 states and beyond). Mais ça ne veut pas dire que ça marchera toujours.
[^] # Re: exponentiel => indecidable
Posté par 태 (site web personnel) . Évalué à 1.
%ocaml
Objective Caml version 3.08.2
# (* fabriquons une fonction qui calcule 2^n,
comme je suis deforme, je l'appelle exp *)
let rec exp = function
| 0 -> 1
| n -> 2*(exp (n-1))
;;
val exp : int -> int = <fun>
# exp 3;;
- : int = 8
# exp 64;;
- : int = 0
Conclusion: 2^64 vaut 0.
Reponse 2 :
Une rapide demonstration par recurrence montre que pour tout nombre entier n superieur a 64, 2^n vaut 0.
Reponse 3 :
%ocaml
[..]
# let rec fibo = function
| 0 -> 1
| 1 -> 1
| k -> (fibo (k-1)) + (fibo (k-2))
;;
val fibo : int -> int = <fun>
# fibo 1;;
- : int = 1
# fibo 10;;
- : int = 89
# fibo 100;;
- : int = 277887173
En un temps certain
Remarque : une fonction de complexité linéaire en l'entrée qui mettrait le meme temps que fibo sur l'entree 1 mettra egalement le meme temps certain sur l'entree 277887173.
Donc les fonctions a complexité linéaire sont à proscrire ?
[^] # Re: exponentiel => indecidable
Posté par hocwp (site web personnel) . Évalué à 2.
$ clisp > (defun exp (n) (if (= n 0) 1 (* 2 (exp (1- n))))) > (exp 3) 8 > (exp 64) 18446744073709551616 > (exp 100) 1267650600228229401496703205376 > (exp 1000) 10715086071862673209484250490600018105614048117055 33607443750388370351051124936122493198378815695858 12759467291755314682518714528569231404359845775746 98574803934567774824230985421074605062371141877954 18215304647498358194126739876755916554394607706291 45711964776865421676604298316526243868372056680693 76'fin bon, ça ne fait pas avancer le schmilblik :)[^] # Re: exponentiel => indecidable
Posté par Matthieu Moy (site web personnel) . Évalué à 3.
Ben n'utilise pas un langage qui te faire croire ça pour un système dont tu veux prouver la fiabilité.
> Remarque : une fonction de complexité linéaire en l'entrée qui mettrait le meme
> temps que fibo sur l'entree 1 mettra egalement le meme temps certain sur
> l'entree 277887173.
Je comprends pas ce que tu veux dire. Fibo non optimisé n'est justement pas linéaire (je sais pas si le compilo CAML sait optimiser ça). Le truc avec fibo, c'est que sa complexité est linéaire en fonction de sa sortie, qui elle même est a peu près une exponentielle de son entrée. Donc, si tu veux utiliser fibo sur une entrée pas trop ridiculement petite (100, j'avais peut-être été optimiste, mais essaye avec 1000 si tu veux), il te faudra des milliards d'années de calcul (ou écrire la version de complexité O(n), pas bien difficile par ailleurs).
[^] # Re: exponentiel => indecidable
Posté par Vivi (site web personnel) . Évalué à 2.
[^] # Re: exponentiel => indecidable
Posté par 태 (site web personnel) . Évalué à 0.
Mais ce que je dis, c'est que le fibo optimisé sur une entrée pas démesurément grande (genre 277887173) prend un temps aussi démesuré.
Donc même un algorithme linéaire n'est pas raisonnable, seuls les algorithmes en temps constant sont viables.
[^] # Re: exponentiel => indecidable
Posté par Matthieu Moy (site web personnel) . Évalué à 2.
> grande (genre 277887173) prend un temps aussi démesuré.
Quand je dis "les algos de verif sont exponentiels", c'est en fonction de la taille du code (nombre de variables par exemple). Des programmes avec 100 variables, tu en vois tous les jours, et tu aimerais bien les verifier pour qu'ils n'aient pas de bugs. Mais tu connais beaucoup de programmes avec 277887173 variables ? (encore une fois, si le chiffre n'est pas assez grand, prend fibo(200))
Pour n'importe quel algo en cst * taille de l'entrée, si cst n'est pas trop grande, je sais que ça va toujours marcher, quelle que soit l'entrée que je lui donne, simplement parce que ma machine n'est capable de stoquer que des entrées de taille "raisonnables". (cst * mon disque dur de 40 Go / le nombre d'instructions que mon proc peut executer en 1 sec = un nombre raisonnable de secondes)
Toi, tu triches, tu mesure la complexité en fonction de la valeur de l'entrée, non de sa taille (c'est vrai que mon exemple de fibbo est un peu pousse au crime :-)
(note : si tu parles en valeur de l'entrée, les algos de crypto, factorisation en facteurs premiers, ... sont en général linéaires. Ce n'est pas ce qui se dit dans la littérature)
[^] # Re: exponentiel => indecidable
Posté par 태 (site web personnel) . Évalué à 2.
Neanmoins, sur 40 Go, tu peux mettre des nombres a 277887173 chiffres sans trop de problemes... Tu peux meme envisager 1000 fois plus
NB: bon, se focaliser sur le nombre que me donne caml (pour un algo fibo un peu ameliore bien sur, la aussi j'ai truandé) est une erreur, vu que ce résultat est faux (pour la meme raison que pour 2^64), la vraie valeur est de l'ordre de 2*10^20.
[^] # Re: exponentiel => indecidable
Posté par Matthieu Moy (site web personnel) . Évalué à 2.
> algo fibo un peu ameliore bien sur, la aussi j'ai truandé) est une
> erreur, vu que ce résultat est faux (pour la meme raison que pour
> 2^64), la vraie valeur est de l'ordre de 2*10^20.
Il me semblait bien que ça pétait bien plus fort que ça avant 100 aussi, ...
Question stupide au passage : Y'a pas moyen de faire faire les tests de débordement arithmétiques en CAML ? (comme en Ada)
[^] # Re: exponentiel => indecidable
Posté par inico (site web personnel) . Évalué à 1.
Comment un nombre superieur a 0 multiplié par lui meme 64 fois peut etre egale a 0 ?
En 4 ieme on manipule des nombres superieur a 2^100 alors si c'était égale a 0, je m'en serai aperçut avant.
[^] # Re: exponentiel => indecidable
Posté par Vivi (site web personnel) . Évalué à 2.
en OCaml l'arithmetique sur les entiers se fait modulo 2^31 (ou 2^63 sur les archis 64 bits).
Mais il existe des bibliothèques de calculs en précision arbitraire ...
# Éléments de réponse
Posté par Duncan Idaho . Évalué à 3.
http://www.sciences.univ-nantes.fr/info/perso/permanents/pmartin/AC(...)
Attention toutefois, autant nos profs adorent que l'on étudie ce qu'ils ont écrit, autant ils ont horreur de la repompe (certains ont même décidé de protéger leur cours par mot de passe...).
[^] # Re: Éléments de réponse
Posté par chl (site web personnel) . Évalué à 4.
Ca me fait doucement rire cette reaction, et cela pour 2 raisons:
1/ Un prof est payé par l'Etat, donc nous tous. Lorsqu'un developeur fait du code, son code appartient a son entreprise. Pourquoi cela devrait etre different pour les profs ?
2/ Combien de profs font des supports de cours en grande partie repompés d'autres livres ?
Les mots de passe sont a mon avis la pour que peu de gens s'appercoivent que leurs cours sont des recopies de livres, et non pas par peur d'etre repompés.
# Quelques pointeurs sur les approches formelles
Posté par David Mentré . Évalué à 2.
J'ai commencé à faire une liste des outils libres permettant de faire de la vérif formelle :
http://gulliver.eu.org/ateliers/fv-tools/index.html(...)
Les outils les plus intéressants pour l'instant me semble ACL2 et Why/Caduceus avec Coq (et Spin (pas libre, mais on a les sources et cela dure depuis/va durer pendant longtemps)).
Je suis en train d'essayer de les utiliser : work in progress.
C'est certain qu'utiliser ces outils, c'est pas de la tarte. Maintenant, je crois que ce n'est qu'avec ce type d'outil qu'on pourra améliorer nos softs.
Dommage que des outils intéressants comme ceux de Coverity ne soient pas libres. Ils sont plus accessibles pour le programmeur.
# Tests de regression
Posté par Alban Crequy (site web personnel) . Évalué à 2.
Source:
http://en.wikiquote.org/wiki/Linus_Torvalds(...)
http://www.ussg.iu.edu/hypermail/linux/kernel/9804.1/0149.html(...)
# RE: Pas si simple
Posté par soral78 . Évalué à 1.
Le B nous permet en effet de limiter la phase de test unitaire, et de sécuriser les phases de relectures/codage.
Par contre elle ne nous permet pas d'aller beaucoup plus loin en elle meme, car la sécurité repose sur le fait que le problème soit bien posé: Rien empèche le spécificateur d'oublier, de mal décrire, .... la description matématique du problème qui si elle est fausse donnera un comportement faux de manière prouvée. Ce que permet B c'est de ne pas se contredire....C'est bien mais inssufisant.
La stratégie complète pour un code de qualité suffisante pour laisser à la machine le soin de nos vies passe donc par:
1- Des relectures croisées, réalisées par des personnes "indépendantes", des différentes productions: la specification, la conception, les tests en passant par le code B ou autre language. Tout le cycle en V est inspecté.
2- Un jeux de test unitaire pour les parties non écrite en B, et fait par une autre personne que le développeur.
3- Un jeu de test de validation permettant de vérifier la "conformité" aux spécifications.
J'ajouterais que la description formel du problème est limité à des choses "relativement" simples, où il est raisonable d'envisager "toutes les situations" possible de fonctionnement.
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.