Define function wp, state wp_correctness

This commit is contained in:
Théophile Bastian 2017-12-06 11:32:57 +01:00
parent 2431f66b07
commit 82eb5f2189

22
wp.v
View file

@ -291,3 +291,25 @@ Proof.
unfold conseq_or_bottom in IHdeduction_m. unfold conseq_or_bottom in IHdeduction_m.
Admitted. Admitted.
(***** Weakest precondition **************************************************)
Fixpoint wp (instr: Instr) (cond: Assert) : Assert := match instr with
| skip =>
cond
| abort =>
assertTop
| assign x expr =>
cond [[ x <- expr expr ]]
| seq s1 s2 =>
wp s1 (wp s2 cond)
| ifelse guard sIf sElse =>
(assertOfExpr guard -> wp sIf cond
/\ (~ (assertOfExpr guard) -> wp sElse cond)) % assert
| while guard body => assertTop
end.
Theorem wp_correctness (instr: Instr) (post: Assert) :
( |= [| wp instr post |] instr [| post |] ) % assert.
Proof.
(* TODO *)
Admitted.