Commit e5e241c0 authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid
Browse files

example blocking semantic

parent bdb05c5e
......@@ -321,18 +321,29 @@ lemma let_subst:
forall t:term, f:fmla, x id':ident, id :mident.
msubst (Flet x t f) id id' = Flet x (msubst_term t id id') (msubst f id id')
lemma eval_subst:
lemma eval_msubst:
forall f:fmla, sigma:env, pi:stack, x:mident, v:ident.
fresh_in_fmla v f ->
(eval_fmla sigma pi (msubst f x v) <->
eval_fmla (IdMap.set sigma x (get_stack v pi)) pi f)
lemma eval_subst:
forall f:fmla, sigma:env, pi:stack, x:ident, v:ident.
fresh_in_fmla v f ->
(eval_fmla sigma pi (subst f x v) <->
eval_fmla sigma (Cons(x, (get_stack v pi)) pi) f)
lemma eval_swap:
forall f:fmla, sigma:env, pi:stack, id1 id2:ident, v1 v2:value.
id1 <> id2 ->
(eval_fmla sigma (Cons (id1,v1) (Cons (id2,v2) pi)) f <->
eval_fmla sigma (Cons (id2,v2) (Cons (id1,v1) pi)) f)
lemma eval_same_var:
forall f:fmla, sigma:env, pi:stack, id:ident, v1 v2:value.
eval_fmla sigma (Cons (id,v1) (Cons (id,v2) pi)) f <->
eval_fmla sigma (Cons (id,v1) pi) f
lemma eval_change_free :
forall f:fmla, sigma:env, pi:stack, id:ident, v:value.
fresh_in_fmla id f ->
......@@ -346,9 +357,22 @@ lemma eval_change_free :
lemma let_equiv :
forall id:ident, id':ident, t:term, f:fmla.
forall sigma:env, pi:stack.
eval_fmla sigma pi (Flet id' t (subst f id id'))
-> eval_fmla sigma pi (Flet id t f)
fresh_in_fmla id' f ->
(eval_fmla sigma pi (Flet id' t (subst f id id'))
-> eval_fmla sigma pi (Flet id t f))
lemma let_equiv2 :
forall id:ident, id':ident, t:term, f:fmla.
forall sigma:env, pi:stack.
fresh_in_fmla id' f ->
eval_fmla sigma pi (Flet id' t (subst f id id'))
-> eval_fmla sigma pi (Flet id t f)
lemma let_implies :
forall id:ident, t:term, p q:fmla.
valid_fmla (Fimplies p q) ->
valid_fmla (Fimplies (Flet id t p) (Flet id t q))
predicate fresh_in_expr (id:ident) (e:expr) =
match e with
| Evalue _ -> true
......@@ -626,6 +650,16 @@ lemma while_rule_ext:
end
theory Simpl_tautology
predicate p
predicate q
lemma simpl_tautology :
(p -> q) <-> (p /\ q <-> p)
end
(** {2 WP calculus} *)
theory WP
......@@ -726,21 +760,16 @@ 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 monotonicite:
forall p q:fmla.
(forall sigma:env, pi:stack.
eval_fmla sigma pi p -> eval_fmla sigma pi q)
->
forall sigma:env, pi:stack, e:expr.
eval_fmla sigma pi (wp e p) ->
eval_fmla sigma pi (wp e q)
lemma distib_conj:
lemma distrib_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 monotonicity:
forall e:expr, p q:fmla.
valid_fmla (Fimplies p q)
-> valid_fmla (Fimplies (wp e p) (wp e q) )
lemma wp_reduction:
forall sigma sigma':env, pi pi':stack, e e':expr.
......
......@@ -380,11 +380,16 @@ Axiom let_subst : forall (t:term) (f:fmla) (x:ident) (id':ident) (id:mident),
((msubst (Flet x t f) id id') = (Flet x (msubst_term t id id') (msubst f id
id'))).
Axiom eval_subst : forall (f:fmla) (sigma:(map mident value)) (pi:(list
Axiom eval_msubst : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (x:mident) (v:ident), (fresh_in_fmla v f) ->
((eval_fmla sigma pi (msubst f x v)) <-> (eval_fmla (set sigma x
(get_stack v pi)) pi f)).
Axiom eval_subst : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (x:ident) (v:ident), (fresh_in_fmla v f) ->
((eval_fmla sigma pi (subst f x v)) <-> (eval_fmla sigma (Cons (x,
(get_stack v pi)) pi) f)).
Axiom eval_swap : forall (f:fmla) (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (id1:ident) (id2:ident) (v1:value) (v2:value),
(~ (id1 = id2)) -> ((eval_fmla sigma (Cons (id1, v1) (Cons (id2, v2) pi))
......@@ -400,8 +405,17 @@ Definition valid_fmla(p:fmla): Prop := forall (sigma:(map mident value))
Axiom let_equiv : forall (id:ident) (id':ident) (t:term) (f:fmla),
forall (sigma:(map mident value)) (pi:(list (ident* value)%type)),
(eval_fmla sigma pi (Flet id' t (subst f id id'))) -> (eval_fmla sigma pi
(Flet id t f)).
(fresh_in_fmla id' f) -> ((eval_fmla sigma pi (Flet id' t (subst f id
id'))) -> (eval_fmla sigma pi (Flet id t f))).
Axiom let_equiv2 : forall (id:ident) (id':ident) (t:term) (f:fmla),
forall (sigma:(map mident value)) (pi:(list (ident* value)%type)),
(fresh_in_fmla id' f) -> ((eval_fmla sigma pi (Flet id' t (subst f id
id'))) -> (eval_fmla sigma pi (Flet id t f))).
Axiom let_implies : forall (id:ident) (t:term) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> (valid_fmla (Fimplies (Flet id t p) (Flet id
t q))).
(* Why3 assumption *)
Set Implicit Arguments.
......@@ -696,16 +710,13 @@ Fixpoint wp(e:expr) (q:fmla) {struct e}: fmla :=
end.
Unset Implicit Arguments.
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 distib_conj : forall (sigma:(map mident value)) (pi:(list (ident*
Axiom distrib_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))).
Axiom monotonicity : forall (e:expr) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> (valid_fmla (Fimplies (wp e p) (wp e q))).
Axiom wp_reduction : forall (sigma:(map mident value)) (sigma':(map mident
value)) (pi:(list (ident* value)%type)) (pi':(list (ident* value)%type))
(e:expr) (e':expr), (one_step sigma pi e sigma' pi' e') -> forall (q:fmla),
......@@ -896,9 +907,9 @@ eexists.
eapply one_step_let_value.
(* case 7: e = if e1 then e2 else e3 *)
clear IHe2 IHe3.
destruct (decide_value e1).
(* case 7.1: e1 not a value *)
clear IHe2 IHe3.
intros sigma pi sigmat pit ty q h1 h2 h3 h4.
inversion h1; subst.
simpl in h3.
......@@ -907,13 +918,14 @@ pose (q' := Fand (Fimplies (Fterm (Tvar result)) (wp e2 q))
fold q' in h3.
generalize (IHe1 sigma pi _ _ _ q' H5); clear IHe1.
intros (h5, h6); auto.
(*
generalize (H0 h2 _ H).
exists sigma'.
exists pi'.
exists (Eif e' e2 e3).
eapply one_step_if_ctxt; auto.
eapply one_step_if_ctxt; auto.*)
admit.
admit.
(* case 7.2: e1 is a value *)
elim H; clear H; intros v He_v.
subst.
......
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