12857

1 
(* Title: HOL/Bali/Trans.thy

12854

2 
ID: $Id$


3 
Author: David von Oheimb


4 
Copyright 1997 Technische Universitaet Muenchen


5 


6 
Operational transition (smallstep) semantics of the


7 
execution of Java expressions and statements


8 


9 
PRELIMINARY!!!!!!!!


10 


11 
*)


12 


13 
Trans = Eval +


14 


15 
consts


16 
texpr_tstmt :: "prog \<Rightarrow> (((expr \<times> state) \<times> (expr \<times> state)) +


17 
((stmt \<times> state) \<times> (stmt \<times> state))) set"


18 


19 
syntax (symbols)


20 
texpr :: "[prog, expr \<times> state, expr \<times> state] \<Rightarrow> bool "("_\<turnstile>_ \<rightarrow>1 _"[61,82,82] 81)


21 
tstmt :: "[prog, stmt \<times> state, stmt \<times> state] \<Rightarrow> bool "("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81)


22 
Ref :: "loc \<Rightarrow> expr"


23 


24 
translations


25 


26 
"G\<turnstile>e_s \<rightarrow>1 ex_s'" == "Inl (e_s, ex_s') \<in> texpr_tstmt G"


27 
"G\<turnstile>s_s \<mapsto>1 s'_s'" == "Inr (s_s, s'_s') \<in> texpr_tstmt G"


28 
"Ref a" == "Lit (Addr a)"


29 


30 
inductive "texpr_tstmt G" intrs


31 


32 
(* evaluation of expression *)


33 
(* cf. 15.5 *)


34 
XcptE "\<lbrakk>\<forall>v. e \<noteq> Lit v\<rbrakk> \\<Longrightarrow>


35 
G\<turnstile>(e,Some xc,s) \<rightarrow>1 (Lit arbitrary,Some xc,s)"


36 


37 
(* cf. 15.8.1 *)


38 
NewC "\<lbrakk>new_Addr (heap s) = Some (a,x);


39 
s' = assign (hupd[a\<mapsto>init_Obj G C]s) (x,s)\<rbrakk> \\<Longrightarrow>


40 
G\<turnstile>(NewC C,None,s) \<rightarrow>1 (Ref a,s')"


41 


42 
(* cf. 15.9.1 *)


43 
NewA1 "\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>


44 
G\<turnstile>(New T[e],None,s) \<rightarrow>1 (New T[e'],s')"


45 
NewA "\<lbrakk>i = the_Intg i'; new_Addr (heap s) = Some (a, x);


46 
s' = assign (hupd[a\<mapsto>init_Arr T i]s)(raise_if (i<#0) NegArrSize x,s)\<rbrakk> \\<Longrightarrow>


47 
G\<turnstile>(New T[Lit i'],None,s) \<rightarrow>1 (Ref a,s')"


48 
(* cf. 15.15 *)


49 
Cast1 "\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>


50 
G\<turnstile>(Cast T e,None,s) \<rightarrow>1 (Cast T e',s')"


51 
Cast "\<lbrakk>x'= raise_if (\<questiondown>G,s\<turnstile>v fits T) ClassCast None\<rbrakk> \\<Longrightarrow>


52 
G\<turnstile>(Cast T (Lit v),None,s) \<rightarrow>1 (Lit v,x',s)"


53 


54 
(* cf. 15.7.1 *)


55 
(*Lit "G\<turnstile>(Lit v,None,s) \<rightarrow>1 (Lit v,None,s)"*)


56 


57 
(* cf. 15.13.1, 15.2 *)


58 
LAcc "\<lbrakk>v = the (locals s vn)\<rbrakk> \\<Longrightarrow>


59 
G\<turnstile>(LAcc vn,None,s) \<rightarrow>1 (Lit v,None,s)"


60 


61 
(* cf. 15.25.1 *)


62 
LAss1 "\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>


63 
G\<turnstile>(f vn:=e,None,s) \<rightarrow>1 (vn:=e',s')"


64 
LAss "G\<turnstile>(f vn:=Lit v,None,s) \<rightarrow>1 (Lit v,None,lupd[vn\<mapsto>v]s)"


65 


66 
(* cf. 15.10.1, 15.2 *)


67 
FAcc1 "\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>


68 
G\<turnstile>({T}e..fn,None,s) \<rightarrow>1 ({T}e'..fn,s')"


69 
FAcc "\<lbrakk>v = the (snd (the_Obj (heap s (the_Addr a'))) (fn,T))\<rbrakk> \\<Longrightarrow>


70 
G\<turnstile>({T}Lit a'..fn,None,s) \<rightarrow>1 (Lit v,np a' None,s)"


71 


72 
(* cf. 15.25.1 *)


73 
FAss1 "\<lbrakk>G\<turnstile>(e1,None,s) \<rightarrow>1 (e1',s')\<rbrakk> \\<Longrightarrow>


74 
G\<turnstile>(f ({T}e1..fn):=e2,None,s) \<rightarrow>1 (f({T}e1'..fn):=e2,s')"


75 
FAss2 "\<lbrakk>G\<turnstile>(e2,np a' None,s) \<rightarrow>1 (e2',s')\<rbrakk> \\<Longrightarrow>


76 
G\<turnstile>(f({T}Lit a'..fn):=e2,None,s) \<rightarrow>1 (f({T}Lit a'..fn):=e2',s')"


77 
FAss "\<lbrakk>a = the_Addr a'; (c,fs) = the_Obj (heap s a);


78 
s'= assign (hupd[a\<mapsto>Obj c (fs[(fn,T)\<mapsto>v])]s) (None,s)\<rbrakk> \\<Longrightarrow>


79 
G\<turnstile>(f({T}Lit a'..fn):=Lit v,None,s) \<rightarrow>1 (Lit v,s')"


80 


81 


82 


83 


84 


85 
(* cf. 15.12.1 *)


86 
AAcc1 "\<lbrakk>G\<turnstile>(e1,None,s) \<rightarrow>1 (e1',s')\<rbrakk> \\<Longrightarrow>


87 
G\<turnstile>(e1[e2],None,s) \<rightarrow>1 (e1'[e2],s')"


88 
AAcc2 "\<lbrakk>G\<turnstile>(e2,None,s) \<rightarrow>1 (e2',s')\<rbrakk> \\<Longrightarrow>


89 
G\<turnstile>(Lit a'[e2],None,s) \<rightarrow>1 (Lit a'[e2'],s')"


90 
AAcc "\<lbrakk>vo = snd (the_Arr (heap s (the_Addr a'))) (the_Intg i');


91 
x' = raise_if (vo = None) IndOutBound (np a' None)\<rbrakk> \\<Longrightarrow>


92 
G\<turnstile>(Lit a'[Lit i'],None,s) \<rightarrow>1 (Lit (the vo),x',s)"


93 


94 


95 
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5, 14.15 *)


96 
Call1 "\<lbrakk>G\<turnstile>(e,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>


97 
G\<turnstile>(e..mn({pT}p),None,s) \<rightarrow>1 (e'..mn({pT}p),s')"


98 
Call2 "\<lbrakk>G\<turnstile>(p,None,s) \<rightarrow>1 (p',s')\<rbrakk> \\<Longrightarrow>


99 
G\<turnstile>(Lit a'..mn({pT}p),None,s) \<rightarrow>1 (Lit a'..mn({pT}p'),s')"


100 
Call "\<lbrakk>a = the_Addr a'; (md,(pn,rT),lvars,blk,res) =


101 
the (cmethd G (fst (the_Obj (h a))) (mn,pT))\<rbrakk> \\<Longrightarrow>


102 
G\<turnstile>(Lit a'..mn({pT}Lit pv),None,(h,l)) \<rightarrow>1


103 
(Body blk res l,np a' x,(h,init_vals lvars[This\<mapsto>a'][Super\<mapsto>a'][pn\<mapsto>pv]))"


104 
Body1 "\<lbrakk>G\<turnstile>(s0,None,s) \<mapsto>1 (s0',s')\<rbrakk> \\<Longrightarrow>


105 
G\<turnstile>(Body s0 e l,None,s) \<rightarrow>1 (Body s0' e l,s')"


106 
Body2 "\<lbrakk>G\<turnstile>(e ,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>


107 
G\<turnstile>(Body Skip e l,None,s) \<rightarrow>1 (Body Skip e' l,s')"


108 
Body "G\<turnstile>(Body Skip (Lit v) l,None,s) \<rightarrow>1 (Lit v,None,(heap s,l))"


109 


110 
(* execution of statements *)


111 


112 
(* cf. 14.1 *)


113 
XcptS "\<lbrakk>s0 \<noteq> Skip\<rbrakk> \\<Longrightarrow>


114 
G\<turnstile>(s0,Some xc,s) \<mapsto>1 (Skip,Some xc,s)"


115 


116 
(* cf. 14.5 *)


117 
(*Skip "G\<turnstile>(Skip,None,s) \<mapsto>1 (Skip,None,s)"*)


118 


119 
(* cf. 14.2 *)


120 
Comp1 "\<lbrakk>G\<turnstile>(s1,None,s) \<mapsto>1 (s1',s')\<rbrakk> \\<Longrightarrow>


121 
G\<turnstile>(s1;; s2,None,s) \<mapsto>1 (s1';; s2,s')"


122 
Comp "G\<turnstile>(Skip;; s2,None,s) \<mapsto>1 (s2,None,s)"


123 


124 


125 


126 


127 


128 


129 
(* cf. 14.7 *)


130 
Expr1 "\<lbrakk>G\<turnstile>(e ,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>


131 
G\<turnstile>(Expr e,None,s) \<mapsto>1 (Expr e',s')"


132 
Expr "G\<turnstile>(Expr (Lit v),None,s) \<mapsto>1 (Skip,None,s)"


133 


134 
(* cf. 14.8.2 *)


135 
If1 "\<lbrakk>G\<turnstile>(e ,None,s) \<rightarrow>1 (e',s')\<rbrakk> \\<Longrightarrow>


136 
G\<turnstile>(If(e) s1 Else s2,None,s) \<mapsto>1 (If(e') s1 Else s2,s')"


137 
If "G\<turnstile>(If(Lit v) s1 Else s2,None,s) \<mapsto>1


138 
(if the_Bool v then s1 else s2,None,s)"


139 


140 
(* cf. 14.10, 14.10.1 *)


141 
Loop "G\<turnstile>(While(e) s0,None,s) \<mapsto>1


142 
(If(e) (s0;; While(e) s0) Else Skip,None,s)"


143 


144 
end
