1(* Title: HOL/Bali/Trans.thy 2 Author: David von Oheimb and Norbert Schirmer 3 4Operational transition (small-step) semantics of the 5execution of Java expressions and statements 6 7PRELIMINARY!!!!!!!! 8*) 9 10theory Trans imports Evaln begin 11 12definition 13 groundVar :: "var \<Rightarrow> bool" where 14 "groundVar v \<longleftrightarrow> (case v of 15 LVar ln \<Rightarrow> True 16 | {accC,statDeclC,stat}e..fn \<Rightarrow> \<exists> a. e=Lit a 17 | e1.[e2] \<Rightarrow> \<exists> a i. e1= Lit a \<and> e2 = Lit i 18 | InsInitV c v \<Rightarrow> False)" 19 20lemma groundVar_cases: 21 assumes ground: "groundVar v" 22 obtains (LVar) ln where "v=LVar ln" 23 | (FVar) accC statDeclC stat a fn where "v={accC,statDeclC,stat}(Lit a)..fn" 24 | (AVar) a i where "v=(Lit a).[Lit i]" 25 using ground LVar FVar AVar 26 by (cases v) (auto simp add: groundVar_def) 27 28definition 29 groundExprs :: "expr list \<Rightarrow> bool" 30 where "groundExprs es \<longleftrightarrow> (\<forall>e \<in> set es. \<exists>v. e = Lit v)" 31 32primrec the_val:: "expr \<Rightarrow> val" 33 where "the_val (Lit v) = v" 34 35primrec the_var:: "prog \<Rightarrow> state \<Rightarrow> var \<Rightarrow> (vvar \<times> state)" where 36 "the_var G s (LVar ln) = (lvar ln (store s),s)" 37| the_var_FVar_def: "the_var G s ({accC,statDeclC,stat}a..fn) =fvar statDeclC stat fn (the_val a) s" 38| the_var_AVar_def: "the_var G s(a.[i]) =avar G (the_val i) (the_val a) s" 39 40lemma the_var_FVar_simp[simp]: 41"the_var G s ({accC,statDeclC,stat}(Lit a)..fn) = fvar statDeclC stat fn a s" 42by (simp) 43declare the_var_FVar_def [simp del] 44 45lemma the_var_AVar_simp: 46"the_var G s ((Lit a).[Lit i]) = avar G i a s" 47by (simp) 48declare the_var_AVar_def [simp del] 49 50abbreviation 51 Ref :: "loc \<Rightarrow> expr" 52 where "Ref a == Lit (Addr a)" 53 54abbreviation 55 SKIP :: "expr" 56 where "SKIP == Lit Unit" 57 58inductive 59 step :: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>1 _"[61,82,82] 81) 60 for G :: prog 61where 62 63(* evaluation of expression *) 64 (* cf. 15.5 *) 65 Abrupt: "\<lbrakk>\<forall>v. t \<noteq> \<langle>Lit v\<rangle>; 66 \<forall> t. t \<noteq> \<langle>l\<bullet> Skip\<rangle>; 67 \<forall> C vn c. t \<noteq> \<langle>Try Skip Catch(C vn) c\<rangle>; 68 \<forall> x c. t \<noteq> \<langle>Skip Finally c\<rangle> \<and> xc \<noteq> Xcpt x; 69 \<forall> a c. t \<noteq> \<langle>FinA a c\<rangle>\<rbrakk> 70 \<Longrightarrow> 71 G\<turnstile>(t,Some xc,s) \<mapsto>1 (\<langle>Lit undefined\<rangle>,Some xc,s)" 72 73| InsInitE: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>, s')\<rbrakk> 74 \<Longrightarrow> 75 G\<turnstile>(\<langle>InsInitE c e\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE c' e\<rangle>, s')" 76 77(* SeqE: "G\<turnstile>(\<langle>Seq Skip e\<rangle>,Norm s) \<mapsto>1 (\<langle>e\<rangle>, Norm s)" *) 78(* Specialised rules to evaluate: 79 InsInitE Skip (NewC C), InisInitE Skip (NewA T[e]) *) 80 81 (* cf. 15.8.1 *) 82| NewC: "G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init C) (NewC C)\<rangle>, Norm s)" 83| NewCInited: "\<lbrakk>G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 84 \<Longrightarrow> 85 G\<turnstile>(\<langle>InsInitE Skip (NewC C)\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')" 86 87 88 89(* Alternative when rule SeqE is present 90NewCInited: "\<lbrakk>inited C (globs s); 91 G\<turnstile> Norm s \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s'\<rbrakk> 92 \<Longrightarrow> 93 G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>, s')" 94 95NewC: 96 "\<lbrakk>\<not> inited C (globs s)\<rbrakk> 97 \<Longrightarrow> 98 G\<turnstile>(\<langle>NewC C\<rangle>,Norm s) \<mapsto>1 (\<langle>Seq (Init C) (NewC C)\<rangle>, Norm s)" 99 100*) 101 (* cf. 15.9.1 *) 102| NewA: 103 "G\<turnstile>(\<langle>New T[e]\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (init_comp_ty T) (New T[e])\<rangle>,Norm s)" 104| InsInitNewAIdx: 105 "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>, s')\<rbrakk> 106 \<Longrightarrow> 107 G\<turnstile>(\<langle>InsInitE Skip (New T[e])\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE Skip (New T[e'])\<rangle>,s')" 108| InsInitNewA: 109 "\<lbrakk>G\<turnstile>abupd (check_neg i) (Norm s) \<midarrow>halloc (Arr T (the_Intg i))\<succ>a\<rightarrow> s' \<rbrakk> 110 \<Longrightarrow> 111 G\<turnstile>(\<langle>InsInitE Skip (New T[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Ref a\<rangle>,s')" 112 113 (* cf. 15.15 *) 114| CastE: 115 "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 116 \<Longrightarrow> 117 G\<turnstile>(\<langle>Cast T e\<rangle>,None,s) \<mapsto>1 (\<langle>Cast T e'\<rangle>,s')" 118| Cast: 119 "\<lbrakk>s' = abupd (raise_if (\<not>G,s\<turnstile>v fits T) ClassCast) (Norm s)\<rbrakk> 120 \<Longrightarrow> 121 G\<turnstile>(\<langle>Cast T (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')" 122 (* can be written without abupd, since we know Norm s *) 123 124 125| InstE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 126 \<Longrightarrow> 127 G\<turnstile>(\<langle>e InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')" 128| Inst: "\<lbrakk>b = (v\<noteq>Null \<and> G,s\<turnstile>v fits RefT T)\<rbrakk> 129 \<Longrightarrow> 130 G\<turnstile>(\<langle>(Lit v) InstOf T\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (Bool b)\<rangle>,s')" 131 132 (* cf. 15.7.1 *) 133(*Lit "G\<turnstile>(Lit v,None,s) \<mapsto>1 (Lit v,None,s)"*) 134 135| UnOpE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s') \<rbrakk> 136 \<Longrightarrow> 137 G\<turnstile>(\<langle>UnOp unop e\<rangle>,Norm s) \<mapsto>1 (\<langle>UnOp unop e'\<rangle>,s')" 138| UnOp: "G\<turnstile>(\<langle>UnOp unop (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (eval_unop unop v)\<rangle>,Norm s)" 139 140| BinOpE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s') \<rbrakk> 141 \<Longrightarrow> 142 G\<turnstile>(\<langle>BinOp binop e1 e2\<rangle>,Norm s) \<mapsto>1 (\<langle>BinOp binop e1' e2\<rangle>,s')" 143| BinOpE2: "\<lbrakk>need_second_arg binop v1; G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') \<rbrakk> 144 \<Longrightarrow> 145 G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 146 \<mapsto>1 (\<langle>BinOp binop (Lit v1) e2'\<rangle>,s')" 147| BinOpTerm: "\<lbrakk>\<not> need_second_arg binop v1\<rbrakk> 148 \<Longrightarrow> 149 G\<turnstile>(\<langle>BinOp binop (Lit v1) e2\<rangle>,Norm s) 150 \<mapsto>1 (\<langle>Lit v1\<rangle>,Norm s)" 151| BinOp: "G\<turnstile>(\<langle>BinOp binop (Lit v1) (Lit v2)\<rangle>,Norm s) 152 \<mapsto>1 (\<langle>Lit (eval_binop binop v1 v2)\<rangle>,Norm s)" 153(* Maybe its more convenient to add: need_second_arg as precondition to BinOp 154 to make the choice between BinOpTerm and BinOp deterministic *) 155 156| Super: "G\<turnstile>(\<langle>Super\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (val_this s)\<rangle>,Norm s)" 157 158| AccVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s') \<rbrakk> 159 \<Longrightarrow> 160 G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Acc va'\<rangle>,s')" 161| Acc: "\<lbrakk>groundVar va; ((v,vf),s') = the_var G (Norm s) va\<rbrakk> 162 \<Longrightarrow> 163 G\<turnstile>(\<langle>Acc va\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')" 164 165(* 166AccLVar: "G\<turnstile>(\<langle>Acc (LVar vn)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit (fst (lvar vn s))\<rangle>,Norm s)" 167AccFVar: "\<lbrakk>((v,vf),s') = fvar statDeclC stat fn a (Norm s)\<rbrakk> 168 \<Longrightarrow> 169 G\<turnstile>(\<langle>Acc ({accC,statDeclC,stat}(Lit a)..fn)\<rangle>,Norm s) 170 \<mapsto>1 (\<langle>Lit v\<rangle>,s')" 171AccAVar: "\<lbrakk>((v,vf),s') = avar G i a (Norm s)\<rbrakk> 172 \<Longrightarrow> 173 G\<turnstile>(\<langle>Acc ((Lit a).[Lit i])\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,s')" 174*) 175| AssVA: "\<lbrakk>G\<turnstile>(\<langle>va\<rangle>,Norm s) \<mapsto>1 (\<langle>va'\<rangle>,s')\<rbrakk> 176 \<Longrightarrow> 177 G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va':=e\<rangle>,s')" 178| AssE: "\<lbrakk>groundVar va; G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 179 \<Longrightarrow> 180 G\<turnstile>(\<langle>va:=e\<rangle>,Norm s) \<mapsto>1 (\<langle>va:=e'\<rangle>,s')" 181| Ass: "\<lbrakk>groundVar va; ((w,f),s') = the_var G (Norm s) va\<rbrakk> 182 \<Longrightarrow> 183 G\<turnstile>(\<langle>va:=(Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit v\<rangle>,assign f v s')" 184 185| CondC: "\<lbrakk>G\<turnstile>(\<langle>e0\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'\<rangle>,s')\<rbrakk> 186 \<Longrightarrow> 187 G\<turnstile>(\<langle>e0? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e0'? e1:e2\<rangle>,s')" 188| Cond: "G\<turnstile>(\<langle>Lit b? e1:e2\<rangle>,Norm s) \<mapsto>1 (\<langle>if the_Bool b then e1 else e2\<rangle>,Norm s)" 189 190 191| CallTarget: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 192 \<Longrightarrow> 193 G\<turnstile>(\<langle>{accC,statT,mode}e\<cdot>mn({pTs}args)\<rangle>,Norm s) 194 \<mapsto>1 (\<langle>{accC,statT,mode}e'\<cdot>mn({pTs}args)\<rangle>,s')" 195| CallArgs: "\<lbrakk>G\<turnstile>(\<langle>args\<rangle>,Norm s) \<mapsto>1 (\<langle>args'\<rangle>,s')\<rbrakk> 196 \<Longrightarrow> 197 G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 198 \<mapsto>1 (\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args')\<rangle>,s')" 199| Call: "\<lbrakk>groundExprs args; vs = map the_val args; 200 D = invocation_declclass G mode s a statT \<lparr>name=mn,parTs=pTs\<rparr>; 201 s'=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs (Norm s)\<rbrakk> 202 \<Longrightarrow> 203 G\<turnstile>(\<langle>{accC,statT,mode}Lit a\<cdot>mn({pTs}args)\<rangle>,Norm s) 204 \<mapsto>1 (\<langle>Callee (locals s) (Methd D \<lparr>name=mn,parTs=pTs\<rparr>)\<rangle>,s')" 205 206| Callee: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 207 \<Longrightarrow> 208 G\<turnstile>(\<langle>Callee lcls_caller e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')" 209 210| CalleeRet: "G\<turnstile>(\<langle>Callee lcls_caller (Lit v)\<rangle>,Norm s) 211 \<mapsto>1 (\<langle>Lit v\<rangle>,(set_lvars lcls_caller (Norm s)))" 212 213| Methd: "G\<turnstile>(\<langle>Methd D sig\<rangle>,Norm s) \<mapsto>1 (\<langle>body G D sig\<rangle>,Norm s)" 214 215| Body: "G\<turnstile>(\<langle>Body D c\<rangle>,Norm s) \<mapsto>1 (\<langle>InsInitE (Init D) (Body D c)\<rangle>,Norm s)" 216 217| InsInitBody: 218 "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 219 \<Longrightarrow> 220 G\<turnstile>(\<langle>InsInitE Skip (Body D c)\<rangle>,Norm s) \<mapsto>1(\<langle>InsInitE Skip (Body D c')\<rangle>,s')" 221| InsInitBodyRet: 222 "G\<turnstile>(\<langle>InsInitE Skip (Body D Skip)\<rangle>,Norm s) 223 \<mapsto>1 (\<langle>Lit (the ((locals s) Result))\<rangle>,abupd (absorb Ret) (Norm s))" 224 225(* LVar: "G\<turnstile>(LVar vn,Norm s)" is already evaluated *) 226 227| FVar: "\<lbrakk>\<not> inited statDeclC (globs s)\<rbrakk> 228 \<Longrightarrow> 229 G\<turnstile>(\<langle>{accC,statDeclC,stat}e..fn\<rangle>,Norm s) 230 \<mapsto>1 (\<langle>InsInitV (Init statDeclC) ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s)" 231| InsInitFVarE: 232 "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 233 \<Longrightarrow> 234 G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}e..fn)\<rangle>,Norm s) 235 \<mapsto>1 (\<langle>InsInitV Skip ({accC,statDeclC,stat}e'..fn)\<rangle>,s')" 236| InsInitFVar: 237 "G\<turnstile>(\<langle>InsInitV Skip ({accC,statDeclC,stat}Lit a..fn)\<rangle>,Norm s) 238 \<mapsto>1 (\<langle>{accC,statDeclC,stat}Lit a..fn\<rangle>,Norm s)" 239\<comment> \<open>Notice, that we do not have literal values for \<open>vars\<close>. 240The rules for accessing variables (\<open>Acc\<close>) and assigning to variables 241(\<open>Ass\<close>), test this with the predicate \<open>groundVar\<close>. After 242initialisation is done and the \<open>FVar\<close> is evaluated, we can't just 243throw away the \<open>InsInitFVar\<close> term and return a literal value, as in the 244cases of \<open>New\<close> or \<open>NewC\<close>. Instead we just return the evaluated 245\<open>FVar\<close> and test for initialisation in the rule \<open>FVar\<close>.\<close> 246 247 248| AVarE1: "\<lbrakk>G\<turnstile>(\<langle>e1\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'\<rangle>,s')\<rbrakk> 249 \<Longrightarrow> 250 G\<turnstile>(\<langle>e1.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>e1'.[e2]\<rangle>,s')" 251 252| AVarE2: "G\<turnstile>(\<langle>e2\<rangle>,Norm s) \<mapsto>1 (\<langle>e2'\<rangle>,s') 253 \<Longrightarrow> 254 G\<turnstile>(\<langle>Lit a.[e2]\<rangle>,Norm s) \<mapsto>1 (\<langle>Lit a.[e2']\<rangle>,s')" 255 256(* AVar: \<langle>(Lit a).[Lit i]\<rangle> is fully evaluated *) 257 258(* evaluation of expression lists *) 259 260 \<comment> \<open>\<open>Nil\<close> is fully evaluated\<close> 261 262| ConsHd: "\<lbrakk>G\<turnstile>(\<langle>e::expr\<rangle>,Norm s) \<mapsto>1 (\<langle>e'::expr\<rangle>,s')\<rbrakk> 263 \<Longrightarrow> 264 G\<turnstile>(\<langle>e#es\<rangle>,Norm s) \<mapsto>1 (\<langle>e'#es\<rangle>,s')" 265 266| ConsTl: "\<lbrakk>G\<turnstile>(\<langle>es\<rangle>,Norm s) \<mapsto>1 (\<langle>es'\<rangle>,s')\<rbrakk> 267 \<Longrightarrow> 268 G\<turnstile>(\<langle>(Lit v)#es\<rangle>,Norm s) \<mapsto>1 (\<langle>(Lit v)#es'\<rangle>,s')" 269 270(* execution of statements *) 271 272 (* cf. 14.5 *) 273| Skip: "G\<turnstile>(\<langle>Skip\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)" 274 275| ExprE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 276 \<Longrightarrow> 277 G\<turnstile>(\<langle>Expr e\<rangle>,Norm s) \<mapsto>1 (\<langle>Expr e'\<rangle>,s')" 278| Expr: "G\<turnstile>(\<langle>Expr (Lit v)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)" 279 280 281| LabC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,Norm s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 282 \<Longrightarrow> 283 G\<turnstile>(\<langle>l\<bullet> c\<rangle>,Norm s) \<mapsto>1 (\<langle>l\<bullet> c'\<rangle>,s')" 284| Lab: "G\<turnstile>(\<langle>l\<bullet> Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>, abupd (absorb l) s)" 285 286 (* cf. 14.2 *) 287| CompC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 288 \<Longrightarrow> 289 G\<turnstile>(\<langle>c1;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1';; c2\<rangle>,s')" 290 291| Comp: "G\<turnstile>(\<langle>Skip;; c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c2\<rangle>,Norm s)" 292 293 (* cf. 14.8.2 *) 294| IfE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle> ,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 295 \<Longrightarrow> 296 G\<turnstile>(\<langle>If(e) s1 Else s2\<rangle>,Norm s) \<mapsto>1 (\<langle>If(e') s1 Else s2\<rangle>,s')" 297| If: "G\<turnstile>(\<langle>If(Lit v) s1 Else s2\<rangle>,Norm s) 298 \<mapsto>1 (\<langle>if the_Bool v then s1 else s2\<rangle>,Norm s)" 299 300 (* cf. 14.10, 14.10.1 *) 301| Loop: "G\<turnstile>(\<langle>l\<bullet> While(e) c\<rangle>,Norm s) 302 \<mapsto>1 (\<langle>If(e) (Cont l\<bullet>c;; l\<bullet> While(e) c) Else Skip\<rangle>,Norm s)" 303 304| Jmp: "G\<turnstile>(\<langle>Jmp j\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,(Some (Jump j), s))" 305 306| ThrowE: "\<lbrakk>G\<turnstile>(\<langle>e\<rangle>,Norm s) \<mapsto>1 (\<langle>e'\<rangle>,s')\<rbrakk> 307 \<Longrightarrow> 308 G\<turnstile>(\<langle>Throw e\<rangle>,Norm s) \<mapsto>1 (\<langle>Throw e'\<rangle>,s')" 309| Throw: "G\<turnstile>(\<langle>Throw (Lit a)\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (throw a) (Norm s))" 310 311| TryC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 312 \<Longrightarrow> 313 G\<turnstile>(\<langle>Try c1 Catch(C vn) c2\<rangle>, Norm s) \<mapsto>1 (\<langle>Try c1' Catch(C vn) c2\<rangle>,s')" 314| Try: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'\<rbrakk> 315 \<Longrightarrow> 316 G\<turnstile>(\<langle>Try Skip Catch(C vn) c2\<rangle>, s) 317 \<mapsto>1 (if G,s'\<turnstile>catch C then (\<langle>c2\<rangle>,new_xcpt_var vn s') 318 else (\<langle>Skip\<rangle>,s'))" 319 320| FinC1: "\<lbrakk>G\<turnstile>(\<langle>c1\<rangle>,Norm s) \<mapsto>1 (\<langle>c1'\<rangle>,s')\<rbrakk> 321 \<Longrightarrow> 322 G\<turnstile>(\<langle>c1 Finally c2\<rangle>,Norm s) \<mapsto>1 (\<langle>c1' Finally c2\<rangle>,s')" 323 324| Fin: "G\<turnstile>(\<langle>Skip Finally c2\<rangle>,(a,s)) \<mapsto>1 (\<langle>FinA a c2\<rangle>,Norm s)" 325 326| FinAC: "\<lbrakk>G\<turnstile>(\<langle>c\<rangle>,s) \<mapsto>1 (\<langle>c'\<rangle>,s')\<rbrakk> 327 \<Longrightarrow> 328 G\<turnstile>(\<langle>FinA a c\<rangle>,s) \<mapsto>1 (\<langle>FinA a c'\<rangle>,s')" 329| FinA: "G\<turnstile>(\<langle>FinA a Skip\<rangle>,s) \<mapsto>1 (\<langle>Skip\<rangle>,abupd (abrupt_if (a\<noteq>None) a) s)" 330 331 332| Init1: "\<lbrakk>inited C (globs s)\<rbrakk> 333 \<Longrightarrow> 334 G\<turnstile>(\<langle>Init C\<rangle>,Norm s) \<mapsto>1 (\<langle>Skip\<rangle>,Norm s)" 335| Init: "\<lbrakk>the (class G C)=c; \<not> inited C (globs s)\<rbrakk> 336 \<Longrightarrow> 337 G\<turnstile>(\<langle>Init C\<rangle>,Norm s) 338 \<mapsto>1 (\<langle>(if C = Object then Skip else (Init (super c)));; 339 Expr (Callee (locals s) (InsInitE (init c) SKIP))\<rangle> 340 ,Norm (init_class_obj G C s))" 341\<comment> \<open>\<open>InsInitE\<close> is just used as trick to embed the statement 342\<open>init c\<close> into an expression\<close> 343| InsInitESKIP: 344 "G\<turnstile>(\<langle>InsInitE Skip SKIP\<rangle>,Norm s) \<mapsto>1 (\<langle>SKIP\<rangle>,Norm s)" 345 346abbreviation 347 stepn:: "[prog, term \<times> state,nat,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>_ _"[61,82,82] 81) 348 where "G\<turnstile>p \<mapsto>n p' \<equiv> (p,p') \<in> {(x, y). step G x y}^^n" 349 350abbreviation 351 steptr:: "[prog,term \<times> state,term \<times> state] \<Rightarrow> bool" ("_\<turnstile>_ \<mapsto>* _"[61,82,82] 81) 352 where "G\<turnstile>p \<mapsto>* p' \<equiv> (p,p') \<in> {(x, y). step G x y}\<^sup>*" 353 354(* Equivalenzen: 355 Bigstep zu Smallstep komplett. 356 Smallstep zu Bigstep, nur wenn nicht die Ausdr��cke Callee, FinA ,\<dots> 357*) 358 359(* 360lemma imp_eval_trans: 361 assumes eval: "G\<turnstile>s0 \<midarrow>t\<succ>\<rightarrow> (v,s1)" 362 shows trans: "G\<turnstile>(t,s0) \<mapsto>* (\<langle>Lit v\<rangle>,s1)" 363*) 364(* Jetzt muss man bei trans nat��rlich wieder unterscheiden: Stmt, Expr, Var! 365 Sowas bl��des: 366 Am besten den Terminus ground auf Var,Stmt,Expr hochziehen und dann 367 the_vals definieren\<dots> 368 G\<turnstile>(t,s0) \<mapsto>* (t',s1) \<and> the_vals t' = v 369*) 370 371 372end 373