Abstract FR:

Cette these s'interesse au probleme de la certification de programmes fonctionnels. Nous etudions une approche tres particuliere. Il est bien connu qu'une preuve mathematique constructive d'une formule affirmant l'existence d'un objet satisfaisant une certaine propriete peut s'interpreter comme une methode effective de construction de l'objet. Dans cette approche, la specification du programme est representee par une formule logique et developper le programme correspond a prouver cette formule. Il existe differentes methodes pour extraire de la preuve mathematique la partie calculatoire qui represente le programme qui, de part sa methode de construction, est certifie correct. Cette these s'interesse au probleme inverse de l'extraction de programme, a savoir etant donnes une specification et un programme, reconstruire une preuve de la specification dont le contenu algorithmique correspond au programme donne. Ce probleme n'est evidemment pas decidable. Le mieux que l'on puisse esperer est d'engendrer un certain nombre d'obligations de preuves portant sur des parties atomiques du programme et correspondant aux proprietes logiques qui doivent etre verifiees. Meme ce but ne peut etre atteint. En effet, la preuve du programme necessite en general de connaitre les proprietes intermediaires des sous-programmes qui peuvent etre plus fortes que la specification initiale. Cette these etudie d'abord une methode d'extraction faible d'un programme a partir d'une preuve qui garde trace des specifications intermediaires. A partir d'un tel programme, on montre qu'il est deterministe de retrouver les obligations de preuves minimales. Ensuite, des methodes heuristiques sont proposees pour retrouver la preuve a partir d'un programme naturel ne comportant que des annotations partielles. Finalement, la these presente la mise en uvre de cette methode comme tactique de l'assistant de preuve coq qui a permis le developpement de differents exemples dont des programmes de tri