From 90ca9bc5bb26f9399653fc378b491ab4bb581a32 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9ophile=20Bastian?= <contact@tobast.fr>
Date: Thu, 16 Nov 2017 15:22:35 +0100
Subject: [PATCH] Implement most operators on assertions

---
 wp.v | 93 ++++++++++++++++++++++++++++++++++++++++++++++--------------
 1 file changed, 72 insertions(+), 21 deletions(-)

diff --git a/wp.v b/wp.v
index 820e00f..c0b37ed 100644
--- a/wp.v
+++ b/wp.v
@@ -66,21 +66,12 @@ Arguments find_lub_correct {T} {chain} _.
 Definition subst: Mem -> Var -> Z -> Mem :=
     fun (m: Mem) (v: Var) (z: Z) (v2: Var) =>
         if nat_eq v v2 then z else m v2.
+Notation "m [ x <- z ]" := (subst m x z) (at level 50, left associativity).
 
 Definition MemCpo := cpo Mem.
 Definition MemError := CpoError Mem.
 Definition MemElem := CpoElem Mem.
 
-Fixpoint repeat_n (n: nat) (inst: Instr) :=
-    let aux := (fix aux (n: nat) (inst: Instr) (acc: Instr) :=
-        match n with
-        | 0 => skip
-        | S n => aux n inst (seq acc inst) end) in
-    aux n inst (skip).
-Definition while_sem_n: Expr -> Instr -> nat -> Instr :=
-    fun guard inst n =>
-        seq (repeat_n n (ifonly guard inst)) (ifonly guard abort).
-
 Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo :=
     match mem with
     | CpoError _ => MemError
@@ -88,17 +79,77 @@ Fixpoint interp (inst: Instr) (mem: MemCpo) : MemCpo :=
         match inst with
         | skip => MemElem mem0
         | abort => MemError
-        | assign v e => (MemElem (subst mem0 v (e mem0)))
+        | assign v e => (MemElem (mem0 [v <- (e mem0)]))
         | seq instr1 instr2 => interp instr2 (interp instr1 (MemElem mem0))
-        | ifelse exp instrIf instrElse =>
-                if ((exp mem0) =? 0) % Z
-                    then interp instrIf (MemElem mem0)
-                    else interp instrElse (MemElem mem0)
-        | while guard instr =>
-                let fix while_chain (guard: Expr) (inst: Instr)
-                    (mem: MemCpo) : (Sequence MemCpo) :=
-                    fun n => interp (while_sem_n guard inst n) mem
-                in find_lub (while_chain guard instr (MemElem mem0))
-
+        | ifelse guard instrIf instrElse =>
+            if ((guard mem0) =? 0) % Z
+                then interp instrIf mem
+                else interp instrElse mem
+        | while guard body =>
+            let fix while_chain (mem: MemCpo) (n: nat): MemCpo :=
+                match n with
+                | 0 => mem
+                | S m =>
+                    match while_chain (MemElem mem0) m with
+                    | CpoError _ => MemError
+                    | CpoElem _ submem =>
+                        if ((guard submem) =? 0) % Z
+                            then interp body (MemElem submem)
+                            else mem
+                    end
+                end
+            in find_lub (fun n =>
+                match while_chain (MemElem mem0) n with
+                | CpoError _ => MemError
+                | CpoElem _ submem =>
+                    if ((guard submem) =? 0) % Z
+                        then MemError
+                        else MemElem submem
+                end)
         end
     end.
+
+(***** Validite, prouvabilite pour Hoare *************************************)
+
+Definition Assert := Mem -> Prop.
+Delimit Scope assert with assert.
+
+Definition assertTop : Assert := fun _ => True.
+Definition assertBot : Assert := fun _ => False.
+
+Definition assertNot : Assert -> Assert :=
+    fun orig mem => ~ (orig mem).
+Notation "~ x" := (assertNot x) (at level 75, right associativity) : assert.
+Definition assertAnd : Assert -> Assert -> Assert :=
+    fun x1 x2 mem => (x1 mem) /\ (x2 mem).
+Infix "/\" := assertAnd : assert.
+Definition assertOr : Assert -> Assert -> Assert :=
+    fun x1 x2 mem => (x1 mem) \/ (x2 mem).
+Infix "\/" := assertOr : assert.
+Definition assertImpl : Assert -> Assert -> Assert :=
+    fun x1 x2 => (~x1 \/ x2) % assert.
+Infix "->" := assertImpl : assert.
+Definition assertForall : Var -> Assert -> Assert :=
+    fun ident asser mem => forall (z: Z), asser (mem [ident <- z]).
+Notation "\-/ x" := (assertForall x) (at level 90, no associativity) : assert.
+Definition existsForall : Var -> Assert -> Assert :=
+    fun ident asser mem => exists (z: Z), asser (mem [ident <- z]).
+Notation "'exists' x" := (existsForall x)
+    (at level 87, no associativity): assert.
+Definition assertMemForall : Assert -> Assert :=
+    fun asser mem => forall (mem: Mem), asser mem.
+Notation "'\-/m' x" := (assertMemForall x)
+    (at level 90, no associativity): assert.
+Definition existsMemForall : Assert -> Assert :=
+    fun asser mem => exists (mem: Mem), asser mem.
+Notation "'exists_m' x" := (existsMemForall x)
+    (at level 87, no associativity): assert.
+
+Definition substAssert : Assert -> Var -> Z -> Assert :=
+    fun asser ident val mem => asser (mem [ident <- val]).
+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)
+    (at level 50, left associativity).