Commit 9966d214 authored by Asma Tafat's avatar Asma Tafat

blocking semantic

parent eb4c08b3
......@@ -52,6 +52,14 @@ predicate var_occurs_in_term (x:ident) (t:term) =
| Tbin t1 _ t2 -> var_occurs_in_term x t1 \/ var_occurs_in_term x t2
end
(* predicate mvar_occurs_in_term (x:mident) (t:term) = *)
(* match t with *)
(* | Tvalue _ -> false *)
(* | Tvar i -> x = i *)
(* | Tderef _ -> false *)
(* | Tbin t1 _ t2 -> mvar_occurs_in_term x t1 \/ mvar_occurs_in_term x t2 *)
(* end *)
(* predicate term_inv (t:term) = *)
(* forall x:ident. var_occurs_in_term x t -> x.ident_index <= t.term_maxvar *)
......@@ -339,10 +347,14 @@ function subst_term (t:term) (r:ident) (v:ident) : term =
mk_tbin (subst_term t1 r v) op (subst_term t2 r v)
end
(** [fresh_in_term id t] is true when [id] does not occur in [t] *)
predicate fresh_in_term (id:ident) (t:term) =
not (var_occurs_in_term id t)
(* predicate mfresh_in_term (id:mident) (t:term) = *)
(* not (mvar_occurs_in_term id t) *)
lemma fresh_in_binop:
forall t t':term, op:operator, v:ident.
fresh_in_term v (mk_tbin t op t') ->
......@@ -364,6 +376,16 @@ predicate fresh_in_fmla (id:ident) (f:fmla) =
| Fforall y ty f -> id <> y /\ fresh_in_fmla id f
end
(* predicate mfresh_in_fmla (id:mident) (f:fmla) = *)
(* match f with *)
(* | Fterm e -> mfresh_in_term id e *)
(* | Fand f1 f2 | Fimplies f1 f2 -> *)
(* mfresh_in_fmla id f1 /\ mfresh_in_fmla id f2 *)
(* | Fnot f -> mfresh_in_fmla id f *)
(* | Flet y t f -> id <> y /\ mfresh_in_term id t /\ mfresh_in_fmla id f *)
(* | Fforall y ty f -> id <> y /\ mfresh_in_fmla id f *)
(* end *)
function subst (f:fmla) (x:ident) (v:ident) : fmla =
match f with
| Fterm e -> Fterm (subst_term e x v)
......@@ -388,6 +410,7 @@ lemma subst_fresh_term :
forall t:term, x:ident, v:ident.
fresh_in_term x t -> subst_term t x v = t
(*Needed ???*)
lemma subst_fresh :
forall f:fmla, x:ident, v:ident.
fresh_in_fmla x f -> subst f x v = f
......@@ -786,6 +809,10 @@ predicate expr_writes (s:expr) (w:Set.set mident) =
function fresh_from (f:fmla) (s:expr) : ident
lemma msubst_fresh :
forall f:fmla, x:mident, s:expr.
msubst f x (fresh_from f s) = f
(* Need it for monotonicity*)
axiom fresh_from_fmla: forall s:expr, f:fmla.
fresh_in_fmla (fresh_from f s) f
......
......@@ -615,6 +615,10 @@ Parameter x: ident.
Parameter y: mident.
Require Import Why3.
Ltac ae := why3 "alt-ergo" timelimit 3.
(* Why3 goal *)
Theorem Test55expr : (many_steps (const (Vint 0%Z):(map mident value))
(Cons (x, (Vint 42%Z)) (Nil :(list (ident* value)%type))) (Ebin (Evar x)
......@@ -640,37 +644,11 @@ apply many_steps_trans with
(s2 := Evalue (eval_bin (get_stack x pi) Oplus (Vint 13)));
auto with *.
apply one_step_bin_value.
apply one_step_var.
pose (s1 := (Ebin (Evar x) Oplus (Evalue (Vint 13)))).
fold s1.
pose (s2 := (Ebin (Evalue (get_stack x pi)) Oplus (Evalue (Vint 13)))).
assert ((one_step (const (Vint 0)) pi s1 (const (Vint 0)) pi s2)).
apply one_step_bin_ctxt1.
apply one_step_var.
pose (s3 := Evalue (eval_bin (get_stack x pi) Oplus (Vint 13))).
assert ((one_step (const (Vint 0)) pi s2 (const (Vint 0)) pi s3)).
apply one_step_bin_value.
replace (1 -1)%Z with 0%Z; auto with *.
assert (Evalue (eval_bin (get_stack x pi) Oplus (Vint 13)) = Evalue (Vint 55)).
admit.
apply many_steps_trans with
(sigma2 := (const (Vint 0))) (pi2 := pi) (s2 := s2); auto.
clear h.
assert (h: 1%Z = ((0%Z) + (1%Z))%Z).
omega.
rewrite h.
apply many_steps_trans with
(sigma2 := (const (Vint 0))) (pi2 := pi) (s2 := s3); auto.
rewrite <- H1.
ae.
rewrite H.
apply many_steps_refl.
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