Commit 78b1cfdc authored by charguer's avatar charguer

wp

parent ac5f8c51
......@@ -7,9 +7,7 @@ Require Import TLC.LibListZ.
(********************************************************************)
(** CFML Buffer *)
(* todo: remove *)
Axiom while_loop_cf_inv_partial :
Lemma while_loop_cf_inv_partial :
forall (I:bool->hprop),
forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop),
(exists b, H ==> I b) ->
......@@ -17,8 +15,9 @@ Axiom while_loop_cf_inv_partial :
(F2 (I true) (# Hexists b, (I b))) ->
(I false ==> Q tt) ->
(While F1 Do F2 Done_) H Q.
Admitted. (* now proved elsewhere *)
Axiom while_loop_cf_inv_partial_gc :
Lemma while_loop_cf_inv_partial_gc :
forall (I:bool->hprop),
forall (F1:~~bool) (F2:~~unit) H (Q:unit->hprop),
(exists b, H ==> I b) ->
......@@ -26,7 +25,7 @@ Axiom while_loop_cf_inv_partial_gc :
(F2 (I true) (# Hexists b, (I b))) ->
(I false ==> Q tt \* Hexists H', H') ->
(While F1 Do F2 Done_) H Q.
Admitted. (* now proved elsewhere *)
(********************************************************************)
......
......@@ -421,7 +421,7 @@ Lemma rule_mlist_length_1 : forall L p,
(MList L p)
(fun r => \[r = val_int (length L)] \* MList L p).
Proof using.
intros L. induction_wf: list_sub_wf L. xcf.
intros L. induction_wf: list_sub_wf L. xcf. fold val_mlist_length.
xapps. xif ;=> C.
{ xchanges~ (MList_not_null_inv_cons p) ;=> x p' L' EL. subst L.
xapps. xapps~ IH.
......
......@@ -1193,3 +1193,32 @@ Qed.
*)
(* ---------------------------------------------------------------------- *)
(** Weakest precondition *)
Require Import LibEpsilon.
Definition wp_spec (t:trm) (Q:val->hprop) (H:hprop) :=
triple t H Q /\ (forall H', triple t H' Q -> H' ==> H).
Definition wp (t:trm) (Q:val->hprop) : hprop :=
epsilon (wp_spec t Q).
Lemma wp_exists : forall t Q, exists H, wp_spec t Q H.
Proof using.
Admitted.
Lemma wp_equiv : forall t H Q,
triple t H Q <-> (H ==> wp t Q).
Proof using.
intros. unfold wp. iff M.
{ spec_epsilon as H' (M1&M2). applys wp_exists.
applys~ M2. }
{ spec_epsilon as H' (M1&M2). applys wp_exists.
applys~ rule_consequence M M1. }
Qed.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment