Up to index of Isabelle/Bali5
theory Evaln = Eval(* Title: isabelle/Bali/Evaln.thy
ID: $Id: Evaln.thy,v 1.32 2000/11/19 19:09:36 oheimb Exp $
Author: David von Oheimb
Copyright 1999 Technische Universitaet Muenchen
Operational evaluation (big-step) semantics of Java expressions and statements
Variant of eval relation with counter for bounded recursive depth
Evaln could completely replace Eval.
*)
Evaln = Eval +
consts
evaln :: "prog \<Rightarrow> (state × term × nat × vals × state) set"
syntax
evaln :: "[prog, state, term, nat, vals * state] => bool"
("_|-_ -_>-_-> _" [61,61,80, 61,61] 60)
evarn :: "[prog, state, var , vvar , nat, state] => bool"
("_|-_ -_=>_-_-> _" [61,61,90,61,61,61] 60)
eval_n:: "[prog, state, expr , val , nat, state] => bool"
("_|-_ -_->_-_-> _" [61,61,80,61,61,61] 60)
evalsn:: "[prog, state, expr list, val list, nat, state] => bool"
("_|-_ -_#>_-_-> _" [61,61,61,61,61,61] 60)
execn :: "[prog, state, stmt , nat, state] => bool"
("_|-_ -_-_-> _" [61,61,65, 61,61] 60)
syntax (xsymbols)
evaln :: "[prog, state, term, nat, vals × state] \<Rightarrow> bool"
("_\<turnstile>_ \<midarrow>_\<succ>\<midarrow>_\<rightarrow> _" [61,61,80, 61,61] 60)
evarn :: "[prog, state, var , vvar , nat, state] \<Rightarrow> bool"
("_\<turnstile>_ \<midarrow>_=\<succ>_\<midarrow>_\<rightarrow> _" [61,61,90,61,61,61] 60)
eval_n:: "[prog, state, expr , val , nat, state] \<Rightarrow> bool"
("_\<turnstile>_ \<midarrow>_-\<succ>_\<midarrow>_\<rightarrow> _" [61,61,80,61,61,61] 60)
evalsn:: "[prog, state, expr list, val list, nat, state] \<Rightarrow> bool"
("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<midarrow>_\<rightarrow> _" [61,61,61,61,61,61] 60)
execn :: "[prog, state, stmt , nat, state] \<Rightarrow> bool"
("_\<turnstile>_ \<midarrow>_\<midarrow>_\<rightarrow> _" [61,61,65, 61,61] 60)
translations
"G\<turnstile>s \<midarrow>t \<succ>\<midarrow>n\<rightarrow> w___s' " == "(s,t,n,w___s') \<in> evaln G"
"G\<turnstile>s \<midarrow>t \<succ>\<midarrow>n\<rightarrow> (w, s')" <= "(s,t,n,w, s') \<in> evaln G"
"G\<turnstile>s \<midarrow>t \<succ>\<midarrow>n\<rightarrow> (w,x,s')" <= "(s,t,n,w,x,s') \<in> evaln G"
"G\<turnstile>s \<midarrow>c \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<midarrow>n\<rightarrow> (\<bullet> ,x,s')"
"G\<turnstile>s \<midarrow>c \<midarrow>n\<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<midarrow>n\<rightarrow> (\<bullet> , s')"
"G\<turnstile>s \<midarrow>e-\<succ>v \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v ,x,s')"
"G\<turnstile>s \<midarrow>e-\<succ>v \<midarrow>n\<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<midarrow>n\<rightarrow> (In1 v , s')"
"G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In2 e\<succ>\<midarrow>n\<rightarrow> (In2 vf,x,s')"
"G\<turnstile>s \<midarrow>e=\<succ>vf \<midarrow>n\<rightarrow> s' " == "G\<turnstile>s \<midarrow>In2 e\<succ>\<midarrow>n\<rightarrow> (In2 vf, s')"
"G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<midarrow>n\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In3 e\<succ>\<midarrow>n\<rightarrow> (In3 v ,x,s')"
"G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<midarrow>n\<rightarrow> s' " == "G\<turnstile>s \<midarrow>In3 e\<succ>\<midarrow>n\<rightarrow> (In3 v , s')"
inductive "evaln G" intrs
(* propagation of exceptions *)
Xcpt "G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<midarrow>n\<rightarrow> (arbitrary3 t,(Some xc,s))"
(* evaluation of variables *)
LVar "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<midarrow>n\<rightarrow> Norm s"
FVar "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init C\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s2;
(v,s2') = fvar C stat fn a' s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>{C,stat}e..fn=\<succ>v\<midarrow>n\<rightarrow> s2'"
AVar "\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1-\<succ>a\<midarrow>n\<rightarrow> s1 ; G\<turnstile>s1 \<midarrow>e2-\<succ>i\<midarrow>n\<rightarrow> s2;
(v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<midarrow>n\<rightarrow> s2'"
(* evaluation of expressions *)
NewC "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init C\<midarrow>n\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>NewC C-\<succ>Addr a\<midarrow>n\<rightarrow> s2"
NewA "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e-\<succ>i'\<midarrow>n\<rightarrow> s2;
G\<turnstile>xupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>New T[e]-\<succ>Addr a\<midarrow>n\<rightarrow> s3"
Cast "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
s2 = xupd (raise_if (¬G,snd s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Cast T e-\<succ>v\<midarrow>n\<rightarrow> s2"
Inst "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1;
b = (v\<noteq>Null \<and> G,snd s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>e InstOf T-\<succ>Bool b\<midarrow>n\<rightarrow> s1"
Lit "G\<turnstile>Norm s \<midarrow>Lit v-\<succ>v\<midarrow>n\<rightarrow> Norm s"
Super "G\<turnstile>Norm s \<midarrow>Super-\<succ>val_this s\<midarrow>n\<rightarrow> Norm s"
Acc "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Acc va-\<succ>v\<midarrow>n\<rightarrow> s1"
Ass "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<midarrow>n\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>e-\<succ>v \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>va:=e-\<succ>v\<midarrow>n\<rightarrow> assign f v s2"
Cond "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0-\<succ>b\<midarrow>n\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>(if the_Bool b then e1 else e2)-\<succ>v\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2-\<succ>v\<midarrow>n\<rightarrow> s2"
Call "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2;
C = target mode (snd s2) a' cT;
G\<turnstile>init_lvars G C (mn,pTs) mode a' vs s2 \<midarrow>Methd C (mn,pTs)-\<succ>v\<midarrow>n\<rightarrow> s3\<rbrakk>
\<Longrightarrow> G\<turnstile>Norm s0 \<midarrow>{t,cT,mode}e..mn({pTs}args)-\<succ>v\<midarrow>n\<rightarrow> (restore_lvars s2 s3)"
Methd "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G C sig-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Methd C sig-\<succ>v\<midarrow>Suc n\<rightarrow> s1"
Body "\<lbrakk>G\<turnstile>Norm s0\<midarrow>init D\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2; G\<turnstile>s2 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s3\<rbrakk>\<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Body D c e-\<succ>v\<midarrow>n\<rightarrow> s3"
(* evaluation of expression lists *)
Nil
"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<midarrow>n\<rightarrow> Norm s0"
Cons "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e -\<succ> v \<midarrow>n\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>es\<doteq>\<succ>vs\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<midarrow>n\<rightarrow> s2"
(* execution of statements *)
Skip "G\<turnstile>Norm s \<midarrow>Skip\<midarrow>n\<rightarrow> Norm s"
Expr "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>v\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Expr e\<midarrow>n\<rightarrow> s1"
Comp "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<midarrow>n\<rightarrow> s1;
G\<turnstile> s1 \<midarrow>c2 \<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>c1;; c2\<midarrow>n\<rightarrow> s2"
If "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
G\<turnstile> s1\<midarrow>(if the_Bool b then c1 else c2)\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<midarrow>n\<rightarrow> s2"
Loop "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>b\<midarrow>n\<rightarrow> s1;
if the_Bool b then (G\<turnstile>s1 \<midarrow>c\<midarrow>n\<rightarrow> s2 \<and> G\<turnstile>s2 \<midarrow>While(e) c\<midarrow>n\<rightarrow> s3)
else s3 = s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>While(e) c\<midarrow>n\<rightarrow> s3"
Throw "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e-\<succ>a'\<midarrow>n\<rightarrow> s1\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Throw e\<midarrow>n\<rightarrow> xupd (throw a') s1"
Try "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2;
if G,s2\<turnstile>catch tn then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<midarrow>n\<rightarrow> s3 else s3 = s2\<rbrakk>\<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(tn vn) c2\<midarrow>n\<rightarrow> s3"
Fin "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<midarrow>n\<rightarrow> (x1,s1);
G\<turnstile>Norm s1 \<midarrow>c2\<midarrow>n\<rightarrow> s2\<rbrakk> \<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<midarrow>n\<rightarrow> xupd (xcpt_if (x1\<noteq>None) x1) s2"
Init "\<lbrakk>the (class G C) = (sc,si,fs,ms,ini);
if inited C (globs s0) then s3 = Norm s0
else (G\<turnstile>Norm (init_class_obj G C s0)
\<midarrow>(if C = Object then Skip else init sc)\<midarrow>n\<rightarrow> s1 \<and>
G\<turnstile>set_lvars empty s1 \<midarrow>ini\<midarrow>n\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk>\<Longrightarrow>
G\<turnstile>Norm s0 \<midarrow>init C\<midarrow>n\<rightarrow> s3"
monos
if_def2
end
theorem evaln_eval:
G|-s -t>-n-> ws ==> G|-s -t>-> ws [!]
theorem Suc_le_D_lemma:
[| Suc n <= m'; !!m. n <= m ==> P (Suc m) |] ==> P m'
theorem evaln_nonstrict:
[| G|-s -t>-n-> ws; n <= m |] ==> G|-s -t>-m-> ws
theorem evaln_max2:
[| G|-s1 -t1>-n1-> ws1; G|-s2 -t2>-n2-> ws2 |] ==> G|-s1 -t1>-max n1 n2-> ws1 & G|-s2 -t2>-max n1 n2-> ws2
theorem evaln_max3:
[| G|-s1 -t1>-n1-> ws1; G|-s2 -t2>-n2-> ws2; G|-s3 -t3>-n3-> ws3 |]
==> G|-s1 -t1>-max (max n1 n2) n3-> ws1 &
G|-s2 -t2>-max (max n1 n2) n3-> ws2 & G|-s3 -t3>-max (max n1 n2) n3-> ws3
theorem eval_evaln:
G|-s -t>-> ws ==> EX n. G|-s -t>-n-> ws
theorem evaln_Inj_elim:
G|-s -t>-n-> (w, s')
==> sum3_case ((%e. EX v. w = In1 v) (+) (%c. w = dummy_res))
(%e. EX v. w = In2 v) (%e. EX v. w = In3 v) t
theorem evaln_expr_eq:
G|-s -In1l t>-n-> (w, s') = (EX v. w = In1 v & G|-s -t->v-n-> s')
theorem evaln_var_eq:
G|-s -In2 t>-n-> (w, s') = (EX vf. w = In2 vf & G|-s -t=>vf-n-> s')
theorem evaln_exprs_eq:
G|-s -In3 t>-n-> (w, s') = (EX vs. w = In3 vs & G|-s -t#>vs-n-> s')
theorem evaln_stmt_eq:
G|-s -In1r t>-n-> (w, s') = (w = dummy_res & G|-s -t-n-> s')
theorem evaln_LitI:
G|-s -Lit v->(if normal s then v else arbitrary)-n-> s
theorem CondI:
[| G|-s -e->b-n-> s1; G|-s1 -(if the_Bool b then e1 else e2)->v-n-> s2 |] ==> G|-s -e ? e1 : e2->(if normal s1 then v else arbitrary)-n-> s2
theorem evaln_SkipI:
G|-s -Skip-n-> s
theorem evaln_ExprI:
G|-s -e->v-n-> s' ==> G|-s -Expr e-n-> s'
theorem evaln_CompI:
[| G|-s -c1-n-> s1; G|-s1 -c2-n-> s2 |] ==> G|-s -c1;; c2-n-> s2
theorem evaln_IfI:
[| G|-s -e->v-n-> s1; G|-s1 -(if the_Bool v then c1 else c2)-n-> s2 |] ==> G|-s -If(e) c1 Else c2-n-> s2
theorem evaln_SkipD:
G|-s -Skip-n-> s' ==> s' = s [!]
theorem evaln_Skip_eq:
G|-s -Skip-n-> s' = (s = s') [!]
theorem evaln_xcpt_lemma:
G|-s -e>-n-> (v, s') ==> fst s = Some xc --> s' = s & v = arbitrary3 e
theorem evaln_xcpt:
G|-(Some xc, s) -e>-n-> (w, s') = (s' = (Some xc, s) & w = arbitrary3 e & G|-(Some xc, s) -e>-n-> (arbitrary3 e, Some xc, s))