1(* Title: HOL/Bali/WellType.thy 2 Author: David von Oheimb 3*) 4subsection \<open>Well-typedness of Java programs\<close> 5 6theory WellType 7imports DeclConcepts 8begin 9 10text \<open> 11improvements over Java Specification 1.0: 12\begin{itemize} 13\item methods of Object can be called upon references of interface or array type 14\end{itemize} 15simplifications: 16\begin{itemize} 17\item the type rules include all static checks on statements and expressions, 18 e.g. definedness of names (of parameters, locals, fields, methods) 19\end{itemize} 20design issues: 21\begin{itemize} 22\item unified type judgment for statements, variables, expressions, 23 expression lists 24\item statements are typed like expressions with dummy type Void 25\item the typing rules take an extra argument that is capable of determining 26 the dynamic type of objects. Therefore, they can be used for both 27 checking static types and determining runtime types in transition semantics. 28\end{itemize} 29\<close> 30 31type_synonym lenv 32 = "(lname, ty) table" \<comment> \<open>local variables, including This and Result\<close> 33 34record env = 35 prg:: "prog" \<comment> \<open>program\<close> 36 cls:: "qtname" \<comment> \<open>current package and class name\<close> 37 lcl:: "lenv" \<comment> \<open>local environment\<close> 38 39translations 40 (type) "lenv" <= (type) "(lname, ty) table" 41 (type) "lenv" <= (type) "lname \<Rightarrow> ty option" 42 (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>" 43 (type) "env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>" 44 45 46abbreviation 47 pkg :: "env \<Rightarrow> pname" \<comment> \<open>select the current package from an environment\<close> 48 where "pkg e == pid (cls e)" 49 50subsubsection "Static overloading: maximally specific methods " 51 52type_synonym 53 emhead = "ref_ty \<times> mhead" 54 55\<comment> \<open>Some mnemotic selectors for emhead\<close> 56definition 57 "declrefT" :: "emhead \<Rightarrow> ref_ty" 58 where "declrefT = fst" 59 60definition 61 "mhd" :: "emhead \<Rightarrow> mhead" 62 where "mhd \<equiv> snd" 63 64lemma declrefT_simp[simp]:"declrefT (r,m) = r" 65by (simp add: declrefT_def) 66 67lemma mhd_simp[simp]:"mhd (r,m) = m" 68by (simp add: mhd_def) 69 70lemma static_mhd_simp[simp]: "static (mhd m) = is_static m" 71by (cases m) (simp add: member_is_static_simp mhd_def) 72 73lemma mhd_resTy_simp [simp]: "resTy (mhd m) = resTy m" 74by (cases m) simp 75 76lemma mhd_is_static_simp [simp]: "is_static (mhd m) = is_static m" 77by (cases m) simp 78 79lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m" 80by (cases m) simp 81 82definition 83 cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" 84 where "cmheads G S C = (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` set_option (accmethd G S C sig))" 85 86definition 87 Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set" where 88 "Objectmheads G S = 89 (\<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) 90 ` set_option (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig))" 91 92definition 93 accObjectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set" 94where 95 "accObjectmheads G S T = 96 (if G\<turnstile>RefT T accessible_in (pid S) 97 then Objectmheads G S 98 else (\<lambda>sig. {}))" 99 100primrec mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set" 101where 102 "mheads G S NullT = (\<lambda>sig. {})" 103| "mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h)) 104 ` accimethds G (pid S) I sig \<union> 105 accObjectmheads G S (IfaceT I) sig)" 106| "mheads G S (ClassT C) = cmheads G S C" 107| "mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)" 108 109definition 110 \<comment> \<open>applicable methods, cf. 15.11.2.1\<close> 111 appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where 112 "appl_methds G S rt = (\<lambda> sig. 113 {(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and> 114 G\<turnstile>(parTs sig)[\<preceq>]pTs'})" 115 116definition 117 \<comment> \<open>more specific methods, cf. 15.11.2.2\<close> 118 more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool" where 119 "more_spec G = (\<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs')" 120(*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*) 121 122definition 123 \<comment> \<open>maximally specific methods, cf. 15.11.2.2\<close> 124 max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list) set" where 125 "max_spec G S rt sig = {m. m \<in>appl_methds G S rt sig \<and> 126 (\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}" 127 128 129lemma max_spec2appl_meths: 130 "x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig" 131by (auto simp: max_spec_def) 132 133lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow> 134 mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'" 135by (auto simp: appl_methds_def) 136 137lemma max_spec2mheads: 138"max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A 139 \<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'" 140apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD) 141done 142 143 144definition 145 empty_dt :: "dyn_ty" 146 where "empty_dt = (\<lambda>a. None)" 147 148definition 149 invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode" where 150 "invmode m e = (if is_static m 151 then Static 152 else if e=Super then SuperM else IntVir)" 153 154lemma invmode_nonstatic [simp]: 155 "invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir" 156apply (unfold invmode_def) 157apply (simp (no_asm) add: member_is_static_simp) 158done 159 160 161lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m" 162apply (unfold invmode_def) 163apply (simp (no_asm)) 164done 165 166 167lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)" 168apply (unfold invmode_def) 169apply (simp (no_asm)) 170done 171 172lemma Null_staticD: 173 "a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null" 174apply (clarsimp simp add: invmode_IntVir_eq) 175done 176 177subsubsection "Typing for unary operations" 178 179primrec unop_type :: "unop \<Rightarrow> prim_ty" 180where 181 "unop_type UPlus = Integer" 182| "unop_type UMinus = Integer" 183| "unop_type UBitNot = Integer" 184| "unop_type UNot = Boolean" 185 186primrec wt_unop :: "unop \<Rightarrow> ty \<Rightarrow> bool" 187where 188 "wt_unop UPlus t = (t = PrimT Integer)" 189| "wt_unop UMinus t = (t = PrimT Integer)" 190| "wt_unop UBitNot t = (t = PrimT Integer)" 191| "wt_unop UNot t = (t = PrimT Boolean)" 192 193subsubsection "Typing for binary operations" 194 195primrec binop_type :: "binop \<Rightarrow> prim_ty" 196where 197 "binop_type Mul = Integer" 198| "binop_type Div = Integer" 199| "binop_type Mod = Integer" 200| "binop_type Plus = Integer" 201| "binop_type Minus = Integer" 202| "binop_type LShift = Integer" 203| "binop_type RShift = Integer" 204| "binop_type RShiftU = Integer" 205| "binop_type Less = Boolean" 206| "binop_type Le = Boolean" 207| "binop_type Greater = Boolean" 208| "binop_type Ge = Boolean" 209| "binop_type Eq = Boolean" 210| "binop_type Neq = Boolean" 211| "binop_type BitAnd = Integer" 212| "binop_type And = Boolean" 213| "binop_type BitXor = Integer" 214| "binop_type Xor = Boolean" 215| "binop_type BitOr = Integer" 216| "binop_type Or = Boolean" 217| "binop_type CondAnd = Boolean" 218| "binop_type CondOr = Boolean" 219 220primrec wt_binop :: "prog \<Rightarrow> binop \<Rightarrow> ty \<Rightarrow> ty \<Rightarrow> bool" 221where 222 "wt_binop G Mul t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 223| "wt_binop G Div t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 224| "wt_binop G Mod t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 225| "wt_binop G Plus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 226| "wt_binop G Minus t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 227| "wt_binop G LShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 228| "wt_binop G RShift t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 229| "wt_binop G RShiftU t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 230| "wt_binop G Less t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 231| "wt_binop G Le t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 232| "wt_binop G Greater t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 233| "wt_binop G Ge t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 234| "wt_binop G Eq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 235| "wt_binop G Neq t1 t2 = (G\<turnstile>t1\<preceq>t2 \<or> G\<turnstile>t2\<preceq>t1)" 236| "wt_binop G BitAnd t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 237| "wt_binop G And t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" 238| "wt_binop G BitXor t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 239| "wt_binop G Xor t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" 240| "wt_binop G BitOr t1 t2 = ((t1 = PrimT Integer) \<and> (t2 = PrimT Integer))" 241| "wt_binop G Or t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" 242| "wt_binop G CondAnd t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" 243| "wt_binop G CondOr t1 t2 = ((t1 = PrimT Boolean) \<and> (t2 = PrimT Boolean))" 244 245subsubsection "Typing for terms" 246 247type_synonym tys = "ty + ty list" 248translations 249 (type) "tys" <= (type) "ty + ty list" 250 251 252inductive wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50) 253 and wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>" [51,51,51] 50) 254 and ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50) 255 and ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50) 256 and ty_exprs :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" 257 ("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50) 258where 259 260 "E,dt\<Turnstile>s\<Colon>\<surd> \<equiv> E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)" 261| "E,dt\<Turnstile>e\<Colon>-T \<equiv> E,dt\<Turnstile>In1l e\<Colon>Inl T" 262| "E,dt\<Turnstile>e\<Colon>=T \<equiv> E,dt\<Turnstile>In2 e\<Colon>Inl T" 263| "E,dt\<Turnstile>e\<Colon>\<doteq>T \<equiv> E,dt\<Turnstile>In3 e\<Colon>Inr T" 264 265\<comment> \<open>well-typed statements\<close> 266 267| Skip: "E,dt\<Turnstile>Skip\<Colon>\<surd>" 268 269| Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow> 270 E,dt\<Turnstile>Expr e\<Colon>\<surd>" 271 \<comment> \<open>cf. 14.6\<close> 272| Lab: "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow> 273 E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" 274 275| Comp: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; 276 E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> 277 E,dt\<Turnstile>c1;; c2\<Colon>\<surd>" 278 279 \<comment> \<open>cf. 14.8\<close> 280| If: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean; 281 E,dt\<Turnstile>c1\<Colon>\<surd>; 282 E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> 283 E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>" 284 285 \<comment> \<open>cf. 14.10\<close> 286| Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean; 287 E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow> 288 E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>" 289 \<comment> \<open>cf. 14.13, 14.15, 14.16\<close> 290| Jmp: "E,dt\<Turnstile>Jmp jump\<Colon>\<surd>" 291 292 \<comment> \<open>cf. 14.16\<close> 293| Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn; 294 prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow> 295 E,dt\<Turnstile>Throw e\<Colon>\<surd>" 296 \<comment> \<open>cf. 14.18\<close> 297| Try: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; 298 lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> 299 \<Longrightarrow> 300 E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>" 301 302 \<comment> \<open>cf. 14.18\<close> 303| Fin: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> 304 E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>" 305 306| Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow> 307 E,dt\<Turnstile>Init C\<Colon>\<surd>" 308 \<comment> \<open>\<^term>\<open>Init\<close> is created on the fly during evaluation (see Eval.thy). 309 The class isn't necessarily accessible from the points \<^term>\<open>Init\<close> 310 is called. Therefor we only demand \<^term>\<open>is_class\<close> and not 311 \<^term>\<open>is_acc_class\<close> here.\<close> 312 313\<comment> \<open>well-typed expressions\<close> 314 315 \<comment> \<open>cf. 15.8\<close> 316| NewC: "\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow> 317 E,dt\<Turnstile>NewC C\<Colon>-Class C" 318 \<comment> \<open>cf. 15.9\<close> 319| NewA: "\<lbrakk>is_acc_type (prg E) (pkg E) T; 320 E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow> 321 E,dt\<Turnstile>New T[i]\<Colon>-T.[]" 322 323 \<comment> \<open>cf. 15.15\<close> 324| Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T'; 325 prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow> 326 E,dt\<Turnstile>Cast T' e\<Colon>-T'" 327 328 \<comment> \<open>cf. 15.19.2\<close> 329| Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T'); 330 prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow> 331 E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean" 332 333 \<comment> \<open>cf. 15.7.1\<close> 334| Lit: "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow> 335 E,dt\<Turnstile>Lit x\<Colon>-T" 336 337| UnOp: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Te; wt_unop unop Te; T=PrimT (unop_type unop)\<rbrakk> 338 \<Longrightarrow> 339 E,dt\<Turnstile>UnOp unop e\<Colon>-T" 340 341| BinOp: "\<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 342 T=PrimT (binop_type binop)\<rbrakk> 343 \<Longrightarrow> 344 E,dt\<Turnstile>BinOp binop e1 e2\<Colon>-T" 345 346 \<comment> \<open>cf. 15.10.2, 15.11.1\<close> 347| Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; 348 class (prg E) C = Some c\<rbrakk> \<Longrightarrow> 349 E,dt\<Turnstile>Super\<Colon>-Class (super c)" 350 351 \<comment> \<open>cf. 15.13.1, 15.10.1, 15.12\<close> 352| Acc: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow> 353 E,dt\<Turnstile>Acc va\<Colon>-T" 354 355 \<comment> \<open>cf. 15.25, 15.25.1\<close> 356| Ass: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This; 357 E,dt\<Turnstile>v \<Colon>-T'; 358 prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow> 359 E,dt\<Turnstile>va:=v\<Colon>-T'" 360 361 \<comment> \<open>cf. 15.24\<close> 362| Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean; 363 E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; 364 prg E\<turnstile>T1\<preceq>T2 \<and> T = T2 \<or> prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow> 365 E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T" 366 367 \<comment> \<open>cf. 15.11.1, 15.11.2, 15.11.3\<close> 368| Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; 369 E,dt\<Turnstile>ps\<Colon>\<doteq>pTs; 370 max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 371 = {((statDeclT,m),pTs')} 372 \<rbrakk> \<Longrightarrow> 373 E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)" 374 375| Methd: "\<lbrakk>is_class (prg E) C; 376 methd (prg E) C sig = Some m; 377 E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow> 378 E,dt\<Turnstile>Methd C sig\<Colon>-T" 379 \<comment> \<open>The class \<^term>\<open>C\<close> is the dynamic class of the method call 380 (cf. Eval.thy). 381 It hasn't got to be directly accessible from the current package 382 \<^term>\<open>(pkg E)\<close>. 383 Only the static class must be accessible (enshured indirectly by 384 \<^term>\<open>Call\<close>). 385 Note that l is just a dummy value. It is only used in the smallstep 386 semantics. To proof typesafety directly for the smallstep semantics 387 we would have to assume conformance of l here!\<close> 388 389| Body: "\<lbrakk>is_class (prg E) D; 390 E,dt\<Turnstile>blk\<Colon>\<surd>; 391 (lcl E) Result = Some T; 392 is_type (prg E) T\<rbrakk> \<Longrightarrow> 393 E,dt\<Turnstile>Body D blk\<Colon>-T" 394\<comment> \<open>The class \<^term>\<open>D\<close> implementing the method must not directly be 395 accessible from the current package \<^term>\<open>(pkg E)\<close>, but can also 396 be indirectly accessible due to inheritance (enshured in \<^term>\<open>Call\<close>) 397 The result type hasn't got to be accessible in Java! (If it is not 398 accessible you can only assign it to Object). 399 For dummy value l see rule \<^term>\<open>Methd\<close>.\<close> 400 401\<comment> \<open>well-typed variables\<close> 402 403 \<comment> \<open>cf. 15.13.1\<close> 404| LVar: "\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow> 405 E,dt\<Turnstile>LVar vn\<Colon>=T" 406 \<comment> \<open>cf. 15.10.1\<close> 407| FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; 408 accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow> 409 E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)" 410 \<comment> \<open>cf. 15.12\<close> 411| AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; 412 E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow> 413 E,dt\<Turnstile>e.[i]\<Colon>=T" 414 415 416\<comment> \<open>well-typed expression lists\<close> 417 418 \<comment> \<open>cf. 15.11.???\<close> 419| Nil: "E,dt\<Turnstile>[]\<Colon>\<doteq>[]" 420 421 \<comment> \<open>cf. 15.11.???\<close> 422| Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>-T; 423 E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow> 424 E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts" 425 426 427(* for purely static typing *) 428abbreviation 429 wt_syntax :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50) 430 where "E\<turnstile>t\<Colon>T == E,empty_dt\<Turnstile>t\<Colon> T" 431 432abbreviation 433 wt_stmt_syntax :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50) 434 where "E\<turnstile>s\<Colon>\<surd> == E\<turnstile>In1r s \<Colon> Inl (PrimT Void)" 435 436abbreviation 437 ty_expr_syntax :: "env \<Rightarrow> [expr, ty] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) 438 where "E\<turnstile>e\<Colon>-T == E\<turnstile>In1l e \<Colon> Inl T" 439 440abbreviation 441 ty_var_syntax :: "env \<Rightarrow> [var, ty] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) 442 where "E\<turnstile>e\<Colon>=T == E\<turnstile>In2 e \<Colon> Inl T" 443 444abbreviation 445 ty_exprs_syntax :: "env \<Rightarrow> [expr list, ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50) 446 where "E\<turnstile>e\<Colon>\<doteq>T == E\<turnstile>In3 e \<Colon> Inr T" 447 448notation (ASCII) 449 wt_syntax ("_|-_::_" [51,51,51] 50) and 450 wt_stmt_syntax ("_|-_:<>" [51,51 ] 50) and 451 ty_expr_syntax ("_|-_:-_" [51,51,51] 50) and 452 ty_var_syntax ("_|-_:=_" [51,51,51] 50) and 453 ty_exprs_syntax ("_|-_:#_" [51,51,51] 50) 454 455declare not_None_eq [simp del] 456declare if_split [split del] if_split_asm [split del] 457declare split_paired_All [simp del] split_paired_Ex [simp del] 458setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close> 459 460inductive_cases wt_elim_cases [cases set]: 461 "E,dt\<Turnstile>In2 (LVar vn) \<Colon>T" 462 "E,dt\<Turnstile>In2 ({accC,statDeclC,s}e..fn)\<Colon>T" 463 "E,dt\<Turnstile>In2 (e.[i]) \<Colon>T" 464 "E,dt\<Turnstile>In1l (NewC C) \<Colon>T" 465 "E,dt\<Turnstile>In1l (New T'[i]) \<Colon>T" 466 "E,dt\<Turnstile>In1l (Cast T' e) \<Colon>T" 467 "E,dt\<Turnstile>In1l (e InstOf T') \<Colon>T" 468 "E,dt\<Turnstile>In1l (Lit x) \<Colon>T" 469 "E,dt\<Turnstile>In1l (UnOp unop e) \<Colon>T" 470 "E,dt\<Turnstile>In1l (BinOp binop e1 e2) \<Colon>T" 471 "E,dt\<Turnstile>In1l (Super) \<Colon>T" 472 "E,dt\<Turnstile>In1l (Acc va) \<Colon>T" 473 "E,dt\<Turnstile>In1l (Ass va v) \<Colon>T" 474 "E,dt\<Turnstile>In1l (e0 ? e1 : e2) \<Colon>T" 475 "E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T" 476 "E,dt\<Turnstile>In1l (Methd C sig) \<Colon>T" 477 "E,dt\<Turnstile>In1l (Body D blk) \<Colon>T" 478 "E,dt\<Turnstile>In3 ([]) \<Colon>Ts" 479 "E,dt\<Turnstile>In3 (e#es) \<Colon>Ts" 480 "E,dt\<Turnstile>In1r Skip \<Colon>x" 481 "E,dt\<Turnstile>In1r (Expr e) \<Colon>x" 482 "E,dt\<Turnstile>In1r (c1;; c2) \<Colon>x" 483 "E,dt\<Turnstile>In1r (l\<bullet> c) \<Colon>x" 484 "E,dt\<Turnstile>In1r (If(e) c1 Else c2) \<Colon>x" 485 "E,dt\<Turnstile>In1r (l\<bullet> While(e) c) \<Colon>x" 486 "E,dt\<Turnstile>In1r (Jmp jump) \<Colon>x" 487 "E,dt\<Turnstile>In1r (Throw e) \<Colon>x" 488 "E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x" 489 "E,dt\<Turnstile>In1r (c1 Finally c2) \<Colon>x" 490 "E,dt\<Turnstile>In1r (Init C) \<Colon>x" 491declare not_None_eq [simp] 492declare if_split [split] if_split_asm [split] 493declare split_paired_All [simp] split_paired_Ex [simp] 494setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close> 495 496lemma is_acc_class_is_accessible: 497 "is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P" 498by (auto simp add: is_acc_class_def) 499 500lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I" 501by (auto simp add: is_acc_iface_def) 502 503lemma is_acc_iface_Iface_is_accessible: 504 "is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P" 505by (auto simp add: is_acc_iface_def) 506 507lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T" 508by (auto simp add: is_acc_type_def) 509 510lemma is_acc_iface_is_accessible: 511 "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P" 512by (auto simp add: is_acc_type_def) 513 514lemma wt_Methd_is_methd: 515 "E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig" 516apply (erule_tac wt_elim_cases) 517apply clarsimp 518apply (erule is_methdI, assumption) 519done 520 521 522text \<open>Special versions of some typing rules, better suited to pattern 523 match the conclusion (no selectors in the conclusion) 524\<close> 525 526lemma wt_Call: 527"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs; 528 max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> 529 = {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E; 530 mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT" 531by (auto elim: wt.Call) 532 533 534lemma invocationTypeExpr_noClassD: 535"\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk> 536 \<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM" 537proof - 538 assume wt: "E\<turnstile>e\<Colon>-RefT statT" 539 show ?thesis 540 proof (cases "e=Super") 541 case True 542 with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases) 543 then show ?thesis by blast 544 next 545 case False then show ?thesis 546 by (auto simp add: invmode_def) 547 qed 548qed 549 550lemma wt_Super: 551"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> 552\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D" 553by (auto elim: wt.Super) 554 555lemma wt_FVar: 556"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f); 557 sf=is_static f; fT=(type f); accC=cls E\<rbrakk> 558\<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT" 559by (auto dest: wt.FVar) 560 561 562lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C" 563by (auto elim: wt_elim_cases intro: "wt.Init") 564 565declare wt.Skip [iff] 566 567lemma wt_StatRef: 568 "is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt" 569apply (rule wt.Cast) 570apply (rule wt.Lit) 571apply (simp (no_asm)) 572apply (simp (no_asm_simp)) 573apply (rule cast.widen) 574apply (simp (no_asm)) 575done 576 577lemma wt_Inj_elim: 578 "\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of 579 In1 ec \<Rightarrow> (case ec of 580 Inl e \<Rightarrow> \<exists>T. U=Inl T 581 | Inr s \<Rightarrow> U=Inl (PrimT Void)) 582 | In2 e \<Rightarrow> (\<exists>T. U=Inl T) 583 | In3 e \<Rightarrow> (\<exists>T. U=Inr T)" 584apply (erule wt.induct) 585apply auto 586done 587 588\<comment> \<open>In the special syntax to distinguish the typing judgements for expressions, 589 statements, variables and expression lists the kind of term corresponds 590 to the kind of type in the end e.g. An statement (injection \<^term>\<open>In3\<close> 591 into terms, always has type void (injection \<^term>\<open>Inl\<close> into the generalised 592 types. The following simplification procedures establish these kinds of 593 correlation.\<close> 594 595lemma wt_expr_eq: "E,dt\<Turnstile>In1l t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T)" 596 by (auto, frule wt_Inj_elim, auto) 597 598lemma wt_var_eq: "E,dt\<Turnstile>In2 t\<Colon>U = (\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T)" 599 by (auto, frule wt_Inj_elim, auto) 600 601lemma wt_exprs_eq: "E,dt\<Turnstile>In3 t\<Colon>U = (\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts)" 602 by (auto, frule wt_Inj_elim, auto) 603 604lemma wt_stmt_eq: "E,dt\<Turnstile>In1r t\<Colon>U = (U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>)" 605 by (auto, frule wt_Inj_elim, auto, frule wt_Inj_elim, auto) 606 607simproc_setup wt_expr ("E,dt\<Turnstile>In1l t\<Colon>U") = \<open> 608 fn _ => fn _ => fn ct => 609 (case Thm.term_of ct of 610 (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE 611 | _ => SOME (mk_meta_eq @{thm wt_expr_eq}))\<close> 612 613simproc_setup wt_var ("E,dt\<Turnstile>In2 t\<Colon>U") = \<open> 614 fn _ => fn _ => fn ct => 615 (case Thm.term_of ct of 616 (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE 617 | _ => SOME (mk_meta_eq @{thm wt_var_eq}))\<close> 618 619simproc_setup wt_exprs ("E,dt\<Turnstile>In3 t\<Colon>U") = \<open> 620 fn _ => fn _ => fn ct => 621 (case Thm.term_of ct of 622 (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE 623 | _ => SOME (mk_meta_eq @{thm wt_exprs_eq}))\<close> 624 625simproc_setup wt_stmt ("E,dt\<Turnstile>In1r t\<Colon>U") = \<open> 626 fn _ => fn _ => fn ct => 627 (case Thm.term_of ct of 628 (_ $ _ $ _ $ _ $ (Const _ $ _)) => NONE 629 | _ => SOME (mk_meta_eq @{thm wt_stmt_eq}))\<close> 630 631lemma wt_elim_BinOp: 632 "\<lbrakk>E,dt\<Turnstile>In1l (BinOp binop e1 e2)\<Colon>T; 633 \<And>T1 T2 T3. 634 \<lbrakk>E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; wt_binop (prg E) binop T1 T2; 635 E,dt\<Turnstile>(if b then In1l e2 else In1r Skip)\<Colon>T3; 636 T = Inl (PrimT (binop_type binop))\<rbrakk> 637 \<Longrightarrow> P\<rbrakk> 638\<Longrightarrow> P" 639apply (erule wt_elim_cases) 640apply (cases b) 641apply auto 642done 643 644lemma Inj_eq_lemma [simp]: 645 "(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))" 646by auto 647 648(* unused *) 649lemma single_valued_tys_lemma [rule_format (no_asm)]: 650 "\<forall>S T. G\<turnstile>S\<preceq>T \<longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T \<Longrightarrow> E,dt\<Turnstile>t\<Colon>T \<Longrightarrow> 651 G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T = T')" 652apply (cases "E", erule wt.induct) 653apply (safe del: disjE) 654apply (simp_all (no_asm_use) split del: if_split_asm) 655apply (safe del: disjE) 656(* 17 subgoals *) 657apply (tactic \<open>ALLGOALS (fn i => 658 if i = 11 then EVERY' 659 [Rule_Insts.thin_tac \<^context> "E,dt\<Turnstile>e0\<Colon>-PrimT Boolean" [(\<^binding>\<open>E\<close>, NONE, NoSyn)], 660 Rule_Insts.thin_tac \<^context> "E,dt\<Turnstile>e1\<Colon>-T1" [(\<^binding>\<open>E\<close>, NONE, NoSyn), (\<^binding>\<open>T1\<close>, NONE, NoSyn)], 661 Rule_Insts.thin_tac \<^context> "E,dt\<Turnstile>e2\<Colon>-T2" [(\<^binding>\<open>E\<close>, NONE, NoSyn), (\<^binding>\<open>T2\<close>, NONE, NoSyn)]] i 662 else Rule_Insts.thin_tac \<^context> "All P" [(\<^binding>\<open>P\<close>, NONE, NoSyn)] i)\<close>) 663(*apply (safe del: disjE elim!: wt_elim_cases)*) 664apply (tactic \<open>ALLGOALS (eresolve_tac \<^context> @{thms wt_elim_cases})\<close>) 665apply (simp_all (no_asm_use) split del: if_split_asm) 666apply (erule_tac [12] V = "All P" for P in thin_rl) (* Call *) 667apply (blast del: equalityCE dest: sym [THEN trans])+ 668done 669 670(* unused *) 671lemma single_valued_tys: 672"ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}" 673apply (unfold single_valued_def) 674apply clarsimp 675apply (rule single_valued_tys_lemma) 676apply (auto intro!: widen_antisym) 677done 678 679lemma typeof_empty_is_type: "typeof (\<lambda>a. None) v = Some T \<Longrightarrow> is_type G T" 680 by (induct v) auto 681 682(* unused *) 683lemma typeof_is_type: "(\<forall>a. v \<noteq> Addr a) \<Longrightarrow> \<exists>T. typeof dt v = Some T \<and> is_type G T" 684 by (induct v) auto 685 686end 687