mpri-coq-project/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).