2017-10-19 14:53:14 +02:00
|
|
|
# mpri-coq-project
|
|
|
|
|
2017-10-26 14:43:31 +02:00
|
|
|
Projet de cours Coq (2.7.1) du MPRI — WP.
|
|
|
|
|
2017-12-08 03:32:53 +01:00
|
|
|
Sujet
|
|
|
|
[ici](http://www.enseignement.polytechnique.fr/informatique/MPRI/2-7-1/wp.html).
|
|
|
|
|
|
|
|
## 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).
|