From 82eb5f21893cd2f0fa1f2332ae502f10c4e2042b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Wed, 6 Dec 2017 11:32:57 +0100
Subject: [PATCH] Define function wp, state wp_correctness

---
 wp.v | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/wp.v b/wp.v
index 44bf484..b0cf148 100644
--- a/wp.v
+++ b/wp.v
@@ -291,3 +291,25 @@ Proof.
           unfold conseq_or_bottom in IHdeduction_m.
 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.