author | wenzelm |
Mon, 25 Feb 2002 20:48:14 +0100 | |
changeset 12937 | 0c4fd7529467 |
parent 12925 | 99131847fb93 |
child 13524 | 604d0f3622d6 |
permissions | -rw-r--r-- |
12857 | 1 |
(* Title: HOL/Bali/Example.thy |
12854 | 2 |
ID: $Id$ |
3 |
Author: David von Oheimb |
|
12858 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
12854 | 5 |
*) |
6 |
header {* Example Bali program *} |
|
7 |
||
8 |
theory Example = Eval + WellForm: |
|
9 |
||
10 |
text {* |
|
11 |
The following example Bali program includes: |
|
12 |
\begin{itemize} |
|
13 |
\item class and interface declarations with inheritance, hiding of fields, |
|
14 |
overriding of methods (with refined result type), array type, |
|
15 |
\item method call (with dynamic binding), parameter access, return expressions, |
|
16 |
\item expression statements, sequential composition, literal values, |
|
17 |
local assignment, local access, field assignment, type cast, |
|
18 |
\item exception generation and propagation, try and catch statement, throw |
|
19 |
statement |
|
20 |
\item instance creation and (default) static initialization |
|
21 |
\end{itemize} |
|
22 |
\begin{verbatim} |
|
23 |
package java_lang |
|
24 |
||
25 |
public interface HasFoo { |
|
26 |
public Base foo(Base z); |
|
27 |
} |
|
28 |
||
29 |
public class Base implements HasFoo { |
|
30 |
static boolean arr[] = new boolean[2]; |
|
31 |
public HasFoo vee; |
|
32 |
public Base foo(Base z) { |
|
33 |
return z; |
|
34 |
} |
|
35 |
} |
|
36 |
||
37 |
public class Ext extends Base { |
|
38 |
public int vee; |
|
39 |
public Ext foo(Base z) { |
|
40 |
((Ext)z).vee = 1; |
|
41 |
return null; |
|
42 |
} |
|
43 |
} |
|
44 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
45 |
public class Main { |
12854 | 46 |
public static void main(String args[]) throws Throwable { |
47 |
Base e = new Ext(); |
|
48 |
try {e.foo(null); } |
|
49 |
catch(NullPointerException z) { |
|
50 |
while(Ext.arr[2]) ; |
|
51 |
} |
|
52 |
} |
|
53 |
} |
|
54 |
\end{verbatim} |
|
55 |
*} |
|
56 |
declare widen.null [intro] |
|
57 |
||
58 |
lemma wf_fdecl_def2: "\<And>fd. wf_fdecl G P fd = is_acc_type G P (type (snd fd))" |
|
59 |
apply (unfold wf_fdecl_def) |
|
60 |
apply (simp (no_asm)) |
|
61 |
done |
|
62 |
||
63 |
declare wf_fdecl_def2 [iff] |
|
64 |
||
65 |
||
66 |
section "type and expression names" |
|
67 |
||
68 |
(** unfortunately cannot simply instantiate tnam **) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
69 |
datatype tnam_ = HasFoo_ | Base_ | Ext_ | Main_ |
12854 | 70 |
datatype vnam_ = arr_ | vee_ | z_ | e_ |
71 |
datatype label_ = lab1_ |
|
72 |
||
73 |
consts |
|
74 |
||
75 |
tnam_ :: "tnam_ \<Rightarrow> tnam" |
|
76 |
vnam_ :: "vnam_ \<Rightarrow> vname" |
|
77 |
label_:: "label_ \<Rightarrow> label" |
|
78 |
axioms (** tnam_, vnam_ and label are intended to be isomorphic |
|
79 |
to tnam, vname and label **) |
|
80 |
||
81 |
inj_tnam_ [simp]: "(tnam_ x = tnam_ y) = (x = y)" |
|
82 |
inj_vnam_ [simp]: "(vnam_ x = vnam_ y) = (x = y)" |
|
83 |
inj_label_ [simp]: "(label_ x = label_ y) = (x = y)" |
|
84 |
||
85 |
||
86 |
surj_tnam_: "\<exists>m. n = tnam_ m" |
|
87 |
surj_vnam_: "\<exists>m. n = vnam_ m" |
|
88 |
surj_label_:" \<exists>m. n = label_ m" |
|
89 |
||
90 |
syntax |
|
91 |
||
92 |
HasFoo :: qtname |
|
93 |
Base :: qtname |
|
94 |
Ext :: qtname |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
95 |
Main :: qtname |
12854 | 96 |
arr :: ename |
97 |
vee :: ename |
|
98 |
z :: ename |
|
99 |
e :: ename |
|
100 |
lab1:: label |
|
101 |
translations |
|
102 |
||
103 |
"HasFoo" == "\<lparr>pid=java_lang,tid=TName (tnam_ HasFoo_)\<rparr>" |
|
104 |
"Base" == "\<lparr>pid=java_lang,tid=TName (tnam_ Base_)\<rparr>" |
|
105 |
"Ext" == "\<lparr>pid=java_lang,tid=TName (tnam_ Ext_)\<rparr>" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
106 |
"Main" == "\<lparr>pid=java_lang,tid=TName (tnam_ Main_)\<rparr>" |
12854 | 107 |
"arr" == "(vnam_ arr_)" |
108 |
"vee" == "(vnam_ vee_)" |
|
109 |
"z" == "(vnam_ z_)" |
|
110 |
"e" == "(vnam_ e_)" |
|
111 |
"lab1" == "label_ lab1_" |
|
112 |
||
113 |
||
114 |
lemma neq_Base_Object [simp]: "Base\<noteq>Object" |
|
115 |
by (simp add: Object_def) |
|
116 |
||
117 |
lemma neq_Ext_Object [simp]: "Ext\<noteq>Object" |
|
118 |
by (simp add: Object_def) |
|
119 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
120 |
lemma neq_Main_Object [simp]: "Main\<noteq>Object" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
121 |
by (simp add: Object_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
122 |
|
12854 | 123 |
lemma neq_Base_SXcpt [simp]: "Base\<noteq>SXcpt xn" |
124 |
by (simp add: SXcpt_def) |
|
125 |
||
126 |
lemma neq_Ext_SXcpt [simp]: "Ext\<noteq>SXcpt xn" |
|
127 |
by (simp add: SXcpt_def) |
|
128 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
129 |
lemma neq_Main_Object [simp]: "Main\<noteq>SXcpt xn" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
130 |
by (simp add: SXcpt_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
131 |
|
12854 | 132 |
section "classes and interfaces" |
133 |
||
134 |
defs |
|
135 |
||
136 |
Object_mdecls_def: "Object_mdecls \<equiv> []" |
|
137 |
SXcpt_mdecls_def: "SXcpt_mdecls \<equiv> []" |
|
138 |
||
139 |
consts |
|
140 |
||
141 |
foo :: mname |
|
142 |
||
143 |
constdefs |
|
144 |
||
145 |
foo_sig :: sig |
|
146 |
"foo_sig \<equiv> \<lparr>name=foo,parTs=[Class Base]\<rparr>" |
|
147 |
||
148 |
foo_mhead :: mhead |
|
149 |
"foo_mhead \<equiv> \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>" |
|
150 |
||
151 |
constdefs |
|
152 |
||
153 |
Base_foo :: mdecl |
|
154 |
"Base_foo \<equiv> (foo_sig, \<lparr>access=Public,static=False,pars=[z],resT=Class Base, |
|
155 |
mbody=\<lparr>lcls=[],stmt=Return (!!z)\<rparr>\<rparr>)" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
156 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
157 |
constdefs |
12854 | 158 |
Ext_foo :: mdecl |
159 |
"Ext_foo \<equiv> (foo_sig, |
|
160 |
\<lparr>access=Public,static=False,pars=[z],resT=Class Ext, |
|
161 |
mbody=\<lparr>lcls=[] |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
162 |
,stmt=Expr({Ext,Ext,False}Cast (Class Ext) (!!z)..vee := |
12854 | 163 |
Lit (Intg 1))\<rparr> |
164 |
\<rparr>)" |
|
165 |
||
166 |
constdefs |
|
167 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
168 |
arr_viewed_from :: "qtname \<Rightarrow> qtname \<Rightarrow> var" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
169 |
"arr_viewed_from accC C \<equiv> {accC,Base,True}StatRef (ClassT C)..arr" |
12854 | 170 |
|
171 |
BaseCl :: class |
|
172 |
"BaseCl \<equiv> \<lparr>access=Public, |
|
173 |
cfields=[(arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>), |
|
174 |
(vee, \<lparr>access=Public,static=False,type=Iface HasFoo \<rparr>)], |
|
175 |
methods=[Base_foo], |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
176 |
init=Expr(arr_viewed_from Base Base |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
177 |
:=New (PrimT Boolean)[Lit (Intg 2)]), |
12854 | 178 |
super=Object, |
179 |
superIfs=[HasFoo]\<rparr>" |
|
180 |
||
181 |
ExtCl :: class |
|
182 |
"ExtCl \<equiv> \<lparr>access=Public, |
|
183 |
cfields=[(vee, \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)], |
|
184 |
methods=[Ext_foo], |
|
185 |
init=Skip, |
|
186 |
super=Base, |
|
187 |
superIfs=[]\<rparr>" |
|
188 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
189 |
MainCl :: class |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
190 |
"MainCl \<equiv> \<lparr>access=Public, |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
191 |
cfields=[], |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
192 |
methods=[], |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
193 |
init=Skip, |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
194 |
super=Object, |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
195 |
superIfs=[]\<rparr>" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
196 |
(* The "main" method is modeled seperately (see tprg) *) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
197 |
|
12854 | 198 |
constdefs |
199 |
||
200 |
HasFooInt :: iface |
|
201 |
"HasFooInt \<equiv> \<lparr>access=Public,imethods=[(foo_sig, foo_mhead)],isuperIfs=[]\<rparr>" |
|
202 |
||
203 |
Ifaces ::"idecl list" |
|
204 |
"Ifaces \<equiv> [(HasFoo,HasFooInt)]" |
|
205 |
||
206 |
"Classes" ::"cdecl list" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
207 |
"Classes \<equiv> [(Base,BaseCl),(Ext,ExtCl),(Main,MainCl)]@standard_classes" |
12854 | 208 |
|
209 |
lemmas table_classes_defs = |
|
210 |
Classes_def standard_classes_def ObjectC_def SXcptC_def |
|
211 |
||
212 |
lemma table_ifaces [simp]: "table_of Ifaces = empty(HasFoo\<mapsto>HasFooInt)" |
|
213 |
apply (unfold Ifaces_def) |
|
214 |
apply (simp (no_asm)) |
|
215 |
done |
|
216 |
||
217 |
lemma table_classes_Object [simp]: |
|
218 |
"table_of Classes Object = Some \<lparr>access=Public,cfields=[] |
|
219 |
,methods=Object_mdecls |
|
220 |
,init=Skip,super=arbitrary,superIfs=[]\<rparr>" |
|
221 |
apply (unfold table_classes_defs) |
|
222 |
apply (simp (no_asm) add:Object_def) |
|
223 |
done |
|
224 |
||
225 |
lemma table_classes_SXcpt [simp]: |
|
226 |
"table_of Classes (SXcpt xn) |
|
227 |
= Some \<lparr>access=Public,cfields=[],methods=SXcpt_mdecls, |
|
228 |
init=Skip, |
|
229 |
super=if xn = Throwable then Object else SXcpt Throwable, |
|
230 |
superIfs=[]\<rparr>" |
|
231 |
apply (unfold table_classes_defs) |
|
232 |
apply (induct_tac xn) |
|
233 |
apply (simp add: Object_def SXcpt_def)+ |
|
234 |
done |
|
235 |
||
236 |
lemma table_classes_HasFoo [simp]: "table_of Classes HasFoo = None" |
|
237 |
apply (unfold table_classes_defs) |
|
238 |
apply (simp (no_asm) add: Object_def SXcpt_def) |
|
239 |
done |
|
240 |
||
241 |
lemma table_classes_Base [simp]: "table_of Classes Base = Some BaseCl" |
|
242 |
apply (unfold table_classes_defs ) |
|
243 |
apply (simp (no_asm) add: Object_def SXcpt_def) |
|
244 |
done |
|
245 |
||
246 |
lemma table_classes_Ext [simp]: "table_of Classes Ext = Some ExtCl" |
|
247 |
apply (unfold table_classes_defs ) |
|
248 |
apply (simp (no_asm) add: Object_def SXcpt_def) |
|
249 |
done |
|
250 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
251 |
lemma table_classes_Main [simp]: "table_of Classes Main = Some MainCl" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
252 |
apply (unfold table_classes_defs ) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
253 |
apply (simp (no_asm) add: Object_def SXcpt_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
254 |
done |
12854 | 255 |
|
256 |
section "program" |
|
257 |
||
258 |
syntax |
|
259 |
tprg :: prog |
|
260 |
||
261 |
translations |
|
262 |
"tprg" == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>" |
|
263 |
||
264 |
constdefs |
|
265 |
test :: "(ty)list \<Rightarrow> stmt" |
|
266 |
"test pTs \<equiv> e:==NewC Ext;; |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
267 |
\<spacespace> Try Expr({Main,ClassT Base,IntVir}!!e\<cdot>foo({pTs}[Lit Null])) |
12854 | 268 |
\<spacespace> Catch((SXcpt NullPointer) z) |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
269 |
(lab1\<bullet> While(Acc |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
270 |
(Acc (arr_viewed_from Main Ext).[Lit (Intg 2)])) Skip)" |
12854 | 271 |
|
272 |
||
273 |
section "well-structuredness" |
|
274 |
||
275 |
lemma not_Object_subcls_any [elim!]: "(Object, C) \<in> (subcls1 tprg)^+ \<Longrightarrow> R" |
|
276 |
apply (auto dest!: tranclD subcls1D) |
|
277 |
done |
|
278 |
||
279 |
lemma not_Throwable_subcls_SXcpt [elim!]: |
|
280 |
"(SXcpt Throwable, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R" |
|
281 |
apply (auto dest!: tranclD subcls1D) |
|
282 |
apply (simp add: Object_def SXcpt_def) |
|
283 |
done |
|
284 |
||
285 |
lemma not_SXcpt_n_subcls_SXcpt_n [elim!]: |
|
286 |
"(SXcpt xn, SXcpt xn) \<in> (subcls1 tprg)^+ \<Longrightarrow> R" |
|
287 |
apply (auto dest!: tranclD subcls1D) |
|
288 |
apply (drule rtranclD) |
|
289 |
apply auto |
|
290 |
done |
|
291 |
||
292 |
lemma not_Base_subcls_Ext [elim!]: "(Base, Ext) \<in> (subcls1 tprg)^+ \<Longrightarrow> R" |
|
293 |
apply (auto dest!: tranclD subcls1D simp add: BaseCl_def) |
|
294 |
done |
|
295 |
||
296 |
lemma not_TName_n_subcls_TName_n [rule_format (no_asm), elim!]: |
|
297 |
"(\<lparr>pid=java_lang,tid=TName tn\<rparr>, \<lparr>pid=java_lang,tid=TName tn\<rparr>) |
|
298 |
\<in> (subcls1 tprg)^+ \<longrightarrow> R" |
|
299 |
apply (rule_tac n1 = "tn" in surj_tnam_ [THEN exE]) |
|
300 |
apply (erule ssubst) |
|
301 |
apply (rule tnam_.induct) |
|
302 |
apply safe |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
303 |
apply (auto dest!: tranclD subcls1D simp add: BaseCl_def ExtCl_def MainCl_def) |
12854 | 304 |
apply (drule rtranclD) |
305 |
apply auto |
|
306 |
done |
|
307 |
||
308 |
||
309 |
lemma ws_idecl_HasFoo: "ws_idecl tprg HasFoo []" |
|
310 |
apply (unfold ws_idecl_def) |
|
311 |
apply (simp (no_asm)) |
|
312 |
done |
|
313 |
||
314 |
lemma ws_cdecl_Object: "ws_cdecl tprg Object any" |
|
315 |
apply (unfold ws_cdecl_def) |
|
316 |
apply auto |
|
317 |
done |
|
318 |
||
319 |
lemma ws_cdecl_Throwable: "ws_cdecl tprg (SXcpt Throwable) Object" |
|
320 |
apply (unfold ws_cdecl_def) |
|
321 |
apply auto |
|
322 |
done |
|
323 |
||
324 |
lemma ws_cdecl_SXcpt: "ws_cdecl tprg (SXcpt xn) (SXcpt Throwable)" |
|
325 |
apply (unfold ws_cdecl_def) |
|
326 |
apply auto |
|
327 |
done |
|
328 |
||
329 |
lemma ws_cdecl_Base: "ws_cdecl tprg Base Object" |
|
330 |
apply (unfold ws_cdecl_def) |
|
331 |
apply auto |
|
332 |
done |
|
333 |
||
334 |
lemma ws_cdecl_Ext: "ws_cdecl tprg Ext Base" |
|
335 |
apply (unfold ws_cdecl_def) |
|
336 |
apply auto |
|
337 |
done |
|
338 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
339 |
lemma ws_cdecl_Main: "ws_cdecl tprg Main Object" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
340 |
apply (unfold ws_cdecl_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
341 |
apply auto |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
342 |
done |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
343 |
|
12854 | 344 |
lemmas ws_cdecls = ws_cdecl_SXcpt ws_cdecl_Object ws_cdecl_Throwable |
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
345 |
ws_cdecl_Base ws_cdecl_Ext ws_cdecl_Main |
12854 | 346 |
|
347 |
declare not_Object_subcls_any [rule del] |
|
348 |
not_Throwable_subcls_SXcpt [rule del] |
|
349 |
not_SXcpt_n_subcls_SXcpt_n [rule del] |
|
350 |
not_Base_subcls_Ext [rule del] not_TName_n_subcls_TName_n [rule del] |
|
351 |
||
352 |
lemma ws_idecl_all: |
|
353 |
"G=tprg \<Longrightarrow> (\<forall>(I,i)\<in>set Ifaces. ws_idecl G I (isuperIfs i))" |
|
354 |
apply (simp (no_asm) add: Ifaces_def HasFooInt_def) |
|
355 |
apply (auto intro!: ws_idecl_HasFoo) |
|
356 |
done |
|
357 |
||
358 |
lemma ws_cdecl_all: "G=tprg \<Longrightarrow> (\<forall>(C,c)\<in>set Classes. ws_cdecl G C (super c))" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
359 |
apply (simp (no_asm) add: Classes_def BaseCl_def ExtCl_def MainCl_def) |
12854 | 360 |
apply (auto intro!: ws_cdecls simp add: standard_classes_def ObjectC_def |
361 |
SXcptC_def) |
|
362 |
done |
|
363 |
||
364 |
lemma ws_tprg: "ws_prog tprg" |
|
365 |
apply (unfold ws_prog_def) |
|
366 |
apply (auto intro!: ws_idecl_all ws_cdecl_all) |
|
367 |
done |
|
368 |
||
369 |
||
370 |
section "misc program properties (independent of well-structuredness)" |
|
371 |
||
372 |
lemma single_iface [simp]: "is_iface tprg I = (I = HasFoo)" |
|
373 |
apply (unfold Ifaces_def) |
|
374 |
apply (simp (no_asm)) |
|
375 |
done |
|
376 |
||
377 |
lemma empty_subint1 [simp]: "subint1 tprg = {}" |
|
378 |
apply (unfold subint1_def Ifaces_def HasFooInt_def) |
|
379 |
apply auto |
|
380 |
done |
|
381 |
||
382 |
lemma unique_ifaces: "unique Ifaces" |
|
383 |
apply (unfold Ifaces_def) |
|
384 |
apply (simp (no_asm)) |
|
385 |
done |
|
386 |
||
387 |
lemma unique_classes: "unique Classes" |
|
388 |
apply (unfold table_classes_defs ) |
|
389 |
apply (simp ) |
|
390 |
done |
|
391 |
||
392 |
lemma SXcpt_subcls_Throwable [simp]: "tprg\<turnstile>SXcpt xn\<preceq>\<^sub>C SXcpt Throwable" |
|
393 |
apply (rule SXcpt_subcls_Throwable_lemma) |
|
394 |
apply auto |
|
395 |
done |
|
396 |
||
397 |
lemma Ext_subclseq_Base [simp]: "tprg\<turnstile>Ext \<preceq>\<^sub>C Base" |
|
398 |
apply (rule subcls_direct1) |
|
399 |
apply (simp (no_asm) add: ExtCl_def) |
|
400 |
apply (simp add: Object_def) |
|
401 |
apply (simp (no_asm)) |
|
402 |
done |
|
403 |
||
404 |
lemma Ext_subcls_Base [simp]: "tprg\<turnstile>Ext \<prec>\<^sub>C Base" |
|
405 |
apply (rule subcls_direct2) |
|
406 |
apply (simp (no_asm) add: ExtCl_def) |
|
407 |
apply (simp add: Object_def) |
|
408 |
apply (simp (no_asm)) |
|
409 |
done |
|
410 |
||
411 |
||
412 |
||
413 |
section "fields and method lookup" |
|
414 |
||
415 |
lemma fields_tprg_Object [simp]: "DeclConcepts.fields tprg Object = []" |
|
416 |
by (rule ws_tprg [THEN fields_emptyI], force+) |
|
417 |
||
418 |
lemma fields_tprg_Throwable [simp]: |
|
419 |
"DeclConcepts.fields tprg (SXcpt Throwable) = []" |
|
420 |
by (rule ws_tprg [THEN fields_emptyI], force+) |
|
421 |
||
422 |
lemma fields_tprg_SXcpt [simp]: "DeclConcepts.fields tprg (SXcpt xn) = []" |
|
423 |
apply (case_tac "xn = Throwable") |
|
424 |
apply (simp (no_asm_simp)) |
|
425 |
by (rule ws_tprg [THEN fields_emptyI], force+) |
|
426 |
||
427 |
lemmas fields_rec_ = fields_rec [OF _ ws_tprg] |
|
428 |
||
429 |
lemma fields_Base [simp]: |
|
430 |
"DeclConcepts.fields tprg Base |
|
431 |
= [((arr,Base), \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>), |
|
432 |
((vee,Base), \<lparr>access=Public,static=False,type=Iface HasFoo \<rparr>)]" |
|
433 |
apply (subst fields_rec_) |
|
434 |
apply (auto simp add: BaseCl_def) |
|
435 |
done |
|
436 |
||
437 |
lemma fields_Ext [simp]: |
|
438 |
"DeclConcepts.fields tprg Ext |
|
439 |
= [((vee,Ext), \<lparr>access=Public,static=False,type= PrimT Integer\<rparr>)] |
|
440 |
@ DeclConcepts.fields tprg Base" |
|
441 |
apply (rule trans) |
|
442 |
apply (rule fields_rec_) |
|
443 |
apply (auto simp add: ExtCl_def Object_def) |
|
444 |
done |
|
445 |
||
446 |
lemmas imethds_rec_ = imethds_rec [OF _ ws_tprg] |
|
447 |
lemmas methd_rec_ = methd_rec [OF _ ws_tprg] |
|
448 |
||
449 |
lemma imethds_HasFoo [simp]: |
|
450 |
"imethds tprg HasFoo = o2s \<circ> empty(foo_sig\<mapsto>(HasFoo, foo_mhead))" |
|
451 |
apply (rule trans) |
|
452 |
apply (rule imethds_rec_) |
|
453 |
apply (auto simp add: HasFooInt_def) |
|
454 |
done |
|
455 |
||
456 |
lemma methd_tprg_Object [simp]: "methd tprg Object = empty" |
|
457 |
apply (subst methd_rec_) |
|
458 |
apply (auto simp add: Object_mdecls_def) |
|
459 |
done |
|
460 |
||
461 |
lemma methd_Base [simp]: |
|
462 |
"methd tprg Base = table_of [(\<lambda>(s,m). (s, Base, m)) Base_foo]" |
|
463 |
apply (rule trans) |
|
464 |
apply (rule methd_rec_) |
|
465 |
apply (auto simp add: BaseCl_def) |
|
466 |
done |
|
467 |
||
468 |
lemma memberid_Base_foo_simp [simp]: |
|
469 |
"memberid (mdecl Base_foo) = mid foo_sig" |
|
470 |
by (simp add: Base_foo_def) |
|
471 |
||
472 |
lemma memberid_Ext_foo_simp [simp]: |
|
473 |
"memberid (mdecl Ext_foo) = mid foo_sig" |
|
474 |
by (simp add: Ext_foo_def) |
|
475 |
||
476 |
lemma Base_declares_foo: |
|
477 |
"tprg\<turnstile>mdecl Base_foo declared_in Base" |
|
478 |
by (auto simp add: declared_in_def cdeclaredmethd_def BaseCl_def Base_foo_def) |
|
479 |
||
480 |
lemma foo_sig_not_undeclared_in_Base: |
|
481 |
"\<not> tprg\<turnstile>mid foo_sig undeclared_in Base" |
|
482 |
proof - |
|
483 |
from Base_declares_foo |
|
484 |
show ?thesis |
|
485 |
by (auto dest!: declared_not_undeclared ) |
|
486 |
qed |
|
487 |
||
488 |
lemma Ext_declares_foo: |
|
489 |
"tprg\<turnstile>mdecl Ext_foo declared_in Ext" |
|
490 |
by (auto simp add: declared_in_def cdeclaredmethd_def ExtCl_def Ext_foo_def) |
|
491 |
||
492 |
lemma foo_sig_not_undeclared_in_Ext: |
|
493 |
"\<not> tprg\<turnstile>mid foo_sig undeclared_in Ext" |
|
494 |
proof - |
|
495 |
from Ext_declares_foo |
|
496 |
show ?thesis |
|
497 |
by (auto dest!: declared_not_undeclared ) |
|
498 |
qed |
|
499 |
||
500 |
lemma Base_foo_not_inherited_in_Ext: |
|
501 |
"\<not> tprg \<turnstile> Ext inherits (Base,mdecl Base_foo)" |
|
502 |
by (auto simp add: inherits_def foo_sig_not_undeclared_in_Ext) |
|
503 |
||
504 |
lemma Ext_method_inheritance: |
|
505 |
"filter_tab (\<lambda>sig m. tprg \<turnstile> Ext inherits method sig m) |
|
506 |
(empty(fst ((\<lambda>(s, m). (s, Base, m)) Base_foo)\<mapsto> |
|
507 |
snd ((\<lambda>(s, m). (s, Base, m)) Base_foo))) |
|
508 |
= empty" |
|
509 |
proof - |
|
510 |
from Base_foo_not_inherited_in_Ext |
|
511 |
show ?thesis |
|
512 |
by (auto intro: filter_tab_all_False simp add: Base_foo_def) |
|
513 |
qed |
|
514 |
||
515 |
||
516 |
lemma methd_Ext [simp]: "methd tprg Ext = |
|
517 |
table_of [(\<lambda>(s,m). (s, Ext, m)) Ext_foo]" |
|
518 |
apply (rule trans) |
|
519 |
apply (rule methd_rec_) |
|
520 |
apply (auto simp add: ExtCl_def Object_def Ext_method_inheritance) |
|
521 |
done |
|
522 |
||
523 |
section "accessibility" |
|
524 |
||
525 |
lemma classesDefined: |
|
526 |
"\<lbrakk>class tprg C = Some c; C\<noteq>Object\<rbrakk> \<Longrightarrow> \<exists> sc. class tprg (super c) = Some sc" |
|
527 |
apply (auto simp add: Classes_def standard_classes_def |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
528 |
BaseCl_def ExtCl_def MainCl_def |
12854 | 529 |
SXcptC_def ObjectC_def) |
530 |
done |
|
531 |
||
532 |
lemma superclassesBase [simp]: "superclasses tprg Base={Object}" |
|
533 |
proof - |
|
534 |
have ws: "ws_prog tprg" by (rule ws_tprg) |
|
535 |
then show ?thesis |
|
536 |
by (auto simp add: superclasses_rec BaseCl_def) |
|
537 |
qed |
|
538 |
||
539 |
lemma superclassesExt [simp]: "superclasses tprg Ext={Base,Object}" |
|
540 |
proof - |
|
541 |
have ws: "ws_prog tprg" by (rule ws_tprg) |
|
542 |
then show ?thesis |
|
543 |
by (auto simp add: superclasses_rec ExtCl_def BaseCl_def) |
|
544 |
qed |
|
545 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
546 |
lemma superclassesMain [simp]: "superclasses tprg Main={Object}" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
547 |
proof - |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
548 |
have ws: "ws_prog tprg" by (rule ws_tprg) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
549 |
then show ?thesis |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
550 |
by (auto simp add: superclasses_rec MainCl_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
551 |
qed |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
552 |
|
12854 | 553 |
lemma HasFoo_accessible[simp]:"tprg\<turnstile>(Iface HasFoo) accessible_in P" |
554 |
by (simp add: accessible_in_RefT_simp is_public_def HasFooInt_def) |
|
555 |
||
556 |
lemma HasFoo_is_acc_iface[simp]: "is_acc_iface tprg P HasFoo" |
|
557 |
by (simp add: is_acc_iface_def) |
|
558 |
||
559 |
lemma HasFoo_is_acc_type[simp]: "is_acc_type tprg P (Iface HasFoo)" |
|
560 |
by (simp add: is_acc_type_def) |
|
561 |
||
562 |
lemma Base_accessible[simp]:"tprg\<turnstile>(Class Base) accessible_in P" |
|
563 |
by (simp add: accessible_in_RefT_simp is_public_def BaseCl_def) |
|
564 |
||
565 |
lemma Base_is_acc_class[simp]: "is_acc_class tprg P Base" |
|
566 |
by (simp add: is_acc_class_def) |
|
567 |
||
568 |
lemma Base_is_acc_type[simp]: "is_acc_type tprg P (Class Base)" |
|
569 |
by (simp add: is_acc_type_def) |
|
570 |
||
571 |
lemma Ext_accessible[simp]:"tprg\<turnstile>(Class Ext) accessible_in P" |
|
572 |
by (simp add: accessible_in_RefT_simp is_public_def ExtCl_def) |
|
573 |
||
574 |
lemma Ext_is_acc_class[simp]: "is_acc_class tprg P Ext" |
|
575 |
by (simp add: is_acc_class_def) |
|
576 |
||
577 |
lemma Ext_is_acc_type[simp]: "is_acc_type tprg P (Class Ext)" |
|
578 |
by (simp add: is_acc_type_def) |
|
579 |
||
580 |
lemma accmethd_tprg_Object [simp]: "accmethd tprg S Object = empty" |
|
581 |
apply (unfold accmethd_def) |
|
582 |
apply (simp) |
|
583 |
done |
|
584 |
||
585 |
lemma snd_special_simp: "snd ((\<lambda>(s, m). (s, a, m)) x) = (a,snd x)" |
|
586 |
by (cases x) (auto) |
|
587 |
||
588 |
lemma fst_special_simp: "fst ((\<lambda>(s, m). (s, a, m)) x) = fst x" |
|
589 |
by (cases x) (auto) |
|
590 |
||
591 |
lemma foo_sig_undeclared_in_Object: |
|
592 |
"tprg\<turnstile>mid foo_sig undeclared_in Object" |
|
593 |
by (auto simp add: undeclared_in_def cdeclaredmethd_def Object_mdecls_def) |
|
594 |
||
595 |
lemma unique_sig_Base_foo: |
|
596 |
"tprg\<turnstile> mdecl (sig, snd Base_foo) declared_in Base \<Longrightarrow> sig=foo_sig" |
|
597 |
by (auto simp add: declared_in_def cdeclaredmethd_def |
|
598 |
Base_foo_def BaseCl_def) |
|
599 |
||
600 |
lemma Base_foo_no_override: |
|
601 |
"tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides old \<Longrightarrow> P" |
|
602 |
apply (drule overrides_commonD) |
|
603 |
apply (clarsimp) |
|
604 |
apply (frule subclsEval) |
|
605 |
apply (rule ws_tprg) |
|
606 |
apply (simp) |
|
607 |
apply (rule classesDefined) |
|
608 |
apply assumption+ |
|
609 |
apply (frule unique_sig_Base_foo) |
|
610 |
apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object |
|
611 |
dest: unique_sig_Base_foo) |
|
612 |
done |
|
613 |
||
614 |
lemma Base_foo_no_stat_override: |
|
615 |
"tprg,sig\<turnstile>(Base,(snd Base_foo)) overrides\<^sub>S old \<Longrightarrow> P" |
|
616 |
apply (drule stat_overrides_commonD) |
|
617 |
apply (clarsimp) |
|
618 |
apply (frule subclsEval) |
|
619 |
apply (rule ws_tprg) |
|
620 |
apply (simp) |
|
621 |
apply (rule classesDefined) |
|
622 |
apply assumption+ |
|
623 |
apply (frule unique_sig_Base_foo) |
|
624 |
apply (auto dest!: declared_not_undeclared intro: foo_sig_undeclared_in_Object |
|
625 |
dest: unique_sig_Base_foo) |
|
626 |
done |
|
627 |
||
628 |
||
629 |
lemma Base_foo_no_hide: |
|
630 |
"tprg,sig\<turnstile>(Base,(snd Base_foo)) hides old \<Longrightarrow> P" |
|
631 |
by (auto dest: hidesD simp add: Base_foo_def member_is_static_simp) |
|
632 |
||
633 |
lemma Ext_foo_no_hide: |
|
634 |
"tprg,sig\<turnstile>(Ext,(snd Ext_foo)) hides old \<Longrightarrow> P" |
|
635 |
by (auto dest: hidesD simp add: Ext_foo_def member_is_static_simp) |
|
636 |
||
637 |
lemma unique_sig_Ext_foo: |
|
638 |
"tprg\<turnstile> mdecl (sig, snd Ext_foo) declared_in Ext \<Longrightarrow> sig=foo_sig" |
|
639 |
by (auto simp add: declared_in_def cdeclaredmethd_def |
|
640 |
Ext_foo_def ExtCl_def) |
|
641 |
||
642 |
lemma Ext_foo_override: |
|
643 |
"tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides old |
|
644 |
\<Longrightarrow> old = (Base,(snd Base_foo))" |
|
645 |
apply (drule overrides_commonD) |
|
646 |
apply (clarsimp) |
|
647 |
apply (frule subclsEval) |
|
648 |
apply (rule ws_tprg) |
|
649 |
apply (simp) |
|
650 |
apply (rule classesDefined) |
|
651 |
apply assumption+ |
|
652 |
apply (frule unique_sig_Ext_foo) |
|
653 |
apply (case_tac "old") |
|
654 |
apply (insert Base_declares_foo foo_sig_undeclared_in_Object) |
|
655 |
apply (auto simp add: ExtCl_def Ext_foo_def |
|
656 |
BaseCl_def Base_foo_def Object_mdecls_def |
|
657 |
split_paired_all |
|
658 |
member_is_static_simp |
|
659 |
dest: declared_not_undeclared unique_declaration) |
|
660 |
done |
|
661 |
||
662 |
lemma Ext_foo_stat_override: |
|
663 |
"tprg,sig\<turnstile>(Ext,(snd Ext_foo)) overrides\<^sub>S old |
|
664 |
\<Longrightarrow> old = (Base,(snd Base_foo))" |
|
665 |
apply (drule stat_overrides_commonD) |
|
666 |
apply (clarsimp) |
|
667 |
apply (frule subclsEval) |
|
668 |
apply (rule ws_tprg) |
|
669 |
apply (simp) |
|
670 |
apply (rule classesDefined) |
|
671 |
apply assumption+ |
|
672 |
apply (frule unique_sig_Ext_foo) |
|
673 |
apply (case_tac "old") |
|
674 |
apply (insert Base_declares_foo foo_sig_undeclared_in_Object) |
|
675 |
apply (auto simp add: ExtCl_def Ext_foo_def |
|
676 |
BaseCl_def Base_foo_def Object_mdecls_def |
|
677 |
split_paired_all |
|
678 |
member_is_static_simp |
|
679 |
dest: declared_not_undeclared unique_declaration) |
|
680 |
done |
|
681 |
||
682 |
lemma Base_foo_member_of_Base: |
|
683 |
"tprg\<turnstile>(Base,mdecl Base_foo) member_of Base" |
|
684 |
by (auto intro!: members.Immediate Base_declares_foo) |
|
685 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
686 |
lemma Base_foo_member_in_Base: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
687 |
"tprg\<turnstile>(Base,mdecl Base_foo) member_in Base" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
688 |
by (rule member_of_to_member_in [OF Base_foo_member_of_Base]) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
689 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
690 |
lemma Base_foo_member_of_Base: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
691 |
"tprg\<turnstile>(Base,mdecl Base_foo) member_of Base" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
692 |
by (auto intro!: members.Immediate Base_declares_foo) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
693 |
|
12854 | 694 |
lemma Ext_foo_member_of_Ext: |
695 |
"tprg\<turnstile>(Ext,mdecl Ext_foo) member_of Ext" |
|
696 |
by (auto intro!: members.Immediate Ext_declares_foo) |
|
697 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
698 |
lemma Ext_foo_member_in_Ext: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
699 |
"tprg\<turnstile>(Ext,mdecl Ext_foo) member_in Ext" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
700 |
by (rule member_of_to_member_in [OF Ext_foo_member_of_Ext]) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
701 |
|
12854 | 702 |
lemma Base_foo_permits_acc: |
703 |
"tprg \<turnstile> (Base, mdecl Base_foo) in Base permits_acc_to S" |
|
704 |
by ( simp add: permits_acc_def Base_foo_def) |
|
705 |
||
706 |
lemma Base_foo_accessible [simp]: |
|
707 |
"tprg\<turnstile>(Base,mdecl Base_foo) of Base accessible_from S" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
708 |
by (auto intro: accessible_fromR.Immediate |
12854 | 709 |
Base_foo_member_of_Base Base_foo_permits_acc) |
710 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
711 |
lemma Base_foo_dyn_accessible [simp]: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
712 |
"tprg\<turnstile>(Base,mdecl Base_foo) in Base dyn_accessible_from S" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
713 |
apply (rule dyn_accessible_fromR.Immediate) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
714 |
apply (rule Base_foo_member_in_Base) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
715 |
apply (rule Base_foo_permits_acc) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
716 |
done |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
717 |
|
12854 | 718 |
lemma accmethd_Base [simp]: |
719 |
"accmethd tprg S Base = methd tprg Base" |
|
720 |
apply (simp add: accmethd_def) |
|
721 |
apply (rule filter_tab_all_True) |
|
722 |
apply (simp add: snd_special_simp fst_special_simp) |
|
723 |
done |
|
724 |
||
725 |
lemma Ext_foo_permits_acc: |
|
726 |
"tprg \<turnstile> (Ext, mdecl Ext_foo) in Ext permits_acc_to S" |
|
727 |
by ( simp add: permits_acc_def Ext_foo_def) |
|
728 |
||
729 |
lemma Ext_foo_accessible [simp]: |
|
730 |
"tprg\<turnstile>(Ext,mdecl Ext_foo) of Ext accessible_from S" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
731 |
by (auto intro: accessible_fromR.Immediate |
12854 | 732 |
Ext_foo_member_of_Ext Ext_foo_permits_acc) |
733 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
734 |
lemma Ext_foo_dyn_accessible [simp]: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
735 |
"tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from S" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
736 |
apply (rule dyn_accessible_fromR.Immediate) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
737 |
apply (rule Ext_foo_member_in_Ext) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
738 |
apply (rule Ext_foo_permits_acc) |
12854 | 739 |
done |
740 |
||
741 |
lemma Ext_foo_overrides_Base_foo: |
|
742 |
"tprg\<turnstile>(Ext,Ext_foo) overrides (Base,Base_foo)" |
|
743 |
proof (rule overridesR.Direct, simp_all) |
|
744 |
show "\<not> is_static Ext_foo" |
|
745 |
by (simp add: member_is_static_simp Ext_foo_def) |
|
746 |
show "\<not> is_static Base_foo" |
|
747 |
by (simp add: member_is_static_simp Base_foo_def) |
|
748 |
show "accmodi Ext_foo \<noteq> Private" |
|
749 |
by (simp add: Ext_foo_def) |
|
750 |
show "msig (Ext, Ext_foo) = msig (Base, Base_foo)" |
|
751 |
by (simp add: Ext_foo_def Base_foo_def) |
|
752 |
show "tprg\<turnstile>mdecl Ext_foo declared_in Ext" |
|
753 |
by (auto intro: Ext_declares_foo) |
|
754 |
show "tprg\<turnstile>mdecl Base_foo declared_in Base" |
|
755 |
by (auto intro: Base_declares_foo) |
|
756 |
show "tprg \<turnstile>(Base, mdecl Base_foo) inheritable_in java_lang" |
|
757 |
by (simp add: inheritable_in_def Base_foo_def) |
|
758 |
show "tprg\<turnstile>resTy Ext_foo\<preceq>resTy Base_foo" |
|
759 |
by (simp add: Ext_foo_def Base_foo_def mhead_resTy_simp) |
|
760 |
qed |
|
761 |
||
762 |
lemma accmethd_Ext [simp]: |
|
763 |
"accmethd tprg S Ext = methd tprg Ext" |
|
764 |
apply (simp add: accmethd_def) |
|
765 |
apply (rule filter_tab_all_True) |
|
766 |
apply (auto simp add: snd_special_simp fst_special_simp) |
|
767 |
done |
|
768 |
||
769 |
lemma cls_Ext: "class tprg Ext = Some ExtCl" |
|
770 |
by simp |
|
771 |
lemma dynmethd_Ext_foo: |
|
772 |
"dynmethd tprg Base Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> |
|
773 |
= Some (Ext,snd Ext_foo)" |
|
774 |
proof - |
|
775 |
have "methd tprg Base \<lparr>name = foo, parTs = [Class Base]\<rparr> |
|
776 |
= Some (Base,snd Base_foo)" and |
|
777 |
"methd tprg Ext \<lparr>name = foo, parTs = [Class Base]\<rparr> |
|
778 |
= Some (Ext,snd Ext_foo)" |
|
779 |
by (auto simp add: Ext_foo_def Base_foo_def foo_sig_def) |
|
780 |
with cls_Ext ws_tprg Ext_foo_overrides_Base_foo |
|
781 |
show ?thesis |
|
782 |
by (auto simp add: dynmethd_rec simp add: Ext_foo_def Base_foo_def) |
|
783 |
qed |
|
784 |
||
785 |
lemma Base_fields_accessible[simp]: |
|
786 |
"accfield tprg S Base |
|
787 |
= table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Base))" |
|
788 |
apply (auto simp add: accfield_def expand_fun_eq Let_def |
|
789 |
accessible_in_RefT_simp |
|
790 |
is_public_def |
|
791 |
BaseCl_def |
|
792 |
permits_acc_def |
|
793 |
declared_in_def |
|
794 |
cdeclaredfield_def |
|
795 |
intro!: filter_tab_all_True_Some filter_tab_None |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
796 |
accessible_fromR.Immediate |
12854 | 797 |
intro: members.Immediate) |
798 |
done |
|
799 |
||
800 |
||
801 |
lemma arr_member_of_Base: |
|
802 |
"tprg\<turnstile>(Base, fdecl (arr, |
|
803 |
\<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>)) |
|
804 |
member_of Base" |
|
805 |
by (auto intro: members.Immediate |
|
806 |
simp add: declared_in_def cdeclaredfield_def BaseCl_def) |
|
807 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
808 |
lemma arr_member_in_Base: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
809 |
"tprg\<turnstile>(Base, fdecl (arr, |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
810 |
\<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>)) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
811 |
member_in Base" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
812 |
by (rule member_of_to_member_in [OF arr_member_of_Base]) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
813 |
|
12854 | 814 |
lemma arr_member_of_Ext: |
815 |
"tprg\<turnstile>(Base, fdecl (arr, |
|
816 |
\<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>)) |
|
817 |
member_of Ext" |
|
818 |
apply (rule members.Inherited) |
|
819 |
apply (simp add: inheritable_in_def) |
|
820 |
apply (simp add: undeclared_in_def cdeclaredfield_def ExtCl_def) |
|
821 |
apply (auto intro: arr_member_of_Base simp add: subcls1_def ExtCl_def) |
|
822 |
done |
|
823 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
824 |
lemma arr_member_in_Ext: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
825 |
"tprg\<turnstile>(Base, fdecl (arr, |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
826 |
\<lparr>access = Public, static = True, type = PrimT Boolean.[]\<rparr>)) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
827 |
member_in Ext" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
828 |
by (rule member_of_to_member_in [OF arr_member_of_Ext]) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
829 |
|
12854 | 830 |
lemma Ext_fields_accessible[simp]: |
831 |
"accfield tprg S Ext |
|
832 |
= table_of((map (\<lambda>((n,d),f).(n,(d,f)))) (DeclConcepts.fields tprg Ext))" |
|
833 |
apply (auto simp add: accfield_def expand_fun_eq Let_def |
|
834 |
accessible_in_RefT_simp |
|
835 |
is_public_def |
|
836 |
BaseCl_def |
|
837 |
ExtCl_def |
|
838 |
permits_acc_def |
|
839 |
intro!: filter_tab_all_True_Some filter_tab_None |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
840 |
accessible_fromR.Immediate) |
12854 | 841 |
apply (auto intro: members.Immediate arr_member_of_Ext |
842 |
simp add: declared_in_def cdeclaredfield_def ExtCl_def) |
|
843 |
done |
|
844 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
845 |
lemma arr_Base_dyn_accessible [simp]: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
846 |
"tprg\<turnstile>(Base, fdecl (arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>)) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
847 |
in Base dyn_accessible_from S" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
848 |
apply (rule dyn_accessible_fromR.Immediate) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
849 |
apply (rule arr_member_in_Base) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
850 |
apply (simp add: permits_acc_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
851 |
done |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
852 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
853 |
lemma arr_Ext_dyn_accessible[simp]: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
854 |
"tprg\<turnstile>(Base, fdecl (arr, \<lparr>access=Public,static=True ,type=PrimT Boolean.[]\<rparr>)) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
855 |
in Ext dyn_accessible_from S" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
856 |
apply (rule dyn_accessible_fromR.Immediate) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
857 |
apply (rule arr_member_in_Ext) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
858 |
apply (simp add: permits_acc_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
859 |
done |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
860 |
|
12854 | 861 |
lemma array_of_PrimT_acc [simp]: |
862 |
"is_acc_type tprg java_lang (PrimT t.[])" |
|
863 |
apply (simp add: is_acc_type_def accessible_in_RefT_simp) |
|
864 |
done |
|
865 |
||
866 |
lemma PrimT_acc [simp]: |
|
867 |
"is_acc_type tprg java_lang (PrimT t)" |
|
868 |
apply (simp add: is_acc_type_def accessible_in_RefT_simp) |
|
869 |
done |
|
870 |
||
871 |
lemma Object_acc [simp]: |
|
872 |
"is_acc_class tprg java_lang Object" |
|
873 |
apply (auto simp add: is_acc_class_def accessible_in_RefT_simp is_public_def) |
|
874 |
done |
|
875 |
||
876 |
||
877 |
section "well-formedness" |
|
878 |
||
879 |
||
880 |
lemma wf_HasFoo: "wf_idecl tprg (HasFoo, HasFooInt)" |
|
881 |
apply (unfold wf_idecl_def HasFooInt_def) |
|
882 |
apply (auto intro!: wf_mheadI ws_idecl_HasFoo |
|
883 |
simp add: foo_sig_def foo_mhead_def mhead_resTy_simp |
|
884 |
member_is_static_simp ) |
|
885 |
done |
|
886 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
887 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
888 |
declare member_is_static_simp [simp] |
12854 | 889 |
declare wt.Skip [rule del] wt.Init [rule del] |
890 |
lemmas Base_foo_defs = Base_foo_def foo_sig_def foo_mhead_def |
|
891 |
lemmas Ext_foo_defs = Ext_foo_def foo_sig_def |
|
892 |
ML {* bind_thms ("wt_intros",map (rewrite_rule [id_def]) (thms "wt.intros")) *} |
|
893 |
lemmas wtIs = wt_Call wt_Super wt_FVar wt_StatRef wt_intros |
|
894 |
||
895 |
lemma wf_Base_foo: "wf_mdecl tprg Base Base_foo" |
|
896 |
apply (unfold Base_foo_defs ) |
|
897 |
apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs |
|
898 |
simp add: mhead_resTy_simp) |
|
899 |
done |
|
900 |
||
901 |
lemma wf_Ext_foo: "wf_mdecl tprg Ext Ext_foo" |
|
902 |
apply (unfold Ext_foo_defs ) |
|
903 |
apply (auto intro!: wf_mdeclI wf_mheadI intro!: wtIs |
|
904 |
simp add: mhead_resTy_simp ) |
|
905 |
apply (rule wt.Cast) |
|
906 |
prefer 2 |
|
907 |
apply simp |
|
908 |
apply (rule_tac [2] narrow.subcls [THEN cast.narrow]) |
|
909 |
apply (auto intro!: wtIs) |
|
910 |
done |
|
911 |
||
912 |
declare mhead_resTy_simp [simp add] |
|
913 |
declare member_is_static_simp [simp add] |
|
914 |
||
915 |
lemma wf_BaseC: "wf_cdecl tprg (Base,BaseCl)" |
|
916 |
apply (unfold wf_cdecl_def BaseCl_def arr_viewed_from_def) |
|
917 |
apply (auto intro!: wf_Base_foo) |
|
918 |
apply (auto intro!: ws_cdecl_Base simp add: Base_foo_def foo_mhead_def) |
|
919 |
apply (auto intro!: wtIs) |
|
920 |
apply (auto simp add: Base_foo_defs entails_def Let_def) |
|
921 |
apply (insert Base_foo_no_stat_override, simp add: Base_foo_def,blast)+ |
|
922 |
apply (insert Base_foo_no_hide , simp add: Base_foo_def,blast) |
|
923 |
done |
|
924 |
||
925 |
||
926 |
lemma wf_ExtC: "wf_cdecl tprg (Ext,ExtCl)" |
|
927 |
apply (unfold wf_cdecl_def ExtCl_def) |
|
928 |
apply (auto intro!: wf_Ext_foo ws_cdecl_Ext) |
|
929 |
apply (auto simp add: entails_def snd_special_simp) |
|
930 |
apply (insert Ext_foo_stat_override) |
|
931 |
apply (force simp add: qmdecl_def Ext_foo_def Base_foo_def) |
|
932 |
apply (force simp add: qmdecl_def Ext_foo_def Base_foo_def) |
|
933 |
apply (force simp add: qmdecl_def Ext_foo_def Base_foo_def) |
|
934 |
apply (insert Ext_foo_no_hide) |
|
935 |
apply (simp_all add: qmdecl_def) |
|
936 |
apply blast+ |
|
937 |
done |
|
938 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
939 |
lemma wf_MainC: "wf_cdecl tprg (Main,MainCl)" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
940 |
apply (unfold wf_cdecl_def MainCl_def) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
941 |
apply (auto intro: ws_cdecl_Main) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
942 |
done |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
943 |
|
12854 | 944 |
lemma wf_idecl_all: "p=tprg \<Longrightarrow> Ball (set Ifaces) (wf_idecl p)" |
945 |
apply (simp (no_asm) add: Ifaces_def) |
|
946 |
apply (simp (no_asm_simp)) |
|
947 |
apply (rule wf_HasFoo) |
|
948 |
done |
|
949 |
||
950 |
lemma wf_cdecl_all_standard_classes: |
|
951 |
"Ball (set standard_classes) (wf_cdecl tprg)" |
|
952 |
apply (unfold standard_classes_def Let_def |
|
953 |
ObjectC_def SXcptC_def Object_mdecls_def SXcpt_mdecls_def) |
|
954 |
apply (simp (no_asm) add: wf_cdecl_def ws_cdecls) |
|
955 |
apply (auto simp add:is_acc_class_def accessible_in_RefT_simp SXcpt_def) |
|
956 |
apply (auto simp add: Object_def Classes_def standard_classes_def |
|
957 |
SXcptC_def SXcpt_def) |
|
958 |
done |
|
959 |
||
960 |
lemma wf_cdecl_all: "p=tprg \<Longrightarrow> Ball (set Classes) (wf_cdecl p)" |
|
961 |
apply (simp (no_asm) add: Classes_def) |
|
962 |
apply (simp (no_asm_simp)) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
963 |
apply (rule wf_BaseC [THEN conjI]) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
964 |
apply (rule wf_ExtC [THEN conjI]) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
965 |
apply (rule wf_MainC [THEN conjI]) |
12854 | 966 |
apply (rule wf_cdecl_all_standard_classes) |
967 |
done |
|
968 |
||
969 |
theorem wf_tprg: "wf_prog tprg" |
|
970 |
apply (unfold wf_prog_def Let_def) |
|
971 |
apply (simp (no_asm) add: unique_ifaces unique_classes) |
|
972 |
apply (rule conjI) |
|
973 |
apply ((simp (no_asm) add: Classes_def standard_classes_def)) |
|
974 |
apply (rule conjI) |
|
975 |
apply (simp add: Object_mdecls_def) |
|
976 |
apply safe |
|
977 |
apply (cut_tac xn_cases_old) (* FIXME (insert xn_cases) *) |
|
978 |
apply (simp (no_asm_simp) add: Classes_def standard_classes_def) |
|
979 |
apply (insert wf_idecl_all) |
|
980 |
apply (insert wf_cdecl_all) |
|
981 |
apply auto |
|
982 |
done |
|
983 |
||
984 |
||
985 |
section "max spec" |
|
986 |
||
987 |
lemma appl_methds_Base_foo: |
|
988 |
"appl_methds tprg S (ClassT Base) \<lparr>name=foo, parTs=[NT]\<rparr> = |
|
989 |
{((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>) |
|
990 |
,[Class Base])}" |
|
991 |
apply (unfold appl_methds_def) |
|
992 |
apply (simp (no_asm)) |
|
993 |
apply (subgoal_tac "tprg\<turnstile>NT\<preceq> Class Base") |
|
994 |
apply (auto simp add: cmheads_def Base_foo_defs) |
|
995 |
done |
|
996 |
||
997 |
lemma max_spec_Base_foo: "max_spec tprg S (ClassT Base) \<lparr>name=foo,parTs=[NT]\<rparr> = |
|
998 |
{((ClassT Base, \<lparr>access=Public,static=False,pars=[z],resT=Class Base\<rparr>) |
|
999 |
, [Class Base])}" |
|
1000 |
apply (unfold max_spec_def) |
|
1001 |
apply (simp (no_asm) add: appl_methds_Base_foo) |
|
1002 |
apply auto |
|
1003 |
done |
|
1004 |
||
1005 |
||
1006 |
section "well-typedness" |
|
1007 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1008 |
lemma wt_test: "\<lparr>prg=tprg,cls=Main,lcl=empty(VName e\<mapsto>Class Base)\<rparr>\<turnstile>test ?pTs\<Colon>\<surd>" |
12854 | 1009 |
apply (unfold test_def arr_viewed_from_def) |
1010 |
(* ?pTs = [Class Base] *) |
|
1011 |
apply (rule wtIs (* ;; *)) |
|
1012 |
apply (rule wtIs (* Ass *)) |
|
1013 |
apply (rule wtIs (* NewC *)) |
|
1014 |
apply (rule wtIs (* LVar *)) |
|
1015 |
apply (simp) |
|
1016 |
apply (simp) |
|
1017 |
apply (simp) |
|
1018 |
apply (rule wtIs (* NewC *)) |
|
1019 |
apply (simp) |
|
1020 |
apply (simp) |
|
1021 |
apply (rule wtIs (* Try *)) |
|
1022 |
prefer 4 |
|
1023 |
apply (simp) |
|
1024 |
defer |
|
1025 |
apply (rule wtIs (* Expr *)) |
|
1026 |
apply (rule wtIs (* Call *)) |
|
1027 |
apply (rule wtIs (* Acc *)) |
|
1028 |
apply (rule wtIs (* LVar *)) |
|
1029 |
apply (simp) |
|
1030 |
apply (simp) |
|
1031 |
apply (rule wtIs (* Cons *)) |
|
1032 |
apply (rule wtIs (* Lit *)) |
|
1033 |
apply (simp) |
|
1034 |
apply (rule wtIs (* Nil *)) |
|
1035 |
apply (simp) |
|
1036 |
apply (rule max_spec_Base_foo) |
|
1037 |
apply (simp) |
|
1038 |
apply (simp) |
|
1039 |
apply (simp) |
|
1040 |
apply (simp) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1041 |
apply (simp) |
12854 | 1042 |
apply (rule wtIs (* While *)) |
1043 |
apply (rule wtIs (* Acc *)) |
|
1044 |
apply (rule wtIs (* AVar *)) |
|
1045 |
apply (rule wtIs (* Acc *)) |
|
1046 |
apply (rule wtIs (* FVar *)) |
|
1047 |
apply (rule wtIs (* StatRef *)) |
|
1048 |
apply (simp) |
|
1049 |
apply (simp) |
|
1050 |
apply (simp ) |
|
1051 |
apply (simp) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1052 |
apply (simp) |
12854 | 1053 |
apply (rule wtIs (* LVar *)) |
1054 |
apply (simp) |
|
1055 |
apply (rule wtIs (* Skip *)) |
|
1056 |
done |
|
1057 |
||
1058 |
||
1059 |
section "execution" |
|
1060 |
||
1061 |
lemma alloc_one: "\<And>a obj. \<lbrakk>the (new_Addr h) = a; atleast_free h (Suc n)\<rbrakk> \<Longrightarrow> |
|
1062 |
new_Addr h = Some a \<and> atleast_free (h(a\<mapsto>obj)) n" |
|
1063 |
apply (frule atleast_free_SucD) |
|
1064 |
apply (drule atleast_free_Suc [THEN iffD1]) |
|
1065 |
apply clarsimp |
|
1066 |
apply (frule new_Addr_SomeI) |
|
1067 |
apply force |
|
1068 |
done |
|
1069 |
||
1070 |
declare fvar_def2 [simp] avar_def2 [simp] init_lvars_def2 [simp] |
|
1071 |
declare init_obj_def [simp] var_tys_def [simp] fields_table_def [simp] |
|
1072 |
declare BaseCl_def [simp] ExtCl_def [simp] Ext_foo_def [simp] |
|
1073 |
Base_foo_defs [simp] |
|
1074 |
||
1075 |
ML {* bind_thms ("eval_intros", map |
|
1076 |
(simplify (simpset() delsimps [thm "Skip_eq"] |
|
1077 |
addsimps [thm "lvar_def"]) o |
|
1078 |
rewrite_rule [thm "assign_def",Let_def]) (thms "eval.intros")) *} |
|
1079 |
lemmas eval_Is = eval_Init eval_StatRef AbruptIs eval_intros |
|
1080 |
||
1081 |
consts |
|
1082 |
a :: loc |
|
1083 |
b :: loc |
|
1084 |
c :: loc |
|
1085 |
||
1086 |
syntax |
|
1087 |
||
1088 |
tprg :: prog |
|
1089 |
||
1090 |
obj_a :: obj |
|
1091 |
obj_b :: obj |
|
1092 |
obj_c :: obj |
|
1093 |
arr_N :: "(vn, val) table" |
|
1094 |
arr_a :: "(vn, val) table" |
|
1095 |
globs1 :: globs |
|
1096 |
globs2 :: globs |
|
1097 |
globs3 :: globs |
|
1098 |
globs8 :: globs |
|
1099 |
locs3 :: locals |
|
1100 |
locs4 :: locals |
|
1101 |
locs8 :: locals |
|
1102 |
s0 :: state |
|
1103 |
s0' :: state |
|
1104 |
s9' :: state |
|
1105 |
s1 :: state |
|
1106 |
s1' :: state |
|
1107 |
s2 :: state |
|
1108 |
s2' :: state |
|
1109 |
s3 :: state |
|
1110 |
s3' :: state |
|
1111 |
s4 :: state |
|
1112 |
s4' :: state |
|
1113 |
s6' :: state |
|
1114 |
s7' :: state |
|
1115 |
s8 :: state |
|
1116 |
s8' :: state |
|
1117 |
||
1118 |
translations |
|
1119 |
||
1120 |
"tprg" == "\<lparr>ifaces=Ifaces,classes=Classes\<rparr>" |
|
1121 |
||
1122 |
"obj_a" <= "\<lparr>tag=Arr (PrimT Boolean) two |
|
1123 |
,values=empty(Inr 0\<mapsto>Bool False)(Inr one\<mapsto>Bool False)\<rparr>" |
|
1124 |
"obj_b" <= "\<lparr>tag=CInst Ext |
|
1125 |
,values=(empty(Inl (vee, Base)\<mapsto>Null ) |
|
1126 |
(Inl (vee, Ext )\<mapsto>Intg 0))\<rparr>" |
|
1127 |
"obj_c" == "\<lparr>tag=CInst (SXcpt NullPointer),values=empty\<rparr>" |
|
1128 |
"arr_N" == "empty(Inl (arr, Base)\<mapsto>Null)" |
|
1129 |
"arr_a" == "empty(Inl (arr, Base)\<mapsto>Addr a)" |
|
1130 |
"globs1" == "empty(Inr Ext \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>) |
|
1131 |
(Inr Base \<mapsto>\<lparr>tag=arbitrary, values=arr_N\<rparr>) |
|
1132 |
(Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>)" |
|
1133 |
"globs2" == "empty(Inr Ext \<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>) |
|
1134 |
(Inr Object\<mapsto>\<lparr>tag=arbitrary, values=empty\<rparr>) |
|
1135 |
(Inl a\<mapsto>obj_a) |
|
1136 |
(Inr Base \<mapsto>\<lparr>tag=arbitrary, values=arr_a\<rparr>)" |
|
1137 |
"globs3" == "globs2(Inl b\<mapsto>obj_b)" |
|
1138 |
"globs8" == "globs3(Inl c\<mapsto>obj_c)" |
|
1139 |
"locs3" == "empty(VName e\<mapsto>Addr b)" |
|
1140 |
"locs4" == "empty(VName z\<mapsto>Null)(Inr()\<mapsto>Addr b)" |
|
1141 |
"locs8" == "locs3(VName z\<mapsto>Addr c)" |
|
1142 |
"s0" == " st empty empty" |
|
1143 |
"s0'" == " Norm s0" |
|
1144 |
"s1" == " st globs1 empty" |
|
1145 |
"s1'" == " Norm s1" |
|
1146 |
"s2" == " st globs2 empty" |
|
1147 |
"s2'" == " Norm s2" |
|
1148 |
"s3" == " st globs3 locs3 " |
|
1149 |
"s3'" == " Norm s3" |
|
1150 |
"s4" == " st globs3 locs4" |
|
1151 |
"s4'" == " Norm s4" |
|
1152 |
"s6'" == "(Some (Xcpt (Std NullPointer)), s4)" |
|
1153 |
"s7'" == "(Some (Xcpt (Std NullPointer)), s3)" |
|
1154 |
"s8" == " st globs8 locs8" |
|
1155 |
"s8'" == " Norm s8" |
|
1156 |
"s9'" == "(Some (Xcpt (Std IndOutBound)), s8)" |
|
1157 |
||
1158 |
||
1159 |
syntax "four"::nat |
|
1160 |
"tree"::nat |
|
1161 |
"two" ::nat |
|
1162 |
"one" ::nat |
|
1163 |
translations |
|
1164 |
"one" == "Suc 0" |
|
1165 |
"two" == "Suc one" |
|
1166 |
"tree" == "Suc two" |
|
1167 |
"four" == "Suc tree" |
|
1168 |
||
1169 |
declare Pair_eq [simp del] |
|
1170 |
lemma exec_test: |
|
1171 |
"\<lbrakk>the (new_Addr (heap s1)) = a; |
|
1172 |
the (new_Addr (heap ?s2)) = b; |
|
1173 |
the (new_Addr (heap ?s3)) = c\<rbrakk> \<Longrightarrow> |
|
1174 |
atleast_free (heap s0) four \<Longrightarrow> |
|
1175 |
tprg\<turnstile>s0' \<midarrow>test [Class Base]\<rightarrow> ?s9'" |
|
1176 |
apply (unfold test_def arr_viewed_from_def) |
|
1177 |
(* ?s9' = s9' *) |
|
1178 |
apply (simp (no_asm_use)) |
|
1179 |
apply (drule (1) alloc_one,clarsimp) |
|
1180 |
apply (rule eval_Is (* ;; *)) |
|
1181 |
apply (erule_tac V = "the (new_Addr ?h) = c" in thin_rl) |
|
1182 |
apply (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl) |
|
1183 |
apply (erule_tac [2] V = "atleast_free ?h four" in thin_rl) |
|
1184 |
apply (rule eval_Is (* Expr *)) |
|
1185 |
apply (rule eval_Is (* Ass *)) |
|
1186 |
apply (rule eval_Is (* LVar *)) |
|
1187 |
apply (rule eval_Is (* NewC *)) |
|
1188 |
(* begin init Ext *) |
|
1189 |
apply (erule_tac V = "the (new_Addr ?h) = b" in thin_rl) |
|
1190 |
apply (erule_tac V = "atleast_free ?h tree" in thin_rl) |
|
1191 |
apply (erule_tac [2] V = "atleast_free ?h four" in thin_rl) |
|
1192 |
apply (erule_tac [2] V = "new_Addr ?h = Some a" in thin_rl) |
|
1193 |
apply (rule eval_Is (* Init Ext *)) |
|
1194 |
apply (simp) |
|
1195 |
apply (rule conjI) |
|
1196 |
prefer 2 apply (rule conjI HOL.refl)+ |
|
1197 |
apply (rule eval_Is (* Init Base *)) |
|
1198 |
apply (simp add: arr_viewed_from_def) |
|
1199 |
apply (rule conjI) |
|
1200 |
apply (rule eval_Is (* Init Object *)) |
|
1201 |
apply (simp) |
|
1202 |
apply (rule conjI, rule HOL.refl)+ |
|
1203 |
apply (rule HOL.refl) |
|
1204 |
apply (simp) |
|
1205 |
apply (rule conjI, rule_tac [2] HOL.refl) |
|
1206 |
apply (rule eval_Is (* Expr *)) |
|
1207 |
apply (rule eval_Is (* Ass *)) |
|
1208 |
apply (rule eval_Is (* FVar *)) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1209 |
apply (rule init_done, simp) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1210 |
apply (rule eval_Is (* StatRef *)) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1211 |
apply (simp) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1212 |
apply (simp add: check_field_access_def Let_def) |
12854 | 1213 |
apply (rule eval_Is (* NewA *)) |
1214 |
apply (simp) |
|
1215 |
apply (rule eval_Is (* Lit *)) |
|
1216 |
apply (simp) |
|
1217 |
apply (rule halloc.New) |
|
1218 |
apply (simp (no_asm_simp)) |
|
1219 |
apply (drule atleast_free_weaken,rotate_tac -1,drule atleast_free_weaken) |
|
1220 |
apply (simp (no_asm_simp)) |
|
1221 |
apply (simp add: upd_gobj_def) |
|
1222 |
(* end init Ext *) |
|
1223 |
apply (rule halloc.New) |
|
1224 |
apply (drule alloc_one) |
|
1225 |
prefer 2 apply fast |
|
1226 |
apply (simp (no_asm_simp)) |
|
1227 |
apply (drule atleast_free_weaken) |
|
1228 |
apply force |
|
1229 |
apply (simp) |
|
1230 |
apply (drule alloc_one) |
|
1231 |
apply (simp (no_asm_simp)) |
|
1232 |
apply clarsimp |
|
1233 |
apply (erule_tac V = "atleast_free ?h tree" in thin_rl) |
|
1234 |
apply (drule_tac x = "a" in new_AddrD2 [THEN spec]) |
|
1235 |
apply (simp (no_asm_use)) |
|
1236 |
apply (rule eval_Is (* Try *)) |
|
1237 |
apply (rule eval_Is (* Expr *)) |
|
1238 |
(* begin method call *) |
|
1239 |
apply (rule eval_Is (* Call *)) |
|
1240 |
apply (rule eval_Is (* Acc *)) |
|
1241 |
apply (rule eval_Is (* LVar *)) |
|
1242 |
apply (rule eval_Is (* Cons *)) |
|
1243 |
apply (rule eval_Is (* Lit *)) |
|
1244 |
apply (rule eval_Is (* Nil *)) |
|
1245 |
apply (simp) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1246 |
apply (simp) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1247 |
apply (subgoal_tac |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1248 |
"tprg\<turnstile>(Ext,mdecl Ext_foo) in Ext dyn_accessible_from Main") |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1249 |
apply (simp add: check_method_access_def Let_def |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1250 |
invocation_declclass_def dynlookup_def dynmethd_Ext_foo) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1251 |
apply (rule Ext_foo_dyn_accessible) |
12854 | 1252 |
apply (rule eval_Is (* Methd *)) |
1253 |
apply (simp add: body_def Let_def) |
|
1254 |
apply (rule eval_Is (* Body *)) |
|
1255 |
apply (rule init_done, simp) |
|
1256 |
apply (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo) |
|
1257 |
apply (simp add: invocation_declclass_def dynlookup_def dynmethd_Ext_foo) |
|
1258 |
apply (rule eval_Is (* Expr *)) |
|
1259 |
apply (rule eval_Is (* Ass *)) |
|
1260 |
apply (rule eval_Is (* FVar *)) |
|
1261 |
apply (rule init_done, simp) |
|
1262 |
apply (rule eval_Is (* Cast *)) |
|
1263 |
apply (rule eval_Is (* Acc *)) |
|
1264 |
apply (rule eval_Is (* LVar *)) |
|
1265 |
apply (simp) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1266 |
apply (simp split del: split_if) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1267 |
apply (simp add: check_field_access_def Let_def) |
12854 | 1268 |
apply (rule eval_Is (* XcptE *)) |
1269 |
apply (simp) |
|
1270 |
(* end method call *) |
|
1271 |
apply (rule sxalloc.intros) |
|
1272 |
apply (rule halloc.New) |
|
1273 |
apply (erule alloc_one [THEN conjunct1]) |
|
1274 |
apply (simp (no_asm_simp)) |
|
1275 |
apply (simp (no_asm_simp)) |
|
1276 |
apply (simp add: gupd_def lupd_def obj_ty_def split del: split_if) |
|
1277 |
apply (drule alloc_one [THEN conjunct1]) |
|
1278 |
apply (simp (no_asm_simp)) |
|
1279 |
apply (erule_tac V = "atleast_free ?h two" in thin_rl) |
|
1280 |
apply (drule_tac x = "a" in new_AddrD2 [THEN spec]) |
|
1281 |
apply simp |
|
1282 |
apply (rule eval_Is (* While *)) |
|
1283 |
apply (rule eval_Is (* Acc *)) |
|
1284 |
apply (rule eval_Is (* AVar *)) |
|
1285 |
apply (rule eval_Is (* Acc *)) |
|
1286 |
apply (rule eval_Is (* FVar *)) |
|
1287 |
apply (rule init_done, simp) |
|
1288 |
apply (rule eval_Is (* StatRef *)) |
|
1289 |
apply (simp) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
1290 |
apply (simp add: check_field_access_def Let_def) |
12854 | 1291 |
apply (rule eval_Is (* Lit *)) |
1292 |
apply (simp (no_asm_simp)) |
|
1293 |
apply (auto simp add: in_bounds_def) |
|
1294 |
done |
|
1295 |
declare Pair_eq [simp] |
|
1296 |
||
1297 |
end |