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