URL: https://linuxfr.org/users/montaigne/journaux/la-preuve-de-programme-o%C3%B9-en-est-on Title: La preuve de programme : où en est-on ? Authors: Ontologia Date: 2009年03月03日T01:09:36+01:00 Tags: génie_logiciel Score: 3 Je suis en train (d'essayer) de lire la thèse de J-C Filliâtre [http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz](http://www.lri.fr/~filliatr/ftp/publis/these.ps.gz) intitulée _Preuve de programmes impératifs en théorie des types_ L'objectif est simple : on pose des contrat pre et post sur un morceaux de code, on peut aussi poser des invariants au sein d'une boucle, et le logiciel ( [http://why.lri.fr/index.fr.html](http://why.lri.fr/index.fr.html) ) qui est tiré de cette thèse : * Prouve la complétude et l'adéquation des contrats au code * **Prouve que le code respecte les contrats** Plus fort que du test unitaire, de la preuve de contrat, c'est tout simplement impressionnant !* Je ne vais pas décrire le principe ici, j'ai trop peur d'avoir mal compris. En gros, le code impératif est traduit dans un code fonctionnel très propre et d'une sémantique très petite , la couverture et la complétude des contrats est ensuite vérifiée pour enfin générer une obligation de preuve qui peut être donnée à [Coq](http://coq.inria.fr/) (Logiciel d'assistance de preuve) ou un démonstrateur automatique comme [Alt-ergo](http://alt-ergo.lri.fr/). (En passant quelqu'un dans la salle saurait-il m'expliquer la différence entre assistant et démonstrateur automatique ?) Ca faisait longtemps que je connaissais ce travail, mais je pensais bêtement que ça ne faisait que de la vérification de cohérence de contrats, je crois que je vais vite tester ça... J'imagine que d'autres outils existent, mais je me demande s'ils ont une telle maturité.. Bref à quand des outils intégrés aux applications Java/J2EE ? ie. la complétude des contrats à poser est-elle véritablement problématique dans une utilisation courante en informatique de gestion ? La taille des programme à prouver est-elle limitée ? Les informations de sorties sont-elles exploitables ? Tout cela pour dire, que même si des outils comme Coq resteront incompréhensible pour le grand public, je pense que des outils comme caduceus ou Krakatoa (respectivement l'adaptation de why à C et Java) ont un grand avenir devant eux, il manque peut être des les packager, des les intégrer à des outils de développement industrialisé comme Maven, mais qu'ils pourraient avoir un impact énorme sur le développement logiciel en général. * J'en avais discuté avec Pierre Weiss au SL 2006, et il était lui même très impressionné par ce travail (et par IsaacOs/Lisaac aussi ;-)