more on wp

examples/hoare_logic/wp.mlw

@@ -4,12 +4,14 @@ theory Imp
 
 (* terms and formulas *)
 
-type operator = Oplus | Ominus | Omult
+type operator = Oplus | Ominus | Omult | Ole
+
+type ident = int
 
 type term =
   | Tconst int
-  | Tvar int  (* de Bruijn index *)
-  | Tderef int (* de Bruijn index *)
+  | Tvar int  (* de Bruijn index ? *)
+  | Tderef ident
   | Tbin term operator term
 
 type fmla =
@@ -25,13 +27,20 @@ type fmla =
 use import int.Int
 use import bool.Bool
 
+type datatype =
+  | Tint | Tbool
+
 type value =
   | Vint int
   | Vbool bool
 
 use import list.List
+use map.Map as IdMap 
+type var_env = list value
+type ref_env = IdMap.map ident value
+
 
-type state = {| var_env : list value; ref_env: list value |}
+type state = {| var_env : var_env; ref_env: ref_env |}
 
 (* semantics of formulas *)
 
@@ -42,34 +51,37 @@ predicate eval_bin (x:value) (op:operator) (y:value) (res:value) =
      | Oplus -> res = Vint (x+y)
      | Ominus -> res = Vint (x-y)
      | Omult -> res = Vint (x*y)
+     | Ole -> res = Vbool (if x <= y then True else False)
      end
   | _,_ -> false
   end
 
-use import list.Nth
+inductive get_env (i:int) (env:list value) (res:value) =
+  | Get_first: 
+    forall x:value, l:list value. get_env 0 (Cons x l) x
+  | Get_next:
+    forall i:int, x r:value, l:list value. i > 0 ->
+      get_env (i-1) l r -> get_env i (Cons x l) x
 
-predicate get_env (i:int) (env:list value) (res:value) =
-  match nth i env with
-  | None -> false
-  | Some v -> v = res
-  end
- 
-  inductive eval_term state term value =
+predicate get_refenv (i:ident) (e:ref_env) (r:value) =
+    IdMap.get e i = r
+
+inductive eval_term state term value =
   | eval_const :
       forall s:state, n:int. eval_term s (Tconst n) (Vint n)
   | eval_var :
       forall s:state, i:int, res:value.
         get_env i (var_env s) res -> eval_term s (Tvar i) res
   | eval_deref :
-      forall s:state, i:int, res:value.
-        get_env i (ref_env s) res -> eval_term s (Tderef i) res
+      forall s:state, i:ident, res:value.
+        get_refenv i (ref_env s) res -> eval_term s (Tderef i) res
   | eval_bin :
       forall s:state, op:operator, t1 t2:term, r1 r2 r:value.
         eval_term s t1 r1 -> eval_term s t2 r2 ->
         eval_bin r1 op r2 r -> eval_term s (Tbin t1 op t2) r
 
-  function my_state :state = 
-    {| var_env = Cons (Vint 42) Nil; ref_env = Nil |}
+  function my_state :state =
+    {| var_env = Cons (Vint 42) Nil; ref_env = IdMap.const (Vint 0) |}
 
   goal Test13 :
     eval_term my_state (Tconst 13) (Vint 13)
@@ -80,21 +92,29 @@ predicate get_env (i:int) (env:list value) (res:value) =
   goal Test55 :
     eval_term my_state (Tbin (Tvar 0) Oplus (Tconst 13)) (Vint 55)
 
-(*
-  predicate eval_fmla (s:state) (f:fmla) (b:bool) =
-    match f with
-      | Fterm t -> eval_term s t with
-            | Verror -> false
-            | Vint n -> n <> 0
-            | Vbool b -> b = True
-     end
-  | Fand f1 f2 ->  eval_fmla s f1 /\ eval_fmla s f2
-  | Fnot f ->  not (eval_fmla s f)
-  | Fimplies f1 f2 ->  eval_fmla s f1 -> eval_fmla s f2
-  | Fforall f ->
-      forall n:int. eval_fmla (Cons (Vint n) s) f
-  end
-*)
+inductive eval_fmla state fmla bool =
+  | eval_term:
+    forall s:state, t:term, b:bool.
+      eval_term s t (Vbool b) -> eval_fmla s (Fterm t) b
+  | eval_and:
+    forall s:state, f1 f2:fmla, b1 b2:bool.
+      eval_fmla s f1 b1 -> eval_fmla s f2 b2 ->
+      eval_fmla s (Fand f1 f2) (andb b1 b2)
+  | eval_not:
+    forall s:state, f:fmla, b:bool.
+      eval_fmla s f b -> eval_fmla s (Fnot f) (notb b)
+  | eval_impl:
+    forall s:state, f1 f2:fmla, b1 b2:bool.
+      eval_fmla s f1 b1 -> eval_fmla s f2 b2 ->
+      eval_fmla s (Fimplies f1 f2) (implb b1 b2)
+  | eval_forall_int_true:
+      forall s:state, f:fmla.
+        (* problem: qu'est-ce qui garanti que s.var_env a exactement
+           autant de debruijn que f ? *)
+        (forall n:int. eval_fmla
+          {| var_env = Cons (Vint n) s.var_env ; ref_env = s.ref_env |}
+          f True) ->
+        eval_fmla s (Fforall f) True
 
 (* substitution *) 
 
@@ -128,30 +148,27 @@ lemma eval_subst:
 
 (* statements *)
 
-(*
-
 type stmt =
   | Sskip
-  | Sassign int term
+  | Sassign ident term
   | Sseq stmt stmt
   | Sif term stmt stmt
-  | Swhile term stmt
+  | Swhile term fmla stmt
 
 lemma check_skip:
   forall s:stmt. s=Sskip \/s<>Sskip
 
-*)
-
 (* small-steps semantics for statements *)
 
-(*
-
 inductive one_step state stmt state stmt =
 
   | one_step_assign:
-      forall s:state, x:ident, e:expr.
+      forall s:state, x:ident, e:term, r:value.
+        eval_term s e r ->
         one_step s (Sassign x e)
-                 (IdMap.set s x (eval_expr s e)) Sskip
+                 {| var_env = s.var_env;
+                    ref_env = (IdMap.set s.ref_env x r) |}
+                 Sskip
 
   | one_step_seq:
       forall s s':state, i1 i1' i2:stmt.
@@ -163,49 +180,52 @@ inductive one_step state stmt state stmt =
         one_step s (Sseq Sskip i) s i
 
   | one_step_if_true:
-      forall s:state, e:expr, i1 i2:stmt.
-        eval_expr s e <> 0 ->
+      forall s:state, e:term, i1 i2:stmt.
+        eval_term s e (Vbool True) ->
           one_step s (Sif e i1 i2) s i1
 
   | one_step_if_false:
-      forall s:state, e:expr, i1 i2:stmt.
-        eval_expr s e = 0 ->
+      forall s:state, e:term, i1 i2:stmt.
+        eval_term s e (Vbool False) ->
           one_step s (Sif e i1 i2) s i2
 
   | one_step_while_true:
-      forall s:state, e:expr, i:stmt.
-        eval_expr s e <> 0 ->
-          one_step s (Swhile e i) s (Sseq i (Swhile e i))
+      forall s:state, e:term, inv:fmla, i:stmt.
+        eval_fmla s inv True ->
+        eval_term s e (Vbool True) ->
+          one_step s (Swhile e inv i) s (Sseq i (Swhile e inv i))
 
   | one_step_while_false:
-      forall s:state, e:expr, i:stmt.
-        eval_expr s e = 0 ->
-          one_step s (Swhile e i) s Sskip
+      forall s:state, e:term, inv:fmla, i:stmt.
+        eval_fmla s inv True ->
+        eval_term s e (Vbool False) ->
+          one_step s (Swhile e inv i) s Sskip
 
   goal Ass42 :
-    let x = mk_ident 0 in
-    let s = IdMap.const 0 in
+    let x = 0 in
     forall s':state.
-      one_step s (Sassign x (Econst 42)) s' Sskip ->
-        IdMap.get s' x = 42
+      one_step my_state (Sassign x (Tconst 42)) s' Sskip ->
+        IdMap.get s'.ref_env x = Vint 42
 
   goal If42 :
-    let x = mk_ident 0 in
-    let s = IdMap.const 0 in
+    let x = 0 in
     forall s1 s2:state, i:stmt.
-      one_step s
-        (Sif (Evar x)
-             (Sassign x (Econst 13))
-             (Sassign x (Econst 42)))
+      one_step my_state
+        (Sif (Tbin (Tvar x) Ole (Tconst 10))
+             (Sassign x (Tconst 13))
+             (Sassign x (Tconst 42)))
         s1 i ->
       one_step s1 i s2 Sskip ->
-        IdMap.get s2 x = 42
+        IdMap.get s2.ref_env x = Vint 42
+
+(*
 
   lemma progress:
     forall s:state, i:stmt.
       i <> Sskip ->
       exists s':state, i':stmt. one_step s i s' i'
 
+*)
 
  (* many steps of execution *)
 
@@ -231,6 +251,8 @@ lemma many_steps_seq:
       n = 1 + n1 + n2
 
 
+(*
+
 predicate valid_fmla (p:fmla) = forall s:state. eval_fmla s p
 
 (* Hoare triples *)
@@ -293,7 +315,12 @@ module WP
     | Sif e i1 i2 ->
         Fand (Fimplies (Fterm e) (wp i1 q))
              (Fimplies (Fnot (Fterm e)) (wp i2 q))
-    | Swhile _ _ -> Fterm (Econst 0)
+    | Swhile e inv i ->
+        Fand inv
+          (Forall (Fand
+                     (Fimplies (Fand (Fterm e) inv) (wp i inv))
+                     (Fimplies (Fand (Fnot (Fterm e)) inv) q))) 
+
     end
     { valid_triple result i q }
 

examples/hoare_logic/wp/why3session.xml

@@ -56,7 +56,7 @@
    expanded="true">
    <goal
     name="Test13"
-    sum="79f3fb3351626d34bfb37da12b0bd140"
+    sum="588a68a35eb40a90e89f2604e6fd3683"
     proved="true"
     expanded="true"
     shape="aeval_termamy_stateaTconstc13aVintc13">
@@ -65,12 +65,12 @@
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.06"/>
+     <result status="valid" time="0.03"/>
     </proof>
    </goal>
    <goal
     name="Test42"
-    sum="1f19dab18a6999ab7e11f82d7e74d850"
+    sum="ad60784608efee681d7bfb6d4657ce64"
     proved="true"
     expanded="true"
     shape="aeval_termamy_stateaTvarc0aVintc42">
@@ -79,42 +79,119 @@
      timelimit="3"
      edited=""
      obsolete="false">
-     <result status="valid" time="0.05"/>
+     <result status="valid" time="0.01"/>
     </proof>
    </goal>
    <goal
     name="Test55"
-    sum="0bf8af91734c8766090834ab82722ed2"
-    proved="false"
+    sum="a416d24c7e960e30780c57a6ed5795aa"
+    proved="true"
     expanded="true"
     shape="aeval_termamy_stateaTbinaTvarc0aOplusaTconstc13aVintc55">
     <proof
      prover="coq"
-     timelimit="3"
-     edited="wp_Imp_Test55_1.v"
-     obsolete="true">
-     <result status="highfailure" time="0.63"/>
+     timelimit="5"
+     edited="wp_Imp_Test55_2.v"
+     obsolete="false">
+     <result status="valid" time="0.52"/>
+    </proof>
+   </goal>
+   <goal
+    name="check_skip"
+    sum="2dfd7981c1282e38fe4d32469fa442c3"
+    proved="true"
+    expanded="true"
+    shape="ainfix =V0aSskipNOainfix =V0aSskipF">
+    <proof
+     prover="alt-ergo"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.04"/>
+    </proof>
+   </goal>
+   <goal
+    name="Ass42"
+    sum="8329fde7dbe71ed5445e3fe0fbff0f00"
+    proved="true"
+    expanded="true"
+    shape="Lc0ainfix =agetaref_envV1V0aVintc42Iaone_stepamy_stateaSassignV0aTconstc42V1aSskipF">
+    <proof
+     prover="cvc3"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="valid" time="0.16"/>
+    </proof>
+   </goal>
+   <goal
+    name="If42"
+    sum="aff6d2fdcb44ce731b6d88a5e11d731e"
+    proved="true"
+    expanded="true"
+    shape="Lc0ainfix =agetaref_envV2V0aVintc42Iaone_stepV1V3V2aSskipIaone_stepamy_stateaSifaTbinaTvarV0aOleaTconstc10aSassignV0aTconstc13aSassignV0aTconstc42V1V3F">
+    <proof
+     prover="coq"
+     timelimit="5"
+     edited="wp_Imp_If42_1.v"
+     obsolete="false">
+     <result status="valid" time="0.82"/>
+    </proof>
+   </goal>
+   <goal
+    name="steps_non_neg"
+    sum="eadba762cc1a40c7895345dfdf01917a"
+    proved="false"
+    expanded="true"
+    shape="ainfix >=V4c0Iamany_stepsV0V2V1V3V4F">
+    <proof
+     prover="cvc3"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="timeout" time="6.06"/>
     </proof>
     <proof
      prover="alt-ergo"
      timelimit="5"
      edited=""
      obsolete="false">
-     <result status="timeout" time="5.08"/>
+     <result status="timeout" time="8.57"/>
     </proof>
+    <proof
+     prover="z3"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="timeout" time="9.84"/>
+    </proof>
+   </goal>
+   <goal
+    name="many_steps_seq"
+    sum="1c58617d16ff2ed20d6a49c7ff3990ad"
+    proved="false"
+    expanded="true"
+    shape="ainfix =V4ainfix +ainfix +c1V6V7Aamany_stepsV5V3V1aSskipV7Aamany_stepsV0V2V5aSskipV6EIamany_stepsV0aSseqV2V3V1aSskipV4F">
     <proof
      prover="cvc3"
      timelimit="5"
-     edited="wp-Imp-Test55_1.cvc"
-     obsolete="true">
-     <result status="timeout" time="5.29"/>
+     edited=""
+     obsolete="false">
+     <result status="timeout" time="6.07"/>
+    </proof>
+    <proof
+     prover="alt-ergo"
+     timelimit="5"
+     edited=""
+     obsolete="false">
+     <result status="timeout" time="8.57"/>
     </proof>
     <proof
      prover="z3"
      timelimit="5"
      edited=""
      obsolete="false">
-     <result status="timeout" time="5.48"/>
+     <result status="timeout" time="10.24"/>
     </proof>
    </goal>
   </theory>

theories/bool.why

@@ -28,6 +28,12 @@ theory Bool
     | True  -> False
     end
 
+  function implb (x y : bool) : bool =
+    match x,y with
+    | True, False -> False
+    | _,_  -> True
+    end
+
 end
 
 theory Ite