1(* Title: HOL/Bali/WellForm.thy 2 Author: David von Oheimb and Norbert Schirmer 3*) 4 5subsection \<open>Well-formedness of Java programs\<close> 6theory WellForm imports DefiniteAssignment begin 7 8text \<open> 9For static checks on expressions and statements, see WellType.thy 10 11improvements over Java Specification 1.0 (cf. 8.4.6.3, 8.4.6.4, 9.4.1): 12\begin{itemize} 13\item a method implementing or overwriting another method may have a result 14 type that widens to the result type of the other method 15 (instead of identical type) 16\item if a method hides another method (both methods have to be static!) 17 there are no restrictions to the result type 18 since the methods have to be static and there is no dynamic binding of 19 static methods 20\item if an interface inherits more than one method with the same signature, the 21 methods need not have identical return types 22\end{itemize} 23simplifications: 24\begin{itemize} 25\item Object and standard exceptions are assumed to be declared like normal 26 classes 27\end{itemize} 28\<close> 29 30subsubsection "well-formed field declarations" 31text \<open>well-formed field declaration (common part for classes and interfaces), 32 cf. 8.3 and (9.3)\<close> 33 34definition 35 wf_fdecl :: "prog \<Rightarrow> pname \<Rightarrow> fdecl \<Rightarrow> bool" 36 where "wf_fdecl G P = (\<lambda>(fn,f). is_acc_type G P (type f))" 37 38lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))" 39apply (unfold wf_fdecl_def) 40apply simp 41done 42 43 44 45subsubsection "well-formed method declarations" 46 (*well-formed method declaration,cf. 8.4, 8.4.1, 8.4.3, 8.4.5, 14.3.2, (9.4)*) 47 (* cf. 14.15, 15.7.2, for scope issues cf. 8.4.1 and 14.3.2 *) 48 49text \<open> 50A method head is wellformed if: 51\begin{itemize} 52\item the signature and the method head agree in the number of parameters 53\item all types of the parameters are visible 54\item the result type is visible 55\item the parameter names are unique 56\end{itemize} 57\<close> 58definition 59 wf_mhead :: "prog \<Rightarrow> pname \<Rightarrow> sig \<Rightarrow> mhead \<Rightarrow> bool" where 60 "wf_mhead G P = (\<lambda> sig mh. length (parTs sig) = length (pars mh) \<and> 61 ( \<forall>T\<in>set (parTs sig). is_acc_type G P T) \<and> 62 is_acc_type G P (resTy mh) \<and> 63 distinct (pars mh))" 64 65 66text \<open> 67A method declaration is wellformed if: 68\begin{itemize} 69\item the method head is wellformed 70\item the names of the local variables are unique 71\item the types of the local variables must be accessible 72\item the local variables don't shadow the parameters 73\item the class of the method is defined 74\item the body statement is welltyped with respect to the 75 modified environment of local names, were the local variables, 76 the parameters the special result variable (Res) and This are assoziated 77 with there types. 78\end{itemize} 79\<close> 80 81definition 82 callee_lcl :: "qtname \<Rightarrow> sig \<Rightarrow> methd \<Rightarrow> lenv" where 83 "callee_lcl C sig m = 84 (\<lambda>k. (case k of 85 EName e 86 \<Rightarrow> (case e of 87 VNam v 88 \<Rightarrow>(table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v 89 | Res \<Rightarrow> Some (resTy m)) 90 | This \<Rightarrow> if is_static m then None else Some (Class C)))" 91 92definition 93 parameters :: "methd \<Rightarrow> lname set" where 94 "parameters m = set (map (EName \<circ> VNam) (pars m)) \<union> (if (static m) then {} else {This})" 95 96definition 97 wf_mdecl :: "prog \<Rightarrow> qtname \<Rightarrow> mdecl \<Rightarrow> bool" where 98 "wf_mdecl G C = 99 (\<lambda>(sig,m). 100 wf_mhead G (pid C) sig (mhead m) \<and> 101 unique (lcls (mbody m)) \<and> 102 (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T) \<and> 103 (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and> 104 jumpNestingOkS {Ret} (stmt (mbody m)) \<and> 105 is_class G C \<and> 106 \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd> \<and> 107 (\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr> 108 \<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A 109 \<and> Result \<in> nrm A))" 110 111lemma callee_lcl_VNam_simp [simp]: 112"callee_lcl C sig m (EName (VNam v)) 113 = (table_of (lcls (mbody m))((pars m)[\<mapsto>](parTs sig))) v" 114by (simp add: callee_lcl_def) 115 116lemma callee_lcl_Res_simp [simp]: 117"callee_lcl C sig m (EName Res) = Some (resTy m)" 118by (simp add: callee_lcl_def) 119 120lemma callee_lcl_This_simp [simp]: 121"callee_lcl C sig m (This) = (if is_static m then None else Some (Class C))" 122by (simp add: callee_lcl_def) 123 124lemma callee_lcl_This_static_simp: 125"is_static m \<Longrightarrow> callee_lcl C sig m (This) = None" 126by simp 127 128lemma callee_lcl_This_not_static_simp: 129"\<not> is_static m \<Longrightarrow> callee_lcl C sig m (This) = Some (Class C)" 130by simp 131 132lemma wf_mheadI: 133"\<lbrakk>length (parTs sig) = length (pars m); \<forall>T\<in>set (parTs sig). is_acc_type G P T; 134 is_acc_type G P (resTy m); distinct (pars m)\<rbrakk> \<Longrightarrow> 135 wf_mhead G P sig m" 136apply (unfold wf_mhead_def) 137apply (simp (no_asm_simp)) 138done 139 140lemma wf_mdeclI: "\<lbrakk> 141 wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m)); 142 (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None); 143 \<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T; 144 jumpNestingOkS {Ret} (stmt (mbody m)); 145 is_class G C; 146 \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>; 147 (\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr> \<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A 148 \<and> Result \<in> nrm A) 149 \<rbrakk> \<Longrightarrow> 150 wf_mdecl G C (sig,m)" 151apply (unfold wf_mdecl_def) 152apply simp 153done 154 155lemma wf_mdeclE [consumes 1]: 156 "\<lbrakk>wf_mdecl G C (sig,m); 157 \<lbrakk>wf_mhead G (pid C) sig (mhead m); unique (lcls (mbody m)); 158 \<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None; 159 \<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T; 160 jumpNestingOkS {Ret} (stmt (mbody m)); 161 is_class G C; 162 \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>(stmt (mbody m))\<Colon>\<surd>; 163 (\<exists> A. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile> parameters m \<guillemotright>\<langle>stmt (mbody m)\<rangle>\<guillemotright> A 164 \<and> Result \<in> nrm A) 165 \<rbrakk> \<Longrightarrow> P 166 \<rbrakk> \<Longrightarrow> P" 167by (unfold wf_mdecl_def) simp 168 169 170lemma wf_mdeclD1: 171"wf_mdecl G C (sig,m) \<Longrightarrow> 172 wf_mhead G (pid C) sig (mhead m) \<and> unique (lcls (mbody m)) \<and> 173 (\<forall>pn\<in>set (pars m). table_of (lcls (mbody m)) pn = None) \<and> 174 (\<forall>(vn,T)\<in>set (lcls (mbody m)). is_acc_type G (pid C) T)" 175apply (unfold wf_mdecl_def) 176apply simp 177done 178 179lemma wf_mdecl_bodyD: 180"wf_mdecl G C (sig,m) \<Longrightarrow> 181 (\<exists>T. \<lparr>prg=G,cls=C,lcl=callee_lcl C sig m\<rparr>\<turnstile>Body C (stmt (mbody m))\<Colon>-T \<and> 182 G\<turnstile>T\<preceq>(resTy m))" 183apply (unfold wf_mdecl_def) 184apply clarify 185apply (rule_tac x="(resTy m)" in exI) 186apply (unfold wf_mhead_def) 187apply (auto simp add: wf_mhead_def is_acc_type_def intro: wt.Body ) 188done 189 190 191(* 192lemma static_Object_methodsE [elim!]: 193 "\<lbrakk>wf_mdecl G Object (sig, m);static m\<rbrakk> \<Longrightarrow> R" 194apply (unfold wf_mdecl_def) 195apply auto 196done 197*) 198 199lemma rT_is_acc_type: 200 "wf_mhead G P sig m \<Longrightarrow> is_acc_type G P (resTy m)" 201apply (unfold wf_mhead_def) 202apply auto 203done 204 205subsubsection "well-formed interface declarations" 206 (* well-formed interface declaration, cf. 9.1, 9.1.2.1, 9.1.3, 9.4 *) 207 208text \<open> 209A interface declaration is wellformed if: 210\begin{itemize} 211\item the interface hierarchy is wellstructured 212\item there is no class with the same name 213\item the method heads are wellformed and not static and have Public access 214\item the methods are uniquely named 215\item all superinterfaces are accessible 216\item the result type of a method overriding a method of Object widens to the 217 result type of the overridden method. 218 Shadowing static methods is forbidden. 219\item the result type of a method overriding a set of methods defined in the 220 superinterfaces widens to each of the corresponding result types 221\end{itemize} 222\<close> 223definition 224 wf_idecl :: "prog \<Rightarrow> idecl \<Rightarrow> bool" where 225 "wf_idecl G = 226 (\<lambda>(I,i). 227 ws_idecl G I (isuperIfs i) \<and> 228 \<not>is_class G I \<and> 229 (\<forall>(sig,mh)\<in>set (imethods i). wf_mhead G (pid I) sig mh \<and> 230 \<not>is_static mh \<and> 231 accmodi mh = Public) \<and> 232 unique (imethods i) \<and> 233 (\<forall> J\<in>set (isuperIfs i). is_acc_iface G (pid I) J) \<and> 234 (table_of (imethods i) 235 hiding (methd G Object) 236 under (\<lambda> new old. accmodi old \<noteq> Private) 237 entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 238 is_static new = is_static old)) \<and> 239 (set_option \<circ> table_of (imethods i) 240 hidings Un_tables((\<lambda>J.(imethds G J))`set (isuperIfs i)) 241 entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old)))" 242 243lemma wf_idecl_mhead: "\<lbrakk>wf_idecl G (I,i); (sig,mh)\<in>set (imethods i)\<rbrakk> \<Longrightarrow> 244 wf_mhead G (pid I) sig mh \<and> \<not>is_static mh \<and> accmodi mh = Public" 245apply (unfold wf_idecl_def) 246apply auto 247done 248 249lemma wf_idecl_hidings: 250"wf_idecl G (I, i) \<Longrightarrow> 251 (\<lambda>s. set_option (table_of (imethods i) s)) 252 hidings Un_tables ((\<lambda>J. imethds G J) ` set (isuperIfs i)) 253 entails \<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old" 254apply (unfold wf_idecl_def o_def) 255apply simp 256done 257 258lemma wf_idecl_hiding: 259"wf_idecl G (I, i) \<Longrightarrow> 260 (table_of (imethods i) 261 hiding (methd G Object) 262 under (\<lambda> new old. accmodi old \<noteq> Private) 263 entails (\<lambda>new old. G\<turnstile>resTy new\<preceq>resTy old \<and> 264 is_static new = is_static old))" 265apply (unfold wf_idecl_def) 266apply simp 267done 268 269lemma wf_idecl_supD: 270"\<lbrakk>wf_idecl G (I,i); J \<in> set (isuperIfs i)\<rbrakk> 271 \<Longrightarrow> is_acc_iface G (pid I) J \<and> (J, I) \<notin> (subint1 G)\<^sup>+" 272apply (unfold wf_idecl_def ws_idecl_def) 273apply auto 274done 275 276subsubsection "well-formed class declarations" 277 (* well-formed class declaration, cf. 8.1, 8.1.2.1, 8.1.2.2, 8.1.3, 8.1.4 and 278 class method declaration, cf. 8.4.3.3, 8.4.6.1, 8.4.6.2, 8.4.6.3, 8.4.6.4 *) 279 280text \<open> 281A class declaration is wellformed if: 282\begin{itemize} 283\item there is no interface with the same name 284\item all superinterfaces are accessible and for all methods implementing 285 an interface method the result type widens to the result type of 286 the interface method, the method is not static and offers at least 287 as much access 288 (this actually means that the method has Public access, since all 289 interface methods have public access) 290\item all field declarations are wellformed and the field names are unique 291\item all method declarations are wellformed and the method names are unique 292\item the initialization statement is welltyped 293\item the classhierarchy is wellstructured 294\item Unless the class is Object: 295 \begin{itemize} 296 \item the superclass is accessible 297 \item for all methods overriding another method (of a superclass )the 298 result type widens to the result type of the overridden method, 299 the access modifier of the new method provides at least as much 300 access as the overwritten one. 301 \item for all methods hiding a method (of a superclass) the hidden 302 method must be static and offer at least as much access rights. 303 Remark: In contrast to the Java Language Specification we don't 304 restrict the result types of the method 305 (as in case of overriding), because there seems to be no reason, 306 since there is no dynamic binding of static methods. 307 (cf. 8.4.6.3 vs. 15.12.1). 308 Stricly speaking the restrictions on the access rights aren't 309 necessary to, since the static type and the access rights 310 together determine which method is to be called statically. 311 But if a class gains more then one static method with the 312 same signature due to inheritance, it is confusing when the 313 method selection depends on the access rights only: 314 e.g. 315 Class C declares static public method foo(). 316 Class D is subclass of C and declares static method foo() 317 with default package access. 318 D.foo() ? if this call is in the same package as D then 319 foo of class D is called, otherwise foo of class C. 320 \end{itemize} 321 322\end{itemize} 323\<close> 324(* to Table *) 325definition 326 entails :: "('a,'b) table \<Rightarrow> ('b \<Rightarrow> bool) \<Rightarrow> bool" ("_ entails _" 20) 327 where "(t entails P) = (\<forall>k. \<forall> x \<in> t k: P x)" 328 329lemma entailsD: 330 "\<lbrakk>t entails P; t k = Some x\<rbrakk> \<Longrightarrow> P x" 331by (simp add: entails_def) 332 333lemma empty_entails[simp]: "Map.empty entails P" 334by (simp add: entails_def) 335 336definition 337 wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where 338 "wf_cdecl G = 339 (\<lambda>(C,c). 340 \<not>is_iface G C \<and> 341 (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and> 342 (\<forall>s. \<forall> im \<in> imethds G I s. 343 (\<exists> cm \<in> methd G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and> 344 \<not> is_static cm \<and> 345 accmodi im \<le> accmodi cm))) \<and> 346 (\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f) \<and> unique (cfields c) \<and> 347 (\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and> 348 jumpNestingOkS {} (init c) \<and> 349 (\<exists> A. \<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<guillemotright> A) \<and> 350 \<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and> 351 (C \<noteq> Object \<longrightarrow> 352 (is_acc_class G (pid C) (super c) \<and> 353 (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 354 entails (\<lambda> new. \<forall> old sig. 355 (G,sig\<turnstile>new overrides\<^sub>S old 356 \<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and> 357 accmodi old \<le> accmodi new \<and> 358 \<not>is_static old)) \<and> 359 (G,sig\<turnstile>new hides old 360 \<longrightarrow> (accmodi old \<le> accmodi new \<and> 361 is_static old)))) 362 )))" 363 364(* 365definition wf_cdecl :: "prog \<Rightarrow> cdecl \<Rightarrow> bool" where 366"wf_cdecl G \<equiv> 367 \<lambda>(C,c). 368 \<not>is_iface G C \<and> 369 (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and> 370 (\<forall>s. \<forall> im \<in> imethds G I s. 371 (\<exists> cm \<in> methd G C s: G\<turnstile>resTy (mthd cm)\<preceq>resTy (mthd im) \<and> 372 \<not> is_static cm \<and> 373 accmodi im \<le> accmodi cm))) \<and> 374 (\<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f) \<and> unique (cfields c) \<and> 375 (\<forall>m\<in>set (methods c). wf_mdecl G C m) \<and> unique (methods c) \<and> 376 \<lparr>prg=G,cls=C,lcl=empty\<rparr>\<turnstile>(init c)\<Colon>\<surd> \<and> ws_cdecl G C (super c) \<and> 377 (C \<noteq> Object \<longrightarrow> 378 (is_acc_class G (pid C) (super c) \<and> 379 (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 380 hiding methd G (super c) 381 under (\<lambda> new old. G\<turnstile>new overrides old) 382 entails (\<lambda> new old. 383 (G\<turnstile>resTy (mthd new)\<preceq>resTy (mthd old) \<and> 384 accmodi old \<le> accmodi new \<and> 385 \<not> is_static old))) \<and> 386 (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 387 hiding methd G (super c) 388 under (\<lambda> new old. G\<turnstile>new hides old) 389 entails (\<lambda> new old. is_static old \<and> 390 accmodi old \<le> accmodi new)) \<and> 391 (table_of (cfields c) hiding accfield G C (super c) 392 entails (\<lambda> newF oldF. accmodi oldF \<le> access newF))))" 393*) 394 395lemma wf_cdeclE [consumes 1]: 396 "\<lbrakk>wf_cdecl G (C,c); 397 \<lbrakk>\<not>is_iface G C; 398 (\<forall>I\<in>set (superIfs c). is_acc_iface G (pid C) I \<and> 399 (\<forall>s. \<forall> im \<in> imethds G I s. 400 (\<exists> cm \<in> methd G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and> 401 \<not> is_static cm \<and> 402 accmodi im \<le> accmodi cm))); 403 \<forall>f\<in>set (cfields c). wf_fdecl G (pid C) f; unique (cfields c); 404 \<forall>m\<in>set (methods c). wf_mdecl G C m; unique (methods c); 405 jumpNestingOkS {} (init c); 406 \<exists> A. \<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile> {} \<guillemotright>\<langle>init c\<rangle>\<guillemotright> A; 407 \<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile>(init c)\<Colon>\<surd>; 408 ws_cdecl G C (super c); 409 (C \<noteq> Object \<longrightarrow> 410 (is_acc_class G (pid C) (super c) \<and> 411 (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 412 entails (\<lambda> new. \<forall> old sig. 413 (G,sig\<turnstile>new overrides\<^sub>S old 414 \<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and> 415 accmodi old \<le> accmodi new \<and> 416 \<not>is_static old)) \<and> 417 (G,sig\<turnstile>new hides old 418 \<longrightarrow> (accmodi old \<le> accmodi new \<and> 419 is_static old)))) 420 ))\<rbrakk> \<Longrightarrow> P 421 \<rbrakk> \<Longrightarrow> P" 422by (unfold wf_cdecl_def) simp 423 424lemma wf_cdecl_unique: 425"wf_cdecl G (C,c) \<Longrightarrow> unique (cfields c) \<and> unique (methods c)" 426apply (unfold wf_cdecl_def) 427apply auto 428done 429 430lemma wf_cdecl_fdecl: 431"\<lbrakk>wf_cdecl G (C,c); f\<in>set (cfields c)\<rbrakk> \<Longrightarrow> wf_fdecl G (pid C) f" 432apply (unfold wf_cdecl_def) 433apply auto 434done 435 436lemma wf_cdecl_mdecl: 437"\<lbrakk>wf_cdecl G (C,c); m\<in>set (methods c)\<rbrakk> \<Longrightarrow> wf_mdecl G C m" 438apply (unfold wf_cdecl_def) 439apply auto 440done 441 442lemma wf_cdecl_impD: 443"\<lbrakk>wf_cdecl G (C,c); I\<in>set (superIfs c)\<rbrakk> 444\<Longrightarrow> is_acc_iface G (pid C) I \<and> 445 (\<forall>s. \<forall>im \<in> imethds G I s. 446 (\<exists>cm \<in> methd G C s: G\<turnstile>resTy cm\<preceq>resTy im \<and> \<not>is_static cm \<and> 447 accmodi im \<le> accmodi cm))" 448apply (unfold wf_cdecl_def) 449apply auto 450done 451 452lemma wf_cdecl_supD: 453"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object\<rbrakk> \<Longrightarrow> 454 is_acc_class G (pid C) (super c) \<and> (super c,C) \<notin> (subcls1 G)\<^sup>+ \<and> 455 (table_of (map (\<lambda> (s,m). (s,C,m)) (methods c)) 456 entails (\<lambda> new. \<forall> old sig. 457 (G,sig\<turnstile>new overrides\<^sub>S old 458 \<longrightarrow> (G\<turnstile>resTy new\<preceq>resTy old \<and> 459 accmodi old \<le> accmodi new \<and> 460 \<not>is_static old)) \<and> 461 (G,sig\<turnstile>new hides old 462 \<longrightarrow> (accmodi old \<le> accmodi new \<and> 463 is_static old))))" 464apply (unfold wf_cdecl_def ws_cdecl_def) 465apply auto 466done 467 468 469lemma wf_cdecl_overrides_SomeD: 470"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM; 471 G,sig\<turnstile>(C,newM) overrides\<^sub>S old 472\<rbrakk> \<Longrightarrow> G\<turnstile>resTy newM\<preceq>resTy old \<and> 473 accmodi old \<le> accmodi newM \<and> 474 \<not> is_static old" 475apply (drule (1) wf_cdecl_supD) 476apply (clarify) 477apply (drule entailsD) 478apply (blast intro: table_of_map_SomeI) 479apply (drule_tac x="old" in spec) 480apply (auto dest: overrides_eq_sigD simp add: msig_def) 481done 482 483lemma wf_cdecl_hides_SomeD: 484"\<lbrakk>wf_cdecl G (C,c); C \<noteq> Object; table_of (methods c) sig = Some newM; 485 G,sig\<turnstile>(C,newM) hides old 486\<rbrakk> \<Longrightarrow> accmodi old \<le> access newM \<and> 487 is_static old" 488apply (drule (1) wf_cdecl_supD) 489apply (clarify) 490apply (drule entailsD) 491apply (blast intro: table_of_map_SomeI) 492apply (drule_tac x="old" in spec) 493apply (auto dest: hides_eq_sigD simp add: msig_def) 494done 495 496lemma wf_cdecl_wt_init: 497 "wf_cdecl G (C, c) \<Longrightarrow> \<lparr>prg=G,cls=C,lcl=Map.empty\<rparr>\<turnstile>init c\<Colon>\<surd>" 498apply (unfold wf_cdecl_def) 499apply auto 500done 501 502 503subsubsection "well-formed programs" 504 (* well-formed program, cf. 8.1, 9.1 *) 505 506text \<open> 507A program declaration is wellformed if: 508\begin{itemize} 509\item the class ObjectC of Object is defined 510\item every method of Object has an access modifier distinct from Package. 511 This is 512 necessary since every interface automatically inherits from Object. 513 We must know, that every time a Object method is "overriden" by an 514 interface method this is also overriden by the class implementing the 515 the interface (see \<open>implement_dynmethd and class_mheadsD\<close>) 516\item all standard Exceptions are defined 517\item all defined interfaces are wellformed 518\item all defined classes are wellformed 519\end{itemize} 520\<close> 521definition 522 wf_prog :: "prog \<Rightarrow> bool" where 523 "wf_prog G = (let is = ifaces G; cs = classes G in 524 ObjectC \<in> set cs \<and> 525 (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package) \<and> 526 (\<forall>xn. SXcptC xn \<in> set cs) \<and> 527 (\<forall>i\<in>set is. wf_idecl G i) \<and> unique is \<and> 528 (\<forall>c\<in>set cs. wf_cdecl G c) \<and> unique cs)" 529 530lemma wf_prog_idecl: "\<lbrakk>iface G I = Some i; wf_prog G\<rbrakk> \<Longrightarrow> wf_idecl G (I,i)" 531apply (unfold wf_prog_def Let_def) 532apply simp 533apply (fast dest: map_of_SomeD) 534done 535 536lemma wf_prog_cdecl: "\<lbrakk>class G C = Some c; wf_prog G\<rbrakk> \<Longrightarrow> wf_cdecl G (C,c)" 537apply (unfold wf_prog_def Let_def) 538apply simp 539apply (fast dest: map_of_SomeD) 540done 541 542lemma wf_prog_Object_mdecls: 543"wf_prog G \<Longrightarrow> (\<forall> m\<in>set Object_mdecls. accmodi m \<noteq> Package)" 544apply (unfold wf_prog_def Let_def) 545apply simp 546done 547 548lemma wf_prog_acc_superD: 549 "\<lbrakk>wf_prog G; class G C = Some c; C \<noteq> Object \<rbrakk> 550 \<Longrightarrow> is_acc_class G (pid C) (super c)" 551by (auto dest: wf_prog_cdecl wf_cdecl_supD) 552 553lemma wf_ws_prog [elim!,simp]: "wf_prog G \<Longrightarrow> ws_prog G" 554apply (unfold wf_prog_def Let_def) 555apply (rule ws_progI) 556apply (simp_all (no_asm)) 557apply (auto simp add: is_acc_class_def is_acc_iface_def 558 dest!: wf_idecl_supD wf_cdecl_supD )+ 559done 560 561lemma class_Object [simp]: 562"wf_prog G \<Longrightarrow> 563 class G Object = Some \<lparr>access=Public,cfields=[],methods=Object_mdecls, 564 init=Skip,super=undefined,superIfs=[]\<rparr>" 565apply (unfold wf_prog_def Let_def ObjectC_def) 566apply (fast dest!: map_of_SomeI) 567done 568 569lemma methd_Object[simp]: "wf_prog G \<Longrightarrow> methd G Object = 570 table_of (map (\<lambda>(s,m). (s, Object, m)) Object_mdecls)" 571apply (subst methd_rec) 572apply (auto simp add: Let_def) 573done 574 575lemma wf_prog_Object_methd: 576"\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> accmodi m \<noteq> Package" 577by (auto dest!: wf_prog_Object_mdecls) (auto dest!: map_of_SomeD) 578 579lemma wf_prog_Object_is_public[intro]: 580 "wf_prog G \<Longrightarrow> is_public G Object" 581by (auto simp add: is_public_def dest: class_Object) 582 583lemma class_SXcpt [simp]: 584"wf_prog G \<Longrightarrow> 585 class G (SXcpt xn) = Some \<lparr>access=Public,cfields=[],methods=SXcpt_mdecls, 586 init=Skip, 587 super=if xn = Throwable then Object 588 else SXcpt Throwable, 589 superIfs=[]\<rparr>" 590apply (unfold wf_prog_def Let_def SXcptC_def) 591apply (fast dest!: map_of_SomeI) 592done 593 594lemma wf_ObjectC [simp]: 595 "wf_cdecl G ObjectC = (\<not>is_iface G Object \<and> Ball (set Object_mdecls) 596 (wf_mdecl G Object) \<and> unique Object_mdecls)" 597apply (unfold wf_cdecl_def ws_cdecl_def ObjectC_def) 598apply (auto intro: da.Skip) 599done 600 601lemma Object_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G Object" 602apply (simp (no_asm_simp)) 603done 604 605lemma Object_is_acc_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_acc_class G S Object" 606apply (simp (no_asm_simp) add: is_acc_class_def is_public_def 607 accessible_in_RefT_simp) 608done 609 610lemma SXcpt_is_class [simp,elim!]: "wf_prog G \<Longrightarrow> is_class G (SXcpt xn)" 611apply (simp (no_asm_simp)) 612done 613 614lemma SXcpt_is_acc_class [simp,elim!]: 615"wf_prog G \<Longrightarrow> is_acc_class G S (SXcpt xn)" 616apply (simp (no_asm_simp) add: is_acc_class_def is_public_def 617 accessible_in_RefT_simp) 618done 619 620lemma fields_Object [simp]: "wf_prog G \<Longrightarrow> DeclConcepts.fields G Object = []" 621by (force intro: fields_emptyI) 622 623lemma accfield_Object [simp]: 624 "wf_prog G \<Longrightarrow> accfield G S Object = Map.empty" 625apply (unfold accfield_def) 626apply (simp (no_asm_simp) add: Let_def) 627done 628 629lemma fields_Throwable [simp]: 630 "wf_prog G \<Longrightarrow> DeclConcepts.fields G (SXcpt Throwable) = []" 631by (force intro: fields_emptyI) 632 633lemma fields_SXcpt [simp]: "wf_prog G \<Longrightarrow> DeclConcepts.fields G (SXcpt xn) = []" 634apply (case_tac "xn = Throwable") 635apply (simp (no_asm_simp)) 636by (force intro: fields_emptyI) 637 638lemmas widen_trans = ws_widen_trans [OF _ _ wf_ws_prog, elim] 639lemma widen_trans2 [elim]: "\<lbrakk>G\<turnstile>U\<preceq>T; G\<turnstile>S\<preceq>U; wf_prog G\<rbrakk> \<Longrightarrow> G\<turnstile>S\<preceq>T" 640apply (erule (2) widen_trans) 641done 642 643lemma Xcpt_subcls_Throwable [simp]: 644"wf_prog G \<Longrightarrow> G\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable" 645apply (rule SXcpt_subcls_Throwable_lemma) 646apply auto 647done 648 649lemma unique_fields: 650 "\<lbrakk>is_class G C; wf_prog G\<rbrakk> \<Longrightarrow> unique (DeclConcepts.fields G C)" 651apply (erule ws_unique_fields) 652apply (erule wf_ws_prog) 653apply (erule (1) wf_prog_cdecl [THEN wf_cdecl_unique [THEN conjunct1]]) 654done 655 656lemma fields_mono: 657"\<lbrakk>table_of (DeclConcepts.fields G C) fn = Some f; G\<turnstile>D\<preceq>\<^sub>C C; 658 is_class G D; wf_prog G\<rbrakk> 659 \<Longrightarrow> table_of (DeclConcepts.fields G D) fn = Some f" 660apply (rule map_of_SomeI) 661apply (erule (1) unique_fields) 662apply (erule (1) map_of_SomeD [THEN fields_mono_lemma]) 663apply (erule wf_ws_prog) 664done 665 666 667lemma fields_is_type [elim]: 668"\<lbrakk>table_of (DeclConcepts.fields G C) m = Some f; wf_prog G; is_class G C\<rbrakk> \<Longrightarrow> 669 is_type G (type f)" 670apply (frule wf_ws_prog) 671apply (force dest: fields_declC [THEN conjunct1] 672 wf_prog_cdecl [THEN wf_cdecl_fdecl] 673 simp add: wf_fdecl_def2 is_acc_type_def) 674done 675 676lemma imethds_wf_mhead [rule_format (no_asm)]: 677"\<lbrakk>m \<in> imethds G I sig; wf_prog G; is_iface G I\<rbrakk> \<Longrightarrow> 678 wf_mhead G (pid (decliface m)) sig (mthd m) \<and> 679 \<not> is_static m \<and> accmodi m = Public" 680apply (frule wf_ws_prog) 681apply (drule (2) imethds_declI [THEN conjunct1]) 682apply clarify 683apply (frule_tac I="(decliface m)" in wf_prog_idecl,assumption) 684apply (drule wf_idecl_mhead) 685apply (erule map_of_SomeD) 686apply (cases m, simp) 687done 688 689lemma methd_wf_mdecl: 690 "\<lbrakk>methd G C sig = Some m; wf_prog G; class G C = Some y\<rbrakk> \<Longrightarrow> 691 G\<turnstile>C\<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m) \<and> 692 wf_mdecl G (declclass m) (sig,(mthd m))" 693apply (frule wf_ws_prog) 694apply (drule (1) methd_declC) 695apply fast 696apply clarsimp 697apply (frule (1) wf_prog_cdecl, erule wf_cdecl_mdecl, erule map_of_SomeD) 698done 699 700(* 701This lemma doesn't hold! 702lemma methd_rT_is_acc_type: 703"\<lbrakk>wf_prog G;methd G C C sig = Some (D,m); 704 class G C = Some y\<rbrakk> 705\<Longrightarrow> is_acc_type G (pid C) (resTy m)" 706The result Type is only visible in the scope of defining class D 707"is_vis_type G (pid D) (resTy m)" but not necessarily in scope of class C! 708(The same is true for the type of pramaters of a method) 709*) 710 711 712lemma methd_rT_is_type: 713"\<lbrakk>wf_prog G;methd G C sig = Some m; 714 class G C = Some y\<rbrakk> 715\<Longrightarrow> is_type G (resTy m)" 716apply (drule (2) methd_wf_mdecl) 717apply clarify 718apply (drule wf_mdeclD1) 719apply clarify 720apply (drule rT_is_acc_type) 721apply (cases m, simp add: is_acc_type_def) 722done 723 724lemma accmethd_rT_is_type: 725"\<lbrakk>wf_prog G;accmethd G S C sig = Some m; 726 class G C = Some y\<rbrakk> 727\<Longrightarrow> is_type G (resTy m)" 728by (auto simp add: accmethd_def 729 intro: methd_rT_is_type) 730 731lemma methd_Object_SomeD: 732"\<lbrakk>wf_prog G;methd G Object sig = Some m\<rbrakk> 733 \<Longrightarrow> declclass m = Object" 734by (auto dest: class_Object simp add: methd_rec ) 735 736lemmas iface_rec_induct' = iface_rec.induct [of "%x y z. P x y"] for P 737 738lemma wf_imethdsD: 739 "\<lbrakk>im \<in> imethds G I sig;wf_prog G; is_iface G I\<rbrakk> 740 \<Longrightarrow> \<not>is_static im \<and> accmodi im = Public" 741proof - 742 assume asm: "wf_prog G" "is_iface G I" "im \<in> imethds G I sig" 743 744 have "wf_prog G \<longrightarrow> 745 (\<forall> i im. iface G I = Some i \<longrightarrow> im \<in> imethds G I sig 746 \<longrightarrow> \<not>is_static im \<and> accmodi im = Public)" (is "?P G I") 747 proof (induct G I rule: iface_rec_induct', intro allI impI) 748 fix G I i im 749 assume hyp: "\<And> i J. iface G I = Some i \<Longrightarrow> ws_prog G \<Longrightarrow> J \<in> set (isuperIfs i) 750 \<Longrightarrow> ?P G J" 751 assume wf: "wf_prog G" and if_I: "iface G I = Some i" and 752 im: "im \<in> imethds G I sig" 753 show "\<not>is_static im \<and> accmodi im = Public" 754 proof - 755 let ?inherited = "Un_tables (imethds G ` set (isuperIfs i))" 756 let ?new = "(set_option \<circ> table_of (map (\<lambda>(s, mh). (s, I, mh)) (imethods i)))" 757 from if_I wf im have imethds:"im \<in> (?inherited \<oplus>\<oplus> ?new) sig" 758 by (simp add: imethds_rec) 759 from wf if_I have 760 wf_supI: "\<forall> J. J \<in> set (isuperIfs i) \<longrightarrow> (\<exists> j. iface G J = Some j)" 761 by (blast dest: wf_prog_idecl wf_idecl_supD is_acc_ifaceD) 762 from wf if_I have 763 "\<forall> im \<in> set (imethods i). \<not> is_static im \<and> accmodi im = Public" 764 by (auto dest!: wf_prog_idecl wf_idecl_mhead) 765 then have new_ok: "\<forall> im. table_of (imethods i) sig = Some im 766 \<longrightarrow> \<not> is_static im \<and> accmodi im = Public" 767 by (auto dest!: table_of_Some_in_set) 768 show ?thesis 769 proof (cases "?new sig = {}") 770 case True 771 from True wf wf_supI if_I imethds hyp 772 show ?thesis by (auto simp del: split_paired_All) 773 next 774 case False 775 from False wf wf_supI if_I imethds new_ok hyp 776 show ?thesis by (auto dest: wf_idecl_hidings hidings_entailsD) 777 qed 778 qed 779 qed 780 with asm show ?thesis by (auto simp del: split_paired_All) 781qed 782 783lemma wf_prog_hidesD: 784 assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G" 785 shows 786 "accmodi old \<le> accmodi new \<and> 787 is_static old" 788proof - 789 from hides 790 obtain c where 791 clsNew: "class G (declclass new) = Some c" and 792 neqObj: "declclass new \<noteq> Object" 793 by (auto dest: hidesD declared_in_classD) 794 with hides obtain newM oldM where 795 newM: "table_of (methods c) (msig new) = Some newM" and 796 new: "new = (declclass new,(msig new),newM)" and 797 old: "old = (declclass old,(msig old),oldM)" and 798 "msig new = msig old" 799 by (cases new,cases old) 800 (auto dest: hidesD 801 simp add: cdeclaredmethd_def declared_in_def) 802 with hides 803 have hides': 804 "G,(msig new)\<turnstile>(declclass new,newM) hides (declclass old,oldM)" 805 by auto 806 from clsNew wf 807 have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl) 808 note wf_cdecl_hides_SomeD [OF this neqObj newM hides'] 809 with new old 810 show ?thesis 811 by (cases new, cases old) auto 812qed 813 814text \<open>Compare this lemma about static 815overriding \<^term>\<open>G \<turnstile>new overrides\<^sub>S old\<close> with the definition of 816dynamic overriding \<^term>\<open>G \<turnstile>new overrides old\<close>. 817Conforming result types and restrictions on the access modifiers of the old 818and the new method are not part of the predicate for static overriding. But 819they are enshured in a wellfromed program. Dynamic overriding has 820no restrictions on the access modifiers but enforces confrom result types 821as precondition. But with some efford we can guarantee the access modifier 822restriction for dynamic overriding, too. See lemma 823\<open>wf_prog_dyn_override_prop\<close>. 824\<close> 825lemma wf_prog_stat_overridesD: 826 assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G" 827 shows 828 "G\<turnstile>resTy new\<preceq>resTy old \<and> 829 accmodi old \<le> accmodi new \<and> 830 \<not> is_static old" 831proof - 832 from stat_override 833 obtain c where 834 clsNew: "class G (declclass new) = Some c" and 835 neqObj: "declclass new \<noteq> Object" 836 by (auto dest: stat_overrides_commonD declared_in_classD) 837 with stat_override obtain newM oldM where 838 newM: "table_of (methods c) (msig new) = Some newM" and 839 new: "new = (declclass new,(msig new),newM)" and 840 old: "old = (declclass old,(msig old),oldM)" and 841 "msig new = msig old" 842 by (cases new,cases old) 843 (auto dest: stat_overrides_commonD 844 simp add: cdeclaredmethd_def declared_in_def) 845 with stat_override 846 have stat_override': 847 "G,(msig new)\<turnstile>(declclass new,newM) overrides\<^sub>S (declclass old,oldM)" 848 by auto 849 from clsNew wf 850 have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl) 851 note wf_cdecl_overrides_SomeD [OF this neqObj newM stat_override'] 852 with new old 853 show ?thesis 854 by (cases new, cases old) auto 855qed 856 857lemma static_to_dynamic_overriding: 858 assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G" 859 shows "G\<turnstile>new overrides old" 860proof - 861 from stat_override 862 show ?thesis (is "?Overrides new old") 863 proof (induct) 864 case (Direct new old superNew) 865 then have stat_override:"G\<turnstile>new overrides\<^sub>S old" 866 by (rule stat_overridesR.Direct) 867 from stat_override wf 868 have resTy_widen: "G\<turnstile>resTy new\<preceq>resTy old" and 869 not_static_old: "\<not> is_static old" 870 by (auto dest: wf_prog_stat_overridesD) 871 have not_private_new: "accmodi new \<noteq> Private" 872 proof - 873 from stat_override 874 have "accmodi old \<noteq> Private" 875 by (rule no_Private_stat_override) 876 moreover 877 from stat_override wf 878 have "accmodi old \<le> accmodi new" 879 by (auto dest: wf_prog_stat_overridesD) 880 ultimately 881 show ?thesis 882 by (auto dest: acc_modi_bottom) 883 qed 884 with Direct resTy_widen not_static_old 885 show "?Overrides new old" 886 by (auto intro: overridesR.Direct stat_override_declclasses_relation) 887 next 888 case (Indirect new inter old) 889 then show "?Overrides new old" 890 by (blast intro: overridesR.Indirect) 891 qed 892qed 893 894lemma non_Package_instance_method_inheritance: 895 assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and 896 accmodi_old: "accmodi old \<noteq> Package" and 897 instance_method: "\<not> is_static old" and 898 subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and 899 old_declared: "G\<turnstile>Method old declared_in (declclass old)" and 900 wf: "wf_prog G" 901 shows "G\<turnstile>Method old member_of C \<or> 902 (\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and> G\<turnstile>Method new member_of C)" 903proof - 904 from wf have ws: "ws_prog G" by auto 905 from old_declared have iscls_declC_old: "is_class G (declclass old)" 906 by (auto simp add: declared_in_def cdeclaredmethd_def) 907 from subcls have iscls_C: "is_class G C" 908 by (blast dest: subcls_is_class) 909 from iscls_C ws old_inheritable subcls 910 show ?thesis (is "?P C old") 911 proof (induct rule: ws_class_induct') 912 case Object 913 assume "G\<turnstile>Object\<prec>\<^sub>C declclass old" 914 then show "?P Object old" 915 by blast 916 next 917 case (Subcls C c) 918 assume cls_C: "class G C = Some c" and 919 neq_C_Obj: "C \<noteq> Object" and 920 hyp: "\<lbrakk>G \<turnstile>Method old inheritable_in pid (super c); 921 G\<turnstile>super c\<prec>\<^sub>C declclass old\<rbrakk> \<Longrightarrow> ?P (super c) old" and 922 inheritable: "G \<turnstile>Method old inheritable_in pid C" and 923 subclsC: "G\<turnstile>C\<prec>\<^sub>C declclass old" 924 from cls_C neq_C_Obj 925 have super: "G\<turnstile>C \<prec>\<^sub>C1 super c" 926 by (rule subcls1I) 927 from wf cls_C neq_C_Obj 928 have accessible_super: "G\<turnstile>(Class (super c)) accessible_in (pid C)" 929 by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD) 930 { 931 fix old 932 assume member_super: "G\<turnstile>Method old member_of (super c)" 933 assume inheritable: "G \<turnstile>Method old inheritable_in pid C" 934 assume instance_method: "\<not> is_static old" 935 from member_super 936 have old_declared: "G\<turnstile>Method old declared_in (declclass old)" 937 by (cases old) (auto dest: member_of_declC) 938 have "?P C old" 939 proof (cases "G\<turnstile>mid (msig old) undeclared_in C") 940 case True 941 with inheritable super accessible_super member_super 942 have "G\<turnstile>Method old member_of C" 943 by (cases old) (auto intro: members.Inherited) 944 then show ?thesis 945 by auto 946 next 947 case False 948 then obtain new_member where 949 "G\<turnstile>new_member declared_in C" and 950 "mid (msig old) = memberid new_member" 951 by (auto dest: not_undeclared_declared) 952 then obtain new where 953 new: "G\<turnstile>Method new declared_in C" and 954 eq_sig: "msig old = msig new" and 955 declC_new: "declclass new = C" 956 by (cases new_member) auto 957 then have member_new: "G\<turnstile>Method new member_of C" 958 by (cases new) (auto intro: members.Immediate) 959 from declC_new super member_super 960 have subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" 961 by (auto dest!: member_of_subclseq_declC 962 dest: r_into_trancl intro: trancl_rtrancl_trancl) 963 show ?thesis 964 proof (cases "is_static new") 965 case False 966 with eq_sig declC_new new old_declared inheritable 967 super member_super subcls_new_old 968 have "G\<turnstile>new overrides\<^sub>S old" 969 by (auto intro!: stat_overridesR.Direct) 970 with member_new show ?thesis 971 by blast 972 next 973 case True 974 with eq_sig declC_new subcls_new_old new old_declared inheritable 975 have "G\<turnstile>new hides old" 976 by (auto intro: hidesI) 977 with wf 978 have "is_static old" 979 by (blast dest: wf_prog_hidesD) 980 with instance_method 981 show ?thesis 982 by (contradiction) 983 qed 984 qed 985 } note hyp_member_super = this 986 from subclsC cls_C 987 have "G\<turnstile>(super c)\<preceq>\<^sub>C declclass old" 988 by (rule subcls_superD) 989 then 990 show "?P C old" 991 proof (cases rule: subclseq_cases) 992 case Eq 993 assume "super c = declclass old" 994 with old_declared 995 have "G\<turnstile>Method old member_of (super c)" 996 by (cases old) (auto intro: members.Immediate) 997 with inheritable instance_method 998 show ?thesis 999 by (blast dest: hyp_member_super) 1000 next 1001 case Subcls 1002 assume "G\<turnstile>super c\<prec>\<^sub>C declclass old" 1003 moreover 1004 from inheritable accmodi_old 1005 have "G \<turnstile>Method old inheritable_in pid (super c)" 1006 by (cases "accmodi old") (auto simp add: inheritable_in_def) 1007 ultimately 1008 have "?P (super c) old" 1009 by (blast dest: hyp) 1010 then show ?thesis 1011 proof 1012 assume "G \<turnstile>Method old member_of super c" 1013 with inheritable instance_method 1014 show ?thesis 1015 by (blast dest: hyp_member_super) 1016 next 1017 assume "\<exists>new. G \<turnstile> new overrides\<^sub>S old \<and> G \<turnstile>Method new member_of super c" 1018 then obtain super_new where 1019 super_new_override: "G \<turnstile> super_new overrides\<^sub>S old" and 1020 super_new_member: "G \<turnstile>Method super_new member_of super c" 1021 by blast 1022 from super_new_override wf 1023 have "accmodi old \<le> accmodi super_new" 1024 by (auto dest: wf_prog_stat_overridesD) 1025 with inheritable accmodi_old 1026 have "G \<turnstile>Method super_new inheritable_in pid C" 1027 by (auto simp add: inheritable_in_def 1028 split: acc_modi.splits 1029 dest: acc_modi_le_Dests) 1030 moreover 1031 from super_new_override 1032 have "\<not> is_static super_new" 1033 by (auto dest: stat_overrides_commonD) 1034 moreover 1035 note super_new_member 1036 ultimately have "?P C super_new" 1037 by (auto dest: hyp_member_super) 1038 then show ?thesis 1039 proof 1040 assume "G \<turnstile>Method super_new member_of C" 1041 with super_new_override 1042 show ?thesis 1043 by blast 1044 next 1045 assume "\<exists>new. G \<turnstile> new overrides\<^sub>S super_new \<and> 1046 G \<turnstile>Method new member_of C" 1047 with super_new_override show ?thesis 1048 by (blast intro: stat_overridesR.Indirect) 1049 qed 1050 qed 1051 qed 1052 qed 1053qed 1054 1055lemma non_Package_instance_method_inheritance_cases: 1056 assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and 1057 accmodi_old: "accmodi old \<noteq> Package" and 1058 instance_method: "\<not> is_static old" and 1059 subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and 1060 old_declared: "G\<turnstile>Method old declared_in (declclass old)" and 1061 wf: "wf_prog G" 1062 obtains (Inheritance) "G\<turnstile>Method old member_of C" 1063 | (Overriding) new where "G\<turnstile> new overrides\<^sub>S old" and "G\<turnstile>Method new member_of C" 1064proof - 1065 from old_inheritable accmodi_old instance_method subcls old_declared wf 1066 Inheritance Overriding 1067 show thesis 1068 by (auto dest: non_Package_instance_method_inheritance) 1069qed 1070 1071lemma dynamic_to_static_overriding: 1072 assumes dyn_override: "G\<turnstile> new overrides old" and 1073 accmodi_old: "accmodi old \<noteq> Package" and 1074 wf: "wf_prog G" 1075 shows "G\<turnstile> new overrides\<^sub>S old" 1076proof - 1077 from dyn_override accmodi_old 1078 show ?thesis (is "?Overrides new old") 1079 proof (induct rule: overridesR.induct) 1080 case (Direct new old) 1081 assume new_declared: "G\<turnstile>Method new declared_in declclass new" 1082 assume eq_sig_new_old: "msig new = msig old" 1083 assume subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" 1084 assume "G \<turnstile>Method old inheritable_in pid (declclass new)" and 1085 "accmodi old \<noteq> Package" and 1086 "\<not> is_static old" and 1087 "G\<turnstile>declclass new\<prec>\<^sub>C declclass old" and 1088 "G\<turnstile>Method old declared_in declclass old" 1089 from this wf 1090 show "?Overrides new old" 1091 proof (cases rule: non_Package_instance_method_inheritance_cases) 1092 case Inheritance 1093 assume "G \<turnstile>Method old member_of declclass new" 1094 then have "G\<turnstile>mid (msig old) undeclared_in declclass new" 1095 proof cases 1096 case Immediate 1097 with subcls_new_old wf show ?thesis 1098 by (auto dest: subcls_irrefl) 1099 next 1100 case Inherited 1101 then show ?thesis 1102 by (cases old) auto 1103 qed 1104 with eq_sig_new_old new_declared 1105 show ?thesis 1106 by (cases old,cases new) (auto dest!: declared_not_undeclared) 1107 next 1108 case (Overriding new') 1109 assume stat_override_new': "G \<turnstile> new' overrides\<^sub>S old" 1110 then have "msig new' = msig old" 1111 by (auto dest: stat_overrides_commonD) 1112 with eq_sig_new_old have eq_sig_new_new': "msig new=msig new'" 1113 by simp 1114 assume "G \<turnstile>Method new' member_of declclass new" 1115 then show ?thesis 1116 proof (cases) 1117 case Immediate 1118 then have declC_new: "declclass new' = declclass new" 1119 by auto 1120 from Immediate 1121 have "G\<turnstile>Method new' declared_in declclass new" 1122 by (cases new') auto 1123 with new_declared eq_sig_new_new' declC_new 1124 have "new=new'" 1125 by (cases new, cases new') (auto dest: unique_declared_in) 1126 with stat_override_new' 1127 show ?thesis 1128 by simp 1129 next 1130 case Inherited 1131 then have "G\<turnstile>mid (msig new') undeclared_in declclass new" 1132 by (cases new') (auto) 1133 with eq_sig_new_new' new_declared 1134 show ?thesis 1135 by (cases new,cases new') (auto dest!: declared_not_undeclared) 1136 qed 1137 qed 1138 next 1139 case (Indirect new inter old) 1140 assume accmodi_old: "accmodi old \<noteq> Package" 1141 assume "accmodi old \<noteq> Package \<Longrightarrow> G \<turnstile> inter overrides\<^sub>S old" 1142 with accmodi_old 1143 have stat_override_inter_old: "G \<turnstile> inter overrides\<^sub>S old" 1144 by blast 1145 moreover 1146 assume hyp_inter: "accmodi inter \<noteq> Package \<Longrightarrow> G \<turnstile> new overrides\<^sub>S inter" 1147 moreover 1148 have "accmodi inter \<noteq> Package" 1149 proof - 1150 from stat_override_inter_old wf 1151 have "accmodi old \<le> accmodi inter" 1152 by (auto dest: wf_prog_stat_overridesD) 1153 with stat_override_inter_old accmodi_old 1154 show ?thesis 1155 by (auto dest!: no_Private_stat_override 1156 split: acc_modi.splits 1157 dest: acc_modi_le_Dests) 1158 qed 1159 ultimately show "?Overrides new old" 1160 by (blast intro: stat_overridesR.Indirect) 1161 qed 1162qed 1163 1164lemma wf_prog_dyn_override_prop: 1165 assumes dyn_override: "G \<turnstile> new overrides old" and 1166 wf: "wf_prog G" 1167 shows "accmodi old \<le> accmodi new" 1168proof (cases "accmodi old = Package") 1169 case True 1170 note old_Package = this 1171 show ?thesis 1172 proof (cases "accmodi old \<le> accmodi new") 1173 case True then show ?thesis . 1174 next 1175 case False 1176 with old_Package 1177 have "accmodi new = Private" 1178 by (cases "accmodi new") (auto simp add: le_acc_def less_acc_def) 1179 with dyn_override 1180 show ?thesis 1181 by (auto dest: overrides_commonD) 1182 qed 1183next 1184 case False 1185 with dyn_override wf 1186 have "G \<turnstile> new overrides\<^sub>S old" 1187 by (blast intro: dynamic_to_static_overriding) 1188 with wf 1189 show ?thesis 1190 by (blast dest: wf_prog_stat_overridesD) 1191qed 1192 1193lemma overrides_Package_old: 1194 assumes dyn_override: "G \<turnstile> new overrides old" and 1195 accmodi_new: "accmodi new = Package" and 1196 wf: "wf_prog G " 1197 shows "accmodi old = Package" 1198proof (cases "accmodi old") 1199 case Private 1200 with dyn_override show ?thesis 1201 by (simp add: no_Private_override) 1202next 1203 case Package 1204 then show ?thesis . 1205next 1206 case Protected 1207 with dyn_override wf 1208 have "G \<turnstile> new overrides\<^sub>S old" 1209 by (auto intro: dynamic_to_static_overriding) 1210 with wf 1211 have "accmodi old \<le> accmodi new" 1212 by (auto dest: wf_prog_stat_overridesD) 1213 with Protected accmodi_new 1214 show ?thesis 1215 by (simp add: less_acc_def le_acc_def) 1216next 1217 case Public 1218 with dyn_override wf 1219 have "G \<turnstile> new overrides\<^sub>S old" 1220 by (auto intro: dynamic_to_static_overriding) 1221 with wf 1222 have "accmodi old \<le> accmodi new" 1223 by (auto dest: wf_prog_stat_overridesD) 1224 with Public accmodi_new 1225 show ?thesis 1226 by (simp add: less_acc_def le_acc_def) 1227qed 1228 1229lemma dyn_override_Package: 1230 assumes dyn_override: "G \<turnstile> new overrides old" and 1231 accmodi_old: "accmodi old = Package" and 1232 accmodi_new: "accmodi new = Package" and 1233 wf: "wf_prog G" 1234 shows "pid (declclass old) = pid (declclass new)" 1235proof - 1236 from dyn_override accmodi_old accmodi_new 1237 show ?thesis (is "?EqPid old new") 1238 proof (induct rule: overridesR.induct) 1239 case (Direct new old) 1240 assume "accmodi old = Package" 1241 "G \<turnstile>Method old inheritable_in pid (declclass new)" 1242 then show "pid (declclass old) = pid (declclass new)" 1243 by (auto simp add: inheritable_in_def) 1244 next 1245 case (Indirect new inter old) 1246 assume accmodi_old: "accmodi old = Package" and 1247 accmodi_new: "accmodi new = Package" 1248 assume "G \<turnstile> new overrides inter" 1249 with accmodi_new wf 1250 have "accmodi inter = Package" 1251 by (auto intro: overrides_Package_old) 1252 with Indirect 1253 show "pid (declclass old) = pid (declclass new)" 1254 by auto 1255 qed 1256qed 1257 1258lemma dyn_override_Package_escape: 1259 assumes dyn_override: "G \<turnstile> new overrides old" and 1260 accmodi_old: "accmodi old = Package" and 1261 outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and 1262 wf: "wf_prog G" 1263 shows "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and> 1264 pid (declclass old) = pid (declclass inter) \<and> 1265 Protected \<le> accmodi inter" 1266proof - 1267 from dyn_override accmodi_old outside_pack 1268 show ?thesis (is "?P new old") 1269 proof (induct rule: overridesR.induct) 1270 case (Direct new old) 1271 assume accmodi_old: "accmodi old = Package" 1272 assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" 1273 assume "G \<turnstile>Method old inheritable_in pid (declclass new)" 1274 with accmodi_old 1275 have "pid (declclass old) = pid (declclass new)" 1276 by (simp add: inheritable_in_def) 1277 with outside_pack 1278 show "?P new old" 1279 by (contradiction) 1280 next 1281 case (Indirect new inter old) 1282 assume accmodi_old: "accmodi old = Package" 1283 assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" 1284 assume override_new_inter: "G \<turnstile> new overrides inter" 1285 assume override_inter_old: "G \<turnstile> inter overrides old" 1286 assume hyp_new_inter: "\<lbrakk>accmodi inter = Package; 1287 pid (declclass inter) \<noteq> pid (declclass new)\<rbrakk> 1288 \<Longrightarrow> ?P new inter" 1289 assume hyp_inter_old: "\<lbrakk>accmodi old = Package; 1290 pid (declclass old) \<noteq> pid (declclass inter)\<rbrakk> 1291 \<Longrightarrow> ?P inter old" 1292 show "?P new old" 1293 proof (cases "pid (declclass old) = pid (declclass inter)") 1294 case True 1295 note same_pack_old_inter = this 1296 show ?thesis 1297 proof (cases "pid (declclass inter) = pid (declclass new)") 1298 case True 1299 with same_pack_old_inter outside_pack 1300 show ?thesis 1301 by auto 1302 next 1303 case False 1304 note diff_pack_inter_new = this 1305 show ?thesis 1306 proof (cases "accmodi inter = Package") 1307 case True 1308 with diff_pack_inter_new hyp_new_inter 1309 obtain newinter where 1310 over_new_newinter: "G \<turnstile> new overrides newinter" and 1311 over_newinter_inter: "G \<turnstile> newinter overrides inter" and 1312 eq_pid: "pid (declclass inter) = pid (declclass newinter)" and 1313 accmodi_newinter: "Protected \<le> accmodi newinter" 1314 by auto 1315 from over_newinter_inter override_inter_old 1316 have "G\<turnstile>newinter overrides old" 1317 by (rule overridesR.Indirect) 1318 moreover 1319 from eq_pid same_pack_old_inter 1320 have "pid (declclass old) = pid (declclass newinter)" 1321 by simp 1322 moreover 1323 note over_new_newinter accmodi_newinter 1324 ultimately show ?thesis 1325 by blast 1326 next 1327 case False 1328 with override_new_inter 1329 have "Protected \<le> accmodi inter" 1330 by (cases "accmodi inter") (auto dest: no_Private_override) 1331 with override_new_inter override_inter_old same_pack_old_inter 1332 show ?thesis 1333 by blast 1334 qed 1335 qed 1336 next 1337 case False 1338 with accmodi_old hyp_inter_old 1339 obtain newinter where 1340 over_inter_newinter: "G \<turnstile> inter overrides newinter" and 1341 over_newinter_old: "G \<turnstile> newinter overrides old" and 1342 eq_pid: "pid (declclass old) = pid (declclass newinter)" and 1343 accmodi_newinter: "Protected \<le> accmodi newinter" 1344 by auto 1345 from override_new_inter over_inter_newinter 1346 have "G \<turnstile> new overrides newinter" 1347 by (rule overridesR.Indirect) 1348 with eq_pid over_newinter_old accmodi_newinter 1349 show ?thesis 1350 by blast 1351 qed 1352 qed 1353qed 1354 1355lemmas class_rec_induct' = class_rec.induct [of "%x y z w. P x y"] for P 1356 1357lemma declclass_widen[rule_format]: 1358 "wf_prog G 1359 \<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 1360 \<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C") 1361proof (induct G C rule: class_rec_induct', intro allI impI) 1362 fix G C c m 1363 assume Hyp: "\<And>c. class G C = Some c \<Longrightarrow> ws_prog G \<Longrightarrow> C \<noteq> Object 1364 \<Longrightarrow> ?P G (super c)" 1365 assume wf: "wf_prog G" and cls_C: "class G C = Some c" and 1366 m: "methd G C sig = Some m" 1367 show "G\<turnstile>C\<preceq>\<^sub>C declclass m" 1368 proof (cases "C=Object") 1369 case True 1370 with wf m show ?thesis by (simp add: methd_Object_SomeD) 1371 next 1372 let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)" 1373 let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))" 1374 case False 1375 with cls_C wf m 1376 have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m " 1377 by (simp add: methd_rec) 1378 show ?thesis 1379 proof (cases "?table sig") 1380 case None 1381 from this methd_C have "?filter (methd G (super c)) sig = Some m" 1382 by simp 1383 moreover 1384 from wf cls_C False obtain sup where "class G (super c) = Some sup" 1385 by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class) 1386 moreover note wf False cls_C 1387 ultimately have "G\<turnstile>super c \<preceq>\<^sub>C declclass m" 1388 by (auto intro: Hyp [rule_format]) 1389 moreover from cls_C False have "G\<turnstile>C \<prec>\<^sub>C1 super c" by (rule subcls1I) 1390 ultimately show ?thesis by - (rule rtrancl_into_rtrancl2) 1391 next 1392 case Some 1393 from this wf False cls_C methd_C show ?thesis by auto 1394 qed 1395 qed 1396qed 1397 1398lemma declclass_methd_Object: 1399 "\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> declclass m = Object" 1400by auto 1401 1402lemma methd_declaredD: 1403 "\<lbrakk>wf_prog G; is_class G C;methd G C sig = Some m\<rbrakk> 1404 \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)" 1405proof - 1406 assume wf: "wf_prog G" 1407 then have ws: "ws_prog G" .. 1408 assume clsC: "is_class G C" 1409 from clsC ws 1410 show "methd G C sig = Some m 1411 \<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)" 1412 proof (induct C rule: ws_class_induct') 1413 case Object 1414 assume "methd G Object sig = Some m" 1415 with wf show ?thesis 1416 by - (rule method_declared_inI, auto) 1417 next 1418 case Subcls 1419 fix C c 1420 assume clsC: "class G C = Some c" 1421 and m: "methd G C sig = Some m" 1422 and hyp: "methd G (super c) sig = Some m \<Longrightarrow> ?thesis" 1423 let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))" 1424 show ?thesis 1425 proof (cases "?newMethods sig") 1426 case None 1427 from None ws clsC m hyp 1428 show ?thesis by (auto intro: method_declared_inI simp add: methd_rec) 1429 next 1430 case Some 1431 from Some ws clsC m 1432 show ?thesis by (auto intro: method_declared_inI simp add: methd_rec) 1433 qed 1434 qed 1435qed 1436 1437lemma methd_rec_Some_cases: 1438 assumes methd_C: "methd G C sig = Some m" and 1439 ws: "ws_prog G" and 1440 clsC: "class G C = Some c" and 1441 neq_C_Obj: "C\<noteq>Object" 1442 obtains (NewMethod) "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m" 1443 | (InheritedMethod) "G\<turnstile>C inherits (method sig m)" and "methd G (super c) sig = Some m" 1444proof - 1445 let ?inherited = "filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m) 1446 (methd G (super c))" 1447 let ?new = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))" 1448 from ws clsC neq_C_Obj methd_C 1449 have methd_unfold: "(?inherited ++ ?new) sig = Some m" 1450 by (simp add: methd_rec) 1451 show thesis 1452 proof (cases "?new sig") 1453 case None 1454 with methd_unfold have "?inherited sig = Some m" 1455 by (auto) 1456 with InheritedMethod show ?thesis by blast 1457 next 1458 case Some 1459 with methd_unfold have "?new sig = Some m" 1460 by auto 1461 with NewMethod show ?thesis by blast 1462 qed 1463qed 1464 1465 1466lemma methd_member_of: 1467 assumes wf: "wf_prog G" 1468 shows 1469 "\<lbrakk>is_class G C; methd G C sig = Some m\<rbrakk> \<Longrightarrow> G\<turnstile>Methd sig m member_of C" 1470 (is "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C") 1471proof - 1472 from wf have ws: "ws_prog G" .. 1473 assume defC: "is_class G C" 1474 from defC ws 1475 show "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C" 1476 proof (induct rule: ws_class_induct') 1477 case Object 1478 with wf have declC: "Object = declclass m" 1479 by (simp add: declclass_methd_Object) 1480 from Object wf have "G\<turnstile>Methd sig m declared_in Object" 1481 by (auto intro: methd_declaredD simp add: declC) 1482 with declC 1483 show "?MemberOf Object" 1484 by (auto intro!: members.Immediate 1485 simp del: methd_Object) 1486 next 1487 case (Subcls C c) 1488 assume clsC: "class G C = Some c" and 1489 neq_C_Obj: "C \<noteq> Object" 1490 assume methd: "?Method C" 1491 from methd ws clsC neq_C_Obj 1492 show "?MemberOf C" 1493 proof (cases rule: methd_rec_Some_cases) 1494 case NewMethod 1495 with clsC show ?thesis 1496 by (auto dest: method_declared_inI intro!: members.Immediate) 1497 next 1498 case InheritedMethod 1499 then show "?thesis" 1500 by (blast dest: inherits_member) 1501 qed 1502 qed 1503qed 1504 1505lemma current_methd: 1506 "\<lbrakk>table_of (methods c) sig = Some new; 1507 ws_prog G; class G C = Some c; C \<noteq> Object; 1508 methd G (super c) sig = Some old\<rbrakk> 1509 \<Longrightarrow> methd G C sig = Some (C,new)" 1510by (auto simp add: methd_rec 1511 intro: filter_tab_SomeI map_add_find_right table_of_map_SomeI) 1512 1513lemma wf_prog_staticD: 1514 assumes wf: "wf_prog G" and 1515 clsC: "class G C = Some c" and 1516 neq_C_Obj: "C \<noteq> Object" and 1517 old: "methd G (super c) sig = Some old" and 1518 accmodi_old: "Protected \<le> accmodi old" and 1519 new: "table_of (methods c) sig = Some new" 1520 shows "is_static new = is_static old" 1521proof - 1522 from clsC wf 1523 have wf_cdecl: "wf_cdecl G (C,c)" by (rule wf_prog_cdecl) 1524 from wf clsC neq_C_Obj 1525 have is_cls_super: "is_class G (super c)" 1526 by (blast dest: wf_prog_acc_superD is_acc_classD) 1527 from wf is_cls_super old 1528 have old_member_of: "G\<turnstile>Methd sig old member_of (super c)" 1529 by (rule methd_member_of) 1530 from old wf is_cls_super 1531 have old_declared: "G\<turnstile>Methd sig old declared_in (declclass old)" 1532 by (auto dest: methd_declared_in_declclass) 1533 from new clsC 1534 have new_declared: "G\<turnstile>Methd sig (C,new) declared_in C" 1535 by (auto intro: method_declared_inI) 1536 note trancl_rtrancl_tranc = trancl_rtrancl_trancl [trans] (* ### in Basis *) 1537 from clsC neq_C_Obj 1538 have subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C1 super c" 1539 by (rule subcls1I) 1540 then have "G\<turnstile>C \<prec>\<^sub>C super c" .. 1541 also from old wf is_cls_super 1542 have "G\<turnstile>super c \<preceq>\<^sub>C (declclass old)" by (auto dest: methd_declC) 1543 finally have subcls_C_old: "G\<turnstile>C \<prec>\<^sub>C (declclass old)" . 1544 from accmodi_old 1545 have inheritable: "G\<turnstile>Methd sig old inheritable_in pid C" 1546 by (auto simp add: inheritable_in_def 1547 dest: acc_modi_le_Dests) 1548 show ?thesis 1549 proof (cases "is_static new") 1550 case True 1551 with subcls_C_old new_declared old_declared inheritable 1552 have "G,sig\<turnstile>(C,new) hides old" 1553 by (auto intro: hidesI) 1554 with True wf_cdecl neq_C_Obj new 1555 show ?thesis 1556 by (auto dest: wf_cdecl_hides_SomeD) 1557 next 1558 case False 1559 with subcls_C_old new_declared old_declared inheritable subcls1_C_super 1560 old_member_of 1561 have "G,sig\<turnstile>(C,new) overrides\<^sub>S old" 1562 by (auto intro: stat_overridesR.Direct) 1563 with False wf_cdecl neq_C_Obj new 1564 show ?thesis 1565 by (auto dest: wf_cdecl_overrides_SomeD) 1566 qed 1567qed 1568 1569lemma inheritable_instance_methd: 1570 assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and 1571 is_cls_D: "is_class G D" and 1572 wf: "wf_prog G" and 1573 old: "methd G D sig = Some old" and 1574 accmodi_old: "Protected \<le> accmodi old" and 1575 not_static_old: "\<not> is_static old" 1576 shows 1577 "\<exists>new. methd G C sig = Some new \<and> 1578 (new = old \<or> G,sig\<turnstile>new overrides\<^sub>S old)" 1579 (is "(\<exists>new. (?Constraint C new old))") 1580proof - 1581 from subclseq_C_D is_cls_D 1582 have is_cls_C: "is_class G C" by (rule subcls_is_class2) 1583 from wf 1584 have ws: "ws_prog G" .. 1585 from is_cls_C ws subclseq_C_D 1586 show "\<exists>new. ?Constraint C new old" 1587 proof (induct rule: ws_class_induct') 1588 case (Object co) 1589 then have eq_D_Obj: "D=Object" by auto 1590 with old 1591 have "?Constraint Object old old" 1592 by auto 1593 with eq_D_Obj 1594 show "\<exists> new. ?Constraint Object new old" by auto 1595 next 1596 case (Subcls C c) 1597 assume hyp: "G\<turnstile>super c\<preceq>\<^sub>C D \<Longrightarrow> \<exists>new. ?Constraint (super c) new old" 1598 assume clsC: "class G C = Some c" 1599 assume neq_C_Obj: "C\<noteq>Object" 1600 from clsC wf 1601 have wf_cdecl: "wf_cdecl G (C,c)" 1602 by (rule wf_prog_cdecl) 1603 from ws clsC neq_C_Obj 1604 have is_cls_super: "is_class G (super c)" 1605 by (auto dest: ws_prog_cdeclD) 1606 from clsC wf neq_C_Obj 1607 have superAccessible: "G\<turnstile>(Class (super c)) accessible_in (pid C)" and 1608 subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C1 super c" 1609 by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD 1610 intro: subcls1I) 1611 show "\<exists>new. ?Constraint C new old" 1612 proof (cases "G\<turnstile>super c\<preceq>\<^sub>C D") 1613 case False 1614 from False Subcls 1615 have eq_C_D: "C=D" 1616 by (auto dest: subclseq_superD) 1617 with old 1618 have "?Constraint C old old" 1619 by auto 1620 with eq_C_D 1621 show "\<exists> new. ?Constraint C new old" by auto 1622 next 1623 case True 1624 with hyp obtain super_method 1625 where super: "?Constraint (super c) super_method old" by blast 1626 from super not_static_old 1627 have not_static_super: "\<not> is_static super_method" 1628 by (auto dest!: stat_overrides_commonD) 1629 from super old wf accmodi_old 1630 have accmodi_super_method: "Protected \<le> accmodi super_method" 1631 by (auto dest!: wf_prog_stat_overridesD) 1632 from super accmodi_old wf 1633 have inheritable: "G\<turnstile>Methd sig super_method inheritable_in (pid C)" 1634 by (auto dest!: wf_prog_stat_overridesD 1635 acc_modi_le_Dests 1636 simp add: inheritable_in_def) 1637 from super wf is_cls_super 1638 have member: "G\<turnstile>Methd sig super_method member_of (super c)" 1639 by (auto intro: methd_member_of) 1640 from member 1641 have decl_super_method: 1642 "G\<turnstile>Methd sig super_method declared_in (declclass super_method)" 1643 by (auto dest: member_of_declC) 1644 from super subcls1_C_super ws is_cls_super 1645 have subcls_C_super: "G\<turnstile>C \<prec>\<^sub>C (declclass super_method)" 1646 by (auto intro: rtrancl_into_trancl2 dest: methd_declC) 1647 show "\<exists> new. ?Constraint C new old" 1648 proof (cases "methd G C sig") 1649 case None 1650 have "methd G (super c) sig = None" 1651 proof - 1652 from clsC ws None 1653 have no_new: "table_of (methods c) sig = None" 1654 by (auto simp add: methd_rec) 1655 with clsC 1656 have undeclared: "G\<turnstile>mid sig undeclared_in C" 1657 by (auto simp add: undeclared_in_def cdeclaredmethd_def) 1658 with inheritable member superAccessible subcls1_C_super 1659 have inherits: "G\<turnstile>C inherits (method sig super_method)" 1660 by (auto simp add: inherits_def) 1661 with clsC ws no_new super neq_C_Obj 1662 have "methd G C sig = Some super_method" 1663 by (auto simp add: methd_rec map_add_def intro: filter_tab_SomeI) 1664 with None show ?thesis 1665 by simp 1666 qed 1667 with super show ?thesis by auto 1668 next 1669 case (Some new) 1670 from this ws clsC neq_C_Obj 1671 show ?thesis 1672 proof (cases rule: methd_rec_Some_cases) 1673 case InheritedMethod 1674 with super Some show ?thesis 1675 by auto 1676 next 1677 case NewMethod 1678 assume new: "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig 1679 = Some new" 1680 from new 1681 have declcls_new: "declclass new = C" 1682 by auto 1683 from wf clsC neq_C_Obj super new not_static_super accmodi_super_method 1684 have not_static_new: "\<not> is_static new" 1685 by (auto dest: wf_prog_staticD) 1686 from clsC new 1687 have decl_new: "G\<turnstile>Methd sig new declared_in C" 1688 by (auto simp add: declared_in_def cdeclaredmethd_def) 1689 from not_static_new decl_new decl_super_method 1690 member subcls1_C_super inheritable declcls_new subcls_C_super 1691 have "G,sig\<turnstile> new overrides\<^sub>S super_method" 1692 by (auto intro: stat_overridesR.Direct) 1693 with super Some 1694 show ?thesis 1695 by (auto intro: stat_overridesR.Indirect) 1696 qed 1697 qed 1698 qed 1699 qed 1700qed 1701 1702lemma inheritable_instance_methd_cases: 1703 assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and 1704 is_cls_D: "is_class G D" and 1705 wf: "wf_prog G" and 1706 old: "methd G D sig = Some old" and 1707 accmodi_old: "Protected \<le> accmodi old" and 1708 not_static_old: "\<not> is_static old" 1709 obtains (Inheritance) "methd G C sig = Some old" 1710 | (Overriding) new where "methd G C sig = Some new" and "G,sig\<turnstile>new overrides\<^sub>S old" 1711proof - 1712 from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 1713 show ?thesis 1714 by (auto dest: inheritable_instance_methd intro: Inheritance Overriding) 1715qed 1716 1717lemma inheritable_instance_methd_props: 1718 assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and 1719 is_cls_D: "is_class G D" and 1720 wf: "wf_prog G" and 1721 old: "methd G D sig = Some old" and 1722 accmodi_old: "Protected \<le> accmodi old" and 1723 not_static_old: "\<not> is_static old" 1724 shows 1725 "\<exists>new. methd G C sig = Some new \<and> 1726 \<not> is_static new \<and> G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le>accmodi new" 1727 (is "(\<exists>new. (?Constraint C new old))") 1728proof - 1729 from subclseq_C_D is_cls_D wf old accmodi_old not_static_old 1730 show ?thesis 1731 proof (cases rule: inheritable_instance_methd_cases) 1732 case Inheritance 1733 with not_static_old accmodi_old show ?thesis by auto 1734 next 1735 case (Overriding new) 1736 then have "\<not> is_static new" by (auto dest: stat_overrides_commonD) 1737 with Overriding not_static_old accmodi_old wf 1738 show ?thesis 1739 by (auto dest!: wf_prog_stat_overridesD) 1740 qed 1741qed 1742 1743(* local lemma *) 1744lemma bexI': "x \<in> A \<Longrightarrow> P x \<Longrightarrow> \<exists>x\<in>A. P x" by blast 1745lemma ballE': "\<forall>x\<in>A. P x \<Longrightarrow> (x \<notin> A \<Longrightarrow> Q) \<Longrightarrow> (P x \<Longrightarrow> Q) \<Longrightarrow> Q" by blast 1746 1747lemma subint_widen_imethds: 1748 assumes irel: "G\<turnstile>I\<preceq>I J" 1749 and wf: "wf_prog G" 1750 and is_iface: "is_iface G J" 1751 and jm: "jm \<in> imethds G J sig" 1752 shows "\<exists>im \<in> imethds G I sig. is_static im = is_static jm \<and> 1753 accmodi im = accmodi jm \<and> 1754 G\<turnstile>resTy im\<preceq>resTy jm" 1755 using irel jm 1756proof (induct rule: converse_rtrancl_induct) 1757 case base 1758 then show ?case by (blast elim: bexI') 1759 next 1760 case (step I SI) 1761 from \<open>G\<turnstile>I \<prec>I1 SI\<close> 1762 obtain i where 1763 ifI: "iface G I = Some i" and 1764 SI: "SI \<in> set (isuperIfs i)" 1765 by (blast dest: subint1D) 1766 1767 let ?newMethods 1768 = "(set_option \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))" 1769 show ?case 1770 proof (cases "?newMethods sig = {}") 1771 case True 1772 with ifI SI step wf 1773 show "?thesis" 1774 by (auto simp add: imethds_rec) 1775 next 1776 case False 1777 from ifI wf False 1778 have imethds: "imethds G I sig = ?newMethods sig" 1779 by (simp add: imethds_rec) 1780 from False 1781 obtain im where 1782 imdef: "im \<in> ?newMethods sig" 1783 by (blast) 1784 with imethds 1785 have im: "im \<in> imethds G I sig" 1786 by (blast) 1787 with im wf ifI 1788 obtain 1789 imStatic: "\<not> is_static im" and 1790 imPublic: "accmodi im = Public" 1791 by (auto dest!: imethds_wf_mhead) 1792 from ifI wf 1793 have wf_I: "wf_idecl G (I,i)" 1794 by (rule wf_prog_idecl) 1795 with SI wf 1796 obtain si where 1797 ifSI: "iface G SI = Some si" and 1798 wf_SI: "wf_idecl G (SI,si)" 1799 by (auto dest!: wf_idecl_supD is_acc_ifaceD 1800 dest: wf_prog_idecl) 1801 from step 1802 obtain sim::"qtname \<times> mhead" where 1803 sim: "sim \<in> imethds G SI sig" and 1804 eq_static_sim_jm: "is_static sim = is_static jm" and 1805 eq_access_sim_jm: "accmodi sim = accmodi jm" and 1806 resTy_widen_sim_jm: "G\<turnstile>resTy sim\<preceq>resTy jm" 1807 by blast 1808 with wf_I SI imdef sim 1809 have "G\<turnstile>resTy im\<preceq>resTy sim" 1810 by (auto dest!: wf_idecl_hidings hidings_entailsD) 1811 with wf resTy_widen_sim_jm 1812 have resTy_widen_im_jm: "G\<turnstile>resTy im\<preceq>resTy jm" 1813 by (blast intro: widen_trans) 1814 from sim wf ifSI 1815 obtain 1816 simStatic: "\<not> is_static sim" and 1817 simPublic: "accmodi sim = Public" 1818 by (auto dest!: imethds_wf_mhead) 1819 from im 1820 imStatic simStatic eq_static_sim_jm 1821 imPublic simPublic eq_access_sim_jm 1822 resTy_widen_im_jm 1823 show ?thesis 1824 by auto 1825 qed 1826qed 1827 1828(* Tactical version *) 1829(* 1830lemma subint_widen_imethds: "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J\<rbrakk> \<Longrightarrow> 1831 \<forall> jm \<in> imethds G J sig. 1832 \<exists> im \<in> imethds G I sig. static (mthd im)=static (mthd jm) \<and> 1833 access (mthd im)= access (mthd jm) \<and> 1834 G\<turnstile>resTy (mthd im)\<preceq>resTy (mthd jm)" 1835apply (erule converse_rtrancl_induct) 1836apply (clarsimp elim!: bexI') 1837apply (frule subint1D) 1838apply clarify 1839apply (erule ballE') 1840apply fast 1841apply (erule_tac V = "?x \<in> imethds G J sig" in thin_rl) 1842apply clarsimp 1843apply (subst imethds_rec, assumption, erule wf_ws_prog) 1844apply (unfold overrides_t_def) 1845apply (drule (1) wf_prog_idecl) 1846apply (frule (3) imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1 1847 [THEN is_acc_ifaceD [THEN conjunct1]]]]) 1848apply (case_tac "(set_option \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i))) 1849 sig ={}") 1850apply force 1851 1852apply (simp only:) 1853apply (simp) 1854apply clarify 1855apply (frule wf_idecl_hidings [THEN hidings_entailsD]) 1856apply blast 1857apply blast 1858apply (rule bexI') 1859apply simp 1860apply (drule table_of_map_SomeI [of _ "sig"]) 1861apply simp 1862 1863apply (frule wf_idecl_mhead [of _ _ _ "sig"]) 1864apply (rule table_of_Some_in_set) 1865apply assumption 1866apply auto 1867done 1868*) 1869 1870 1871(* local lemma *) 1872lemma implmt1_methd: 1873 "\<And>sig. \<lbrakk>G\<turnstile>C\<leadsto>1I; wf_prog G; im \<in> imethds G I sig\<rbrakk> \<Longrightarrow> 1874 \<exists>cm \<in>methd G C sig: \<not> is_static cm \<and> \<not> is_static im \<and> 1875 G\<turnstile>resTy cm\<preceq>resTy im \<and> 1876 accmodi im = Public \<and> accmodi cm = Public" 1877apply (drule implmt1D) 1878apply clarify 1879apply (drule (2) wf_prog_cdecl [THEN wf_cdecl_impD]) 1880apply (frule (1) imethds_wf_mhead) 1881apply (simp add: is_acc_iface_def) 1882apply (force) 1883done 1884 1885 1886(* local lemma *) 1887lemma implmt_methd [rule_format (no_asm)]: 1888"\<lbrakk>wf_prog G; G\<turnstile>C\<leadsto>I\<rbrakk> \<Longrightarrow> is_iface G I \<longrightarrow> 1889 (\<forall> im \<in>imethds G I sig. 1890 \<exists> cm\<in>methd G C sig: \<not>is_static cm \<and> \<not> is_static im \<and> 1891 G\<turnstile>resTy cm\<preceq>resTy im \<and> 1892 accmodi im = Public \<and> accmodi cm = Public)" 1893apply (frule implmt_is_class) 1894apply (erule implmt.induct) 1895apply safe 1896apply (drule (2) implmt1_methd) 1897apply fast 1898apply (drule (1) subint_widen_imethds) 1899apply simp 1900apply assumption 1901apply clarify 1902apply (drule (2) implmt1_methd) 1903apply (force) 1904apply (frule subcls1D) 1905apply (drule (1) bspec) 1906apply clarify 1907apply (drule (3) r_into_rtrancl [THEN inheritable_instance_methd_props, 1908 OF _ implmt_is_class]) 1909apply auto 1910done 1911 1912lemma mheadsD [rule_format (no_asm)]: 1913"emh \<in> mheads G S t sig \<longrightarrow> wf_prog G \<longrightarrow> 1914 (\<exists>C D m. t = ClassT C \<and> declrefT emh = ClassT D \<and> 1915 accmethd G S C sig = Some m \<and> 1916 (declclass m = D) \<and> mhead (mthd m) = (mhd emh)) \<or> 1917 (\<exists>I. t = IfaceT I \<and> ((\<exists>im. im \<in> accimethds G (pid S) I sig \<and> 1918 mthd im = mhd emh) \<or> 1919 (\<exists>m. G\<turnstile>Iface I accessible_in (pid S) \<and> accmethd G S Object sig = Some m \<and> 1920 accmodi m \<noteq> Private \<and> 1921 declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh))) \<or> 1922 (\<exists>T m. t = ArrayT T \<and> G\<turnstile>Array T accessible_in (pid S) \<and> 1923 accmethd G S Object sig = Some m \<and> accmodi m \<noteq> Private \<and> 1924 declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh)" 1925apply (rule_tac ref_ty1="t" in ref_ty_ty.induct [THEN conjunct1]) 1926apply auto 1927apply (auto simp add: cmheads_def accObjectmheads_def Objectmheads_def) 1928apply (auto dest!: accmethd_SomeD) 1929done 1930 1931lemma mheads_cases: 1932 assumes "emh \<in> mheads G S t sig" and "wf_prog G" 1933 obtains (Class_methd) C D m where 1934 "t = ClassT C" "declrefT emh = ClassT D" "accmethd G S C sig = Some m" 1935 "declclass m = D" "mhead (mthd m) = mhd emh" 1936 | (Iface_methd) I im where "t = IfaceT I" 1937 "im \<in> accimethds G (pid S) I sig" "mthd im = mhd emh" 1938 | (Iface_Object_methd) I m where 1939 "t = IfaceT I" "G\<turnstile>Iface I accessible_in (pid S)" 1940 "accmethd G S Object sig = Some m" "accmodi m \<noteq> Private" 1941 "declrefT emh = ClassT Object" "mhead (mthd m) = mhd emh" 1942 | (Array_Object_methd) T m where 1943 "t = ArrayT T" "G\<turnstile>Array T accessible_in (pid S)" 1944 "accmethd G S Object sig = Some m" "accmodi m \<noteq> Private" 1945 "declrefT emh = ClassT Object" "mhead (mthd m) = mhd emh" 1946using assms by (blast dest!: mheadsD) 1947 1948lemma declclassD[rule_format]: 1949 "\<lbrakk>wf_prog G;class G C = Some c; methd G C sig = Some m; 1950 class G (declclass m) = Some d\<rbrakk> 1951 \<Longrightarrow> table_of (methods d) sig = Some (mthd m)" 1952proof - 1953 assume wf: "wf_prog G" 1954 then have ws: "ws_prog G" .. 1955 assume clsC: "class G C = Some c" 1956 from clsC ws 1957 show "\<And> m d. \<lbrakk>methd G C sig = Some m; class G (declclass m) = Some d\<rbrakk> 1958 \<Longrightarrow> table_of (methods d) sig = Some (mthd m)" 1959 proof (induct rule: ws_class_induct) 1960 case Object 1961 with wf show "?thesis m d" by auto 1962 next 1963 case (Subcls C c) 1964 let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig" 1965 show "?thesis m d" 1966 proof (cases "?newMethods") 1967 case None 1968 from None ws Subcls 1969 show "?thesis" by (auto simp add: methd_rec) (rule Subcls) 1970 next 1971 case Some 1972 from Some ws Subcls 1973 show "?thesis" 1974 by (auto simp add: methd_rec 1975 dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class) 1976 qed 1977 qed 1978qed 1979 1980lemma dynmethd_Object: 1981 assumes statM: "methd G Object sig = Some statM" and 1982 "private": "accmodi statM = Private" and 1983 is_cls_C: "is_class G C" and 1984 wf: "wf_prog G" 1985 shows "dynmethd G Object C sig = Some statM" 1986proof - 1987 from is_cls_C wf 1988 have subclseq: "G\<turnstile>C \<preceq>\<^sub>C Object" 1989 by (auto intro: subcls_ObjectI) 1990 from wf have ws: "ws_prog G" 1991 by simp 1992 from wf 1993 have is_cls_Obj: "is_class G Object" 1994 by simp 1995 from statM subclseq is_cls_Obj ws "private" 1996 show ?thesis 1997 proof (cases rule: dynmethd_cases) 1998 case Static then show ?thesis . 1999 next 2000 case Overrides 2001 with "private" show ?thesis 2002 by (auto dest: no_Private_override) 2003 qed 2004qed 2005 2006lemma wf_imethds_hiding_objmethdsD: 2007 assumes old: "methd G Object sig = Some old" and 2008 is_if_I: "is_iface G I" and 2009 wf: "wf_prog G" and 2010 not_private: "accmodi old \<noteq> Private" and 2011 new: "new \<in> imethds G I sig" 2012 shows "G\<turnstile>resTy new\<preceq>resTy old \<and> is_static new = is_static old" (is "?P new") 2013proof - 2014 from wf have ws: "ws_prog G" by simp 2015 { 2016 fix I i new 2017 assume ifI: "iface G I = Some i" 2018 assume new: "table_of (imethods i) sig = Some new" 2019 from ifI new not_private wf old 2020 have "?P (I,new)" 2021 by (auto dest!: wf_prog_idecl wf_idecl_hiding cond_hiding_entailsD 2022 simp del: methd_Object) 2023 } note hyp_newmethod = this 2024 from is_if_I ws new 2025 show ?thesis 2026 proof (induct rule: ws_interface_induct) 2027 case (Step I i) 2028 assume ifI: "iface G I = Some i" 2029 assume new: "new \<in> imethds G I sig" 2030 from Step 2031 have hyp: "\<forall> J \<in> set (isuperIfs i). (new \<in> imethds G J sig \<longrightarrow> ?P new)" 2032 by auto 2033 from new ifI ws 2034 show "?P new" 2035 proof (cases rule: imethds_cases) 2036 case NewMethod 2037 with ifI hyp_newmethod 2038 show ?thesis 2039 by auto 2040 next 2041 case (InheritedMethod J) 2042 assume "J \<in> set (isuperIfs i)" 2043 "new \<in> imethds G J sig" 2044 with hyp 2045 show "?thesis" 2046 by auto 2047 qed 2048 qed 2049qed 2050 2051text \<open> 2052Which dynamic classes are valid to look up a member of a distinct static type? 2053We have to distinct class members (named static members in Java) 2054from instance members. Class members are global to all Objects of a class, 2055instance members are local to a single Object instance. If a member is 2056equipped with the static modifier it is a class member, else it is an 2057instance member. 2058The following table gives an overview of the current framework. We assume 2059to have a reference with static type statT and a dynamic class dynC. Between 2060both of these types the widening relation holds 2061\<^term>\<open>G\<turnstile>Class dynC\<preceq> statT\<close>. Unfortunately this ordinary widening relation 2062isn't enough to describe the valid lookup classes, since we must cope the 2063special cases of arrays and interfaces,too. If we statically expect an array or 2064inteface we may lookup a field or a method in Object which isn't covered in 2065the widening relation. 2066 2067statT field instance method static (class) method 2068------------------------------------------------------------------------ 2069 NullT / / / 2070 Iface / dynC Object 2071 Class dynC dynC dynC 2072 Array / Object Object 2073 2074In most cases we con lookup the member in the dynamic class. But as an 2075interface can't declare new static methods, nor an array can define new 2076methods at all, we have to lookup methods in the base class Object. 2077 2078The limitation to classes in the field column is artificial and comes out 2079of the typing rule for the field access (see rule \<open>FVar\<close> in the 2080welltyping relation \<^term>\<open>wt\<close> in theory WellType). 2081I stems out of the fact, that Object 2082indeed has no non private fields. So interfaces and arrays can actually 2083have no fields at all and a field access would be senseless. (In Java 2084interfaces are allowed to declare new fields but in current Bali not!). 2085So there is no principal reason why we should not allow Objects to declare 2086non private fields. Then we would get the following column: 2087 2088 statT field 2089----------------- 2090 NullT / 2091 Iface Object 2092 Class dynC 2093 Array Object 2094\<close> 2095primrec valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool" 2096 ("_,_ \<turnstile> _ valid'_lookup'_cls'_for _" [61,61,61,61] 60) 2097where 2098 "G,NullT \<turnstile> dynC valid_lookup_cls_for static_membr = False" 2099| "G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr 2100 = (if static_membr 2101 then dynC=Object 2102 else G\<turnstile>Class dynC\<preceq> Iface I)" 2103| "G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C" 2104| "G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)" 2105 2106lemma valid_lookup_cls_is_class: 2107 assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and 2108 ty_statT: "isrtype G statT" and 2109 wf: "wf_prog G" 2110 shows "is_class G dynC" 2111proof (cases statT) 2112 case NullT 2113 with dynC ty_statT show ?thesis 2114 by (auto dest: widen_NT2) 2115next 2116 case (IfaceT I) 2117 with dynC wf show ?thesis 2118 by (auto dest: implmt_is_class) 2119next 2120 case (ClassT C) 2121 with dynC ty_statT show ?thesis 2122 by (auto dest: subcls_is_class2) 2123next 2124 case (ArrayT T) 2125 with dynC wf show ?thesis 2126 by (auto) 2127qed 2128 2129declare split_paired_All [simp del] split_paired_Ex [simp del] 2130setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close> 2131setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close> 2132 2133lemma dynamic_mheadsD: 2134"\<lbrakk>emh \<in> mheads G S statT sig; 2135 G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh); 2136 isrtype G statT; wf_prog G 2137 \<rbrakk> \<Longrightarrow> \<exists>m \<in> dynlookup G statT dynC sig: 2138 is_static m=is_static emh \<and> G\<turnstile>resTy m\<preceq>resTy emh" 2139proof - 2140 assume emh: "emh \<in> mheads G S statT sig" 2141 and wf: "wf_prog G" 2142 and dynC_Prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh)" 2143 and istype: "isrtype G statT" 2144 from dynC_Prop istype wf 2145 obtain y where 2146 dynC: "class G dynC = Some y" 2147 by (auto dest: valid_lookup_cls_is_class) 2148 from emh wf show ?thesis 2149 proof (cases rule: mheads_cases) 2150 case Class_methd 2151 fix statC statDeclC sm 2152 assume statC: "statT = ClassT statC" 2153 assume "accmethd G S statC sig = Some sm" 2154 then have sm: "methd G statC sig = Some sm" 2155 by (blast dest: accmethd_SomeD) 2156 assume eq_mheads: "mhead (mthd sm) = mhd emh" 2157 from statC 2158 have dynlookup: "dynlookup G statT dynC sig = dynmethd G statC dynC sig" 2159 by (simp add: dynlookup_def) 2160 from wf statC istype dynC_Prop sm 2161 obtain dm where 2162 "dynmethd G statC dynC sig = Some dm" 2163 "is_static dm = is_static sm" 2164 "G\<turnstile>resTy dm\<preceq>resTy sm" 2165 by (force dest!: ws_dynmethd accmethd_SomeD) 2166 with dynlookup eq_mheads 2167 show ?thesis 2168 by (cases emh type: prod) (auto) 2169 next 2170 case Iface_methd 2171 fix I im 2172 assume statI: "statT = IfaceT I" and 2173 eq_mheads: "mthd im = mhd emh" and 2174 "im \<in> accimethds G (pid S) I sig" 2175 then have im: "im \<in> imethds G I sig" 2176 by (blast dest: accimethdsD) 2177 with istype statI eq_mheads wf 2178 have not_static_emh: "\<not> is_static emh" 2179 by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead) 2180 from statI im 2181 have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig" 2182 by (auto simp add: dynlookup_def dynimethd_def) 2183 from wf dynC_Prop statI istype im not_static_emh 2184 obtain dm where 2185 "methd G dynC sig = Some dm" 2186 "is_static dm = is_static im" 2187 "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" 2188 by (force dest: implmt_methd) 2189 with dynlookup eq_mheads 2190 show ?thesis 2191 by (cases emh type: prod) (auto) 2192 next 2193 case Iface_Object_methd 2194 fix I sm 2195 assume statI: "statT = IfaceT I" and 2196 sm: "accmethd G S Object sig = Some sm" and 2197 eq_mheads: "mhead (mthd sm) = mhd emh" and 2198 nPriv: "accmodi sm \<noteq> Private" 2199 show ?thesis 2200 proof (cases "imethds G I sig = {}") 2201 case True 2202 with statI 2203 have dynlookup: "dynlookup G statT dynC sig = dynmethd G Object dynC sig" 2204 by (simp add: dynlookup_def dynimethd_def) 2205 from wf dynC 2206 have subclsObj: "G\<turnstile>dynC \<preceq>\<^sub>C Object" 2207 by (auto intro: subcls_ObjectI) 2208 from wf dynC dynC_Prop istype sm subclsObj 2209 obtain dm where 2210 "dynmethd G Object dynC sig = Some dm" 2211 "is_static dm = is_static sm" 2212 "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd sm)" 2213 by (auto dest!: ws_dynmethd accmethd_SomeD 2214 intro: class_Object [OF wf] intro: that) 2215 with dynlookup eq_mheads 2216 show ?thesis 2217 by (cases emh type: prod) (auto) 2218 next 2219 case False 2220 with statI 2221 have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig" 2222 by (simp add: dynlookup_def dynimethd_def) 2223 from istype statI 2224 have "is_iface G I" 2225 by auto 2226 with wf sm nPriv False 2227 obtain im where 2228 im: "im \<in> imethds G I sig" and 2229 eq_stat: "is_static im = is_static sm" and 2230 resProp: "G\<turnstile>resTy (mthd im)\<preceq>resTy (mthd sm)" 2231 by (auto dest: wf_imethds_hiding_objmethdsD accmethd_SomeD) 2232 from im wf statI istype eq_stat eq_mheads 2233 have not_static_sm: "\<not> is_static emh" 2234 by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead) 2235 from im wf dynC_Prop dynC istype statI not_static_sm 2236 obtain dm where 2237 "methd G dynC sig = Some dm" 2238 "is_static dm = is_static im" 2239 "G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" 2240 by (auto dest: implmt_methd) 2241 with wf eq_stat resProp dynlookup eq_mheads 2242 show ?thesis 2243 by (cases emh type: prod) (auto intro: widen_trans) 2244 qed 2245 next 2246 case Array_Object_methd 2247 fix T sm 2248 assume statArr: "statT = ArrayT T" and 2249 sm: "accmethd G S Object sig = Some sm" and 2250 eq_mheads: "mhead (mthd sm) = mhd emh" 2251 from statArr dynC_Prop wf 2252 have dynlookup: "dynlookup G statT dynC sig = methd G Object sig" 2253 by (auto simp add: dynlookup_def dynmethd_C_C) 2254 with sm eq_mheads sm 2255 show ?thesis 2256 by (cases emh type: prod) (auto dest: accmethd_SomeD) 2257 qed 2258qed 2259declare split_paired_All [simp] split_paired_Ex [simp] 2260setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close> 2261setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close> 2262 2263(* Tactical version *) 2264(* 2265lemma dynamic_mheadsD: " 2266 \<lbrakk>emh \<in> mheads G S statT sig; wf_prog G; class G dynC = Some y; 2267 if (\<exists>T. statT=ArrayT T) then dynC=Object else G\<turnstile>Class dynC\<preceq>RefT statT; 2268 isrtype G statT\<rbrakk> \<Longrightarrow> 2269 \<exists>m \<in> dynlookup G statT dynC sig: 2270 static (mthd m)=static (mhd emh) \<and> G\<turnstile>resTy (mthd m)\<preceq>resTy (mhd emh)" 2271apply (drule mheadsD) 2272apply safe 2273 -- reftype statT is a class 2274apply (case_tac "\<exists>T. ClassT C = ArrayT T") 2275apply (simp) 2276 2277apply (clarsimp simp add: dynlookup_def ) 2278apply (frule_tac statC="C" and dynC="dynC" and sig="sig" 2279 in ws_dynmethd) 2280apply assumption+ 2281apply (case_tac "emh") 2282apply (force dest: accmethd_SomeD) 2283 2284 -- reftype statT is a interface, method defined in interface 2285apply (clarsimp simp add: dynlookup_def) 2286apply (drule (1) implmt_methd) 2287apply blast 2288apply blast 2289apply (clarify) 2290apply (unfold dynimethd_def) 2291apply (rule_tac x="cm" in bexI) 2292apply (case_tac "emh") 2293apply force 2294 2295apply force 2296 2297 -- reftype statT is a interface, method defined in Object 2298apply (simp add: dynlookup_def) 2299apply (simp only: dynimethd_def) 2300apply (case_tac "imethds G I sig = {}") 2301apply simp 2302apply (frule_tac statC="Object" and dynC="dynC" and sig="sig" 2303 in ws_dynmethd) 2304apply (blast intro: subcls_ObjectI wf_ws_prog) 2305apply (blast dest: class_Object) 2306apply (case_tac "emh") 2307apply (force dest: accmethd_SomeD) 2308 2309apply simp 2310apply (subgoal_tac "\<exists> im. im \<in> imethds G I sig") 2311prefer 2 apply blast 2312apply clarify 2313apply (frule (1) implmt_methd) 2314apply simp 2315apply blast 2316apply (clarify dest!: accmethd_SomeD) 2317apply (frule (4) iface_overrides_Object) 2318apply clarify 2319apply (case_tac emh) 2320apply force 2321 2322 -- reftype statT is a array 2323apply (simp add: dynlookup_def) 2324apply (case_tac emh) 2325apply (force dest: accmethd_SomeD simp add: dynmethd_def) 2326done 2327*) 2328 2329(* FIXME occasionally convert to ws_class_induct*) 2330lemma methd_declclass: 2331"\<lbrakk>class G C = Some c; wf_prog G; methd G C sig = Some m\<rbrakk> 2332 \<Longrightarrow> methd G (declclass m) sig = Some m" 2333proof - 2334 assume asm: "class G C = Some c" "wf_prog G" "methd G C sig = Some m" 2335 have "wf_prog G \<longrightarrow> 2336 (\<forall> c m. class G C = Some c \<longrightarrow> methd G C sig = Some m 2337 \<longrightarrow> methd G (declclass m) sig = Some m)" (is "?P G C") 2338 proof (induct G C rule: class_rec_induct', intro allI impI) 2339 fix G C c m 2340 assume hyp: "\<And>c. class G C = Some c \<Longrightarrow> ws_prog G \<Longrightarrow> C \<noteq> Object \<Longrightarrow> 2341 ?P G (super c)" 2342 assume wf: "wf_prog G" and cls_C: "class G C = Some c" and 2343 m: "methd G C sig = Some m" 2344 show "methd G (declclass m) sig = Some m" 2345 proof (cases "C=Object") 2346 case True 2347 with wf m show ?thesis by (auto intro: table_of_map_SomeI) 2348 next 2349 let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)" 2350 let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))" 2351 case False 2352 with cls_C wf m 2353 have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m " 2354 by (simp add: methd_rec) 2355 show ?thesis 2356 proof (cases "?table sig") 2357 case None 2358 from this methd_C have "?filter (methd G (super c)) sig = Some m" 2359 by simp 2360 moreover 2361 from wf cls_C False obtain sup where "class G (super c) = Some sup" 2362 by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class) 2363 moreover note wf False cls_C 2364 ultimately show ?thesis by (auto intro: hyp [rule_format]) 2365 next 2366 case Some 2367 from this methd_C m show ?thesis by auto 2368 qed 2369 qed 2370 qed 2371 with asm show ?thesis by auto 2372qed 2373 2374lemma dynmethd_declclass: 2375 "\<lbrakk>dynmethd G statC dynC sig = Some m; 2376 wf_prog G; is_class G statC 2377 \<rbrakk> \<Longrightarrow> methd G (declclass m) sig = Some m" 2378by (auto dest: dynmethd_declC) 2379 2380lemma dynlookup_declC: 2381 "\<lbrakk>dynlookup G statT dynC sig = Some m; wf_prog G; 2382 is_class G dynC;isrtype G statT 2383 \<rbrakk> \<Longrightarrow> G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m)" 2384by (cases "statT") 2385 (auto simp add: dynlookup_def dynimethd_def 2386 dest: methd_declC dynmethd_declC) 2387 2388lemma dynlookup_Array_declclassD [simp]: 2389"\<lbrakk>dynlookup G (ArrayT T) Object sig = Some dm;wf_prog G\<rbrakk> 2390 \<Longrightarrow> declclass dm = Object" 2391proof - 2392 assume dynL: "dynlookup G (ArrayT T) Object sig = Some dm" 2393 assume wf: "wf_prog G" 2394 from wf have ws: "ws_prog G" by auto 2395 from wf have is_cls_Obj: "is_class G Object" by auto 2396 from dynL wf 2397 show ?thesis 2398 by (auto simp add: dynlookup_def dynmethd_C_C [OF is_cls_Obj ws] 2399 dest: methd_Object_SomeD) 2400qed 2401 2402 2403declare split_paired_All [simp del] split_paired_Ex [simp del] 2404setup \<open>map_theory_simpset (fn ctxt => ctxt delloop "split_all_tac")\<close> 2405setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close> 2406 2407lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow> wf_prog (prg E) \<longrightarrow> 2408 dt=empty_dt \<longrightarrow> (case T of 2409 Inl T \<Rightarrow> is_type (prg E) T 2410 | Inr Ts \<Rightarrow> Ball (set Ts) (is_type (prg E)))" 2411apply (unfold empty_dt_def) 2412apply (erule wt.induct) 2413apply (auto split del: if_split_asm simp del: snd_conv 2414 simp add: is_acc_class_def is_acc_type_def) 2415apply (erule typeof_empty_is_type) 2416apply (frule (1) wf_prog_cdecl [THEN wf_cdecl_supD], 2417 force simp del: snd_conv, clarsimp simp add: is_acc_class_def) 2418apply (drule (1) max_spec2mheads [THEN conjunct1, THEN mheadsD]) 2419apply (drule_tac [2] accfield_fields) 2420apply (frule class_Object) 2421apply (auto dest: accmethd_rT_is_type 2422 imethds_wf_mhead [THEN conjunct1, THEN rT_is_acc_type] 2423 dest!:accimethdsD 2424 simp del: class_Object 2425 simp add: is_acc_type_def 2426 ) 2427done 2428declare split_paired_All [simp] split_paired_Ex [simp] 2429setup \<open>map_theory_claset (fn ctxt => ctxt addSbefore ("split_all_tac", split_all_tac))\<close> 2430setup \<open>map_theory_simpset (fn ctxt => ctxt addloop ("split_all_tac", split_all_tac))\<close> 2431 2432lemma ty_expr_is_type: 2433"\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T" 2434by (auto dest!: wt_is_type) 2435lemma ty_var_is_type: 2436"\<lbrakk>E\<turnstile>v\<Colon>=T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T" 2437by (auto dest!: wt_is_type) 2438lemma ty_exprs_is_type: 2439"\<lbrakk>E\<turnstile>es\<Colon>\<doteq>Ts; wf_prog (prg E)\<rbrakk> \<Longrightarrow> Ball (set Ts) (is_type (prg E))" 2440by (auto dest!: wt_is_type) 2441 2442 2443lemma static_mheadsD: 2444 "\<lbrakk> emh \<in> mheads G S t sig; wf_prog G; E\<turnstile>e\<Colon>-RefT t; prg E=G ; 2445 invmode (mhd emh) e \<noteq> IntVir 2446 \<rbrakk> \<Longrightarrow> \<exists>m. ( (\<exists> C. t = ClassT C \<and> accmethd G S C sig = Some m) 2447 \<or> (\<forall> C. t \<noteq> ClassT C \<and> accmethd G S Object sig = Some m )) \<and> 2448 declrefT emh = ClassT (declclass m) \<and> mhead (mthd m) = (mhd emh)" 2449apply (subgoal_tac "is_static emh \<or> e = Super") 2450defer apply (force simp add: invmode_def) 2451apply (frule ty_expr_is_type) 2452apply simp 2453apply (case_tac "is_static emh") 2454apply (frule (1) mheadsD) 2455apply clarsimp 2456apply safe 2457apply blast 2458apply (auto dest!: imethds_wf_mhead 2459 accmethd_SomeD 2460 accimethdsD 2461 simp add: accObjectmheads_def Objectmheads_def) 2462 2463apply (erule wt_elim_cases) 2464apply (force simp add: cmheads_def) 2465done 2466 2467lemma wt_MethdI: 2468"\<lbrakk>methd G C sig = Some m; wf_prog G; 2469 class G C = Some c\<rbrakk> \<Longrightarrow> 2470 \<exists>T. \<lparr>prg=G,cls=(declclass m), 2471 lcl=callee_lcl (declclass m) sig (mthd m)\<rparr>\<turnstile> Methd C sig\<Colon>-T \<and> G\<turnstile>T\<preceq>resTy m" 2472apply (frule (2) methd_wf_mdecl, clarify) 2473apply (force dest!: wf_mdecl_bodyD intro!: wt.Methd) 2474done 2475 2476subsection "accessibility concerns" 2477 2478lemma mheads_type_accessible: 2479 "\<lbrakk>emh \<in> mheads G S T sig; wf_prog G\<rbrakk> 2480 \<Longrightarrow> G\<turnstile>RefT T accessible_in (pid S)" 2481by (erule mheads_cases) 2482 (auto dest: accmethd_SomeD accessible_from_commonD accimethdsD) 2483 2484lemma static_to_dynamic_accessible_from_aux: 2485"\<lbrakk>G\<turnstile>m of C accessible_from accC;wf_prog G\<rbrakk> 2486 \<Longrightarrow> G\<turnstile>m in C dyn_accessible_from accC" 2487proof (induct rule: accessible_fromR.induct) 2488qed (auto intro: dyn_accessible_fromR.intros 2489 member_of_to_member_in 2490 static_to_dynamic_overriding) 2491 2492lemma static_to_dynamic_accessible_from: 2493 assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and 2494 subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and 2495 wf: "wf_prog G" 2496 shows "G\<turnstile>m in dynC dyn_accessible_from accC" 2497proof - 2498 from stat_acc subclseq 2499 show ?thesis (is "?Dyn_accessible m") 2500 proof (induct rule: accessible_fromR.induct) 2501 case (Immediate m statC) 2502 then show "?Dyn_accessible m" 2503 by (blast intro: dyn_accessible_fromR.Immediate 2504 member_inI 2505 permits_acc_inheritance) 2506 next 2507 case (Overriding m _ _) 2508 with wf show "?Dyn_accessible m" 2509 by (blast intro: dyn_accessible_fromR.Overriding 2510 member_inI 2511 static_to_dynamic_overriding 2512 rtrancl_trancl_trancl 2513 static_to_dynamic_accessible_from_aux) 2514 qed 2515qed 2516 2517lemma static_to_dynamic_accessible_from_static: 2518 assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and 2519 static: "is_static m" and 2520 wf: "wf_prog G" 2521 shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC" 2522proof - 2523 from stat_acc wf 2524 have "G\<turnstile>m in statC dyn_accessible_from accC" 2525 by (auto intro: static_to_dynamic_accessible_from) 2526 from this static 2527 show ?thesis 2528 by (rule dyn_accessible_from_static_declC) 2529qed 2530 2531lemma dynmethd_member_in: 2532 assumes m: "dynmethd G statC dynC sig = Some m" and 2533 iscls_statC: "is_class G statC" and 2534 wf: "wf_prog G" 2535 shows "G\<turnstile>Methd sig m member_in dynC" 2536proof - 2537 from m 2538 have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" 2539 by (auto simp add: dynmethd_def) 2540 from subclseq iscls_statC 2541 have iscls_dynC: "is_class G dynC" 2542 by (rule subcls_is_class2) 2543 from iscls_dynC iscls_statC wf m 2544 have "G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m) \<and> 2545 methd G (declclass m) sig = Some m" 2546 by - (drule dynmethd_declC, auto) 2547 with wf 2548 show ?thesis 2549 by (auto intro: member_inI dest: methd_member_of) 2550qed 2551 2552lemma dynmethd_access_prop: 2553 assumes statM: "methd G statC sig = Some statM" and 2554 stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" and 2555 dynM: "dynmethd G statC dynC sig = Some dynM" and 2556 wf: "wf_prog G" 2557 shows "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC" 2558proof - 2559 from wf have ws: "ws_prog G" .. 2560 from dynM 2561 have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" 2562 by (auto simp add: dynmethd_def) 2563 from stat_acc 2564 have is_cls_statC: "is_class G statC" 2565 by (auto dest: accessible_from_commonD member_of_is_classD) 2566 with subclseq 2567 have is_cls_dynC: "is_class G dynC" 2568 by (rule subcls_is_class2) 2569 from is_cls_statC statM wf 2570 have member_statC: "G\<turnstile>Methd sig statM member_of statC" 2571 by (auto intro: methd_member_of) 2572 from stat_acc 2573 have statC_acc: "G\<turnstile>Class statC accessible_in (pid accC)" 2574 by (auto dest: accessible_from_commonD) 2575 from statM subclseq is_cls_statC ws 2576 show ?thesis 2577 proof (cases rule: dynmethd_cases) 2578 case Static 2579 assume dynmethd: "dynmethd G statC dynC sig = Some statM" 2580 with dynM have eq_dynM_statM: "dynM=statM" 2581 by simp 2582 with stat_acc subclseq wf 2583 show ?thesis 2584 by (auto intro: static_to_dynamic_accessible_from) 2585 next 2586 case (Overrides newM) 2587 assume dynmethd: "dynmethd G statC dynC sig = Some newM" 2588 assume override: "G,sig\<turnstile>newM overrides statM" 2589 assume neq: "newM\<noteq>statM" 2590 from dynmethd dynM 2591 have eq_dynM_newM: "dynM=newM" 2592 by simp 2593 from dynmethd eq_dynM_newM wf is_cls_statC 2594 have "G\<turnstile>Methd sig dynM member_in dynC" 2595 by (auto intro: dynmethd_member_in) 2596 moreover 2597 from subclseq 2598 have "G\<turnstile>dynC\<prec>\<^sub>C statC" 2599 proof (cases rule: subclseq_cases) 2600 case Eq 2601 assume "dynC=statC" 2602 moreover 2603 from is_cls_statC obtain c 2604 where "class G statC = Some c" 2605 by auto 2606 moreover 2607 note statM ws dynmethd 2608 ultimately 2609 have "newM=statM" 2610 by (auto simp add: dynmethd_C_C) 2611 with neq show ?thesis 2612 by (contradiction) 2613 next 2614 case Subcls then show ?thesis . 2615 qed 2616 moreover 2617 from stat_acc wf 2618 have "G\<turnstile>Methd sig statM in statC dyn_accessible_from accC" 2619 by (blast intro: static_to_dynamic_accessible_from) 2620 moreover 2621 note override eq_dynM_newM 2622 ultimately show ?thesis 2623 by (cases dynM,cases statM) (auto intro: dyn_accessible_fromR.Overriding) 2624 qed 2625qed 2626 2627lemma implmt_methd_access: 2628 fixes accC::qtname 2629 assumes iface_methd: "imethds G I sig \<noteq> {}" and 2630 implements: "G\<turnstile>dynC\<leadsto>I" and 2631 isif_I: "is_iface G I" and 2632 wf: "wf_prog G" 2633 shows "\<exists> dynM. methd G dynC sig = Some dynM \<and> 2634 G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC" 2635proof - 2636 from implements 2637 have iscls_dynC: "is_class G dynC" by (rule implmt_is_class) 2638 from iface_methd 2639 obtain im 2640 where "im \<in> imethds G I sig" 2641 by auto 2642 with wf implements isif_I 2643 obtain dynM 2644 where dynM: "methd G dynC sig = Some dynM" and 2645 pub: "accmodi dynM = Public" 2646 by (blast dest: implmt_methd) 2647 with iscls_dynC wf 2648 have "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC" 2649 by (auto intro!: dyn_accessible_fromR.Immediate 2650 intro: methd_member_of member_of_to_member_in 2651 simp add: permits_acc_def) 2652 with dynM 2653 show ?thesis 2654 by blast 2655qed 2656 2657corollary implmt_dynimethd_access: 2658 fixes accC::qtname 2659 assumes iface_methd: "imethds G I sig \<noteq> {}" and 2660 implements: "G\<turnstile>dynC\<leadsto>I" and 2661 isif_I: "is_iface G I" and 2662 wf: "wf_prog G" 2663 shows "\<exists> dynM. dynimethd G I dynC sig = Some dynM \<and> 2664 G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC" 2665proof - 2666 from iface_methd 2667 have "dynimethd G I dynC sig = methd G dynC sig" 2668 by (simp add: dynimethd_def) 2669 with iface_methd implements isif_I wf 2670 show ?thesis 2671 by (simp only:) 2672 (blast intro: implmt_methd_access) 2673qed 2674 2675lemma dynlookup_access_prop: 2676 assumes emh: "emh \<in> mheads G accC statT sig" and 2677 dynM: "dynlookup G statT dynC sig = Some dynM" and 2678 dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for is_static emh" and 2679 isT_statT: "isrtype G statT" and 2680 wf: "wf_prog G" 2681 shows "G \<turnstile>Methd sig dynM in dynC dyn_accessible_from accC" 2682proof - 2683 from emh wf 2684 have statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)" 2685 by (rule mheads_type_accessible) 2686 from dynC_prop isT_statT wf 2687 have iscls_dynC: "is_class G dynC" 2688 by (rule valid_lookup_cls_is_class) 2689 from emh dynC_prop isT_statT wf dynM 2690 have eq_static: "is_static emh = is_static dynM" 2691 by (auto dest: dynamic_mheadsD) 2692 from emh wf show ?thesis 2693 proof (cases rule: mheads_cases) 2694 case (Class_methd statC _ statM) 2695 assume statT: "statT = ClassT statC" 2696 assume "accmethd G accC statC sig = Some statM" 2697 then have statM: "methd G statC sig = Some statM" and 2698 stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" 2699 by (auto dest: accmethd_SomeD) 2700 from dynM statT 2701 have dynM': "dynmethd G statC dynC sig = Some dynM" 2702 by (simp add: dynlookup_def) 2703 from statM stat_acc wf dynM' 2704 show ?thesis 2705 by (auto dest!: dynmethd_access_prop) 2706 next 2707 case (Iface_methd I im) 2708 then have iface_methd: "imethds G I sig \<noteq> {}" and 2709 statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)" 2710 by (auto dest: accimethdsD) 2711 assume statT: "statT = IfaceT I" 2712 assume im: "im \<in> accimethds G (pid accC) I sig" 2713 assume eq_mhds: "mthd im = mhd emh" 2714 from dynM statT 2715 have dynM': "dynimethd G I dynC sig = Some dynM" 2716 by (simp add: dynlookup_def) 2717 from isT_statT statT 2718 have isif_I: "is_iface G I" 2719 by simp 2720 show ?thesis 2721 proof (cases "is_static emh") 2722 case False 2723 with statT dynC_prop 2724 have widen_dynC: "G\<turnstile>Class dynC \<preceq> RefT statT" 2725 by simp 2726 from statT widen_dynC 2727 have implmnt: "G\<turnstile>dynC\<leadsto>I" 2728 by auto 2729 from eq_static False 2730 have not_static_dynM: "\<not> is_static dynM" 2731 by simp 2732 from iface_methd implmnt isif_I wf dynM' 2733 show ?thesis 2734 by - (drule implmt_dynimethd_access, auto) 2735 next 2736 case True 2737 assume "is_static emh" 2738 moreover 2739 from wf isT_statT statT im 2740 have "\<not> is_static im" 2741 by (auto dest: accimethdsD wf_prog_idecl imethds_wf_mhead) 2742 moreover note eq_mhds 2743 ultimately show ?thesis 2744 by (cases emh) auto 2745 qed 2746 next 2747 case (Iface_Object_methd I statM) 2748 assume statT: "statT = IfaceT I" 2749 assume "accmethd G accC Object sig = Some statM" 2750 then have statM: "methd G Object sig = Some statM" and 2751 stat_acc: "G\<turnstile>Methd sig statM of Object accessible_from accC" 2752 by (auto dest: accmethd_SomeD) 2753 assume not_Private_statM: "accmodi statM \<noteq> Private" 2754 assume eq_mhds: "mhead (mthd statM) = mhd emh" 2755 from iscls_dynC wf 2756 have widen_dynC_Obj: "G\<turnstile>dynC \<preceq>\<^sub>C Object" 2757 by (auto intro: subcls_ObjectI) 2758 show ?thesis 2759 proof (cases "imethds G I sig = {}") 2760 case True 2761 from dynM statT True 2762 have dynM': "dynmethd G Object dynC sig = Some dynM" 2763 by (simp add: dynlookup_def dynimethd_def) 2764 from statT 2765 have "G\<turnstile>RefT statT \<preceq>Class Object" 2766 by auto 2767 with statM statT_acc stat_acc widen_dynC_Obj statT isT_statT 2768 wf dynM' eq_static dynC_prop 2769 show ?thesis 2770 by - (drule dynmethd_access_prop,force+) 2771 next 2772 case False 2773 then obtain im where 2774 im: "im \<in> imethds G I sig" 2775 by auto 2776 have not_static_emh: "\<not> is_static emh" 2777 proof - 2778 from im statM statT isT_statT wf not_Private_statM 2779 have "is_static im = is_static statM" 2780 by (fastforce dest: wf_imethds_hiding_objmethdsD) 2781 with wf isT_statT statT im 2782 have "\<not> is_static statM" 2783 by (auto dest: wf_prog_idecl imethds_wf_mhead) 2784 with eq_mhds 2785 show ?thesis 2786 by (cases emh) auto 2787 qed 2788 with statT dynC_prop 2789 have implmnt: "G\<turnstile>dynC\<leadsto>I" 2790 by simp 2791 with isT_statT statT 2792 have isif_I: "is_iface G I" 2793 by simp 2794 from dynM statT 2795 have dynM': "dynimethd G I dynC sig = Some dynM" 2796 by (simp add: dynlookup_def) 2797 from False implmnt isif_I wf dynM' 2798 show ?thesis 2799 by - (drule implmt_dynimethd_access, auto) 2800 qed 2801 next 2802 case (Array_Object_methd T statM) 2803 assume statT: "statT = ArrayT T" 2804 assume "accmethd G accC Object sig = Some statM" 2805 then have statM: "methd G Object sig = Some statM" and 2806 stat_acc: "G\<turnstile>Methd sig statM of Object accessible_from accC" 2807 by (auto dest: accmethd_SomeD) 2808 from statT dynC_prop 2809 have dynC_Obj: "dynC = Object" 2810 by simp 2811 then 2812 have widen_dynC_Obj: "G\<turnstile>Class dynC \<preceq> Class Object" 2813 by simp 2814 from dynM statT 2815 have dynM': "dynmethd G Object dynC sig = Some dynM" 2816 by (simp add: dynlookup_def) 2817 from statM statT_acc stat_acc dynM' wf widen_dynC_Obj 2818 statT isT_statT 2819 show ?thesis 2820 by - (drule dynmethd_access_prop, simp+) 2821 qed 2822qed 2823 2824lemma dynlookup_access: 2825 assumes emh: "emh \<in> mheads G accC statT sig" and 2826 dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh) " and 2827 isT_statT: "isrtype G statT" and 2828 wf: "wf_prog G" 2829 shows "\<exists> dynM. dynlookup G statT dynC sig = Some dynM \<and> 2830 G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC" 2831proof - 2832 from dynC_prop isT_statT wf 2833 have is_cls_dynC: "is_class G dynC" 2834 by (auto dest: valid_lookup_cls_is_class) 2835 with emh wf dynC_prop isT_statT 2836 obtain dynM where 2837 "dynlookup G statT dynC sig = Some dynM" 2838 by - (drule dynamic_mheadsD,auto) 2839 with emh dynC_prop isT_statT wf 2840 show ?thesis 2841 by (blast intro: dynlookup_access_prop) 2842qed 2843 2844lemma stat_overrides_Package_old: 2845 assumes stat_override: "G \<turnstile> new overrides\<^sub>S old" and 2846 accmodi_new: "accmodi new = Package" and 2847 wf: "wf_prog G " 2848 shows "accmodi old = Package" 2849proof - 2850 from stat_override wf 2851 have "accmodi old \<le> accmodi new" 2852 by (auto dest: wf_prog_stat_overridesD) 2853 with stat_override accmodi_new show ?thesis 2854 by (cases "accmodi old") (auto dest: no_Private_stat_override 2855 dest: acc_modi_le_Dests) 2856qed 2857 2858subsubsection \<open>Properties of dynamic accessibility\<close> 2859 2860lemma dyn_accessible_Private: 2861 assumes dyn_acc: "G \<turnstile> m in C dyn_accessible_from accC" and 2862 priv: "accmodi m = Private" 2863 shows "accC = declclass m" 2864proof - 2865 from dyn_acc priv 2866 show ?thesis 2867 proof (induct) 2868 case (Immediate m C) 2869 from \<open>G \<turnstile> m in C permits_acc_from accC\<close> and \<open>accmodi m = Private\<close> 2870 show ?case 2871 by (simp add: permits_acc_def) 2872 next 2873 case Overriding 2874 then show ?case 2875 by (auto dest!: overrides_commonD) 2876 qed 2877qed 2878 2879text \<open>\<open>dyn_accessible_Package\<close> only works with the \<open>wf_prog\<close> assumption. 2880Without it. it is easy to leaf the Package! 2881\<close> 2882lemma dyn_accessible_Package: 2883 "\<lbrakk>G \<turnstile> m in C dyn_accessible_from accC; accmodi m = Package; 2884 wf_prog G\<rbrakk> 2885 \<Longrightarrow> pid accC = pid (declclass m)" 2886proof - 2887 assume wf: "wf_prog G " 2888 assume accessible: "G \<turnstile> m in C dyn_accessible_from accC" 2889 then show "accmodi m = Package 2890 \<Longrightarrow> pid accC = pid (declclass m)" 2891 (is "?Pack m \<Longrightarrow> ?P m") 2892 proof (induct rule: dyn_accessible_fromR.induct) 2893 case (Immediate m C) 2894 assume "G\<turnstile>m member_in C" 2895 "G \<turnstile> m in C permits_acc_from accC" 2896 "accmodi m = Package" 2897 then show "?P m" 2898 by (auto simp add: permits_acc_def) 2899 next 2900 case (Overriding new declC newm old Sup C) 2901 assume member_new: "G \<turnstile> new member_in C" and 2902 new: "new = (declC, mdecl newm)" and 2903 override: "G \<turnstile> (declC, newm) overrides old" and 2904 subcls_C_Sup: "G\<turnstile>C \<prec>\<^sub>C Sup" and 2905 acc_old: "G \<turnstile> methdMembr old in Sup dyn_accessible_from accC" and 2906 hyp: "?Pack (methdMembr old) \<Longrightarrow> ?P (methdMembr old)" and 2907 accmodi_new: "accmodi new = Package" 2908 from override accmodi_new new wf 2909 have accmodi_old: "accmodi old = Package" 2910 by (auto dest: overrides_Package_old) 2911 with hyp 2912 have P_sup: "?P (methdMembr old)" 2913 by (simp) 2914 from wf override new accmodi_old accmodi_new 2915 have eq_pid_new_old: "pid (declclass new) = pid (declclass old)" 2916 by (auto dest: dyn_override_Package) 2917 with eq_pid_new_old P_sup show "?P new" 2918 by auto 2919 qed 2920qed 2921 2922text \<open>For fields we don't need the wellformedness of the program, since 2923there is no overriding\<close> 2924lemma dyn_accessible_field_Package: 2925 assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and 2926 pack: "accmodi f = Package" and 2927 field: "is_field f" 2928 shows "pid accC = pid (declclass f)" 2929proof - 2930 from dyn_acc pack field 2931 show ?thesis 2932 proof (induct) 2933 case (Immediate f C) 2934 from \<open>G \<turnstile> f in C permits_acc_from accC\<close> and \<open>accmodi f = Package\<close> 2935 show ?case 2936 by (simp add: permits_acc_def) 2937 next 2938 case Overriding 2939 then show ?case by (simp add: is_field_def) 2940 qed 2941qed 2942 2943text \<open>\<open>dyn_accessible_instance_field_Protected\<close> only works for fields 2944since methods can break the package bounds due to overriding 2945\<close> 2946lemma dyn_accessible_instance_field_Protected: 2947 assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and 2948 prot: "accmodi f = Protected" and 2949 field: "is_field f" and 2950 instance_field: "\<not> is_static f" and 2951 outside: "pid (declclass f) \<noteq> pid accC" 2952 shows "G\<turnstile> C \<preceq>\<^sub>C accC" 2953proof - 2954 from dyn_acc prot field instance_field outside 2955 show ?thesis 2956 proof (induct) 2957 case (Immediate f C) 2958 note \<open>G \<turnstile> f in C permits_acc_from accC\<close> 2959 moreover 2960 assume "accmodi f = Protected" and "is_field f" and "\<not> is_static f" and 2961 "pid (declclass f) \<noteq> pid accC" 2962 ultimately 2963 show "G\<turnstile> C \<preceq>\<^sub>C accC" 2964 by (auto simp add: permits_acc_def) 2965 next 2966 case Overriding 2967 then show ?case by (simp add: is_field_def) 2968 qed 2969qed 2970 2971lemma dyn_accessible_static_field_Protected: 2972 assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and 2973 prot: "accmodi f = Protected" and 2974 field: "is_field f" and 2975 static_field: "is_static f" and 2976 outside: "pid (declclass f) \<noteq> pid accC" 2977 shows "G\<turnstile> accC \<preceq>\<^sub>C declclass f \<and> G\<turnstile>C \<preceq>\<^sub>C declclass f" 2978proof - 2979 from dyn_acc prot field static_field outside 2980 show ?thesis 2981 proof (induct) 2982 case (Immediate f C) 2983 assume "accmodi f = Protected" and "is_field f" and "is_static f" and 2984 "pid (declclass f) \<noteq> pid accC" 2985 moreover 2986 note \<open>G \<turnstile> f in C permits_acc_from accC\<close> 2987 ultimately 2988 have "G\<turnstile> accC \<preceq>\<^sub>C declclass f" 2989 by (auto simp add: permits_acc_def) 2990 moreover 2991 from \<open>G \<turnstile> f member_in C\<close> 2992 have "G\<turnstile>C \<preceq>\<^sub>C declclass f" 2993 by (rule member_in_class_relation) 2994 ultimately show ?case 2995 by blast 2996 next 2997 case Overriding 2998 then show ?case by (simp add: is_field_def) 2999 qed 3000qed 3001 3002end 3003