author | schirmer |
Wed, 27 Feb 2002 08:52:09 +0100 | |
changeset 12962 | a24ffe84a06a |
parent 12937 | 0c4fd7529467 |
child 12963 | 73fb6a200e36 |
permissions | -rw-r--r-- |
12857 | 1 |
(* Title: HOL/Bali/WellForm.thy |
12854 | 2 |
ID: $Id$ |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
3 |
Author: David von Oheimb and Norbert Schirmer |
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" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
34 |
text {* well-formed field declaration (common part for classes and interfaces), |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
35 |
cf. 8.3 and (9.3) *} |
12854 | 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)) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
101 |
| This \<Rightarrow> if is_static m then None else Some (Class C)) |
12854 | 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)) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
125 |
| This \<Rightarrow> if is_static m then None else Some (Class C)) |
12854 | 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)) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
152 |
| This \<Rightarrow> if is_static m then None else Some (Class C)) |
12854 | 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: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
721 |
assumes hides: "G \<turnstile>new hides old" and wf: "wf_prog G" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
722 |
shows |
12854 | 723 |
"accmodi old \<le> accmodi new \<and> |
724 |
is_static old" |
|
725 |
proof - |
|
726 |
from hides |
|
727 |
obtain c where |
|
728 |
clsNew: "class G (declclass new) = Some c" and |
|
729 |
neqObj: "declclass new \<noteq> Object" |
|
730 |
by (auto dest: hidesD declared_in_classD) |
|
731 |
with hides obtain newM oldM where |
|
732 |
newM: "table_of (methods c) (msig new) = Some newM" and |
|
733 |
new: "new = (declclass new,(msig new),newM)" and |
|
734 |
old: "old = (declclass old,(msig old),oldM)" and |
|
735 |
"msig new = msig old" |
|
736 |
by (cases new,cases old) |
|
737 |
(auto dest: hidesD |
|
738 |
simp add: cdeclaredmethd_def declared_in_def) |
|
739 |
with hides |
|
740 |
have hides': |
|
741 |
"G,(msig new)\<turnstile>(declclass new,newM) hides (declclass old,oldM)" |
|
742 |
by auto |
|
743 |
from clsNew wf |
|
744 |
have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl) |
|
745 |
note wf_cdecl_hides_SomeD [OF this neqObj newM hides'] |
|
746 |
with new old |
|
747 |
show ?thesis |
|
748 |
by (cases new, cases old) auto |
|
749 |
qed |
|
750 |
||
751 |
text {* Compare this lemma about static |
|
752 |
overriding @{term "G \<turnstile>new overrides\<^sub>S old"} with the definition of |
|
753 |
dynamic overriding @{term "G \<turnstile>new overrides old"}. |
|
754 |
Conforming result types and restrictions on the access modifiers of the old |
|
755 |
and the new method are not part of the predicate for static overriding. But |
|
756 |
they are enshured in a wellfromed program. Dynamic overriding has |
|
757 |
no restrictions on the access modifiers but enforces confrom result types |
|
758 |
as precondition. But with some efford we can guarantee the access modifier |
|
759 |
restriction for dynamic overriding, too. See lemma |
|
760 |
@{text wf_prog_dyn_override_prop}. |
|
761 |
*} |
|
762 |
lemma wf_prog_stat_overridesD: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
763 |
assumes stat_override: "G \<turnstile>new overrides\<^sub>S old" and wf: "wf_prog G" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
764 |
shows |
12854 | 765 |
"G\<turnstile>resTy new\<preceq>resTy old \<and> |
766 |
accmodi old \<le> accmodi new \<and> |
|
767 |
\<not> is_static old" |
|
768 |
proof - |
|
769 |
from stat_override |
|
770 |
obtain c where |
|
771 |
clsNew: "class G (declclass new) = Some c" and |
|
772 |
neqObj: "declclass new \<noteq> Object" |
|
773 |
by (auto dest: stat_overrides_commonD declared_in_classD) |
|
774 |
with stat_override obtain newM oldM where |
|
775 |
newM: "table_of (methods c) (msig new) = Some newM" and |
|
776 |
new: "new = (declclass new,(msig new),newM)" and |
|
777 |
old: "old = (declclass old,(msig old),oldM)" and |
|
778 |
"msig new = msig old" |
|
779 |
by (cases new,cases old) |
|
780 |
(auto dest: stat_overrides_commonD |
|
781 |
simp add: cdeclaredmethd_def declared_in_def) |
|
782 |
with stat_override |
|
783 |
have stat_override': |
|
784 |
"G,(msig new)\<turnstile>(declclass new,newM) overrides\<^sub>S (declclass old,oldM)" |
|
785 |
by auto |
|
786 |
from clsNew wf |
|
787 |
have "wf_cdecl G (declclass new,c)" by (blast intro: wf_prog_cdecl) |
|
788 |
note wf_cdecl_overrides_SomeD [OF this neqObj newM stat_override'] |
|
789 |
with new old |
|
790 |
show ?thesis |
|
791 |
by (cases new, cases old) auto |
|
792 |
qed |
|
793 |
||
794 |
lemma static_to_dynamic_overriding: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
795 |
assumes stat_override: "G\<turnstile>new overrides\<^sub>S old" and wf : "wf_prog G" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
796 |
shows "G\<turnstile>new overrides old" |
12854 | 797 |
proof - |
798 |
from stat_override |
|
799 |
show ?thesis (is "?Overrides new old") |
|
800 |
proof (induct) |
|
801 |
case (Direct new old superNew) |
|
802 |
then have stat_override:"G\<turnstile>new overrides\<^sub>S old" |
|
803 |
by (rule stat_overridesR.Direct) |
|
804 |
from stat_override wf |
|
805 |
have resTy_widen: "G\<turnstile>resTy new\<preceq>resTy old" and |
|
806 |
not_static_old: "\<not> is_static old" |
|
807 |
by (auto dest: wf_prog_stat_overridesD) |
|
808 |
have not_private_new: "accmodi new \<noteq> Private" |
|
809 |
proof - |
|
810 |
from stat_override |
|
811 |
have "accmodi old \<noteq> Private" |
|
812 |
by (rule no_Private_stat_override) |
|
813 |
moreover |
|
814 |
from stat_override wf |
|
815 |
have "accmodi old \<le> accmodi new" |
|
816 |
by (auto dest: wf_prog_stat_overridesD) |
|
817 |
ultimately |
|
818 |
show ?thesis |
|
819 |
by (auto dest: acc_modi_bottom) |
|
820 |
qed |
|
821 |
with Direct resTy_widen not_static_old |
|
822 |
show "?Overrides new old" |
|
12962
a24ffe84a06a
Cleaning up the definition of static overriding.
schirmer
parents:
12937
diff
changeset
|
823 |
by (auto intro: overridesR.Direct stat_override_declclasses_relation) |
12854 | 824 |
next |
825 |
case (Indirect inter new old) |
|
826 |
then show "?Overrides new old" |
|
827 |
by (blast intro: overridesR.Indirect) |
|
828 |
qed |
|
829 |
qed |
|
830 |
||
831 |
lemma non_Package_instance_method_inheritance: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
832 |
assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
833 |
accmodi_old: "accmodi old \<noteq> Package" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
834 |
instance_method: "\<not> is_static old" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
835 |
subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
836 |
old_declared: "G\<turnstile>Method old declared_in (declclass old)" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
837 |
wf: "wf_prog G" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
838 |
shows "G\<turnstile>Method old member_of C \<or> |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
839 |
(\<exists> new. G\<turnstile> new overrides\<^sub>S old \<and> G\<turnstile>Method new member_of C)" |
12854 | 840 |
proof - |
841 |
from wf have ws: "ws_prog G" by auto |
|
842 |
from old_declared have iscls_declC_old: "is_class G (declclass old)" |
|
843 |
by (auto simp add: declared_in_def cdeclaredmethd_def) |
|
844 |
from subcls have iscls_C: "is_class G C" |
|
845 |
by (blast dest: subcls_is_class) |
|
846 |
from iscls_C ws old_inheritable subcls |
|
847 |
show ?thesis (is "?P C old") |
|
848 |
proof (induct rule: ws_class_induct') |
|
849 |
case Object |
|
850 |
assume "G\<turnstile>Object\<prec>\<^sub>C declclass old" |
|
851 |
then show "?P Object old" |
|
852 |
by blast |
|
853 |
next |
|
854 |
case (Subcls C c) |
|
855 |
assume cls_C: "class G C = Some c" and |
|
856 |
neq_C_Obj: "C \<noteq> Object" and |
|
857 |
hyp: "\<lbrakk>G \<turnstile>Method old inheritable_in pid (super c); |
|
858 |
G\<turnstile>super c\<prec>\<^sub>C declclass old\<rbrakk> \<Longrightarrow> ?P (super c) old" and |
|
859 |
inheritable: "G \<turnstile>Method old inheritable_in pid C" and |
|
860 |
subclsC: "G\<turnstile>C\<prec>\<^sub>C declclass old" |
|
861 |
from cls_C neq_C_Obj |
|
862 |
have super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" |
|
863 |
by (rule subcls1I) |
|
864 |
from wf cls_C neq_C_Obj |
|
865 |
have accessible_super: "G\<turnstile>(Class (super c)) accessible_in (pid C)" |
|
866 |
by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD) |
|
867 |
{ |
|
868 |
fix old |
|
869 |
assume member_super: "G\<turnstile>Method old member_of (super c)" |
|
870 |
assume inheritable: "G \<turnstile>Method old inheritable_in pid C" |
|
871 |
assume instance_method: "\<not> is_static old" |
|
872 |
from member_super |
|
873 |
have old_declared: "G\<turnstile>Method old declared_in (declclass old)" |
|
874 |
by (cases old) (auto dest: member_of_declC) |
|
875 |
have "?P C old" |
|
876 |
proof (cases "G\<turnstile>mid (msig old) undeclared_in C") |
|
877 |
case True |
|
878 |
with inheritable super accessible_super member_super |
|
879 |
have "G\<turnstile>Method old member_of C" |
|
880 |
by (cases old) (auto intro: members.Inherited) |
|
881 |
then show ?thesis |
|
882 |
by auto |
|
883 |
next |
|
884 |
case False |
|
885 |
then obtain new_member where |
|
886 |
"G\<turnstile>new_member declared_in C" and |
|
887 |
"mid (msig old) = memberid new_member" |
|
888 |
by (auto dest: not_undeclared_declared) |
|
889 |
then obtain new where |
|
890 |
new: "G\<turnstile>Method new declared_in C" and |
|
891 |
eq_sig: "msig old = msig new" and |
|
892 |
declC_new: "declclass new = C" |
|
893 |
by (cases new_member) auto |
|
894 |
then have member_new: "G\<turnstile>Method new member_of C" |
|
895 |
by (cases new) (auto intro: members.Immediate) |
|
896 |
from declC_new super member_super |
|
897 |
have subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" |
|
898 |
by (auto dest!: member_of_subclseq_declC |
|
899 |
dest: r_into_trancl intro: trancl_rtrancl_trancl) |
|
900 |
show ?thesis |
|
901 |
proof (cases "is_static new") |
|
902 |
case False |
|
903 |
with eq_sig declC_new new old_declared inheritable |
|
904 |
super member_super subcls_new_old |
|
905 |
have "G\<turnstile>new overrides\<^sub>S old" |
|
906 |
by (auto intro!: stat_overridesR.Direct) |
|
907 |
with member_new show ?thesis |
|
908 |
by blast |
|
909 |
next |
|
910 |
case True |
|
911 |
with eq_sig declC_new subcls_new_old new old_declared inheritable |
|
912 |
have "G\<turnstile>new hides old" |
|
913 |
by (auto intro: hidesI) |
|
914 |
with wf |
|
915 |
have "is_static old" |
|
916 |
by (blast dest: wf_prog_hidesD) |
|
917 |
with instance_method |
|
918 |
show ?thesis |
|
919 |
by (contradiction) |
|
920 |
qed |
|
921 |
qed |
|
922 |
} note hyp_member_super = this |
|
923 |
from subclsC cls_C |
|
924 |
have "G\<turnstile>(super c)\<preceq>\<^sub>C declclass old" |
|
925 |
by (rule subcls_superD) |
|
926 |
then |
|
927 |
show "?P C old" |
|
928 |
proof (cases rule: subclseq_cases) |
|
929 |
case Eq |
|
930 |
assume "super c = declclass old" |
|
931 |
with old_declared |
|
932 |
have "G\<turnstile>Method old member_of (super c)" |
|
933 |
by (cases old) (auto intro: members.Immediate) |
|
934 |
with inheritable instance_method |
|
935 |
show ?thesis |
|
936 |
by (blast dest: hyp_member_super) |
|
937 |
next |
|
938 |
case Subcls |
|
939 |
assume "G\<turnstile>super c\<prec>\<^sub>C declclass old" |
|
940 |
moreover |
|
941 |
from inheritable accmodi_old |
|
942 |
have "G \<turnstile>Method old inheritable_in pid (super c)" |
|
943 |
by (cases "accmodi old") (auto simp add: inheritable_in_def) |
|
944 |
ultimately |
|
945 |
have "?P (super c) old" |
|
946 |
by (blast dest: hyp) |
|
947 |
then show ?thesis |
|
948 |
proof |
|
949 |
assume "G \<turnstile>Method old member_of super c" |
|
950 |
with inheritable instance_method |
|
951 |
show ?thesis |
|
952 |
by (blast dest: hyp_member_super) |
|
953 |
next |
|
954 |
assume "\<exists>new. G \<turnstile> new overrides\<^sub>S old \<and> G \<turnstile>Method new member_of super c" |
|
955 |
then obtain super_new where |
|
956 |
super_new_override: "G \<turnstile> super_new overrides\<^sub>S old" and |
|
957 |
super_new_member: "G \<turnstile>Method super_new member_of super c" |
|
958 |
by blast |
|
959 |
from super_new_override wf |
|
960 |
have "accmodi old \<le> accmodi super_new" |
|
961 |
by (auto dest: wf_prog_stat_overridesD) |
|
962 |
with inheritable accmodi_old |
|
963 |
have "G \<turnstile>Method super_new inheritable_in pid C" |
|
964 |
by (auto simp add: inheritable_in_def |
|
965 |
split: acc_modi.splits |
|
966 |
dest: acc_modi_le_Dests) |
|
967 |
moreover |
|
968 |
from super_new_override |
|
969 |
have "\<not> is_static super_new" |
|
970 |
by (auto dest: stat_overrides_commonD) |
|
971 |
moreover |
|
972 |
note super_new_member |
|
973 |
ultimately have "?P C super_new" |
|
974 |
by (auto dest: hyp_member_super) |
|
975 |
then show ?thesis |
|
976 |
proof |
|
977 |
assume "G \<turnstile>Method super_new member_of C" |
|
978 |
with super_new_override |
|
979 |
show ?thesis |
|
980 |
by blast |
|
981 |
next |
|
982 |
assume "\<exists>new. G \<turnstile> new overrides\<^sub>S super_new \<and> |
|
983 |
G \<turnstile>Method new member_of C" |
|
984 |
with super_new_override show ?thesis |
|
985 |
by (blast intro: stat_overridesR.Indirect) |
|
986 |
qed |
|
987 |
qed |
|
988 |
qed |
|
989 |
qed |
|
990 |
qed |
|
991 |
||
992 |
lemma non_Package_instance_method_inheritance_cases [consumes 6, |
|
993 |
case_names Inheritance Overriding]: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
994 |
assumes old_inheritable: "G\<turnstile>Method old inheritable_in (pid C)" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
995 |
accmodi_old: "accmodi old \<noteq> Package" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
996 |
instance_method: "\<not> is_static old" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
997 |
subcls: "G\<turnstile>C \<prec>\<^sub>C declclass old" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
998 |
old_declared: "G\<turnstile>Method old declared_in (declclass old)" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
999 |
wf: "wf_prog G" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1000 |
inheritance: "G\<turnstile>Method old member_of C \<Longrightarrow> P" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1001 |
overriding: "\<And> new. |
12854 | 1002 |
\<lbrakk>G\<turnstile> new overrides\<^sub>S old;G\<turnstile>Method new member_of C\<rbrakk> |
1003 |
\<Longrightarrow> P" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1004 |
shows P |
12854 | 1005 |
proof - |
1006 |
from old_inheritable accmodi_old instance_method subcls old_declared wf |
|
1007 |
inheritance overriding |
|
1008 |
show ?thesis |
|
1009 |
by (auto dest: non_Package_instance_method_inheritance) |
|
1010 |
qed |
|
1011 |
||
1012 |
lemma dynamic_to_static_overriding: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1013 |
assumes dyn_override: "G\<turnstile> new overrides old" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1014 |
accmodi_old: "accmodi old \<noteq> Package" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1015 |
wf: "wf_prog G" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1016 |
shows "G\<turnstile> new overrides\<^sub>S old" |
12854 | 1017 |
proof - |
1018 |
from dyn_override accmodi_old |
|
1019 |
show ?thesis (is "?Overrides new old") |
|
1020 |
proof (induct rule: overridesR.induct) |
|
1021 |
case (Direct new old) |
|
1022 |
assume new_declared: "G\<turnstile>Method new declared_in declclass new" |
|
1023 |
assume eq_sig_new_old: "msig new = msig old" |
|
1024 |
assume subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" |
|
1025 |
assume "G \<turnstile>Method old inheritable_in pid (declclass new)" and |
|
1026 |
"accmodi old \<noteq> Package" and |
|
1027 |
"\<not> is_static old" and |
|
1028 |
"G\<turnstile>declclass new\<prec>\<^sub>C declclass old" and |
|
1029 |
"G\<turnstile>Method old declared_in declclass old" |
|
1030 |
from this wf |
|
1031 |
show "?Overrides new old" |
|
1032 |
proof (cases rule: non_Package_instance_method_inheritance_cases) |
|
1033 |
case Inheritance |
|
1034 |
assume "G \<turnstile>Method old member_of declclass new" |
|
1035 |
then have "G\<turnstile>mid (msig old) undeclared_in declclass new" |
|
1036 |
proof cases |
|
1037 |
case Immediate |
|
1038 |
with subcls_new_old wf show ?thesis |
|
1039 |
by (auto dest: subcls_irrefl) |
|
1040 |
next |
|
1041 |
case Inherited |
|
1042 |
then show ?thesis |
|
1043 |
by (cases old) auto |
|
1044 |
qed |
|
1045 |
with eq_sig_new_old new_declared |
|
1046 |
show ?thesis |
|
1047 |
by (cases old,cases new) (auto dest!: declared_not_undeclared) |
|
1048 |
next |
|
1049 |
case (Overriding new') |
|
1050 |
assume stat_override_new': "G \<turnstile> new' overrides\<^sub>S old" |
|
1051 |
then have "msig new' = msig old" |
|
1052 |
by (auto dest: stat_overrides_commonD) |
|
1053 |
with eq_sig_new_old have eq_sig_new_new': "msig new=msig new'" |
|
1054 |
by simp |
|
1055 |
assume "G \<turnstile>Method new' member_of declclass new" |
|
1056 |
then show ?thesis |
|
1057 |
proof (cases) |
|
1058 |
case Immediate |
|
1059 |
then have declC_new: "declclass new' = declclass new" |
|
1060 |
by auto |
|
1061 |
from Immediate |
|
1062 |
have "G\<turnstile>Method new' declared_in declclass new" |
|
1063 |
by (cases new') auto |
|
1064 |
with new_declared eq_sig_new_new' declC_new |
|
1065 |
have "new=new'" |
|
1066 |
by (cases new, cases new') (auto dest: unique_declared_in) |
|
1067 |
with stat_override_new' |
|
1068 |
show ?thesis |
|
1069 |
by simp |
|
1070 |
next |
|
1071 |
case Inherited |
|
1072 |
then have "G\<turnstile>mid (msig new') undeclared_in declclass new" |
|
1073 |
by (cases new') (auto) |
|
1074 |
with eq_sig_new_new' new_declared |
|
1075 |
show ?thesis |
|
1076 |
by (cases new,cases new') (auto dest!: declared_not_undeclared) |
|
1077 |
qed |
|
1078 |
qed |
|
1079 |
next |
|
1080 |
case (Indirect inter new old) |
|
1081 |
assume accmodi_old: "accmodi old \<noteq> Package" |
|
1082 |
assume "accmodi old \<noteq> Package \<Longrightarrow> G \<turnstile> inter overrides\<^sub>S old" |
|
1083 |
with accmodi_old |
|
1084 |
have stat_override_inter_old: "G \<turnstile> inter overrides\<^sub>S old" |
|
1085 |
by blast |
|
1086 |
moreover |
|
1087 |
assume hyp_inter: "accmodi inter \<noteq> Package \<Longrightarrow> G \<turnstile> new overrides\<^sub>S inter" |
|
1088 |
moreover |
|
1089 |
have "accmodi inter \<noteq> Package" |
|
1090 |
proof - |
|
1091 |
from stat_override_inter_old wf |
|
1092 |
have "accmodi old \<le> accmodi inter" |
|
1093 |
by (auto dest: wf_prog_stat_overridesD) |
|
1094 |
with stat_override_inter_old accmodi_old |
|
1095 |
show ?thesis |
|
1096 |
by (auto dest!: no_Private_stat_override |
|
1097 |
split: acc_modi.splits |
|
1098 |
dest: acc_modi_le_Dests) |
|
1099 |
qed |
|
1100 |
ultimately show "?Overrides new old" |
|
1101 |
by (blast intro: stat_overridesR.Indirect) |
|
1102 |
qed |
|
1103 |
qed |
|
1104 |
||
1105 |
lemma wf_prog_dyn_override_prop: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1106 |
assumes dyn_override: "G \<turnstile> new overrides old" and |
12854 | 1107 |
wf: "wf_prog G" |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1108 |
shows "accmodi old \<le> accmodi new" |
12854 | 1109 |
proof (cases "accmodi old = Package") |
1110 |
case True |
|
1111 |
note old_Package = this |
|
1112 |
show ?thesis |
|
1113 |
proof (cases "accmodi old \<le> accmodi new") |
|
1114 |
case True then show ?thesis . |
|
1115 |
next |
|
1116 |
case False |
|
1117 |
with old_Package |
|
1118 |
have "accmodi new = Private" |
|
1119 |
by (cases "accmodi new") (auto simp add: le_acc_def less_acc_def) |
|
1120 |
with dyn_override |
|
1121 |
show ?thesis |
|
1122 |
by (auto dest: overrides_commonD) |
|
1123 |
qed |
|
1124 |
next |
|
1125 |
case False |
|
1126 |
with dyn_override wf |
|
1127 |
have "G \<turnstile> new overrides\<^sub>S old" |
|
1128 |
by (blast intro: dynamic_to_static_overriding) |
|
1129 |
with wf |
|
1130 |
show ?thesis |
|
1131 |
by (blast dest: wf_prog_stat_overridesD) |
|
1132 |
qed |
|
1133 |
||
1134 |
lemma overrides_Package_old: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1135 |
assumes dyn_override: "G \<turnstile> new overrides old" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1136 |
accmodi_new: "accmodi new = Package" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1137 |
wf: "wf_prog G " |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1138 |
shows "accmodi old = Package" |
12854 | 1139 |
proof (cases "accmodi old") |
1140 |
case Private |
|
1141 |
with dyn_override show ?thesis |
|
1142 |
by (simp add: no_Private_override) |
|
1143 |
next |
|
1144 |
case Package |
|
1145 |
then show ?thesis . |
|
1146 |
next |
|
1147 |
case Protected |
|
1148 |
with dyn_override wf |
|
1149 |
have "G \<turnstile> new overrides\<^sub>S old" |
|
1150 |
by (auto intro: dynamic_to_static_overriding) |
|
1151 |
with wf |
|
1152 |
have "accmodi old \<le> accmodi new" |
|
1153 |
by (auto dest: wf_prog_stat_overridesD) |
|
1154 |
with Protected accmodi_new |
|
1155 |
show ?thesis |
|
1156 |
by (simp add: less_acc_def le_acc_def) |
|
1157 |
next |
|
1158 |
case Public |
|
1159 |
with dyn_override wf |
|
1160 |
have "G \<turnstile> new overrides\<^sub>S old" |
|
1161 |
by (auto intro: dynamic_to_static_overriding) |
|
1162 |
with wf |
|
1163 |
have "accmodi old \<le> accmodi new" |
|
1164 |
by (auto dest: wf_prog_stat_overridesD) |
|
1165 |
with Public accmodi_new |
|
1166 |
show ?thesis |
|
1167 |
by (simp add: less_acc_def le_acc_def) |
|
1168 |
qed |
|
1169 |
||
1170 |
lemma dyn_override_Package: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1171 |
assumes dyn_override: "G \<turnstile> new overrides old" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1172 |
accmodi_old: "accmodi old = Package" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1173 |
accmodi_new: "accmodi new = Package" and |
12854 | 1174 |
wf: "wf_prog G" |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1175 |
shows "pid (declclass old) = pid (declclass new)" |
12854 | 1176 |
proof - |
1177 |
from dyn_override accmodi_old accmodi_new |
|
1178 |
show ?thesis (is "?EqPid old new") |
|
1179 |
proof (induct rule: overridesR.induct) |
|
1180 |
case (Direct new old) |
|
1181 |
assume "accmodi old = Package" |
|
1182 |
"G \<turnstile>Method old inheritable_in pid (declclass new)" |
|
1183 |
then show "pid (declclass old) = pid (declclass new)" |
|
1184 |
by (auto simp add: inheritable_in_def) |
|
1185 |
next |
|
1186 |
case (Indirect inter new old) |
|
1187 |
assume accmodi_old: "accmodi old = Package" and |
|
1188 |
accmodi_new: "accmodi new = Package" |
|
1189 |
assume "G \<turnstile> new overrides inter" |
|
1190 |
with accmodi_new wf |
|
1191 |
have "accmodi inter = Package" |
|
1192 |
by (auto intro: overrides_Package_old) |
|
1193 |
with Indirect |
|
1194 |
show "pid (declclass old) = pid (declclass new)" |
|
1195 |
by auto |
|
1196 |
qed |
|
1197 |
qed |
|
1198 |
||
1199 |
lemma dyn_override_Package_escape: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1200 |
assumes dyn_override: "G \<turnstile> new overrides old" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1201 |
accmodi_old: "accmodi old = Package" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1202 |
outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" and |
12854 | 1203 |
wf: "wf_prog G" |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1204 |
shows "\<exists> inter. G \<turnstile> new overrides inter \<and> G \<turnstile> inter overrides old \<and> |
12854 | 1205 |
pid (declclass old) = pid (declclass inter) \<and> |
1206 |
Protected \<le> accmodi inter" |
|
1207 |
proof - |
|
1208 |
from dyn_override accmodi_old outside_pack |
|
1209 |
show ?thesis (is "?P new old") |
|
1210 |
proof (induct rule: overridesR.induct) |
|
1211 |
case (Direct new old) |
|
1212 |
assume accmodi_old: "accmodi old = Package" |
|
1213 |
assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" |
|
1214 |
assume "G \<turnstile>Method old inheritable_in pid (declclass new)" |
|
1215 |
with accmodi_old |
|
1216 |
have "pid (declclass old) = pid (declclass new)" |
|
1217 |
by (simp add: inheritable_in_def) |
|
1218 |
with outside_pack |
|
1219 |
show "?P new old" |
|
1220 |
by (contradiction) |
|
1221 |
next |
|
1222 |
case (Indirect inter new old) |
|
1223 |
assume accmodi_old: "accmodi old = Package" |
|
1224 |
assume outside_pack: "pid (declclass old) \<noteq> pid (declclass new)" |
|
1225 |
assume override_new_inter: "G \<turnstile> new overrides inter" |
|
1226 |
assume override_inter_old: "G \<turnstile> inter overrides old" |
|
1227 |
assume hyp_new_inter: "\<lbrakk>accmodi inter = Package; |
|
1228 |
pid (declclass inter) \<noteq> pid (declclass new)\<rbrakk> |
|
1229 |
\<Longrightarrow> ?P new inter" |
|
1230 |
assume hyp_inter_old: "\<lbrakk>accmodi old = Package; |
|
1231 |
pid (declclass old) \<noteq> pid (declclass inter)\<rbrakk> |
|
1232 |
\<Longrightarrow> ?P inter old" |
|
1233 |
show "?P new old" |
|
1234 |
proof (cases "pid (declclass old) = pid (declclass inter)") |
|
1235 |
case True |
|
1236 |
note same_pack_old_inter = this |
|
1237 |
show ?thesis |
|
1238 |
proof (cases "pid (declclass inter) = pid (declclass new)") |
|
1239 |
case True |
|
1240 |
with same_pack_old_inter outside_pack |
|
1241 |
show ?thesis |
|
1242 |
by auto |
|
1243 |
next |
|
1244 |
case False |
|
1245 |
note diff_pack_inter_new = this |
|
1246 |
show ?thesis |
|
1247 |
proof (cases "accmodi inter = Package") |
|
1248 |
case True |
|
1249 |
with diff_pack_inter_new hyp_new_inter |
|
1250 |
obtain newinter where |
|
1251 |
over_new_newinter: "G \<turnstile> new overrides newinter" and |
|
1252 |
over_newinter_inter: "G \<turnstile> newinter overrides inter" and |
|
1253 |
eq_pid: "pid (declclass inter) = pid (declclass newinter)" and |
|
1254 |
accmodi_newinter: "Protected \<le> accmodi newinter" |
|
1255 |
by auto |
|
1256 |
from over_newinter_inter override_inter_old |
|
1257 |
have "G\<turnstile>newinter overrides old" |
|
1258 |
by (rule overridesR.Indirect) |
|
1259 |
moreover |
|
1260 |
from eq_pid same_pack_old_inter |
|
1261 |
have "pid (declclass old) = pid (declclass newinter)" |
|
1262 |
by simp |
|
1263 |
moreover |
|
1264 |
note over_new_newinter accmodi_newinter |
|
1265 |
ultimately show ?thesis |
|
1266 |
by blast |
|
1267 |
next |
|
1268 |
case False |
|
1269 |
with override_new_inter |
|
1270 |
have "Protected \<le> accmodi inter" |
|
1271 |
by (cases "accmodi inter") (auto dest: no_Private_override) |
|
1272 |
with override_new_inter override_inter_old same_pack_old_inter |
|
1273 |
show ?thesis |
|
1274 |
by blast |
|
1275 |
qed |
|
1276 |
qed |
|
1277 |
next |
|
1278 |
case False |
|
1279 |
with accmodi_old hyp_inter_old |
|
1280 |
obtain newinter where |
|
1281 |
over_inter_newinter: "G \<turnstile> inter overrides newinter" and |
|
1282 |
over_newinter_old: "G \<turnstile> newinter overrides old" and |
|
1283 |
eq_pid: "pid (declclass old) = pid (declclass newinter)" and |
|
1284 |
accmodi_newinter: "Protected \<le> accmodi newinter" |
|
1285 |
by auto |
|
1286 |
from override_new_inter over_inter_newinter |
|
1287 |
have "G \<turnstile> new overrides newinter" |
|
1288 |
by (rule overridesR.Indirect) |
|
1289 |
with eq_pid over_newinter_old accmodi_newinter |
|
1290 |
show ?thesis |
|
1291 |
by blast |
|
1292 |
qed |
|
1293 |
qed |
|
1294 |
qed |
|
1295 |
||
1296 |
lemma declclass_widen[rule_format]: |
|
1297 |
"wf_prog G |
|
1298 |
\<longrightarrow> (\<forall>c m. class G C = Some c \<longrightarrow> methd G C sig = Some m |
|
1299 |
\<longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m)" (is "?P G C") |
|
1300 |
proof (rule class_rec.induct,intro allI impI) |
|
1301 |
fix G C c m |
|
1302 |
assume Hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c |
|
1303 |
\<longrightarrow> ?P G (super c)" |
|
1304 |
assume wf: "wf_prog G" and cls_C: "class G C = Some c" and |
|
1305 |
m: "methd G C sig = Some m" |
|
1306 |
show "G\<turnstile>C\<preceq>\<^sub>C declclass m" |
|
1307 |
proof (cases "C=Object") |
|
1308 |
case True |
|
1309 |
with wf m show ?thesis by (simp add: methd_Object_SomeD) |
|
1310 |
next |
|
1311 |
let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)" |
|
1312 |
let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))" |
|
1313 |
case False |
|
1314 |
with cls_C wf m |
|
1315 |
have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m " |
|
1316 |
by (simp add: methd_rec) |
|
1317 |
show ?thesis |
|
1318 |
proof (cases "?table sig") |
|
1319 |
case None |
|
1320 |
from this methd_C have "?filter (methd G (super c)) sig = Some m" |
|
1321 |
by simp |
|
1322 |
moreover |
|
1323 |
from wf cls_C False obtain sup where "class G (super c) = Some sup" |
|
1324 |
by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
1325 |
moreover note wf False cls_C |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
1326 |
ultimately have "G\<turnstile>super c \<preceq>\<^sub>C declclass m" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
1327 |
by (auto intro: Hyp [rule_format]) |
12854 | 1328 |
moreover from cls_C False have "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" by (rule subcls1I) |
1329 |
ultimately show ?thesis by - (rule rtrancl_into_rtrancl2) |
|
1330 |
next |
|
1331 |
case Some |
|
1332 |
from this wf False cls_C methd_C show ?thesis by auto |
|
1333 |
qed |
|
1334 |
qed |
|
1335 |
qed |
|
1336 |
||
1337 |
lemma declclass_methd_Object: |
|
1338 |
"\<lbrakk>wf_prog G; methd G Object sig = Some m\<rbrakk> \<Longrightarrow> declclass m = Object" |
|
1339 |
by auto |
|
1340 |
||
1341 |
lemma methd_declaredD: |
|
1342 |
"\<lbrakk>wf_prog G; is_class G C;methd G C sig = Some m\<rbrakk> |
|
1343 |
\<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)" |
|
1344 |
proof - |
|
1345 |
assume wf: "wf_prog G" |
|
1346 |
then have ws: "ws_prog G" .. |
|
1347 |
assume clsC: "is_class G C" |
|
1348 |
from clsC ws |
|
1349 |
show "methd G C sig = Some m |
|
1350 |
\<Longrightarrow> G\<turnstile>(mdecl (sig,mthd m)) declared_in (declclass m)" |
|
1351 |
(is "PROP ?P C") |
|
1352 |
proof (induct ?P C rule: ws_class_induct') |
|
1353 |
case Object |
|
1354 |
assume "methd G Object sig = Some m" |
|
1355 |
with wf show ?thesis |
|
1356 |
by - (rule method_declared_inI, auto) |
|
1357 |
next |
|
1358 |
case Subcls |
|
1359 |
fix C c |
|
1360 |
assume clsC: "class G C = Some c" |
|
1361 |
and m: "methd G C sig = Some m" |
|
1362 |
and hyp: "methd G (super c) sig = Some m \<Longrightarrow> ?thesis" |
|
1363 |
let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))" |
|
1364 |
show ?thesis |
|
1365 |
proof (cases "?newMethods sig") |
|
1366 |
case None |
|
1367 |
from None ws clsC m hyp |
|
1368 |
show ?thesis by (auto intro: method_declared_inI simp add: methd_rec) |
|
1369 |
next |
|
1370 |
case Some |
|
1371 |
from Some ws clsC m |
|
1372 |
show ?thesis by (auto intro: method_declared_inI simp add: methd_rec) |
|
1373 |
qed |
|
1374 |
qed |
|
1375 |
qed |
|
1376 |
||
1377 |
lemma methd_rec_Some_cases [consumes 4, case_names NewMethod InheritedMethod]: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1378 |
assumes methd_C: "methd G C sig = Some m" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1379 |
ws: "ws_prog G" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1380 |
clsC: "class G C = Some c" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1381 |
neq_C_Obj: "C\<noteq>Object" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1382 |
shows |
12854 | 1383 |
"\<lbrakk>table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig = Some m \<Longrightarrow> P; |
1384 |
\<lbrakk>G\<turnstile>C inherits (method sig m); methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P |
|
1385 |
\<rbrakk> \<Longrightarrow> P" |
|
1386 |
proof - |
|
1387 |
let ?inherited = "filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m) |
|
1388 |
(methd G (super c))" |
|
1389 |
let ?new = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))" |
|
1390 |
from ws clsC neq_C_Obj methd_C |
|
1391 |
have methd_unfold: "(?inherited ++ ?new) sig = Some m" |
|
1392 |
by (simp add: methd_rec) |
|
1393 |
assume NewMethod: "?new sig = Some m \<Longrightarrow> P" |
|
1394 |
assume InheritedMethod: "\<lbrakk>G\<turnstile>C inherits (method sig m); |
|
1395 |
methd G (super c) sig = Some m\<rbrakk> \<Longrightarrow> P" |
|
1396 |
show P |
|
1397 |
proof (cases "?new sig") |
|
1398 |
case None |
|
1399 |
with methd_unfold have "?inherited sig = Some m" |
|
1400 |
by (auto) |
|
1401 |
with InheritedMethod show P by blast |
|
1402 |
next |
|
1403 |
case Some |
|
1404 |
with methd_unfold have "?new sig = Some m" |
|
1405 |
by auto |
|
1406 |
with NewMethod show P by blast |
|
1407 |
qed |
|
1408 |
qed |
|
1409 |
||
1410 |
||
1411 |
lemma methd_member_of: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1412 |
assumes wf: "wf_prog G" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1413 |
shows |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1414 |
"\<lbrakk>is_class G C; methd G C sig = Some m\<rbrakk> \<Longrightarrow> G\<turnstile>Methd sig m member_of C" |
12854 | 1415 |
(is "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C") |
1416 |
proof - |
|
1417 |
from wf have ws: "ws_prog G" .. |
|
1418 |
assume defC: "is_class G C" |
|
1419 |
from defC ws |
|
1420 |
show "?Class C \<Longrightarrow> ?Method C \<Longrightarrow> ?MemberOf C" |
|
1421 |
proof (induct rule: ws_class_induct') |
|
1422 |
case Object |
|
1423 |
with wf have declC: "declclass m = Object" |
|
1424 |
by (blast intro: declclass_methd_Object) |
|
1425 |
with Object wf have "G\<turnstile>Methd sig m declared_in Object" |
|
1426 |
by (auto dest: methd_declaredD simp del: methd_Object) |
|
1427 |
with declC |
|
1428 |
show "?MemberOf Object" |
|
1429 |
by (auto intro!: members.Immediate |
|
1430 |
simp del: methd_Object) |
|
1431 |
next |
|
1432 |
case (Subcls C c) |
|
1433 |
assume clsC: "class G C = Some c" and |
|
1434 |
neq_C_Obj: "C \<noteq> Object" |
|
1435 |
assume methd: "?Method C" |
|
1436 |
from methd ws clsC neq_C_Obj |
|
1437 |
show "?MemberOf C" |
|
1438 |
proof (cases rule: methd_rec_Some_cases) |
|
1439 |
case NewMethod |
|
1440 |
with clsC show ?thesis |
|
1441 |
by (auto dest: method_declared_inI intro!: members.Immediate) |
|
1442 |
next |
|
1443 |
case InheritedMethod |
|
1444 |
then show "?thesis" |
|
1445 |
by (blast dest: inherits_member) |
|
1446 |
qed |
|
1447 |
qed |
|
1448 |
qed |
|
1449 |
||
1450 |
lemma current_methd: |
|
1451 |
"\<lbrakk>table_of (methods c) sig = Some new; |
|
1452 |
ws_prog G; class G C = Some c; C \<noteq> Object; |
|
1453 |
methd G (super c) sig = Some old\<rbrakk> |
|
1454 |
\<Longrightarrow> methd G C sig = Some (C,new)" |
|
1455 |
by (auto simp add: methd_rec |
|
1456 |
intro: filter_tab_SomeI override_find_right table_of_map_SomeI) |
|
1457 |
||
1458 |
lemma wf_prog_staticD: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1459 |
assumes wf: "wf_prog G" and |
12854 | 1460 |
clsC: "class G C = Some c" and |
1461 |
neq_C_Obj: "C \<noteq> Object" and |
|
1462 |
old: "methd G (super c) sig = Some old" and |
|
1463 |
accmodi_old: "Protected \<le> accmodi old" and |
|
1464 |
new: "table_of (methods c) sig = Some new" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1465 |
shows "is_static new = is_static old" |
12854 | 1466 |
proof - |
1467 |
from clsC wf |
|
1468 |
have wf_cdecl: "wf_cdecl G (C,c)" by (rule wf_prog_cdecl) |
|
1469 |
from wf clsC neq_C_Obj |
|
1470 |
have is_cls_super: "is_class G (super c)" |
|
1471 |
by (blast dest: wf_prog_acc_superD is_acc_classD) |
|
1472 |
from wf is_cls_super old |
|
1473 |
have old_member_of: "G\<turnstile>Methd sig old member_of (super c)" |
|
1474 |
by (rule methd_member_of) |
|
1475 |
from old wf is_cls_super |
|
1476 |
have old_declared: "G\<turnstile>Methd sig old declared_in (declclass old)" |
|
1477 |
by (auto dest: methd_declared_in_declclass) |
|
1478 |
from new clsC |
|
1479 |
have new_declared: "G\<turnstile>Methd sig (C,new) declared_in C" |
|
1480 |
by (auto intro: method_declared_inI) |
|
1481 |
note trancl_rtrancl_tranc = trancl_rtrancl_trancl [trans] (* ### in Basis *) |
|
1482 |
from clsC neq_C_Obj |
|
1483 |
have subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" |
|
1484 |
by (rule subcls1I) |
|
1485 |
then have "G\<turnstile>C \<prec>\<^sub>C super c" .. |
|
1486 |
also from old wf is_cls_super |
|
1487 |
have "G\<turnstile>super c \<preceq>\<^sub>C (declclass old)" by (auto dest: methd_declC) |
|
1488 |
finally have subcls_C_old: "G\<turnstile>C \<prec>\<^sub>C (declclass old)" . |
|
1489 |
from accmodi_old |
|
1490 |
have inheritable: "G\<turnstile>Methd sig old inheritable_in pid C" |
|
1491 |
by (auto simp add: inheritable_in_def |
|
1492 |
dest: acc_modi_le_Dests) |
|
1493 |
show ?thesis |
|
1494 |
proof (cases "is_static new") |
|
1495 |
case True |
|
1496 |
with subcls_C_old new_declared old_declared inheritable |
|
1497 |
have "G,sig\<turnstile>(C,new) hides old" |
|
1498 |
by (auto intro: hidesI) |
|
1499 |
with True wf_cdecl neq_C_Obj new |
|
1500 |
show ?thesis |
|
1501 |
by (auto dest: wf_cdecl_hides_SomeD) |
|
1502 |
next |
|
1503 |
case False |
|
1504 |
with subcls_C_old new_declared old_declared inheritable subcls1_C_super |
|
1505 |
old_member_of |
|
1506 |
have "G,sig\<turnstile>(C,new) overrides\<^sub>S old" |
|
1507 |
by (auto intro: stat_overridesR.Direct) |
|
1508 |
with False wf_cdecl neq_C_Obj new |
|
1509 |
show ?thesis |
|
1510 |
by (auto dest: wf_cdecl_overrides_SomeD) |
|
1511 |
qed |
|
1512 |
qed |
|
1513 |
||
1514 |
lemma inheritable_instance_methd: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1515 |
assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and |
12854 | 1516 |
is_cls_D: "is_class G D" and |
1517 |
wf: "wf_prog G" and |
|
1518 |
old: "methd G D sig = Some old" and |
|
1519 |
accmodi_old: "Protected \<le> accmodi old" and |
|
1520 |
not_static_old: "\<not> is_static old" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1521 |
shows |
12854 | 1522 |
"\<exists>new. methd G C sig = Some new \<and> |
1523 |
(new = old \<or> G,sig\<turnstile>new overrides\<^sub>S old)" |
|
1524 |
(is "(\<exists>new. (?Constraint C new old))") |
|
1525 |
proof - |
|
1526 |
from subclseq_C_D is_cls_D |
|
1527 |
have is_cls_C: "is_class G C" by (rule subcls_is_class2) |
|
1528 |
from wf |
|
1529 |
have ws: "ws_prog G" .. |
|
1530 |
from is_cls_C ws subclseq_C_D |
|
1531 |
show "\<exists>new. ?Constraint C new old" |
|
1532 |
proof (induct rule: ws_class_induct') |
|
1533 |
case (Object co) |
|
1534 |
then have eq_D_Obj: "D=Object" by auto |
|
1535 |
with old |
|
1536 |
have "?Constraint Object old old" |
|
1537 |
by auto |
|
1538 |
with eq_D_Obj |
|
1539 |
show "\<exists> new. ?Constraint Object new old" by auto |
|
1540 |
next |
|
1541 |
case (Subcls C c) |
|
1542 |
assume hyp: "G\<turnstile>super c\<preceq>\<^sub>C D \<Longrightarrow> \<exists>new. ?Constraint (super c) new old" |
|
1543 |
assume clsC: "class G C = Some c" |
|
1544 |
assume neq_C_Obj: "C\<noteq>Object" |
|
1545 |
from clsC wf |
|
1546 |
have wf_cdecl: "wf_cdecl G (C,c)" |
|
1547 |
by (rule wf_prog_cdecl) |
|
1548 |
from ws clsC neq_C_Obj |
|
1549 |
have is_cls_super: "is_class G (super c)" |
|
1550 |
by (auto dest: ws_prog_cdeclD) |
|
1551 |
from clsC wf neq_C_Obj |
|
1552 |
have superAccessible: "G\<turnstile>(Class (super c)) accessible_in (pid C)" and |
|
1553 |
subcls1_C_super: "G\<turnstile>C \<prec>\<^sub>C\<^sub>1 super c" |
|
1554 |
by (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_classD |
|
1555 |
intro: subcls1I) |
|
1556 |
show "\<exists>new. ?Constraint C new old" |
|
1557 |
proof (cases "G\<turnstile>super c\<preceq>\<^sub>C D") |
|
1558 |
case False |
|
1559 |
from False Subcls |
|
1560 |
have eq_C_D: "C=D" |
|
1561 |
by (auto dest: subclseq_superD) |
|
1562 |
with old |
|
1563 |
have "?Constraint C old old" |
|
1564 |
by auto |
|
1565 |
with eq_C_D |
|
1566 |
show "\<exists> new. ?Constraint C new old" by auto |
|
1567 |
next |
|
1568 |
case True |
|
1569 |
with hyp obtain super_method |
|
1570 |
where super: "?Constraint (super c) super_method old" by blast |
|
1571 |
from super not_static_old |
|
1572 |
have not_static_super: "\<not> is_static super_method" |
|
1573 |
by (auto dest!: stat_overrides_commonD) |
|
1574 |
from super old wf accmodi_old |
|
1575 |
have accmodi_super_method: "Protected \<le> accmodi super_method" |
|
1576 |
by (auto dest!: wf_prog_stat_overridesD |
|
1577 |
intro: order_trans) |
|
1578 |
from super accmodi_old wf |
|
1579 |
have inheritable: "G\<turnstile>Methd sig super_method inheritable_in (pid C)" |
|
1580 |
by (auto dest!: wf_prog_stat_overridesD |
|
1581 |
acc_modi_le_Dests |
|
1582 |
simp add: inheritable_in_def) |
|
1583 |
from super wf is_cls_super |
|
1584 |
have member: "G\<turnstile>Methd sig super_method member_of (super c)" |
|
1585 |
by (auto intro: methd_member_of) |
|
1586 |
from member |
|
1587 |
have decl_super_method: |
|
1588 |
"G\<turnstile>Methd sig super_method declared_in (declclass super_method)" |
|
1589 |
by (auto dest: member_of_declC) |
|
1590 |
from super subcls1_C_super ws is_cls_super |
|
1591 |
have subcls_C_super: "G\<turnstile>C \<prec>\<^sub>C (declclass super_method)" |
|
1592 |
by (auto intro: rtrancl_into_trancl2 dest: methd_declC) |
|
1593 |
show "\<exists> new. ?Constraint C new old" |
|
1594 |
proof (cases "methd G C sig") |
|
1595 |
case None |
|
1596 |
have "methd G (super c) sig = None" |
|
1597 |
proof - |
|
1598 |
from clsC ws None |
|
1599 |
have no_new: "table_of (methods c) sig = None" |
|
1600 |
by (auto simp add: methd_rec) |
|
1601 |
with clsC |
|
1602 |
have undeclared: "G\<turnstile>mid sig undeclared_in C" |
|
1603 |
by (auto simp add: undeclared_in_def cdeclaredmethd_def) |
|
1604 |
with inheritable member superAccessible subcls1_C_super |
|
1605 |
have inherits: "G\<turnstile>C inherits (method sig super_method)" |
|
1606 |
by (auto simp add: inherits_def) |
|
1607 |
with clsC ws no_new super neq_C_Obj |
|
1608 |
have "methd G C sig = Some super_method" |
|
1609 |
by (auto simp add: methd_rec override_def |
|
1610 |
intro: filter_tab_SomeI) |
|
1611 |
with None show ?thesis |
|
1612 |
by simp |
|
1613 |
qed |
|
1614 |
with super show ?thesis by auto |
|
1615 |
next |
|
1616 |
case (Some new) |
|
1617 |
from this ws clsC neq_C_Obj |
|
1618 |
show ?thesis |
|
1619 |
proof (cases rule: methd_rec_Some_cases) |
|
1620 |
case InheritedMethod |
|
1621 |
with super Some show ?thesis |
|
1622 |
by auto |
|
1623 |
next |
|
1624 |
case NewMethod |
|
1625 |
assume new: "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig |
|
1626 |
= Some new" |
|
1627 |
from new |
|
1628 |
have declcls_new: "declclass new = C" |
|
1629 |
by auto |
|
1630 |
from wf clsC neq_C_Obj super new not_static_super accmodi_super_method |
|
1631 |
have not_static_new: "\<not> is_static new" |
|
1632 |
by (auto dest: wf_prog_staticD) |
|
1633 |
from clsC new |
|
1634 |
have decl_new: "G\<turnstile>Methd sig new declared_in C" |
|
1635 |
by (auto simp add: declared_in_def cdeclaredmethd_def) |
|
1636 |
from not_static_new decl_new decl_super_method |
|
1637 |
member subcls1_C_super inheritable declcls_new subcls_C_super |
|
1638 |
have "G,sig\<turnstile> new overrides\<^sub>S super_method" |
|
1639 |
by (auto intro: stat_overridesR.Direct) |
|
1640 |
with super Some |
|
1641 |
show ?thesis |
|
1642 |
by (auto intro: stat_overridesR.Indirect) |
|
1643 |
qed |
|
1644 |
qed |
|
1645 |
qed |
|
1646 |
qed |
|
1647 |
qed |
|
1648 |
||
1649 |
lemma inheritable_instance_methd_cases [consumes 6 |
|
1650 |
, case_names Inheritance Overriding]: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1651 |
assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and |
12854 | 1652 |
is_cls_D: "is_class G D" and |
1653 |
wf: "wf_prog G" and |
|
1654 |
old: "methd G D sig = Some old" and |
|
1655 |
accmodi_old: "Protected \<le> accmodi old" and |
|
1656 |
not_static_old: "\<not> is_static old" and |
|
1657 |
inheritance: "methd G C sig = Some old \<Longrightarrow> P" and |
|
1658 |
overriding: "\<And> new. \<lbrakk>methd G C sig = Some new; |
|
1659 |
G,sig\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> P" |
|
1660 |
||
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1661 |
shows P |
12854 | 1662 |
proof - |
1663 |
from subclseq_C_D is_cls_D wf old accmodi_old not_static_old |
|
1664 |
show ?thesis |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
1665 |
by (auto dest: inheritable_instance_methd intro: inheritance overriding) |
12854 | 1666 |
qed |
1667 |
||
1668 |
lemma inheritable_instance_methd_props: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1669 |
assumes subclseq_C_D: "G\<turnstile>C \<preceq>\<^sub>C D" and |
12854 | 1670 |
is_cls_D: "is_class G D" and |
1671 |
wf: "wf_prog G" and |
|
1672 |
old: "methd G D sig = Some old" and |
|
1673 |
accmodi_old: "Protected \<le> accmodi old" and |
|
1674 |
not_static_old: "\<not> is_static old" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1675 |
shows |
12854 | 1676 |
"\<exists>new. methd G C sig = Some new \<and> |
1677 |
\<not> is_static new \<and> G\<turnstile>resTy new\<preceq>resTy old \<and> accmodi old \<le>accmodi new" |
|
1678 |
(is "(\<exists>new. (?Constraint C new old))") |
|
1679 |
proof - |
|
1680 |
from subclseq_C_D is_cls_D wf old accmodi_old not_static_old |
|
1681 |
show ?thesis |
|
1682 |
proof (cases rule: inheritable_instance_methd_cases) |
|
1683 |
case Inheritance |
|
1684 |
with not_static_old accmodi_old show ?thesis by auto |
|
1685 |
next |
|
1686 |
case (Overriding new) |
|
1687 |
then have "\<not> is_static new" by (auto dest: stat_overrides_commonD) |
|
1688 |
with Overriding not_static_old accmodi_old wf |
|
1689 |
show ?thesis |
|
1690 |
by (auto dest!: wf_prog_stat_overridesD |
|
1691 |
intro: order_trans) |
|
1692 |
qed |
|
1693 |
qed |
|
1694 |
||
1695 |
(* ### Probleme: Die tollen methd_subcls_cases Lemma wird warscheinlich |
|
1696 |
kaum gebraucht: |
|
1697 |
Redundanz: stat_overrides.Direct old declared in declclass old folgt aus |
|
1698 |
member of |
|
1699 |
Problem: Predikate wie overrides, sind global üper die Hierarchie hinweg |
|
1700 |
definiert, aber oft barucht man eben zusätlich Induktion |
|
1701 |
: von super c auf C; Dann ist aber auss dem Kontext |
|
1702 |
die Unterscheidung in die 5 fälle overkill, |
|
1703 |
da man dann warscheinlich meistens eh in einem speziellen |
|
1704 |
Fall kommt (durch die Hypothesen) |
|
1705 |
*) |
|
1706 |
||
1707 |
(* local lemma *) |
|
1708 |
ML {* bind_thm("bexI'",permute_prems 0 1 bexI) *} |
|
1709 |
ML {* bind_thm("ballE'",permute_prems 1 1 ballE) *} |
|
1710 |
lemma subint_widen_imethds: |
|
1711 |
"\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J; jm \<in> imethds G J sig\<rbrakk> \<Longrightarrow> |
|
1712 |
\<exists> im \<in> imethds G I sig. is_static im = is_static jm \<and> |
|
1713 |
accmodi im = accmodi jm \<and> |
|
1714 |
G\<turnstile>resTy im\<preceq>resTy jm" |
|
1715 |
proof - |
|
1716 |
assume irel: "G\<turnstile>I\<preceq>I J" and |
|
1717 |
wf: "wf_prog G" and |
|
1718 |
is_iface: "is_iface G J" |
|
1719 |
from irel show "jm \<in> imethds G J sig \<Longrightarrow> ?thesis" |
|
1720 |
(is "PROP ?P I" is "PROP ?Prem J \<Longrightarrow> ?Concl I") |
|
1721 |
proof (induct ?P I rule: converse_rtrancl_induct) |
|
1722 |
case Id |
|
1723 |
assume "jm \<in> imethds G J sig" |
|
1724 |
then show "?Concl J" by (blast elim: bexI') |
|
1725 |
next |
|
1726 |
case Step |
|
1727 |
fix I SI |
|
1728 |
assume subint1_I_SI: "G\<turnstile>I \<prec>I1 SI" and |
|
1729 |
subint_SI_J: "G\<turnstile>SI \<preceq>I J" and |
|
1730 |
hyp: "PROP ?P SI" and |
|
1731 |
jm: "jm \<in> imethds G J sig" |
|
1732 |
from subint1_I_SI |
|
1733 |
obtain i where |
|
1734 |
ifI: "iface G I = Some i" and |
|
1735 |
SI: "SI \<in> set (isuperIfs i)" |
|
1736 |
by (blast dest: subint1D) |
|
1737 |
||
1738 |
let ?newMethods |
|
1739 |
= "(o2s \<circ> table_of (map (\<lambda>(sig, mh). (sig, I, mh)) (imethods i)))" |
|
1740 |
show "?Concl I" |
|
1741 |
proof (cases "?newMethods sig = {}") |
|
1742 |
case True |
|
1743 |
with ifI SI hyp wf jm |
|
1744 |
show "?thesis" |
|
1745 |
by (auto simp add: imethds_rec) |
|
1746 |
next |
|
1747 |
case False |
|
1748 |
from ifI wf False |
|
1749 |
have imethds: "imethds G I sig = ?newMethods sig" |
|
1750 |
by (simp add: imethds_rec) |
|
1751 |
from False |
|
1752 |
obtain im where |
|
1753 |
imdef: "im \<in> ?newMethods sig" |
|
1754 |
by (blast) |
|
1755 |
with imethds |
|
1756 |
have im: "im \<in> imethds G I sig" |
|
1757 |
by (blast) |
|
1758 |
with im wf ifI |
|
1759 |
obtain |
|
1760 |
imStatic: "\<not> is_static im" and |
|
1761 |
imPublic: "accmodi im = Public" |
|
1762 |
by (auto dest!: imethds_wf_mhead) |
|
1763 |
from ifI wf |
|
1764 |
have wf_I: "wf_idecl G (I,i)" |
|
1765 |
by (rule wf_prog_idecl) |
|
1766 |
with SI wf |
|
1767 |
obtain si where |
|
1768 |
ifSI: "iface G SI = Some si" and |
|
1769 |
wf_SI: "wf_idecl G (SI,si)" |
|
1770 |
by (auto dest!: wf_idecl_supD is_acc_ifaceD |
|
1771 |
dest: wf_prog_idecl) |
|
1772 |
from jm hyp |
|
1773 |
obtain sim::"qtname \<times> mhead" where |
|
1774 |
sim: "sim \<in> imethds G SI sig" and |
|
1775 |
eq_static_sim_jm: "is_static sim = is_static jm" and |
|
1776 |
eq_access_sim_jm: "accmodi sim = accmodi jm" and |
|
1777 |
resTy_widen_sim_jm: "G\<turnstile>resTy sim\<preceq>resTy jm" |
|
1778 |
by blast |
|
1779 |
with wf_I SI imdef sim |
|
1780 |
have "G\<turnstile>resTy im\<preceq>resTy sim" |
|
1781 |
by (auto dest!: wf_idecl_hidings hidings_entailsD) |
|
1782 |
with wf resTy_widen_sim_jm |
|
1783 |
have resTy_widen_im_jm: "G\<turnstile>resTy im\<preceq>resTy jm" |
|
1784 |
by (blast intro: widen_trans) |
|
1785 |
from sim wf ifSI |
|
1786 |
obtain |
|
1787 |
simStatic: "\<not> is_static sim" and |
|
1788 |
simPublic: "accmodi sim = Public" |
|
1789 |
by (auto dest!: imethds_wf_mhead) |
|
1790 |
from im |
|
1791 |
imStatic simStatic eq_static_sim_jm |
|
1792 |
imPublic simPublic eq_access_sim_jm |
|
1793 |
resTy_widen_im_jm |
|
1794 |
show ?thesis |
|
1795 |
by auto |
|
1796 |
qed |
|
1797 |
qed |
|
1798 |
qed |
|
1799 |
||
1800 |
(* Tactical version *) |
|
1801 |
(* |
|
1802 |
lemma subint_widen_imethds: "\<lbrakk>G\<turnstile>I\<preceq>I J; wf_prog G; is_iface G J\<rbrakk> \<Longrightarrow> |
|
1803 |
\<forall> jm \<in> imethds G J sig. |
|
1804 |
\<exists> im \<in> imethds G I sig. static (mthd im)=static (mthd jm) \<and> |
|
1805 |
access (mthd im)= access (mthd jm) \<and> |
|
1806 |
G\<turnstile>resTy (mthd im)\<preceq>resTy (mthd jm)" |
|
1807 |
apply (erule converse_rtrancl_induct) |
|
1808 |
apply (clarsimp elim!: bexI') |
|
1809 |
apply (frule subint1D) |
|
1810 |
apply clarify |
|
1811 |
apply (erule ballE') |
|
1812 |
apply fast |
|
1813 |
apply (erule_tac V = "?x \<in> imethds G J sig" in thin_rl) |
|
1814 |
apply clarsimp |
|
1815 |
apply (subst imethds_rec, assumption, erule wf_ws_prog) |
|
1816 |
apply (unfold overrides_t_def) |
|
1817 |
apply (drule (1) wf_prog_idecl) |
|
1818 |
apply (frule (3) imethds_wf_mhead [OF _ _ wf_idecl_supD [THEN conjunct1 |
|
1819 |
[THEN is_acc_ifaceD [THEN conjunct1]]]]) |
|
1820 |
apply (case_tac "(o2s \<circ> table_of (map (\<lambda>(s, mh). (s, y, mh)) (imethods i))) |
|
1821 |
sig ={}") |
|
1822 |
apply force |
|
1823 |
||
1824 |
apply (simp only:) |
|
1825 |
apply (simp) |
|
1826 |
apply clarify |
|
1827 |
apply (frule wf_idecl_hidings [THEN hidings_entailsD]) |
|
1828 |
apply blast |
|
1829 |
apply blast |
|
1830 |
apply (rule bexI') |
|
1831 |
apply simp |
|
1832 |
apply (drule table_of_map_SomeI [of _ "sig"]) |
|
1833 |
apply simp |
|
1834 |
||
1835 |
apply (frule wf_idecl_mhead [of _ _ _ "sig"]) |
|
1836 |
apply (rule table_of_Some_in_set) |
|
1837 |
apply assumption |
|
1838 |
apply auto |
|
1839 |
done |
|
1840 |
*) |
|
1841 |
||
1842 |
||
1843 |
(* local lemma *) |
|
1844 |
lemma implmt1_methd: |
|
1845 |
"\<And>sig. \<lbrakk>G\<turnstile>C\<leadsto>1I; wf_prog G; im \<in> imethds G I sig\<rbrakk> \<Longrightarrow> |
|
1846 |
\<exists>cm \<in>methd G C sig: \<not> is_static cm \<and> \<not> is_static im \<and> |
|
1847 |
G\<turnstile>resTy cm\<preceq>resTy im \<and> |
|
1848 |
accmodi im = Public \<and> accmodi cm = Public" |
|
1849 |
apply (drule implmt1D) |
|
1850 |
apply clarify |
|
1851 |
apply (drule (2) wf_prog_cdecl [THEN wf_cdecl_impD]) |
|
1852 |
apply (frule (1) imethds_wf_mhead) |
|
1853 |
apply (simp add: is_acc_iface_def) |
|
1854 |
apply (force) |
|
1855 |
done |
|
1856 |
||
1857 |
||
1858 |
(* local lemma *) |
|
1859 |
lemma implmt_methd [rule_format (no_asm)]: |
|
1860 |
"\<lbrakk>wf_prog G; G\<turnstile>C\<leadsto>I\<rbrakk> \<Longrightarrow> is_iface G I \<longrightarrow> |
|
1861 |
(\<forall> im \<in>imethds G I sig. |
|
1862 |
\<exists> cm\<in>methd G C sig: \<not>is_static cm \<and> \<not> is_static im \<and> |
|
1863 |
G\<turnstile>resTy cm\<preceq>resTy im \<and> |
|
1864 |
accmodi im = Public \<and> accmodi cm = Public)" |
|
1865 |
apply (frule implmt_is_class) |
|
1866 |
apply (erule implmt.induct) |
|
1867 |
apply safe |
|
1868 |
apply (drule (2) implmt1_methd) |
|
1869 |
apply fast |
|
1870 |
apply (drule (1) subint_widen_imethds) |
|
1871 |
apply simp |
|
1872 |
apply assumption |
|
1873 |
apply clarify |
|
1874 |
apply (drule (2) implmt1_methd) |
|
1875 |
apply (force) |
|
1876 |
apply (frule subcls1D) |
|
1877 |
apply (drule (1) bspec) |
|
1878 |
apply clarify |
|
1879 |
apply (drule (3) r_into_rtrancl [THEN inheritable_instance_methd_props, |
|
1880 |
OF _ implmt_is_class]) |
|
1881 |
apply auto |
|
1882 |
done |
|
1883 |
||
1884 |
lemma mheadsD [rule_format (no_asm)]: |
|
1885 |
"emh \<in> mheads G S t sig \<longrightarrow> wf_prog G \<longrightarrow> |
|
1886 |
(\<exists>C D m. t = ClassT C \<and> declrefT emh = ClassT D \<and> |
|
1887 |
accmethd G S C sig = Some m \<and> |
|
1888 |
(declclass m = D) \<and> mhead (mthd m) = (mhd emh)) \<or> |
|
1889 |
(\<exists>I. t = IfaceT I \<and> ((\<exists>im. im \<in> accimethds G (pid S) I sig \<and> |
|
1890 |
mthd im = mhd emh) \<or> |
|
1891 |
(\<exists>m. G\<turnstile>Iface I accessible_in (pid S) \<and> accmethd G S Object sig = Some m \<and> |
|
1892 |
accmodi m \<noteq> Private \<and> |
|
1893 |
declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh))) \<or> |
|
1894 |
(\<exists>T m. t = ArrayT T \<and> G\<turnstile>Array T accessible_in (pid S) \<and> |
|
1895 |
accmethd G S Object sig = Some m \<and> accmodi m \<noteq> Private \<and> |
|
1896 |
declrefT emh = ClassT Object \<and> mhead (mthd m) = mhd emh)" |
|
1897 |
apply (rule_tac "ref_ty1"="t" in ref_ty_ty.induct [THEN conjunct1]) |
|
1898 |
apply auto |
|
1899 |
apply (auto simp add: cmheads_def accObjectmheads_def Objectmheads_def) |
|
1900 |
apply (auto dest!: accmethd_SomeD) |
|
1901 |
done |
|
1902 |
||
1903 |
lemma mheads_cases [consumes 2, case_names Class_methd |
|
1904 |
Iface_methd Iface_Object_methd Array_Object_methd]: |
|
1905 |
"\<lbrakk>emh \<in> mheads G S t sig; wf_prog G; |
|
1906 |
\<And> C D m. \<lbrakk>t = ClassT C;declrefT emh = ClassT D; accmethd G S C sig = Some m; |
|
1907 |
(declclass m = D); mhead (mthd m) = (mhd emh)\<rbrakk> \<Longrightarrow> P emh; |
|
1908 |
\<And> I im. \<lbrakk>t = IfaceT I; im \<in> accimethds G (pid S) I sig; mthd im = mhd emh\<rbrakk> |
|
1909 |
\<Longrightarrow> P emh; |
|
1910 |
\<And> I m. \<lbrakk>t = IfaceT I; G\<turnstile>Iface I accessible_in (pid S); |
|
1911 |
accmethd G S Object sig = Some m; accmodi m \<noteq> Private; |
|
1912 |
declrefT emh = ClassT Object; mhead (mthd m) = mhd emh\<rbrakk> \<Longrightarrow> P emh; |
|
1913 |
\<And> T m. \<lbrakk>t = ArrayT T;G\<turnstile>Array T accessible_in (pid S); |
|
1914 |
accmethd G S Object sig = Some m; accmodi m \<noteq> Private; |
|
1915 |
declrefT emh = ClassT Object; mhead (mthd m) = mhd emh\<rbrakk> \<Longrightarrow> P emh |
|
1916 |
\<rbrakk> \<Longrightarrow> P emh" |
|
1917 |
by (blast dest!: mheadsD) |
|
1918 |
||
1919 |
lemma declclassD[rule_format]: |
|
1920 |
"\<lbrakk>wf_prog G;class G C = Some c; methd G C sig = Some m; |
|
1921 |
class G (declclass m) = Some d\<rbrakk> |
|
1922 |
\<Longrightarrow> table_of (methods d) sig = Some (mthd m)" |
|
1923 |
proof - |
|
1924 |
assume wf: "wf_prog G" |
|
1925 |
then have ws: "ws_prog G" .. |
|
1926 |
assume clsC: "class G C = Some c" |
|
1927 |
from clsC ws |
|
1928 |
show "\<And> m d. \<lbrakk>methd G C sig = Some m; class G (declclass m) = Some d\<rbrakk> |
|
1929 |
\<Longrightarrow> table_of (methods d) sig = Some (mthd m)" |
|
1930 |
(is "PROP ?P C") |
|
1931 |
proof (induct ?P C rule: ws_class_induct) |
|
1932 |
case Object |
|
1933 |
fix m d |
|
1934 |
assume "methd G Object sig = Some m" |
|
1935 |
"class G (declclass m) = Some d" |
|
1936 |
with wf show "?thesis m d" by auto |
|
1937 |
next |
|
1938 |
case Subcls |
|
1939 |
fix C c m d |
|
1940 |
assume hyp: "PROP ?P (super c)" |
|
1941 |
and m: "methd G C sig = Some m" |
|
1942 |
and declC: "class G (declclass m) = Some d" |
|
1943 |
and clsC: "class G C = Some c" |
|
1944 |
and nObj: "C \<noteq> Object" |
|
1945 |
let ?newMethods = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig" |
|
1946 |
show "?thesis m d" |
|
1947 |
proof (cases "?newMethods") |
|
1948 |
case None |
|
1949 |
from None clsC nObj ws m declC hyp |
|
1950 |
show "?thesis" by (auto simp add: methd_rec) |
|
1951 |
next |
|
1952 |
case Some |
|
1953 |
from Some clsC nObj ws m declC hyp |
|
1954 |
show "?thesis" |
|
1955 |
by (auto simp add: methd_rec |
|
1956 |
dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class) |
|
1957 |
qed |
|
1958 |
qed |
|
1959 |
qed |
|
1960 |
||
1961 |
(* Tactical version *) |
|
1962 |
(* |
|
1963 |
lemma declclassD[rule_format]: |
|
1964 |
"wf_prog G \<longrightarrow> |
|
1965 |
(\<forall> c d m. class G C = Some c \<longrightarrow> methd G C sig = Some m \<longrightarrow> |
|
1966 |
class G (declclass m) = Some d |
|
1967 |
\<longrightarrow> table_of (methods d) sig = Some (mthd m))" |
|
1968 |
apply (rule class_rec.induct) |
|
1969 |
apply (rule impI) |
|
1970 |
apply (rule allI)+ |
|
1971 |
apply (rule impI) |
|
1972 |
apply (case_tac "C=Object") |
|
1973 |
apply (force simp add: methd_rec) |
|
1974 |
||
1975 |
apply (subst methd_rec) |
|
1976 |
apply (blast dest: wf_ws_prog)+ |
|
1977 |
apply (case_tac "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c)) sig") |
|
1978 |
apply (auto dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class) |
|
1979 |
done |
|
1980 |
*) |
|
1981 |
||
1982 |
lemma dynmethd_Object: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1983 |
assumes statM: "methd G Object sig = Some statM" and |
12854 | 1984 |
private: "accmodi statM = Private" and |
1985 |
is_cls_C: "is_class G C" and |
|
1986 |
wf: "wf_prog G" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
1987 |
shows "dynmethd G Object C sig = Some statM" |
12854 | 1988 |
proof - |
1989 |
from is_cls_C wf |
|
1990 |
have subclseq: "G\<turnstile>C \<preceq>\<^sub>C Object" |
|
1991 |
by (auto intro: subcls_ObjectI) |
|
1992 |
from wf have ws: "ws_prog G" |
|
1993 |
by simp |
|
1994 |
from wf |
|
1995 |
have is_cls_Obj: "is_class G Object" |
|
1996 |
by simp |
|
1997 |
from statM subclseq is_cls_Obj ws private |
|
1998 |
show ?thesis |
|
1999 |
proof (cases rule: dynmethd_cases) |
|
2000 |
case Static then show ?thesis . |
|
2001 |
next |
|
2002 |
case Overrides |
|
2003 |
with private show ?thesis |
|
2004 |
by (auto dest: no_Private_override) |
|
2005 |
qed |
|
2006 |
qed |
|
2007 |
||
2008 |
lemma wf_imethds_hiding_objmethdsD: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2009 |
assumes old: "methd G Object sig = Some old" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2010 |
is_if_I: "is_iface G I" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2011 |
wf: "wf_prog G" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2012 |
not_private: "accmodi old \<noteq> Private" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2013 |
new: "new \<in> imethds G I sig" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2014 |
shows "G\<turnstile>resTy new\<preceq>resTy old \<and> is_static new = is_static old" (is "?P new") |
12854 | 2015 |
proof - |
2016 |
from wf have ws: "ws_prog G" by simp |
|
2017 |
{ |
|
2018 |
fix I i new |
|
2019 |
assume ifI: "iface G I = Some i" |
|
2020 |
assume new: "table_of (imethods i) sig = Some new" |
|
2021 |
from ifI new not_private wf old |
|
2022 |
have "?P (I,new)" |
|
2023 |
by (auto dest!: wf_prog_idecl wf_idecl_hiding cond_hiding_entailsD |
|
2024 |
simp del: methd_Object) |
|
2025 |
} note hyp_newmethod = this |
|
2026 |
from is_if_I ws new |
|
2027 |
show ?thesis |
|
2028 |
proof (induct rule: ws_interface_induct) |
|
2029 |
case (Step I i) |
|
2030 |
assume ifI: "iface G I = Some i" |
|
2031 |
assume new: "new \<in> imethds G I sig" |
|
2032 |
from Step |
|
2033 |
have hyp: "\<forall> J \<in> set (isuperIfs i). (new \<in> imethds G J sig \<longrightarrow> ?P new)" |
|
2034 |
by auto |
|
2035 |
from new ifI ws |
|
2036 |
show "?P new" |
|
2037 |
proof (cases rule: imethds_cases) |
|
2038 |
case NewMethod |
|
2039 |
with ifI hyp_newmethod |
|
2040 |
show ?thesis |
|
2041 |
by auto |
|
2042 |
next |
|
2043 |
case (InheritedMethod J) |
|
2044 |
assume "J \<in> set (isuperIfs i)" |
|
2045 |
"new \<in> imethds G J sig" |
|
2046 |
with hyp |
|
2047 |
show "?thesis" |
|
2048 |
by auto |
|
2049 |
qed |
|
2050 |
qed |
|
2051 |
qed |
|
2052 |
||
2053 |
text {* |
|
2054 |
Which dynamic classes are valid to look up a member of a distinct static type? |
|
2055 |
We have to distinct class members (named static members in Java) |
|
2056 |
from instance members. Class members are global to all Objects of a class, |
|
2057 |
instance members are local to a single Object instance. If a member is |
|
2058 |
equipped with the static modifier it is a class member, else it is an |
|
2059 |
instance member. |
|
2060 |
The following table gives an overview of the current framework. We assume |
|
2061 |
to have a reference with static type statT and a dynamic class dynC. Between |
|
2062 |
both of these types the widening relation holds |
|
2063 |
@{term "G\<turnstile>Class dynC\<preceq> statT"}. Unfortunately this ordinary widening relation |
|
2064 |
isn't enough to describe the valid lookup classes, since we must cope the |
|
2065 |
special cases of arrays and interfaces,too. If we statically expect an array or |
|
2066 |
inteface we may lookup a field or a method in Object which isn't covered in |
|
2067 |
the widening relation. |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2068 |
|
12854 | 2069 |
statT field instance method static (class) method |
2070 |
------------------------------------------------------------------------ |
|
2071 |
NullT / / / |
|
2072 |
Iface / dynC Object |
|
2073 |
Class dynC dynC dynC |
|
2074 |
Array / Object Object |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2075 |
|
12854 | 2076 |
In most cases we con lookup the member in the dynamic class. But as an |
2077 |
interface can't declare new static methods, nor an array can define new |
|
2078 |
methods at all, we have to lookup methods in the base class Object. |
|
2079 |
||
2080 |
The limitation to classes in the field column is artificial and comes out |
|
2081 |
of the typing rule for the field access (see rule @{text "FVar"} in the |
|
2082 |
welltyping relation @{term "wt"} in theory WellType). |
|
2083 |
I stems out of the fact, that Object |
|
2084 |
indeed has no non private fields. So interfaces and arrays can actually |
|
2085 |
have no fields at all and a field access would be senseless. (In Java |
|
2086 |
interfaces are allowed to declare new fields but in current Bali not!). |
|
2087 |
So there is no principal reason why we should not allow Objects to declare |
|
2088 |
non private fields. Then we would get the following column: |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2089 |
|
12854 | 2090 |
statT field |
2091 |
----------------- |
|
2092 |
NullT / |
|
2093 |
Iface Object |
|
2094 |
Class dynC |
|
2095 |
Array Object |
|
2096 |
*} |
|
2097 |
consts valid_lookup_cls:: "prog \<Rightarrow> ref_ty \<Rightarrow> qtname \<Rightarrow> bool \<Rightarrow> bool" |
|
2098 |
("_,_ \<turnstile> _ valid'_lookup'_cls'_for _" [61,61,61,61] 60) |
|
2099 |
primrec |
|
2100 |
"G,NullT \<turnstile> dynC valid_lookup_cls_for static_membr = False" |
|
2101 |
"G,IfaceT I \<turnstile> dynC valid_lookup_cls_for static_membr |
|
2102 |
= (if static_membr |
|
2103 |
then dynC=Object |
|
2104 |
else G\<turnstile>Class dynC\<preceq> Iface I)" |
|
2105 |
"G,ClassT C \<turnstile> dynC valid_lookup_cls_for static_membr = G\<turnstile>Class dynC\<preceq> Class C" |
|
2106 |
"G,ArrayT T \<turnstile> dynC valid_lookup_cls_for static_membr = (dynC=Object)" |
|
2107 |
||
2108 |
lemma valid_lookup_cls_is_class: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2109 |
assumes dynC: "G,statT \<turnstile> dynC valid_lookup_cls_for static_membr" and |
12854 | 2110 |
ty_statT: "isrtype G statT" and |
2111 |
wf: "wf_prog G" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2112 |
shows "is_class G dynC" |
12854 | 2113 |
proof (cases statT) |
2114 |
case NullT |
|
2115 |
with dynC ty_statT show ?thesis |
|
2116 |
by (auto dest: widen_NT2) |
|
2117 |
next |
|
2118 |
case (IfaceT I) |
|
2119 |
with dynC wf show ?thesis |
|
2120 |
by (auto dest: implmt_is_class) |
|
2121 |
next |
|
2122 |
case (ClassT C) |
|
2123 |
with dynC ty_statT show ?thesis |
|
2124 |
by (auto dest: subcls_is_class2) |
|
2125 |
next |
|
2126 |
case (ArrayT T) |
|
2127 |
with dynC wf show ?thesis |
|
2128 |
by (auto) |
|
2129 |
qed |
|
2130 |
||
2131 |
declare split_paired_All [simp del] split_paired_Ex [simp del] |
|
2132 |
ML_setup {* |
|
2133 |
simpset_ref() := simpset() delloop "split_all_tac"; |
|
2134 |
claset_ref () := claset () delSWrapper "split_all_tac" |
|
2135 |
*} |
|
2136 |
lemma dynamic_mheadsD: |
|
2137 |
"\<lbrakk>emh \<in> mheads G S statT sig; |
|
2138 |
G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh); |
|
2139 |
isrtype G statT; wf_prog G |
|
2140 |
\<rbrakk> \<Longrightarrow> \<exists>m \<in> dynlookup G statT dynC sig: |
|
2141 |
is_static m=is_static emh \<and> G\<turnstile>resTy m\<preceq>resTy emh" |
|
2142 |
proof - |
|
2143 |
assume emh: "emh \<in> mheads G S statT sig" |
|
2144 |
and wf: "wf_prog G" |
|
2145 |
and dynC_Prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh)" |
|
2146 |
and istype: "isrtype G statT" |
|
2147 |
from dynC_Prop istype wf |
|
2148 |
obtain y where |
|
2149 |
dynC: "class G dynC = Some y" |
|
2150 |
by (auto dest: valid_lookup_cls_is_class) |
|
2151 |
from emh wf show ?thesis |
|
2152 |
proof (cases rule: mheads_cases) |
|
2153 |
case Class_methd |
|
2154 |
fix statC statDeclC sm |
|
2155 |
assume statC: "statT = ClassT statC" |
|
2156 |
assume "accmethd G S statC sig = Some sm" |
|
2157 |
then have sm: "methd G statC sig = Some sm" |
|
2158 |
by (blast dest: accmethd_SomeD) |
|
2159 |
assume eq_mheads: "mhead (mthd sm) = mhd emh" |
|
2160 |
from statC |
|
2161 |
have dynlookup: "dynlookup G statT dynC sig = dynmethd G statC dynC sig" |
|
2162 |
by (simp add: dynlookup_def) |
|
2163 |
from wf statC istype dynC_Prop sm |
|
2164 |
obtain dm where |
|
2165 |
"dynmethd G statC dynC sig = Some dm" |
|
2166 |
"is_static dm = is_static sm" |
|
2167 |
"G\<turnstile>resTy dm\<preceq>resTy sm" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2168 |
by (force dest!: ws_dynmethd accmethd_SomeD) |
12854 | 2169 |
with dynlookup eq_mheads |
2170 |
show ?thesis |
|
2171 |
by (cases emh type: *) (auto) |
|
2172 |
next |
|
2173 |
case Iface_methd |
|
2174 |
fix I im |
|
2175 |
assume statI: "statT = IfaceT I" and |
|
2176 |
eq_mheads: "mthd im = mhd emh" and |
|
2177 |
"im \<in> accimethds G (pid S) I sig" |
|
2178 |
then have im: "im \<in> imethds G I sig" |
|
2179 |
by (blast dest: accimethdsD) |
|
2180 |
with istype statI eq_mheads wf |
|
2181 |
have not_static_emh: "\<not> is_static emh" |
|
2182 |
by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead) |
|
2183 |
from statI im |
|
2184 |
have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig" |
|
2185 |
by (auto simp add: dynlookup_def dynimethd_def) |
|
2186 |
from wf dynC_Prop statI istype im not_static_emh |
|
2187 |
obtain dm where |
|
2188 |
"methd G dynC sig = Some dm" |
|
2189 |
"is_static dm = is_static im" |
|
2190 |
"G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2191 |
by (force dest: implmt_methd) |
12854 | 2192 |
with dynlookup eq_mheads |
2193 |
show ?thesis |
|
2194 |
by (cases emh type: *) (auto) |
|
2195 |
next |
|
2196 |
case Iface_Object_methd |
|
2197 |
fix I sm |
|
2198 |
assume statI: "statT = IfaceT I" and |
|
2199 |
sm: "accmethd G S Object sig = Some sm" and |
|
2200 |
eq_mheads: "mhead (mthd sm) = mhd emh" and |
|
2201 |
nPriv: "accmodi sm \<noteq> Private" |
|
2202 |
show ?thesis |
|
2203 |
proof (cases "imethds G I sig = {}") |
|
2204 |
case True |
|
2205 |
with statI |
|
2206 |
have dynlookup: "dynlookup G statT dynC sig = dynmethd G Object dynC sig" |
|
2207 |
by (simp add: dynlookup_def dynimethd_def) |
|
2208 |
from wf dynC |
|
2209 |
have subclsObj: "G\<turnstile>dynC \<preceq>\<^sub>C Object" |
|
2210 |
by (auto intro: subcls_ObjectI) |
|
2211 |
from wf dynC dynC_Prop istype sm subclsObj |
|
2212 |
obtain dm where |
|
2213 |
"dynmethd G Object dynC sig = Some dm" |
|
2214 |
"is_static dm = is_static sm" |
|
2215 |
"G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd sm)" |
|
2216 |
by (auto dest!: ws_dynmethd accmethd_SomeD |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2217 |
intro: class_Object [OF wf] intro: that) |
12854 | 2218 |
with dynlookup eq_mheads |
2219 |
show ?thesis |
|
2220 |
by (cases emh type: *) (auto) |
|
2221 |
next |
|
2222 |
case False |
|
2223 |
with statI |
|
2224 |
have dynlookup: "dynlookup G statT dynC sig = methd G dynC sig" |
|
2225 |
by (simp add: dynlookup_def dynimethd_def) |
|
2226 |
from istype statI |
|
2227 |
have "is_iface G I" |
|
2228 |
by auto |
|
2229 |
with wf sm nPriv False |
|
2230 |
obtain im where |
|
2231 |
im: "im \<in> imethds G I sig" and |
|
2232 |
eq_stat: "is_static im = is_static sm" and |
|
2233 |
resProp: "G\<turnstile>resTy (mthd im)\<preceq>resTy (mthd sm)" |
|
2234 |
by (auto dest: wf_imethds_hiding_objmethdsD accmethd_SomeD) |
|
2235 |
from im wf statI istype eq_stat eq_mheads |
|
2236 |
have not_static_sm: "\<not> is_static emh" |
|
2237 |
by (cases emh) (auto dest: wf_prog_idecl imethds_wf_mhead) |
|
2238 |
from im wf dynC_Prop dynC istype statI not_static_sm |
|
2239 |
obtain dm where |
|
2240 |
"methd G dynC sig = Some dm" |
|
2241 |
"is_static dm = is_static im" |
|
2242 |
"G\<turnstile>resTy (mthd dm)\<preceq>resTy (mthd im)" |
|
2243 |
by (auto dest: implmt_methd) |
|
2244 |
with wf eq_stat resProp dynlookup eq_mheads |
|
2245 |
show ?thesis |
|
2246 |
by (cases emh type: *) (auto intro: widen_trans) |
|
2247 |
qed |
|
2248 |
next |
|
2249 |
case Array_Object_methd |
|
2250 |
fix T sm |
|
2251 |
assume statArr: "statT = ArrayT T" and |
|
2252 |
sm: "accmethd G S Object sig = Some sm" and |
|
2253 |
eq_mheads: "mhead (mthd sm) = mhd emh" |
|
2254 |
from statArr dynC_Prop wf |
|
2255 |
have dynlookup: "dynlookup G statT dynC sig = methd G Object sig" |
|
2256 |
by (auto simp add: dynlookup_def dynmethd_C_C) |
|
2257 |
with sm eq_mheads sm |
|
2258 |
show ?thesis |
|
2259 |
by (cases emh type: *) (auto dest: accmethd_SomeD) |
|
2260 |
qed |
|
2261 |
qed |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2262 |
declare split_paired_All [simp] split_paired_Ex [simp] |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2263 |
ML_setup {* |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2264 |
claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac); |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2265 |
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2266 |
*} |
12854 | 2267 |
|
2268 |
(* Tactical version *) |
|
2269 |
(* |
|
2270 |
lemma dynamic_mheadsD: " |
|
2271 |
\<lbrakk>emh \<in> mheads G S statT sig; wf_prog G; class G dynC = Some y; |
|
2272 |
if (\<exists>T. statT=ArrayT T) then dynC=Object else G\<turnstile>Class dynC\<preceq>RefT statT; |
|
2273 |
isrtype G statT\<rbrakk> \<Longrightarrow> |
|
2274 |
\<exists>m \<in> dynlookup G statT dynC sig: |
|
2275 |
static (mthd m)=static (mhd emh) \<and> G\<turnstile>resTy (mthd m)\<preceq>resTy (mhd emh)" |
|
2276 |
apply (drule mheadsD) |
|
2277 |
apply safe |
|
2278 |
-- reftype statT is a class |
|
2279 |
apply (case_tac "\<exists>T. ClassT C = ArrayT T") |
|
2280 |
apply (simp) |
|
2281 |
||
2282 |
apply (clarsimp simp add: dynlookup_def ) |
|
2283 |
apply (frule_tac statC="C" and dynC="dynC" and sig="sig" |
|
2284 |
in ws_dynmethd) |
|
2285 |
apply assumption+ |
|
2286 |
apply (case_tac "emh") |
|
2287 |
apply (force dest: accmethd_SomeD) |
|
2288 |
||
2289 |
-- reftype statT is a interface, method defined in interface |
|
2290 |
apply (clarsimp simp add: dynlookup_def) |
|
2291 |
apply (drule (1) implmt_methd) |
|
2292 |
apply blast |
|
2293 |
apply blast |
|
2294 |
apply (clarify) |
|
2295 |
apply (unfold dynimethd_def) |
|
2296 |
apply (rule_tac x="cm" in bexI) |
|
2297 |
apply (case_tac "emh") |
|
2298 |
apply force |
|
2299 |
||
2300 |
apply force |
|
2301 |
||
2302 |
-- reftype statT is a interface, method defined in Object |
|
2303 |
apply (simp add: dynlookup_def) |
|
2304 |
apply (simp only: dynimethd_def) |
|
2305 |
apply (case_tac "imethds G I sig = {}") |
|
2306 |
apply simp |
|
2307 |
apply (frule_tac statC="Object" and dynC="dynC" and sig="sig" |
|
2308 |
in ws_dynmethd) |
|
2309 |
apply (blast intro: subcls_ObjectI wf_ws_prog) |
|
2310 |
apply (blast dest: class_Object) |
|
2311 |
apply (case_tac "emh") |
|
2312 |
apply (force dest: accmethd_SomeD) |
|
2313 |
||
2314 |
apply simp |
|
2315 |
apply (subgoal_tac "\<exists> im. im \<in> imethds G I sig") |
|
2316 |
prefer 2 apply blast |
|
2317 |
apply clarify |
|
2318 |
apply (frule (1) implmt_methd) |
|
2319 |
apply simp |
|
2320 |
apply blast |
|
2321 |
apply (clarify dest!: accmethd_SomeD) |
|
2322 |
apply (frule (4) iface_overrides_Object) |
|
2323 |
apply clarify |
|
2324 |
apply (case_tac emh) |
|
2325 |
apply force |
|
2326 |
||
2327 |
-- reftype statT is a array |
|
2328 |
apply (simp add: dynlookup_def) |
|
2329 |
apply (case_tac emh) |
|
2330 |
apply (force dest: accmethd_SomeD simp add: dynmethd_def) |
|
2331 |
done |
|
2332 |
*) |
|
2333 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2334 |
(* FIXME occasionally convert to ws_class_induct*) |
12854 | 2335 |
lemma methd_declclass: |
2336 |
"\<lbrakk>class G C = Some c; wf_prog G; methd G C sig = Some m\<rbrakk> |
|
2337 |
\<Longrightarrow> methd G (declclass m) sig = Some m" |
|
2338 |
proof - |
|
2339 |
assume asm: "class G C = Some c" "wf_prog G" "methd G C sig = Some m" |
|
2340 |
have "wf_prog G \<longrightarrow> |
|
2341 |
(\<forall> c m. class G C = Some c \<longrightarrow> methd G C sig = Some m |
|
2342 |
\<longrightarrow> methd G (declclass m) sig = Some m)" (is "?P G C") |
|
2343 |
proof (rule class_rec.induct,intro allI impI) |
|
2344 |
fix G C c m |
|
2345 |
assume hyp: "\<forall>c. C \<noteq> Object \<and> ws_prog G \<and> class G C = Some c \<longrightarrow> |
|
2346 |
?P G (super c)" |
|
2347 |
assume wf: "wf_prog G" and cls_C: "class G C = Some c" and |
|
2348 |
m: "methd G C sig = Some m" |
|
2349 |
show "methd G (declclass m) sig = Some m" |
|
2350 |
proof (cases "C=Object") |
|
2351 |
case True |
|
2352 |
with wf m show ?thesis by (auto intro: table_of_map_SomeI) |
|
2353 |
next |
|
2354 |
let ?filter="filter_tab (\<lambda>sig m. G\<turnstile>C inherits method sig m)" |
|
2355 |
let ?table = "table_of (map (\<lambda>(s, m). (s, C, m)) (methods c))" |
|
2356 |
case False |
|
2357 |
with cls_C wf m |
|
2358 |
have methd_C: "(?filter (methd G (super c)) ++ ?table) sig = Some m " |
|
2359 |
by (simp add: methd_rec) |
|
2360 |
show ?thesis |
|
2361 |
proof (cases "?table sig") |
|
2362 |
case None |
|
2363 |
from this methd_C have "?filter (methd G (super c)) sig = Some m" |
|
2364 |
by simp |
|
2365 |
moreover |
|
2366 |
from wf cls_C False obtain sup where "class G (super c) = Some sup" |
|
2367 |
by (blast dest: wf_prog_cdecl wf_cdecl_supD is_acc_class_is_class) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2368 |
moreover note wf False cls_C |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2369 |
ultimately show ?thesis by (auto intro: hyp [rule_format]) |
12854 | 2370 |
next |
2371 |
case Some |
|
2372 |
from this methd_C m show ?thesis by auto |
|
2373 |
qed |
|
2374 |
qed |
|
2375 |
qed |
|
2376 |
with asm show ?thesis by auto |
|
2377 |
qed |
|
2378 |
||
2379 |
lemma dynmethd_declclass: |
|
2380 |
"\<lbrakk>dynmethd G statC dynC sig = Some m; |
|
2381 |
wf_prog G; is_class G statC |
|
2382 |
\<rbrakk> \<Longrightarrow> methd G (declclass m) sig = Some m" |
|
2383 |
by (auto dest: dynmethd_declC) |
|
2384 |
||
2385 |
lemma dynlookup_declC: |
|
2386 |
"\<lbrakk>dynlookup G statT dynC sig = Some m; wf_prog G; |
|
2387 |
is_class G dynC;isrtype G statT |
|
2388 |
\<rbrakk> \<Longrightarrow> G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m)" |
|
2389 |
by (cases "statT") |
|
2390 |
(auto simp add: dynlookup_def dynimethd_def |
|
2391 |
dest: methd_declC dynmethd_declC) |
|
2392 |
||
2393 |
lemma dynlookup_Array_declclassD [simp]: |
|
2394 |
"\<lbrakk>dynlookup G (ArrayT T) Object sig = Some dm;wf_prog G\<rbrakk> |
|
2395 |
\<Longrightarrow> declclass dm = Object" |
|
2396 |
proof - |
|
2397 |
assume dynL: "dynlookup G (ArrayT T) Object sig = Some dm" |
|
2398 |
assume wf: "wf_prog G" |
|
2399 |
from wf have ws: "ws_prog G" by auto |
|
2400 |
from wf have is_cls_Obj: "is_class G Object" by auto |
|
2401 |
from dynL wf |
|
2402 |
show ?thesis |
|
2403 |
by (auto simp add: dynlookup_def dynmethd_C_C [OF is_cls_Obj ws] |
|
2404 |
dest: methd_Object_SomeD) |
|
2405 |
qed |
|
2406 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2407 |
|
12854 | 2408 |
declare split_paired_All [simp del] split_paired_Ex [simp del] |
2409 |
ML_setup {* |
|
2410 |
simpset_ref() := simpset() delloop "split_all_tac"; |
|
2411 |
claset_ref () := claset () delSWrapper "split_all_tac" |
|
2412 |
*} |
|
2413 |
lemma wt_is_type: "E,dt\<Turnstile>v\<Colon>T \<Longrightarrow> wf_prog (prg E) \<longrightarrow> |
|
2414 |
dt=empty_dt \<longrightarrow> (case T of |
|
2415 |
Inl T \<Rightarrow> is_type (prg E) T |
|
2416 |
| Inr Ts \<Rightarrow> Ball (set Ts) (is_type (prg E)))" |
|
2417 |
apply (unfold empty_dt_def) |
|
2418 |
apply (erule wt.induct) |
|
2419 |
apply (auto split del: split_if_asm simp del: snd_conv |
|
2420 |
simp add: is_acc_class_def is_acc_type_def) |
|
2421 |
apply (erule typeof_empty_is_type) |
|
2422 |
apply (frule (1) wf_prog_cdecl [THEN wf_cdecl_supD], rotate_tac -1, |
|
2423 |
force simp del: snd_conv, clarsimp simp add: is_acc_class_def) |
|
2424 |
apply (drule (1) max_spec2mheads [THEN conjunct1, THEN mheadsD]) |
|
2425 |
apply (drule_tac [2] accfield_fields) |
|
2426 |
apply (frule class_Object) |
|
2427 |
apply (auto dest: accmethd_rT_is_type |
|
2428 |
imethds_wf_mhead [THEN conjunct1, THEN rT_is_acc_type] |
|
2429 |
dest!:accimethdsD |
|
2430 |
simp del: class_Object |
|
2431 |
simp add: is_acc_type_def |
|
2432 |
) |
|
2433 |
done |
|
2434 |
declare split_paired_All [simp] split_paired_Ex [simp] |
|
2435 |
ML_setup {* |
|
2436 |
claset_ref() := claset() addSbefore ("split_all_tac", split_all_tac); |
|
2437 |
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) |
|
2438 |
*} |
|
2439 |
||
2440 |
lemma ty_expr_is_type: |
|
2441 |
"\<lbrakk>E\<turnstile>e\<Colon>-T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T" |
|
2442 |
by (auto dest!: wt_is_type) |
|
2443 |
lemma ty_var_is_type: |
|
2444 |
"\<lbrakk>E\<turnstile>v\<Colon>=T; wf_prog (prg E)\<rbrakk> \<Longrightarrow> is_type (prg E) T" |
|
2445 |
by (auto dest!: wt_is_type) |
|
2446 |
lemma ty_exprs_is_type: |
|
2447 |
"\<lbrakk>E\<turnstile>es\<Colon>\<doteq>Ts; wf_prog (prg E)\<rbrakk> \<Longrightarrow> Ball (set Ts) (is_type (prg E))" |
|
2448 |
by (auto dest!: wt_is_type) |
|
2449 |
||
2450 |
||
2451 |
lemma static_mheadsD: |
|
2452 |
"\<lbrakk> emh \<in> mheads G S t sig; wf_prog G; E\<turnstile>e\<Colon>-RefT t; prg E=G ; |
|
2453 |
invmode (mhd emh) e \<noteq> IntVir |
|
2454 |
\<rbrakk> \<Longrightarrow> \<exists>m. ( (\<exists> C. t = ClassT C \<and> accmethd G S C sig = Some m) |
|
2455 |
\<or> (\<forall> C. t \<noteq> ClassT C \<and> accmethd G S Object sig = Some m )) \<and> |
|
2456 |
declrefT emh = ClassT (declclass m) \<and> mhead (mthd m) = (mhd emh)" |
|
2457 |
apply (subgoal_tac "is_static emh \<or> e = Super") |
|
2458 |
defer apply (force simp add: invmode_def) |
|
2459 |
apply (frule ty_expr_is_type) |
|
2460 |
apply simp |
|
2461 |
apply (case_tac "is_static emh") |
|
2462 |
apply (frule (1) mheadsD) |
|
2463 |
apply clarsimp |
|
2464 |
apply safe |
|
2465 |
apply blast |
|
2466 |
apply (auto dest!: imethds_wf_mhead |
|
2467 |
accmethd_SomeD |
|
2468 |
accimethdsD |
|
2469 |
simp add: accObjectmheads_def Objectmheads_def) |
|
2470 |
||
2471 |
apply (erule wt_elim_cases) |
|
2472 |
apply (force simp add: cmheads_def) |
|
2473 |
done |
|
2474 |
||
2475 |
lemma wt_MethdI: |
|
2476 |
"\<lbrakk>methd G C sig = Some m; wf_prog G; |
|
2477 |
class G C = Some c\<rbrakk> \<Longrightarrow> |
|
2478 |
\<exists>T. \<lparr>prg=G,cls=(declclass m), |
|
2479 |
lcl=\<lambda> k. |
|
2480 |
(case k of |
|
2481 |
EName e |
|
2482 |
\<Rightarrow> (case e of |
|
2483 |
VNam v |
|
2484 |
\<Rightarrow> (table_of (lcls (mbody (mthd m))) |
|
2485 |
((pars (mthd m))[\<mapsto>](parTs sig))) v |
|
2486 |
| Res \<Rightarrow> Some (resTy (mthd m))) |
|
2487 |
| This \<Rightarrow> if is_static m then None else Some (Class (declclass m))) |
|
2488 |
\<rparr>\<turnstile> Methd C sig\<Colon>-T \<and> G\<turnstile>T\<preceq>resTy m" |
|
2489 |
apply (frule (2) methd_wf_mdecl, clarify) |
|
2490 |
apply (force dest!: wf_mdecl_bodyD intro!: wt.Methd) |
|
2491 |
done |
|
2492 |
||
2493 |
subsection "accessibility concerns" |
|
2494 |
||
2495 |
lemma mheads_type_accessible: |
|
2496 |
"\<lbrakk>emh \<in> mheads G S T sig; wf_prog G\<rbrakk> |
|
2497 |
\<Longrightarrow> G\<turnstile>RefT T accessible_in (pid S)" |
|
2498 |
by (erule mheads_cases) |
|
2499 |
(auto dest: accmethd_SomeD accessible_from_commonD accimethdsD) |
|
2500 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2501 |
lemma static_to_dynamic_accessible_from_aux: |
12854 | 2502 |
"\<lbrakk>G\<turnstile>m of C accessible_from accC;wf_prog G\<rbrakk> |
2503 |
\<Longrightarrow> G\<turnstile>m in C dyn_accessible_from accC" |
|
2504 |
proof (induct rule: accessible_fromR.induct) |
|
2505 |
qed (auto intro: dyn_accessible_fromR.intros |
|
2506 |
member_of_to_member_in |
|
2507 |
static_to_dynamic_overriding) |
|
2508 |
||
2509 |
lemma static_to_dynamic_accessible_from: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2510 |
assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and |
12854 | 2511 |
subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and |
2512 |
wf: "wf_prog G" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2513 |
shows "G\<turnstile>m in dynC dyn_accessible_from accC" |
12854 | 2514 |
proof - |
2515 |
from stat_acc subclseq |
|
2516 |
show ?thesis (is "?Dyn_accessible m") |
|
2517 |
proof (induct rule: accessible_fromR.induct) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2518 |
case (Immediate statC m) |
12854 | 2519 |
then show "?Dyn_accessible m" |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2520 |
by (blast intro: dyn_accessible_fromR.Immediate |
12854 | 2521 |
member_inI |
2522 |
permits_acc_inheritance) |
|
2523 |
next |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2524 |
case (Overriding _ _ m) |
12854 | 2525 |
with wf show "?Dyn_accessible m" |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2526 |
by (blast intro: dyn_accessible_fromR.Overriding |
12854 | 2527 |
member_inI |
2528 |
static_to_dynamic_overriding |
|
2529 |
rtrancl_trancl_trancl |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2530 |
static_to_dynamic_accessible_from_aux) |
12854 | 2531 |
qed |
2532 |
qed |
|
2533 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2534 |
lemma static_to_dynamic_accessible_from_static: |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2535 |
assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2536 |
static: "is_static m" and |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2537 |
wf: "wf_prog G" |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2538 |
shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC" |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2539 |
proof - |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2540 |
from stat_acc wf |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2541 |
have "G\<turnstile>m in statC dyn_accessible_from accC" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2542 |
by (auto intro: static_to_dynamic_accessible_from) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2543 |
from this static |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2544 |
show ?thesis |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2545 |
by (rule dyn_accessible_from_static_declC) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2546 |
qed |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2547 |
|
12854 | 2548 |
lemma dynmethd_member_in: |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2549 |
assumes m: "dynmethd G statC dynC sig = Some m" and |
12854 | 2550 |
iscls_statC: "is_class G statC" and |
2551 |
wf: "wf_prog G" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2552 |
shows "G\<turnstile>Methd sig m member_in dynC" |
12854 | 2553 |
proof - |
2554 |
from m |
|
2555 |
have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" |
|
2556 |
by (auto simp add: dynmethd_def) |
|
2557 |
from subclseq iscls_statC |
|
2558 |
have iscls_dynC: "is_class G dynC" |
|
2559 |
by (rule subcls_is_class2) |
|
2560 |
from iscls_dynC iscls_statC wf m |
|
2561 |
have "G\<turnstile>dynC \<preceq>\<^sub>C (declclass m) \<and> is_class G (declclass m) \<and> |
|
2562 |
methd G (declclass m) sig = Some m" |
|
2563 |
by - (drule dynmethd_declC, auto) |
|
2564 |
with wf |
|
2565 |
show ?thesis |
|
2566 |
by (auto intro: member_inI dest: methd_member_of) |
|
2567 |
qed |
|
2568 |
||
2569 |
lemma dynmethd_access_prop: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2570 |
assumes statM: "methd G statC sig = Some statM" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2571 |
stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2572 |
dynM: "dynmethd G statC dynC sig = Some dynM" and |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2573 |
wf: "wf_prog G" |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2574 |
shows "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC" |
12854 | 2575 |
proof - |
2576 |
from wf have ws: "ws_prog G" .. |
|
2577 |
from dynM |
|
2578 |
have subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" |
|
2579 |
by (auto simp add: dynmethd_def) |
|
2580 |
from stat_acc |
|
2581 |
have is_cls_statC: "is_class G statC" |
|
2582 |
by (auto dest: accessible_from_commonD member_of_is_classD) |
|
2583 |
with subclseq |
|
2584 |
have is_cls_dynC: "is_class G dynC" |
|
2585 |
by (rule subcls_is_class2) |
|
2586 |
from is_cls_statC statM wf |
|
2587 |
have member_statC: "G\<turnstile>Methd sig statM member_of statC" |
|
2588 |
by (auto intro: methd_member_of) |
|
2589 |
from stat_acc |
|
2590 |
have statC_acc: "G\<turnstile>Class statC accessible_in (pid accC)" |
|
2591 |
by (auto dest: accessible_from_commonD) |
|
2592 |
from statM subclseq is_cls_statC ws |
|
2593 |
show ?thesis |
|
2594 |
proof (cases rule: dynmethd_cases) |
|
2595 |
case Static |
|
2596 |
assume dynmethd: "dynmethd G statC dynC sig = Some statM" |
|
2597 |
with dynM have eq_dynM_statM: "dynM=statM" |
|
2598 |
by simp |
|
2599 |
with stat_acc subclseq wf |
|
2600 |
show ?thesis |
|
2601 |
by (auto intro: static_to_dynamic_accessible_from) |
|
2602 |
next |
|
2603 |
case (Overrides newM) |
|
2604 |
assume dynmethd: "dynmethd G statC dynC sig = Some newM" |
|
2605 |
assume override: "G,sig\<turnstile>newM overrides statM" |
|
2606 |
assume neq: "newM\<noteq>statM" |
|
2607 |
from dynmethd dynM |
|
2608 |
have eq_dynM_newM: "dynM=newM" |
|
2609 |
by simp |
|
2610 |
from dynmethd eq_dynM_newM wf is_cls_statC |
|
2611 |
have "G\<turnstile>Methd sig dynM member_in dynC" |
|
2612 |
by (auto intro: dynmethd_member_in) |
|
2613 |
moreover |
|
2614 |
from subclseq |
|
2615 |
have "G\<turnstile>dynC\<prec>\<^sub>C statC" |
|
2616 |
proof (cases rule: subclseq_cases) |
|
2617 |
case Eq |
|
2618 |
assume "dynC=statC" |
|
2619 |
moreover |
|
2620 |
from is_cls_statC obtain c |
|
2621 |
where "class G statC = Some c" |
|
2622 |
by auto |
|
2623 |
moreover |
|
2624 |
note statM ws dynmethd |
|
2625 |
ultimately |
|
2626 |
have "newM=statM" |
|
2627 |
by (auto simp add: dynmethd_C_C) |
|
2628 |
with neq show ?thesis |
|
2629 |
by (contradiction) |
|
2630 |
next |
|
2631 |
case Subcls show ?thesis . |
|
2632 |
qed |
|
2633 |
moreover |
|
2634 |
from stat_acc wf |
|
2635 |
have "G\<turnstile>Methd sig statM in statC dyn_accessible_from accC" |
|
2636 |
by (blast intro: static_to_dynamic_accessible_from) |
|
2637 |
moreover |
|
2638 |
note override eq_dynM_newM |
|
2639 |
ultimately show ?thesis |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2640 |
by (cases dynM,cases statM) (auto intro: dyn_accessible_fromR.Overriding) |
12854 | 2641 |
qed |
2642 |
qed |
|
2643 |
||
2644 |
lemma implmt_methd_access: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2645 |
fixes accC::qtname |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2646 |
assumes iface_methd: "imethds G I sig \<noteq> {}" and |
12854 | 2647 |
implements: "G\<turnstile>dynC\<leadsto>I" and |
2648 |
isif_I: "is_iface G I" and |
|
2649 |
wf: "wf_prog G" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2650 |
shows "\<exists> dynM. methd G dynC sig = Some dynM \<and> |
12854 | 2651 |
G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC" |
2652 |
proof - |
|
2653 |
from implements |
|
2654 |
have iscls_dynC: "is_class G dynC" by (rule implmt_is_class) |
|
2655 |
from iface_methd |
|
2656 |
obtain im |
|
2657 |
where "im \<in> imethds G I sig" |
|
2658 |
by auto |
|
2659 |
with wf implements isif_I |
|
2660 |
obtain dynM |
|
2661 |
where dynM: "methd G dynC sig = Some dynM" and |
|
2662 |
pub: "accmodi dynM = Public" |
|
2663 |
by (blast dest: implmt_methd) |
|
2664 |
with iscls_dynC wf |
|
2665 |
have "G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2666 |
by (auto intro!: dyn_accessible_fromR.Immediate |
12854 | 2667 |
intro: methd_member_of member_of_to_member_in |
2668 |
simp add: permits_acc_def) |
|
2669 |
with dynM |
|
2670 |
show ?thesis |
|
2671 |
by blast |
|
2672 |
qed |
|
2673 |
||
2674 |
corollary implmt_dynimethd_access: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2675 |
fixes accC::qtname |
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2676 |
assumes iface_methd: "imethds G I sig \<noteq> {}" and |
12854 | 2677 |
implements: "G\<turnstile>dynC\<leadsto>I" and |
2678 |
isif_I: "is_iface G I" and |
|
2679 |
wf: "wf_prog G" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2680 |
shows "\<exists> dynM. dynimethd G I dynC sig = Some dynM \<and> |
12854 | 2681 |
G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC" |
2682 |
proof - |
|
2683 |
from iface_methd |
|
2684 |
have "dynimethd G I dynC sig = methd G dynC sig" |
|
2685 |
by (simp add: dynimethd_def) |
|
2686 |
with iface_methd implements isif_I wf |
|
2687 |
show ?thesis |
|
2688 |
by (simp only:) |
|
2689 |
(blast intro: implmt_methd_access) |
|
2690 |
qed |
|
2691 |
||
2692 |
lemma dynlookup_access_prop: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2693 |
assumes emh: "emh \<in> mheads G accC statT sig" and |
12854 | 2694 |
dynM: "dynlookup G statT dynC sig = Some dynM" and |
2695 |
dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for is_static emh" and |
|
2696 |
isT_statT: "isrtype G statT" and |
|
2697 |
wf: "wf_prog G" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2698 |
shows "G \<turnstile>Methd sig dynM in dynC dyn_accessible_from accC" |
12854 | 2699 |
proof - |
2700 |
from emh wf |
|
2701 |
have statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)" |
|
2702 |
by (rule mheads_type_accessible) |
|
2703 |
from dynC_prop isT_statT wf |
|
2704 |
have iscls_dynC: "is_class G dynC" |
|
2705 |
by (rule valid_lookup_cls_is_class) |
|
2706 |
from emh dynC_prop isT_statT wf dynM |
|
2707 |
have eq_static: "is_static emh = is_static dynM" |
|
2708 |
by (auto dest: dynamic_mheadsD) |
|
2709 |
from emh wf show ?thesis |
|
2710 |
proof (cases rule: mheads_cases) |
|
2711 |
case (Class_methd statC _ statM) |
|
2712 |
assume statT: "statT = ClassT statC" |
|
2713 |
assume "accmethd G accC statC sig = Some statM" |
|
2714 |
then have statM: "methd G statC sig = Some statM" and |
|
2715 |
stat_acc: "G\<turnstile>Methd sig statM of statC accessible_from accC" |
|
2716 |
by (auto dest: accmethd_SomeD) |
|
2717 |
from dynM statT |
|
2718 |
have dynM': "dynmethd G statC dynC sig = Some dynM" |
|
2719 |
by (simp add: dynlookup_def) |
|
2720 |
from statM stat_acc wf dynM' |
|
2721 |
show ?thesis |
|
2722 |
by (auto dest!: dynmethd_access_prop) |
|
2723 |
next |
|
2724 |
case (Iface_methd I im) |
|
2725 |
then have iface_methd: "imethds G I sig \<noteq> {}" and |
|
2726 |
statT_acc: "G\<turnstile>RefT statT accessible_in (pid accC)" |
|
2727 |
by (auto dest: accimethdsD) |
|
2728 |
assume statT: "statT = IfaceT I" |
|
2729 |
assume im: "im \<in> accimethds G (pid accC) I sig" |
|
2730 |
assume eq_mhds: "mthd im = mhd emh" |
|
2731 |
from dynM statT |
|
2732 |
have dynM': "dynimethd G I dynC sig = Some dynM" |
|
2733 |
by (simp add: dynlookup_def) |
|
2734 |
from isT_statT statT |
|
2735 |
have isif_I: "is_iface G I" |
|
2736 |
by simp |
|
2737 |
show ?thesis |
|
2738 |
proof (cases "is_static emh") |
|
2739 |
case False |
|
2740 |
with statT dynC_prop |
|
2741 |
have widen_dynC: "G\<turnstile>Class dynC \<preceq> RefT statT" |
|
2742 |
by simp |
|
2743 |
from statT widen_dynC |
|
2744 |
have implmnt: "G\<turnstile>dynC\<leadsto>I" |
|
2745 |
by auto |
|
2746 |
from eq_static False |
|
2747 |
have not_static_dynM: "\<not> is_static dynM" |
|
2748 |
by simp |
|
2749 |
from iface_methd implmnt isif_I wf dynM' |
|
2750 |
show ?thesis |
|
2751 |
by - (drule implmt_dynimethd_access, auto) |
|
2752 |
next |
|
2753 |
case True |
|
2754 |
assume "is_static emh" |
|
2755 |
moreover |
|
2756 |
from wf isT_statT statT im |
|
2757 |
have "\<not> is_static im" |
|
2758 |
by (auto dest: accimethdsD wf_prog_idecl imethds_wf_mhead) |
|
2759 |
moreover note eq_mhds |
|
2760 |
ultimately show ?thesis |
|
2761 |
by (cases emh) auto |
|
2762 |
qed |
|
2763 |
next |
|
2764 |
case (Iface_Object_methd I statM) |
|
2765 |
assume statT: "statT = IfaceT I" |
|
2766 |
assume "accmethd G accC Object sig = Some statM" |
|
2767 |
then have statM: "methd G Object sig = Some statM" and |
|
2768 |
stat_acc: "G\<turnstile>Methd sig statM of Object accessible_from accC" |
|
2769 |
by (auto dest: accmethd_SomeD) |
|
2770 |
assume not_Private_statM: "accmodi statM \<noteq> Private" |
|
2771 |
assume eq_mhds: "mhead (mthd statM) = mhd emh" |
|
2772 |
from iscls_dynC wf |
|
2773 |
have widen_dynC_Obj: "G\<turnstile>dynC \<preceq>\<^sub>C Object" |
|
2774 |
by (auto intro: subcls_ObjectI) |
|
2775 |
show ?thesis |
|
2776 |
proof (cases "imethds G I sig = {}") |
|
2777 |
case True |
|
2778 |
from dynM statT True |
|
2779 |
have dynM': "dynmethd G Object dynC sig = Some dynM" |
|
2780 |
by (simp add: dynlookup_def dynimethd_def) |
|
2781 |
from statT |
|
2782 |
have "G\<turnstile>RefT statT \<preceq>Class Object" |
|
2783 |
by auto |
|
2784 |
with statM statT_acc stat_acc widen_dynC_Obj statT isT_statT |
|
2785 |
wf dynM' eq_static dynC_prop |
|
2786 |
show ?thesis |
|
2787 |
by - (drule dynmethd_access_prop,force+) |
|
2788 |
next |
|
2789 |
case False |
|
2790 |
then obtain im where |
|
2791 |
im: "im \<in> imethds G I sig" |
|
2792 |
by auto |
|
2793 |
have not_static_emh: "\<not> is_static emh" |
|
2794 |
proof - |
|
2795 |
from im statM statT isT_statT wf not_Private_statM |
|
2796 |
have "is_static im = is_static statM" |
|
2797 |
by (auto dest: wf_imethds_hiding_objmethdsD) |
|
2798 |
with wf isT_statT statT im |
|
2799 |
have "\<not> is_static statM" |
|
2800 |
by (auto dest: wf_prog_idecl imethds_wf_mhead) |
|
2801 |
with eq_mhds |
|
2802 |
show ?thesis |
|
2803 |
by (cases emh) auto |
|
2804 |
qed |
|
2805 |
with statT dynC_prop |
|
2806 |
have implmnt: "G\<turnstile>dynC\<leadsto>I" |
|
2807 |
by simp |
|
2808 |
with isT_statT statT |
|
2809 |
have isif_I: "is_iface G I" |
|
2810 |
by simp |
|
2811 |
from dynM statT |
|
2812 |
have dynM': "dynimethd G I dynC sig = Some dynM" |
|
2813 |
by (simp add: dynlookup_def) |
|
2814 |
from False implmnt isif_I wf dynM' |
|
2815 |
show ?thesis |
|
2816 |
by - (drule implmt_dynimethd_access, auto) |
|
2817 |
qed |
|
2818 |
next |
|
2819 |
case (Array_Object_methd T statM) |
|
2820 |
assume statT: "statT = ArrayT T" |
|
2821 |
assume "accmethd G accC Object sig = Some statM" |
|
2822 |
then have statM: "methd G Object sig = Some statM" and |
|
2823 |
stat_acc: "G\<turnstile>Methd sig statM of Object accessible_from accC" |
|
2824 |
by (auto dest: accmethd_SomeD) |
|
2825 |
from statT dynC_prop |
|
2826 |
have dynC_Obj: "dynC = Object" |
|
2827 |
by simp |
|
2828 |
then |
|
2829 |
have widen_dynC_Obj: "G\<turnstile>Class dynC \<preceq> Class Object" |
|
2830 |
by simp |
|
2831 |
from dynM statT |
|
2832 |
have dynM': "dynmethd G Object dynC sig = Some dynM" |
|
2833 |
by (simp add: dynlookup_def) |
|
2834 |
from statM statT_acc stat_acc dynM' wf widen_dynC_Obj |
|
2835 |
statT isT_statT |
|
2836 |
show ?thesis |
|
2837 |
by - (drule dynmethd_access_prop, simp+) |
|
2838 |
qed |
|
2839 |
qed |
|
2840 |
||
2841 |
lemma dynlookup_access: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2842 |
assumes emh: "emh \<in> mheads G accC statT sig" and |
12854 | 2843 |
dynC_prop: "G,statT \<turnstile> dynC valid_lookup_cls_for (is_static emh) " and |
2844 |
isT_statT: "isrtype G statT" and |
|
2845 |
wf: "wf_prog G" |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2846 |
shows "\<exists> dynM. dynlookup G statT dynC sig = Some dynM \<and> |
12854 | 2847 |
G\<turnstile>Methd sig dynM in dynC dyn_accessible_from accC" |
2848 |
proof - |
|
2849 |
from dynC_prop isT_statT wf |
|
2850 |
have is_cls_dynC: "is_class G dynC" |
|
2851 |
by (auto dest: valid_lookup_cls_is_class) |
|
2852 |
with emh wf dynC_prop isT_statT |
|
2853 |
obtain dynM where |
|
2854 |
"dynlookup G statT dynC sig = Some dynM" |
|
2855 |
by - (drule dynamic_mheadsD,auto) |
|
2856 |
with emh dynC_prop isT_statT wf |
|
2857 |
show ?thesis |
|
2858 |
by (blast intro: dynlookup_access_prop) |
|
2859 |
qed |
|
2860 |
||
2861 |
lemma stat_overrides_Package_old: |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2862 |
assumes stat_override: "G \<turnstile> new overrides\<^sub>S old" and |
12854 | 2863 |
accmodi_new: "accmodi new = Package" and |
2864 |
wf: "wf_prog G " |
|
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2865 |
shows "accmodi old = Package" |
12854 | 2866 |
proof - |
2867 |
from stat_override wf |
|
2868 |
have "accmodi old \<le> accmodi new" |
|
2869 |
by (auto dest: wf_prog_stat_overridesD) |
|
2870 |
with stat_override accmodi_new show ?thesis |
|
2871 |
by (cases "accmodi old") (auto dest: no_Private_stat_override |
|
2872 |
dest: acc_modi_le_Dests) |
|
2873 |
qed |
|
2874 |
||
2875 |
text {* @{text dyn_accessible_Package} only works with the @{text wf_prog} assumption. |
|
2876 |
Without it. it is easy to leaf the Package! |
|
2877 |
*} |
|
2878 |
lemma dyn_accessible_Package: |
|
2879 |
"\<lbrakk>G \<turnstile> m in C dyn_accessible_from accC; accmodi m = Package; |
|
2880 |
wf_prog G\<rbrakk> |
|
2881 |
\<Longrightarrow> pid accC = pid (declclass m)" |
|
2882 |
proof - |
|
2883 |
assume wf: "wf_prog G " |
|
2884 |
assume accessible: "G \<turnstile> m in C dyn_accessible_from accC" |
|
2885 |
then show "accmodi m = Package |
|
2886 |
\<Longrightarrow> pid accC = pid (declclass m)" |
|
2887 |
(is "?Pack m \<Longrightarrow> ?P m") |
|
2888 |
proof (induct rule: dyn_accessible_fromR.induct) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2889 |
case (Immediate C m) |
12854 | 2890 |
assume "G\<turnstile>m member_in C" |
2891 |
"G \<turnstile> m in C permits_acc_to accC" |
|
2892 |
"accmodi m = Package" |
|
2893 |
then show "?P m" |
|
2894 |
by (auto simp add: permits_acc_def) |
|
2895 |
next |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2896 |
case (Overriding declC C new newm old Sup) |
12854 | 2897 |
assume member_new: "G \<turnstile> new member_in C" and |
2898 |
new: "new = (declC, mdecl newm)" and |
|
2899 |
override: "G \<turnstile> (declC, newm) overrides old" and |
|
2900 |
subcls_C_Sup: "G\<turnstile>C \<prec>\<^sub>C Sup" and |
|
2901 |
acc_old: "G \<turnstile> methdMembr old in Sup dyn_accessible_from accC" and |
|
2902 |
hyp: "?Pack (methdMembr old) \<Longrightarrow> ?P (methdMembr old)" and |
|
2903 |
accmodi_new: "accmodi new = Package" |
|
2904 |
from override accmodi_new new wf |
|
2905 |
have accmodi_old: "accmodi old = Package" |
|
2906 |
by (auto dest: overrides_Package_old) |
|
2907 |
with hyp |
|
2908 |
have P_sup: "?P (methdMembr old)" |
|
2909 |
by (simp) |
|
2910 |
from wf override new accmodi_old accmodi_new |
|
2911 |
have eq_pid_new_old: "pid (declclass new) = pid (declclass old)" |
|
2912 |
by (auto dest: dyn_override_Package) |
|
2913 |
with eq_pid_new_old P_sup show "?P new" |
|
2914 |
by auto |
|
2915 |
qed |
|
2916 |
qed |
|
2917 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2918 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2919 |
text {* @{text dyn_accessible_instance_field_Protected} only works for fields |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2920 |
since methods can break the package bounds due to overriding |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2921 |
*} |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2922 |
lemma dyn_accessible_instance_field_Protected: |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2923 |
assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2924 |
prot: "accmodi f = Protected" and |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2925 |
field: "is_field f" and |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2926 |
instance_field: "\<not> is_static f" and |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2927 |
outside: "pid (declclass f) \<noteq> pid accC" |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2928 |
shows "G\<turnstile> C \<preceq>\<^sub>C accC" |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2929 |
proof - |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2930 |
from dyn_acc prot field instance_field outside |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2931 |
show ?thesis |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2932 |
proof (induct) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2933 |
case (Immediate C f) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2934 |
have "G \<turnstile> f in C permits_acc_to accC" . |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2935 |
moreover |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2936 |
assume "accmodi f = Protected" and "is_field f" and "\<not> is_static f" and |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2937 |
"pid (declclass f) \<noteq> pid accC" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2938 |
ultimately |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2939 |
show "G\<turnstile> C \<preceq>\<^sub>C accC" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2940 |
by (auto simp add: permits_acc_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2941 |
next |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2942 |
case Overriding |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2943 |
then show ?case by (simp add: is_field_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2944 |
qed |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2945 |
qed |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2946 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2947 |
lemma dyn_accessible_static_field_Protected: |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2948 |
assumes dyn_acc: "G \<turnstile> f in C dyn_accessible_from accC" and |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2949 |
prot: "accmodi f = Protected" and |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2950 |
field: "is_field f" and |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2951 |
static_field: "is_static f" and |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2952 |
outside: "pid (declclass f) \<noteq> pid accC" |
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset
|
2953 |
shows "G\<turnstile> accC \<preceq>\<^sub>C declclass f \<and> G\<turnstile>C \<preceq>\<^sub>C declclass f" |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2954 |
proof - |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2955 |
from dyn_acc prot field static_field outside |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2956 |
show ?thesis |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2957 |
proof (induct) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2958 |
case (Immediate C f) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2959 |
assume "accmodi f = Protected" and "is_field f" and "is_static f" and |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2960 |
"pid (declclass f) \<noteq> pid accC" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2961 |
moreover |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2962 |
have "G \<turnstile> f in C permits_acc_to accC" . |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2963 |
ultimately |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2964 |
have "G\<turnstile> accC \<preceq>\<^sub>C declclass f" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2965 |
by (auto simp add: permits_acc_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2966 |
moreover |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2967 |
have "G \<turnstile> f member_in C" . |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2968 |
then have "G\<turnstile>C \<preceq>\<^sub>C declclass f" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2969 |
by (rule member_in_class_relation) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2970 |
ultimately show ?case |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2971 |
by blast |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2972 |
next |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2973 |
case Overriding |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2974 |
then show ?case by (simp add: is_field_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2975 |
qed |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2976 |
qed |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12893
diff
changeset
|
2977 |
|
12854 | 2978 |
end |