Commit 685c7122 authored by atafat's avatar atafat

blocking semantic: monotonicity

parent faa676b0
......@@ -383,10 +383,16 @@ lemma eval_change_free :
fresh_in_fmla id f ->
(eval_fmla sigma (Cons (id,v) pi) f <-> eval_fmla sigma pi f)
(** [valid_fmla f] is true when [f] is valid in any environment *)
(** [valid_fmla f] is true when [f] is valid in any environment *)
predicate valid_fmla (p:fmla) = forall sigma:env, pi:stack. eval_fmla sigma pi p
axiom msubst_implies :
forall p q:fmla.
valid_fmla (Fimplies p q) ->
forall sigma:env, pi:stack, x:mident, id:ident.
fresh_in_fmla id (Fand p q) ->
eval_fmla sigma (Cons (id, (get_env x sigma)) pi) (Fimplies (msubst p x id) (msubst q x id))
(** let id' = t in f[id <- id'] <=> let id = t in f*)
lemma let_equiv :
forall id:ident, id':ident, t:term, f:fmla.
......@@ -675,8 +681,8 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
axiom abstract_effects_monotonic :
forall s:stmt, f:fmla.
valid_fmla f ->
valid_fmla (abstract_effects s f)
forall sigma:env, pi:stack. eval_fmla sigma pi f ->
forall sigma:env, pi:stack. eval_fmla sigma pi (abstract_effects s f)
function wp (s:stmt) (q:fmla) : fmla =
match s with
......@@ -749,4 +755,3 @@ Local Variables:
compile-command: "why3ide blocking_semantics3.mlw"
End:
*)
......@@ -670,7 +670,9 @@ Axiom abstract_effects_generalize : forall (sigma:(map mident value))
(abstract_effects s f)) -> (eval_fmla sigma pi f).
Axiom abstract_effects_monotonic : forall (s:stmt) (f:fmla),
(valid_fmla f) -> (valid_fmla (abstract_effects s f)).
forall (sigma:(map mident value)) (pi:(list (ident* value)%type)),
(eval_fmla sigma pi f) -> forall (sigma1:(map mident value)) (pi1:(list
(ident* value)%type)), (eval_fmla sigma1 pi1 (abstract_effects s f)).
(* Why3 assumption *)
Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla :=
......@@ -709,6 +711,16 @@ destruct s; auto.
unfold valid_fmla; simpl.
intros H1 p q H2 sigma pi (H3 & H4).
split; auto.
generalize (abstract_effects_monotonic _ _ H4).
apply abstract_effects_monotonic with (sigma := sigma) (pi:=pi).
simpl.
split; simpl; intros (H5 & H6);
apply abstract_effects_generalize in H4;
simpl in H4; destruct H4.
(* True *)
apply H; auto.
(* False *)
apply H2.
apply H0; auto.
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