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