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