Commit 5ce32daf authored by charguer's avatar charguer

wp

parent dbf9e439
(* ---------------------------------------------------------------------- *)
(** Weakest precondition, alternative (incomplete) *)
Module WP2.
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.
End WP2.
......@@ -1196,29 +1196,19 @@ 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).
Module WP.
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.
Hexists H, H \* \[triple t H Q].
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. }
{ hsimpl. rew_heap~. }
{ applys~ rule_consequence (rm M). xpull~. }
Qed.
End WP.
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