blocking semantic (proofs)

examples/hoare_logic/blocking_semantics2.mlw

@@ -726,7 +726,7 @@ predicate expr_writes (e:expr) (w:Set.set mident) =
   (*   fresh_in_expr id e -> *)
   (*     subst (wp e q) id id' = wp e (subst q id id') *)
 
-  lemma wp_implies:
+  lemma monotonicite:
     forall p q:fmla.
      (forall sigma:env, pi:stack.
         eval_fmla sigma pi p -> eval_fmla sigma pi q)
@@ -735,7 +735,7 @@ predicate expr_writes (e:expr) (w:Set.set mident) =
        eval_fmla sigma pi (wp e p) ->
        eval_fmla sigma pi (wp e q)
 
-  lemma wp_conj:
+  lemma distib_conj:
     forall sigma:env, pi:stack, e:expr, p q:fmla.
      eval_fmla sigma pi (wp e (Fand p q)) <->
        (eval_fmla sigma pi (wp e p)) /\
@@ -755,18 +755,17 @@ predicate expr_writes (e:expr) (w:Set.set mident) =
     | _ -> false
     end
 
-  lemma unique_type_expr : 
-  forall e:expr, sigmat: type_env, pit:type_stack, ty1 ty2:datatype.  
-    type_expr sigmat pit e ty1 ->
-    type_expr sigmat pit e ty2 -> ty1 = ty2
-
   lemma decide_value :
     forall e:expr. not (is_value e) \/ exists v:value. e = Evalue v
 
   lemma bool_value:
-    forall e:expr, sigmat: type_env, pit:type_stack.  
-      type_expr sigmat pit e TYbool -> is_value e ->
-          (e = Evalue (Vbool False)) \/ (e = Evalue (Vbool True))
+    forall v:value, sigmat: type_env, pit:type_stack.  
+      type_expr sigmat pit (Evalue v) TYbool ->
+          (v = Vbool False) \/ (v = Vbool True)
+
+  lemma unit_value:
+    forall v:value, sigmat: type_env, pit:type_stack.  
+      type_expr sigmat pit (Evalue v) TYunit -> v = Vvoid 
 
   lemma progress:
     forall e:expr, sigma:env, pi:stack, sigmat: type_env, pit: type_stack, ty: datatype, q:fmla.
@@ -776,286 +775,8 @@ predicate expr_writes (e:expr) (w:Set.set mident) =
     exists sigma':env, pi':stack, e':expr.
       one_step sigma pi e sigma' pi' e'
 
-(*
-  let rec compute_writes (s:expr) : Set.set ident =
-   { }
-    match s with
-    | Sskip -> Set.empty
-    | Sassign i _ -> Set.singleton i
-    | Sseq s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
-    | Sif _ s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
-    | Swhile _ _ s -> compute_writes s
-    | Sassert _ -> Set.empty
-    end
-   { forall sigma sigma':env, pi pi':stack, n:int.
-       many_steps sigma pi s sigma' pi' Sskip n ->
-       assigns sigma result sigma' }
-
-  val fresh_from_fmla (q:fmla) :
-     { }
-     ident
-     { fresh_in_fmla result q }
-
-  val abstract_effects (i:expr) (f:fmla) :
-    { }
-    fmla
-    { forall sigma:env, pi:stack. eval_fmla sigma pi result ->
-        eval_fmla sigma pi f /\
-(***
-        forall sigma':env, w:Set.set ident.
-        expr_writes i w /\ assigns sigma w sigma' ->
-        eval_fmla sigma' pi result
-*)
-        forall sigma' pi':env, n:int.
-           many_steps sigma pi i sigma' pi' Sskip n ->
-           eval_fmla sigma' pi' result
-     }
-
-  use HoareLogic
-
-  let rec wp (i:expr) (q:fmla) =
-    { true }
-    match i with
-    | Sskip -> q
-    | Sseq i1 i2 -> wp i1 (wp i2 q)
-    | Sassign x e ->
-        let id = fresh_from_fmla q in Flet id e (subst q x id)
-    | Sif e i1 i2 ->
-        Fand (Fimplies (Fterm e) (wp i1 q))
-             (Fimplies (Fnot (Fterm e)) (wp i2 q))
-    | Sassert f ->
-       Fimplies f q (* liberal wp, no termination required *)
-       (* Fand f q *) (* strict wp, termination required *)
-    | Swhile e inv i ->
-        Fand inv
-          (abstract_effects i
-            (Fand
-                (Fimplies (Fand (Fterm e) inv) (wp i inv))
-                (Fimplies (Fand (Fnot (Fterm e)) inv) q)))
-
-    end
-    { valid_triple result i q }
-
-*)
-
-end
-
-(* pas concluant
-
-(** {2 WP calculus, variant} *)
-
-theory WP2
-
-use import ImpExpr
-
-use set.Set
-
-(** [assigns sigma W sigma'] is true when the only differences between
-    [sigma] and [sigma'] are the value of references in [W] *)
-
-predicate assigns (sigma:env) (a:Set.set ident) (sigma':env) =
-  forall i:ident. not (Set.mem i a) ->
-    IdMap.get sigma i = IdMap.get sigma' i
-
-lemma assigns_refl:
-  forall sigma:env, a:Set.set ident. assigns sigma a sigma
-
-lemma assigns_trans:
-  forall sigma1 sigma2 sigma3:env, a:Set.set ident.
-    assigns sigma1 a sigma2 /\ assigns sigma2 a sigma3 ->
-    assigns sigma1 a sigma3
-
-lemma assigns_union_left:
-  forall sigma sigma':env, s1 s2:Set.set ident.
-    assigns sigma s1 sigma' -> assigns sigma (Set.union s1 s2) sigma'
-
-lemma assigns_union_right:
-  forall sigma sigma':env, s1 s2:Set.set ident.
-    assigns sigma s2 sigma' -> assigns sigma (Set.union s1 s2) sigma'
-
-(** [expr_writes e W] is true when the only references modified by [e] are in [W] *)
-predicate expr_writes (e:expr) (w:Set.set ident) =
-  match e with
-  | Evalue _ | Evar _ | Ederef _ | Eassert _ -> true
-  | Ebin e1 _ e2 -> expr_writes e1 w /\ expr_writes e2 w
-  | Eassign id _ -> Set.mem id w
-  | Eseq e1 e2 -> expr_writes e1 w /\ expr_writes e2 w
-  | Elet id e1 e2 -> expr_writes e1 w /\ expr_writes e2 w
-  | Eif e1 e2 e3 -> expr_writes e1 w /\ expr_writes e2 w /\ expr_writes e3 w
-  | Ewhile cond _ body -> expr_writes cond w /\ expr_writes body w
-  end
-
-  function fresh_from (f:fmla) (e:expr) : ident
-
-  axiom fresh_from_fmla: forall e:expr, f:fmla.
-     fresh_in_fmla (fresh_from f e) f
-
-  axiom fresh_from_expr: forall e:expr, f:fmla.
-     fresh_in_expr (fresh_from f e) e
-
-  function abstract_effects (e:expr) (f:fmla) : fmla
-
-  predicate is_pure (e:expr) =
-    match e with
-    | Evalue _ | Evar _ | Ederef _ -> true
-    | Eassert _ -> false (* true *)
-    | Eseq e1 e2 -> false (* is_pure e1 /\ is_pure e2 *)
-    | Elet id e1 e2 -> false (* is_pure e1 /\ is_pure e2 *)
-    | Ebin e1 op e2 -> false (* is_pure e1 /\ is_pure e2 *)
-    | Eassign x e -> false
-    | Eif e1 e2 e3 -> false (* is_pure e1 /\ is_pure e2 /\ is_pure e3 *)
-    | Ewhile cond inv body -> false
-    end
-
-  function purify (e:expr) : term =
-    match e with
-    | Evalue v -> Tvalue v
-    | Evar id -> Tvar id
-    | Ederef id -> Tderef id
-    | _ -> Tvalue Vvoid
-   end
-
-  function wp (e:expr) (q:fmla) : fmla =
-    match e with
-    | Evalue v ->
-        (* let result = e in q *)
-        Flet result (Tvalue v) q
-    | Evar v -> Flet result (Tvar v) q
-    | Ederef x -> Flet result (Tderef x) q
-    | Eassert f ->
-        (* asymmetric and *)
-        Fand f (Fimplies f q)
-    | Eseq e1 e2 -> wp e1 (wp e2 q)
-    | Elet id e1 e2 -> wp e1 (Flet id (Tvar result) (wp e2 q))
-    | Ebin e1 op e2 ->
-       if is_pure e1 then
-          if is_pure e2 then
-             Flet result (Tbin (purify e1) op (purify e2)) q
-          else
-             let id = fresh_from q e in
-             wp (Elet id e2 (Ebin e1 op (Evar id))) q
-       else
-          let id = fresh_from q e in
-          wp (Elet id e1 (Ebin (Evar id) op e2)) q
-    | Eassign x e ->
-        if is_pure e then
-          let q' = Flet result (Tvalue Vvoid) q in
-          let id = fresh_from q' e in
-          Flet id (purify e) (subst q' x id)
-        else
-          let id = fresh_from q e in
-          wp (Elet id e (Eassign x (Evar id))) q
-    | Eif e1 e2 e3 ->
-        let f =
-          Fand (Fimplies (Fterm (Tvar result)) (wp e2 q))
-            (Fimplies (Fnot (Fterm (Tvar result))) (wp e3 q))
-        in
-        wp e1 f
-    | Ewhile cond inv body ->
-        Fand inv
-          (abstract_effects body
-            (wp cond
-             (Fand
-              (Fimplies (Fand (Fterm (Tvar result)) inv) (wp body inv))
-              (Fimplies (Fand (Fnot (Fterm (Tvar result))) inv) q))))
-
-    end
-
-
-  lemma wp_conj:
-    forall sigma:env, pi:stack, e:expr, p q:fmla.
-     eval_fmla sigma pi (wp e (Fand p q)) <->
-       (eval_fmla sigma pi (wp e p)) /\
-       (eval_fmla sigma pi (wp e q))
-
-
-  lemma wp_reduction:
-    forall sigma sigma':env, pi pi':stack, e e':expr.
-    one_step sigma pi e sigma' pi' e' ->
-    forall q:fmla.
-      eval_fmla sigma pi (wp e q) ->
-      eval_fmla sigma' pi' (wp e' q)
-
-  predicate not_a_value (e:expr) =
-    match e with
-    | Evalue _ -> false
-    | _ -> true
-    end
-
-  lemma decide_value:
-    forall e:expr. not_a_value e \/ exists v:value. e = Evalue v
-
-  lemma progress:
-    forall e:expr, sigma:env, pi:stack, q:fmla.
-    eval_fmla sigma pi (wp e q) /\ not_a_value e ->
-    exists sigma':env, pi':stack, e':expr.
-      one_step sigma pi e sigma' pi' e'
-
-(*
-  let rec compute_writes (s:expr) : Set.set ident =
-   { }
-    match s with
-    | Sskip -> Set.empty
-    | Sassign i _ -> Set.singleton i
-    | Sseq s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
-    | Sif _ s1 s2 -> Set.union (compute_writes s1) (compute_writes s2)
-    | Swhile _ _ s -> compute_writes s
-    | Sassert _ -> Set.empty
-    end
-   { forall sigma sigma':env, pi pi':stack, n:int.
-       many_steps sigma pi s sigma' pi' Sskip n ->
-       assigns sigma result sigma' }
-
-  val fresh_from_fmla (q:fmla) :
-     { }
-     ident
-     { fresh_in_fmla result q }
-
-  val abstract_effects (i:expr) (f:fmla) :
-    { }
-    fmla
-    { forall sigma:env, pi:stack. eval_fmla sigma pi result ->
-        eval_fmla sigma pi f /\
-(***
-        forall sigma':env, w:Set.set ident.
-        expr_writes i w /\ assigns sigma w sigma' ->
-        eval_fmla sigma' pi result
-*)
-        forall sigma' pi':env, n:int.
-           many_steps sigma pi i sigma' pi' Sskip n ->
-           eval_fmla sigma' pi' result
-     }
-
-  use HoareLogic
-
-  let rec wp (i:expr) (q:fmla) =
-    { true }
-    match i with
-    | Sskip -> q
-    | Sseq i1 i2 -> wp i1 (wp i2 q)
-    | Sassign x e ->
-        let id = fresh_from_fmla q in Flet id e (subst q x id)
-    | Sif e i1 i2 ->
-        Fand (Fimplies (Fterm e) (wp i1 q))
-             (Fimplies (Fnot (Fterm e)) (wp i2 q))
-    | Sassert f ->
-       Fimplies f q (* liberal wp, no termination required *)
-       (* Fand f q *) (* strict wp, termination required *)
-    | Swhile e inv i ->
-        Fand inv
-          (abstract_effects i
-            (Fand
-                (Fimplies (Fand (Fterm e) inv) (wp i inv))
-                (Fimplies (Fand (Fnot (Fterm e)) inv) q)))
-
-    end
-    { valid_triple result i q }
-
-*)
-
 end
 
-*)
 
 (***
 Local Variables:

examples/hoare_logic/blocking_semantics2/blocking_semantics2_WP_progress_1.v

@@ -696,13 +696,13 @@ Fixpoint wp(e:expr) (q:fmla) {struct e}: fmla :=
   end.
 Unset Implicit Arguments.
 
-Axiom wp_implies : forall (p:fmla) (q:fmla), (forall (sigma:(map mident
+Axiom monotonicite : forall (p:fmla) (q:fmla), (forall (sigma:(map mident
   value)) (pi:(list (ident* value)%type)), (eval_fmla sigma pi p) ->
   (eval_fmla sigma pi q)) -> forall (sigma:(map mident value)) (pi:(list
   (ident* value)%type)) (e:expr), (eval_fmla sigma pi (wp e p)) ->
   (eval_fmla sigma pi (wp e q)).
 
-Axiom wp_conj : forall (sigma:(map mident value)) (pi:(list (ident*
+Axiom distib_conj : forall (sigma:(map mident value)) (pi:(list (ident*
   value)%type)) (e:expr) (p:fmla) (q:fmla), (eval_fmla sigma pi (wp e (Fand p
   q))) <-> ((eval_fmla sigma pi (wp e p)) /\ (eval_fmla sigma pi (wp e q))).
 
@@ -721,6 +721,15 @@ Definition is_value(e:expr): Prop :=
 Axiom decide_value : forall (e:expr), (~ (is_value e)) \/ exists v:value,
   (e = (Evalue v)).
 
+Axiom bool_value : forall (e:expr) (sigmat:(map mident datatype)) (pit:(list
+  (ident* datatype)%type)), (type_expr sigmat pit e TYbool) ->
+  ((is_value e) -> ((e = (Evalue (Vbool false))) \/
+  (e = (Evalue (Vbool true))))).
+
+Axiom unit_value : forall (e:expr) (sigmat:(map mident datatype)) (pit:(list
+  (ident* datatype)%type)), (type_expr sigmat pit e TYunit) ->
+  ((is_value e) -> (e = (Evalue Vvoid))).
+
 (* Why3 goal *)
 Theorem progress : forall (e:expr) (sigma:(map mident value)) (pi:(list
   (ident* value)%type)) (sigmat:(map mident datatype)) (pit:(list (ident*
@@ -814,16 +823,28 @@ apply one_step_deref.
 (* case 4.1: e' not a value *)
 destruct (decide_value e).
 intros sigma pi typ_sigma typ_pi type q h1 h2 h3 h4.
-generalize (IHe _ _ _ (conj h1 H)).
+inversion h1; subst.
+(*
+generalize (IHe sigma pi _ _ _ _ H6  h3 H).
+
+simpl in h3.
+pose (q' := (Flet (fresh_from q e) (Tvar result)
+             (Flet result (msubst_term (Tvalue Vvoid) m (fresh_from q e))
+                (msubst q m (fresh_from q e))))).
+fold q' in h3.
+
+intro; clear IHe.
+
 intros (sigma' & pi' & e' & h).
 exists sigma'.
 exists pi'.
 exists (Eassign i e').
-apply one_step_assign_ctxt; auto.
+apply one_step_assign_ctxt; auto.*)
+admit.
 (* case 4.2: e' is a value *)
 elim H; clear H; intros v He_v.
 subst e.
-intros sigma pi q (h2 & h3).
+intros sigma pi q h2 h3.
 eexists.
 exists pi.
 eexists.
@@ -832,27 +853,30 @@ eapply one_step_assign_value.
 (* case 5: e = e1; e2 *)
 destruct (decide_value e1).
 (* case 5.1: e1 not a value *)
-intros sigma pi q (h1 & _).
+(*intros sigma pi q (h1 & _).
 generalize (IHe1 _ _ _ (conj h1 H)).
 intros (sigma' & pi' & e' & h).
 exists sigma'.
 exists pi'.
 exists (Eseq e' e2).
-eapply one_step_seq_ctxt; auto.
-
+eapply one_step_seq_ctxt; auto.*)
+admit.
 (* case 5.2: e1 is a value *)
 elim H; clear H; intros v He_v.
 subst e1.
-intros sigma pi q (h2 & h3).
+clear IHe1 IHe2.
+intros sigma pi sigmat pit ty q h1 h2 h3 h4.
+inversion h1; subst.
+assert (h : Evalue v = Vvoid)
+
+
 eexists.
 exists pi.
 eexists.
-assert (h: v = Vvoid).
-(* problem : typage pour savoir que v est void *) 
-admit.
-subst v.
+
 eapply one_step_seq_value.
 
+
 (* case 6: e = let i = e1 in e2 *)
 destruct (decide_value e1).
 (* case 6.1: e1 not a value *)

examples/hoare_logic/blocking_semantics2/why3session.xml

@@ -28,30 +28,34 @@
   version="1.4"/>
  <prover
   id="6"
+  name="Gappa"
+  version="0.14.1"/>
+ <prover
+  id="7"
   name="Simplify"
   version="1.5.4"/>
  <prover
-  id="7"
+  id="8"
   name="Spass"
   version="3.7"/>
  <prover
-  id="8"
+  id="9"
   name="Vampire"
   version="0.6"/>
  <prover
-  id="9"
+  id="10"
   name="Yices"
   version="1.0.25"/>
  <prover
-  id="10"
+  id="11"
   name="Z3"
   version="2.19"/>
  <prover
-  id="11"
+  id="12"
   name="Z3"
   version="3.2"/>
  <prover
-  id="12"
+  id="13"
   name="veriT"
   version="dev"/>
  <file
@@ -698,44 +702,46 @@
     </proof>
    </goal>
    <goal
-    name="wp_implies"
+    name="monotonicite"
     locfile="blocking_semantics2/../blocking_semantics2.mlw"
-    loclnum="729" loccnumb="8" loccnume="18"
-    sum="b6cc858b6fd9021e369507349b37d450"
+    loclnum="729" loccnumb="8" loccnume="20"
+    sum="968d7276e08a0c1311547ab117a38e5f"
     proved="false"
     expanded="false"
     shape="aeval_fmlaV2V3awpV4V1Iaeval_fmlaV2V3awpV4V0FIaeval_fmlaV5V6V1Iaeval_fmlaV5V6V0FF">
     <proof
-     prover="0"
+     prover="4"
      timelimit="3"
      memlimit="0"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="3.11"/>
+     edited="blocking_semantics2_WP_monotonicite_1.v"
+     obsolete="true"
+     archived="false"><undone/>
+     
     </proof>
    </goal>
    <goal
-    name="wp_conj"
+    name="distib_conj"
     locfile="blocking_semantics2/../blocking_semantics2.mlw"
-    loclnum="738" loccnumb="8" loccnume="15"
-    sum="23b08f704d04d428d797d85ae2c3604c"
+    loclnum="738" loccnumb="8" loccnume="19"
+    sum="e60575064b55782ffe8f8558d7a46584"
     proved="false"
     expanded="false"
     shape="aeval_fmlaV0V1awpV2V4Aaeval_fmlaV0V1awpV2V3qaeval_fmlaV0V1awpV2aFandV3V4F">
     <proof
-     prover="0"
+     prover="4"
      timelimit="3"
      memlimit="0"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="3.01"/>
+     edited="blocking_semantics2_WP_distib_conj_1.v"
+     obsolete="true"
+     archived="false"><undone/>
+     
     </proof>
    </goal>
    <goal
     name="wp_reduction"
     locfile="blocking_semantics2/../blocking_semantics2.mlw"
     loclnum="745" loccnumb="8" loccnume="20"
-    sum="90ce1e7997a6f9374db99d5513603a36"
+    sum="5059669b3b3a48cbf6d38d4db4c9921b"
     proved="false"
     expanded="false"
     shape="aeval_fmlaV1V3awpV5V6Iaeval_fmlaV0V2awpV4V6FIaone_stepV0V2V4V1V3V5F">
@@ -743,50 +749,26 @@
      prover="0"
      timelimit="3"
      memlimit="0"
-     obsolete="false"
+     obsolete="true"
      archived="false">
      <result status="timeout" time="3.01"/>
     </proof>
    </goal>
    <goal
-    name="unique_type_expr"
+    name="decide_value"
     locfile="blocking_semantics2/../blocking_semantics2.mlw"
-    loclnum="758" loccnumb="8" loccnume="24"
-    sum="0b3e72d881397d52b7b4cb3762a45cdf"
-    proved="false"
+    loclnum="758" loccnumb="8" loccnume="20"
+    sum="f83215fbe97c484fb91635a552886b42"
+    proved="true"
     expanded="false"
-    shape="ainfix =V3V4Iatype_exprV1V2V0V4Iatype_exprV1V2V0V3F">
-    <proof
-     prover="7"
-     timelimit="3"
-     memlimit="0"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="3.03"/>
-    </proof>
-    <proof
-     prover="10"
-     timelimit="3"
-     memlimit="0"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="3.02"/>
-    </proof>
+    shape="ainfix =V0aEvalueV1EOais_valueV0NF">
     <proof
      prover="2"
      timelimit="3"
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="3.03"/>
-    </proof>
-    <proof
-     prover="0"
-     timelimit="3"
-     memlimit="0"
-     obsolete="false"
-     archived="false">
-     <result status="timeout" time="3.02"/>
+     <result status="valid" time="0.10"/>
     </proof>
     <proof
      prover="3"
@@ -794,100 +776,75 @@
      memlimit="0"
      obsolete="false"
      archived="false">
-     <result status="timeout" time="3.05"/>
+     <result status="valid" time="0.11"/>
     </proof>
+   </goal>
+   <goal
+    name="bool_value"
+    locfile="blocking_semantics2/../blocking_semantics2.mlw"
+    loclnum="761" loccnumb="8" loccnume="18"
+    sum="c55b461e39acf5f00cb3885269caf6da"
+    proved="false"
+    expanded="true"
+    shape="ainfix =V0aVboolaTrueOainfix =V0aVboolaFalseIatype_exprV1V2aEvalueV0aTYboolF">
     <proof
-     prover="12"
+     prover="11"
      timelimit="3"
      memlimit="0"
-     obsolete="false"
+     obsolete="true"
      archived="false">
-     <result status="highfailure" time="0.00"/>