Axiomatize Hoare provability |-

wp.v

@@ -147,9 +147,54 @@ Notation "'exists_m' x" := (existsMemForall x)
 
 Definition substAssert : Assert -> Var -> Z -> Assert :=
     fun asser ident val mem => asser (mem [ident <- val]).
-Notation "a < x <- z >" := (substAssert a x z)
+Notation "a [[ x <- z ]]" := (substAssert a x z)
     (at level 50, left associativity).
 Definition substAssertExpr : Assert -> Var -> Expr -> Assert :=
     fun asser ident expr mem => asser (mem [ident <- (expr mem)]).
-Notation "a < x <- 'expr' z >" := (substAssertExpr a x z)
+Notation "a [[ x <- 'expr' z ]]" := (substAssertExpr a x z)
     (at level 50, left associativity).
+
+Definition assertOfExpr : Expr -> Assert :=
+    fun expr mem => expr mem <> 0%Z.
+
+Definition assertImplLogical : Assert -> Assert -> Prop :=
+    fun a1 a2 => forall (m : Mem), (a1 m) -> (a2 m).
+
+
+(***** Hoare provability *****************************************************)
+
+Parameter  hoare_provability : Assert -> Instr -> Assert -> Prop.
+Notation "[| pre  |] instr  [| post |]" := (hoare_provability pre instr post)
+        (at level 30): assert.
+
+Axiom h_skip: forall (asser: Assert), ( [|asser|] skip [|asser|]) % assert.
+Axiom h_abort: forall (a1:Assert), forall (a2: Assert),
+    ([|a1|] abort [|a2|]) % assert.
+Axiom h_assign: forall (asser: Assert), forall (x: Var), forall (e: Expr),
+    ([| asser [[ x <- expr e ]] |] (assign x e) [|asser|]) % assert.
+Axiom h_conseq:
+    forall (a1: Assert), forall (a1': Assert),
+    forall (a2: Assert), forall (a2': Assert),
+    forall (s: Instr),
+    ([| a1' |] s [| a2' |]) % assert ->
+            (assertImplLogical a1 a1') ->
+            (assertImplLogical a2' a2) ->
+            ([| a1 |] s [| a2 |]) % assert.
+Axiom h_seq:
+    forall (a1: Assert), forall (a2: Assert), forall (a3: Assert),
+    forall (s1: Instr), forall (s2: Instr),
+    ([|a1|] s1 [|a2|]) % assert -> ([|a2|] s2 [|a3|]) % assert ->
+            ([|a1|] (seq s1 s2) [|a3|]) % assert.
+Axiom h_if:
+    forall (a1: Assert), forall (a2: Assert),
+    forall (e: Expr),
+    forall (s1: Instr), forall (s2: Instr),
+    ([| a1 /\ (assertOfExpr e) |] s1 [| a2 |]) % assert ->
+        ([| a1 /\ ~ (assertOfExpr e) |] s2 [| a2 |]) % assert ->
+        ([| a1 |] (ifelse e s1 s2) [| a2 |]) % assert.
+Axiom h_while:
+    forall (inv: Assert),
+    forall (e: Expr),
+    forall (s: Instr),
+    ([| inv /\ (assertOfExpr e) |] s [| inv |]) % assert ->
+        ([| inv |] (while e s) [| inv /\ ~ (assertOfExpr e) |]) % assert.