Dans le cadre de la présentation de CompCert et Coq (pour le cours ACSS en Ensimag 2A), voilà un exemple de formalisation du calcul de WP en Coq. En effet, un calcul de WP est en cas particulier de compilateur: étant donné un programme et une postcondition, ce calcul produit une précondition (la plus faible) qui détermine les états initiaux du programme pour lesquels la postcondition est satisfaite dans l'état final. Par cet exemple, le but est de montrer comment on formalise un langage (ici, c'est un petit langage impératif très simple), avec sa syntaxe et sa sémantique; puis, comment on définit un traitement sur ce langage (ici le calcul de WP) et on prouve la correction de ce traitement.
Au delà de cette introduction à Coq, cette formalisation permet de mieux comprendre la logique de Hoare, au coeur du plugin WP de Frama-C vu précédemment dans le cours ACSS.
Ce langage est définit dans le module HoareLogicDefs
Le calcul de WP est défini par récursion structurelle sur la syntaxe des programmes, par la fonction synt_wp: ImpProg → (Pred → Pred). Il s'agit de la définition en correction partielle (qui donne une précondition sous l'hypothèse que le programme termine). Cette définition correspond exactement à celle vue en cours: dans le cas de l'instruction Iwhile, la précondition exige l'existence d'un invariant de boucle appelé inv dans la formule générée. Le cas du WP en correction totale est défini ici dans le cadre (plus général que celui vu en cours) où la terminaison est prouvée à l'aide d'une relation bien-fondée plutôt qu'un variant.
Le théorème de correction (en correction partielle) correspond à la propriété présentée en introduction: si la précondition retournée par synt_wp est vérifiée par l'état initial, alors tout état final vérifie la postcondition. Ce lemme correspond à wp_sound: l'énoncé utilise la définition sémantique de WLP, elle-même basée sur la relation exec mentionnée ci-dessus.
Tout le code source Coq commenté est disponible en ligne et fait partie d'un tutoriel sur Coq, appelé Hoare logic Tutorial.
Pour aller encore plus loin, on peut attaquer la bible Software Foundations qui formalise une grande partie de la théorie de la programmation et de la vérification en Coq.
Enfin le code Coq de CompCert est aussi bien documenté en ligne.