tobast/mpri-coq-project
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity
Projet de cours Coq (2.7.1) du MPRI — WP.
25 commits 4 branches 0 tags 448 KiB
Find a file
Théophile Bastian 08bad28fa9 Update README
2017-12-08 03:34:05 +01:00
.gitignore Initial commit 2017-10-19 14:53:14 +02:00
LICENSE Initial commit 2017-10-19 14:53:14 +02:00
README.md Update README 2017-12-08 03:34:05 +01:00
wp.v Remove a few admitted points for certain_termination 2017-12-08 03:17:55 +01:00

README.md

mpri-coq-project

Projet de cours Coq (2.7.1) du MPRI — WP.

Sujet ici.

Résultats admis

  • Une partie de certain_termination a été admise (il s'agit du lemme 1.6 du sujet). En particulier, les propriétés souhaitées sur n sont dérivées d'un lemme admis moins fort qui donne l'existence de n (certain_termination_exists_minimal).

  • Le point (3) de ce lemme a égalememnt été admis, il aurait dû être prouvé à partir de l'axiome lub_is_first_correct.

Résultats obtenus

Toutes les étapes du sujet jusqu'à la 8 (incluse) ont été traitées, c'est-à-dire que wp et wps sont définies et prouvées correctes, à l'exception des boucles while. Les invariants sont présents dans la structure, mais on pose wp(while _, φ) = Bottom. Autrement dit, dès lors qu'un while est présent, wp(_, _) devient bottom. Ceci est toujours vrai, et est prouvé dans le projet.

Ce qui n'est pas fait

Les invariants ne sont pas pris en compte. Tout est en place pour, mais j'ai manqué de temps sur la fin pour finir ce projet. J'ai simplement eu du mal à adapter la preuve de wp (et la preuve de wps aurait immédiatement suivi).