Comme certains l'ont souligné, il n'y a que les méthodes formelles qui permettent d'obtenir des garanties fortes (ou du moins plus forte que le test ;-).
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.
# Quelques pointeurs sur les approches formelles
Posté par David Mentré . En réponse au journal couverture de code. É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.