Commit 7c91d500 authored by Asma Tafat-Bouzid's avatar Asma Tafat-Bouzid

blocking semantic expression : proof

parent 427427a8
......@@ -242,7 +242,6 @@ function eval_term (sigma:env) (pi:stack) (t:term) : value =
eval_bin (eval_term sigma pi t1) op (eval_term sigma pi t2)
end
lemma eval_bool_term:
forall sigma:env, pi:stack, sigmat:type_env, pit:type_stack, t:term.
type_term sigmat pit t TYbool ->
......
......@@ -299,6 +299,25 @@ predicate eval_fmla (sigma:env) (pi:stack) (f:fmla) =
| Fforall x TYunit f -> eval_fmla sigma (Cons (x,Vvoid) pi) f
end
function eval_expr (sigma:env) (pi:stack) (e:expr) : value =
match e with
| Evalue v -> v
| Evar id -> get_stack id pi
| Ederef id -> get_env id sigma
| Ebin e1 op e2 ->
eval_bin (eval_expr sigma pi e1) op (eval_expr sigma pi e2)
| Eassign id e1
| Eseq e1 e2
| Elet id e1 e2 -> void
| Eif e1 e2 e3 ->
if ((eval_expr sigma pi e1) = (Vbool True))
then eval_expr sigma pi e2
else eval_expr sigma pi e3
| Eassert f -> eval_fmla f
| Ewhile expr fmla expr ->
end
(** substitution of a reference [r] by a logic variable [v]
warning: proper behavior only guaranted if [v] is "fresh",
i.e index(v) > term_maxvar(t) *)
......@@ -632,13 +651,13 @@ goal Test42 :
eval_term my_sigma my_pi (Tvar x) = Vint 42
goal Test42expr :
many_steps my_sigma my_pi (Evar x) my_sigma my_pi (Evalue (Vint 42)) 1
one_step my_sigma my_pi (Evar x) my_sigma my_pi (Evalue (Vint 42))
goal Test0 :
eval_term my_sigma my_pi (Tderef y) = Vint 0
goal Test0expr :
many_steps my_sigma my_pi (Ederef y) my_sigma my_pi (Evalue (Vint 0)) 1
one_step my_sigma my_pi (Ederef y) my_sigma my_pi (Evalue (Vint 0))
goal Test55 :
eval_term my_sigma my_pi (Tbin (Tvar x) Oplus (Tvalue (Vint 13))) = Vint 55
......
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