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

update blocking semantics3

parent 9d44ae57
...@@ -709,9 +709,9 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) = ...@@ -709,9 +709,9 @@ predicate stmt_writes (s:stmt) (w:Set.set mident) =
lemma distrib_conj: lemma distrib_conj:
forall sigma:env, pi:stack, s:stmt, p q:fmla. forall sigma:env, pi:stack, s:stmt, p q:fmla.
eval_fmla sigma pi (wp s (Fand p q)) <-> (eval_fmla sigma pi (wp s p)) /\
(eval_fmla sigma pi (wp s p)) /\ (eval_fmla sigma pi (wp s q)) ->
(eval_fmla sigma pi (wp s q)) eval_fmla sigma pi (wp s (Fand p q))
(* (*
lemma monotonicity: lemma monotonicity:
......
...@@ -499,7 +499,7 @@ Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt ...@@ -499,7 +499,7 @@ Inductive one_step : (map mident value) -> (list (ident* value)%type) -> stmt
value)%type)) (cond:term) (inv:fmla) (body:stmt), (eval_fmla sigma pi value)%type)) (cond:term) (inv:fmla) (body:stmt), (eval_fmla sigma pi
inv) -> (((eval_term sigma pi cond) = (Vbool true)) -> (one_step sigma inv) -> (((eval_term sigma pi cond) = (Vbool true)) -> (one_step sigma
pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body)))) pi (Swhile cond inv body) sigma pi (Sseq body (Swhile cond inv body))))
| one_step_while_falsee : forall (sigma:(map mident value)) (pi:(list | one_step_while_false : forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (cond:term) (inv:fmla) (body:stmt), (ident* value)%type)) (cond:term) (inv:fmla) (body:stmt),
(eval_fmla sigma pi inv) -> (((eval_term sigma pi (eval_fmla sigma pi inv) -> (((eval_term sigma pi
cond) = (Vbool false)) -> (one_step sigma pi (Swhile cond inv body) cond) = (Vbool false)) -> (one_step sigma pi (Swhile cond inv body)
...@@ -665,6 +665,10 @@ Axiom fresh_from_stmt : forall (s:stmt) (f:fmla), ...@@ -665,6 +665,10 @@ Axiom fresh_from_stmt : forall (s:stmt) (f:fmla),
Parameter abstract_effects: stmt -> fmla -> fmla. Parameter abstract_effects: stmt -> fmla -> fmla.
Axiom abstract_effects_generalize : forall (sigma:(map mident value))
(pi:(list (ident* value)%type)) (s:stmt) (f:fmla), (eval_fmla sigma pi
(abstract_effects s f)) -> (eval_fmla sigma pi f).
(* Why3 assumption *) (* Why3 assumption *)
Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla := Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla :=
match s with match s with
...@@ -680,13 +684,15 @@ Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla := ...@@ -680,13 +684,15 @@ Fixpoint wp(s:stmt) (q:fmla) {struct s}: fmla :=
(Fimplies (Fand (Fnot (Fterm cond)) inv) q)))) (Fimplies (Fand (Fnot (Fterm cond)) inv) q))))
end. end.
Axiom abstract_effects_writes : forall (sigma:(map mident value)) (pi:(list
(ident* value)%type)) (s:stmt) (q:fmla), (eval_fmla sigma pi
(abstract_effects s q)) -> (eval_fmla sigma pi (wp s (abstract_effects s
q))).
Axiom distrib_conj : forall (sigma:(map mident value)) (pi:(list (ident* Axiom distrib_conj : forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (s:stmt) (p:fmla) (q:fmla), (eval_fmla sigma pi (wp s (Fand p value)%type)) (s:stmt) (p:fmla) (q:fmla), (eval_fmla sigma pi (wp s (Fand p
q))) <-> ((eval_fmla sigma pi (wp s p)) /\ (eval_fmla sigma pi (wp s q))). q))) <-> ((eval_fmla sigma pi (wp s p)) /\ (eval_fmla sigma pi (wp s q))).
Axiom monotonicity : forall (s:stmt) (p:fmla) (q:fmla),
(valid_fmla (Fimplies p q)) -> (valid_fmla (Fimplies (wp s p) (wp s q))).
Axiom wp_reduction : forall (sigma:(map mident value)) (sigma':(map mident Axiom wp_reduction : forall (sigma:(map mident value)) (sigma':(map mident
value)) (pi:(list (ident* value)%type)) (pi':(list (ident* value)%type)) value)) (pi:(list (ident* value)%type)) (pi':(list (ident* value)%type))
(s:stmt) (s':stmt), (one_step sigma pi s sigma' pi' s') -> forall (q:fmla), (s:stmt) (s':stmt), (one_step sigma pi s sigma' pi' s') -> forall (q:fmla),
......
...@@ -690,8 +690,8 @@ Axiom abstract_effects_writes : forall (sigma:(map mident value)) (pi:(list ...@@ -690,8 +690,8 @@ Axiom abstract_effects_writes : forall (sigma:(map mident value)) (pi:(list
q))). q))).
Axiom distrib_conj : forall (sigma:(map mident value)) (pi:(list (ident* Axiom distrib_conj : forall (sigma:(map mident value)) (pi:(list (ident*
value)%type)) (s:stmt) (p:fmla) (q:fmla), (eval_fmla sigma pi (wp s (Fand p value)%type)) (s:stmt) (p:fmla) (q:fmla), ((eval_fmla sigma pi (wp s p)) /\
q))) <-> ((eval_fmla sigma pi (wp s p)) /\ (eval_fmla sigma pi (wp s q))). (eval_fmla sigma pi (wp s q))) -> (eval_fmla sigma pi (wp s (Fand p q))).
(* Why3 goal *) (* Why3 goal *)
Theorem wp_reduction : forall (sigma:(map mident value)) (sigma':(map mident Theorem wp_reduction : forall (sigma:(map mident value)) (sigma':(map mident
...@@ -735,7 +735,7 @@ intuition. ...@@ -735,7 +735,7 @@ intuition.
simpl. simpl.
simpl in Hq. simpl in Hq.
destruct Hq as (h1 & h2). destruct Hq as (h1 & h2).
rewrite distrib_conj; split. apply distrib_conj; split.
generalize (abstract_effects_generalize _ _ _ _ h2). generalize (abstract_effects_generalize _ _ _ _ h2).
intros h3. intros h3.
simpl in h3. simpl in h3.
......
Supports Markdown
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