Ben en fait dans l'ingénierie classique les méthodes formelles sont déjà la norme suffit de remplacer le terme «méthode formelle» par «résistance des matériaux» ou «thermodynamique» etc...
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 Joris R (site web personnel, Mastodon) . En réponse au journal La preuve de programme : où en est-on ?. É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