13633
|
1 |
(* Title: HOL/MicroJava/BV/BVNoTypeErrors.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Gerwin Klein
|
|
4 |
*)
|
|
5 |
|
|
6 |
header {* \isaheader{Welltyped Programs produce no Type Errors} *}
|
|
7 |
|
16417
|
8 |
theory BVNoTypeError imports JVMDefensive BVSpecTypeSafe begin
|
13633
|
9 |
|
|
10 |
text {*
|
|
11 |
Some simple lemmas about the type testing functions of the
|
|
12 |
defensive JVM:
|
|
13 |
*}
|
|
14 |
lemma typeof_NoneD [simp,dest]:
|
|
15 |
"typeof (\<lambda>v. None) v = Some x \<Longrightarrow> \<not>isAddr v"
|
|
16 |
by (cases v) auto
|
|
17 |
|
|
18 |
lemma isRef_def2:
|
|
19 |
"isRef v = (v = Null \<or> (\<exists>loc. v = Addr loc))"
|
|
20 |
by (cases v) (auto simp add: isRef_def)
|
|
21 |
|
|
22 |
lemma app'Store[simp]:
|
|
23 |
"app' (Store idx, G, pc, maxs, rT, (ST,LT)) = (\<exists>T ST'. ST = T#ST' \<and> idx < length LT)"
|
|
24 |
by (cases ST, auto)
|
|
25 |
|
|
26 |
lemma app'GetField[simp]:
|
|
27 |
"app' (Getfield F C, G, pc, maxs, rT, (ST,LT)) =
|
|
28 |
(\<exists>oT vT ST'. ST = oT#ST' \<and> is_class G C \<and>
|
|
29 |
field (G,C) F = Some (C,vT) \<and> G \<turnstile> oT \<preceq> Class C)"
|
|
30 |
by (cases ST, auto)
|
|
31 |
|
|
32 |
lemma app'PutField[simp]:
|
|
33 |
"app' (Putfield F C, G, pc, maxs, rT, (ST,LT)) =
|
|
34 |
(\<exists>vT vT' oT ST'. ST = vT#oT#ST' \<and> is_class G C \<and>
|
|
35 |
field (G,C) F = Some (C, vT') \<and>
|
|
36 |
G \<turnstile> oT \<preceq> Class C \<and> G \<turnstile> vT \<preceq> vT')"
|
|
37 |
apply rule
|
|
38 |
defer
|
|
39 |
apply clarsimp
|
|
40 |
apply (cases ST)
|
|
41 |
apply simp
|
|
42 |
apply (cases "tl ST")
|
|
43 |
apply auto
|
|
44 |
done
|
|
45 |
|
|
46 |
lemma app'Checkcast[simp]:
|
|
47 |
"app' (Checkcast C, G, pc, maxs, rT, (ST,LT)) =
|
|
48 |
(\<exists>rT ST'. ST = RefT rT#ST' \<and> is_class G C)"
|
|
49 |
apply rule
|
|
50 |
defer
|
|
51 |
apply clarsimp
|
|
52 |
apply (cases ST)
|
|
53 |
apply simp
|
|
54 |
apply (cases "hd ST")
|
|
55 |
defer
|
|
56 |
apply simp
|
|
57 |
apply simp
|
|
58 |
done
|
|
59 |
|
|
60 |
|
|
61 |
lemma app'Pop[simp]:
|
|
62 |
"app' (Pop, G, pc, maxs, rT, (ST,LT)) = (\<exists>T ST'. ST = T#ST')"
|
|
63 |
by (cases ST, auto)
|
|
64 |
|
|
65 |
|
|
66 |
lemma app'Dup[simp]:
|
|
67 |
"app' (Dup, G, pc, maxs, rT, (ST,LT)) =
|
|
68 |
(\<exists>T ST'. ST = T#ST' \<and> length ST < maxs)"
|
|
69 |
by (cases ST, auto)
|
|
70 |
|
|
71 |
|
|
72 |
lemma app'Dup_x1[simp]:
|
|
73 |
"app' (Dup_x1, G, pc, maxs, rT, (ST,LT)) =
|
|
74 |
(\<exists>T1 T2 ST'. ST = T1#T2#ST' \<and> length ST < maxs)"
|
|
75 |
by (cases ST, simp, cases "tl ST", auto)
|
|
76 |
|
|
77 |
|
|
78 |
lemma app'Dup_x2[simp]:
|
|
79 |
"app' (Dup_x2, G, pc, maxs, rT, (ST,LT)) =
|
|
80 |
(\<exists>T1 T2 T3 ST'. ST = T1#T2#T3#ST' \<and> length ST < maxs)"
|
|
81 |
by (cases ST, simp, cases "tl ST", simp, cases "tl (tl ST)", auto)
|
|
82 |
|
|
83 |
|
|
84 |
lemma app'Swap[simp]:
|
|
85 |
"app' (Swap, G, pc, maxs, rT, (ST,LT)) = (\<exists>T1 T2 ST'. ST = T1#T2#ST')"
|
|
86 |
by (cases ST, simp, cases "tl ST", auto)
|
|
87 |
|
|
88 |
|
|
89 |
lemma app'IAdd[simp]:
|
|
90 |
"app' (IAdd, G, pc, maxs, rT, (ST,LT)) =
|
|
91 |
(\<exists>ST'. ST = PrimT Integer#PrimT Integer#ST')"
|
|
92 |
apply (cases ST)
|
|
93 |
apply simp
|
|
94 |
apply simp
|
|
95 |
apply (case_tac a)
|
|
96 |
apply auto
|
|
97 |
apply (case_tac prim_ty)
|
|
98 |
apply auto
|
|
99 |
apply (case_tac prim_ty)
|
|
100 |
apply auto
|
|
101 |
apply (case_tac list)
|
|
102 |
apply auto
|
|
103 |
apply (case_tac a)
|
|
104 |
apply auto
|
|
105 |
apply (case_tac prim_ty)
|
|
106 |
apply auto
|
|
107 |
done
|
|
108 |
|
|
109 |
|
|
110 |
lemma app'Ifcmpeq[simp]:
|
|
111 |
"app' (Ifcmpeq b, G, pc, maxs, rT, (ST,LT)) =
|
|
112 |
(\<exists>T1 T2 ST'. ST = T1#T2#ST' \<and> 0 \<le> b + int pc \<and>
|
|
113 |
((\<exists>p. T1 = PrimT p \<and> T1 = T2) \<or>
|
|
114 |
(\<exists>r r'. T1 = RefT r \<and> T2 = RefT r')))"
|
|
115 |
apply auto
|
|
116 |
apply (cases ST)
|
|
117 |
apply simp
|
|
118 |
apply (cases "tl ST")
|
|
119 |
apply (case_tac a)
|
|
120 |
apply auto
|
|
121 |
done
|
|
122 |
|
|
123 |
|
|
124 |
lemma app'Return[simp]:
|
|
125 |
"app' (Return, G, pc, maxs, rT, (ST,LT)) =
|
|
126 |
(\<exists>T ST'. ST = T#ST'\<and> G \<turnstile> T \<preceq> rT)"
|
|
127 |
by (cases ST, auto)
|
|
128 |
|
|
129 |
|
|
130 |
lemma app'Throw[simp]:
|
|
131 |
"app' (Throw, G, pc, maxs, rT, (ST,LT)) =
|
|
132 |
(\<exists>ST' r. ST = RefT r#ST')"
|
|
133 |
apply (cases ST, simp)
|
|
134 |
apply (cases "hd ST")
|
|
135 |
apply auto
|
|
136 |
done
|
|
137 |
|
|
138 |
|
|
139 |
lemma app'Invoke[simp]:
|
|
140 |
"app' (Invoke C mn fpTs, G, pc, maxs, rT, ST, LT) =
|
|
141 |
(\<exists>apTs X ST' mD' rT' b'.
|
|
142 |
ST = (rev apTs) @ X # ST' \<and>
|
|
143 |
length apTs = length fpTs \<and> is_class G C \<and>
|
|
144 |
(\<forall>(aT,fT)\<in>set(zip apTs fpTs). G \<turnstile> aT \<preceq> fT) \<and>
|
|
145 |
method (G,C) (mn,fpTs) = Some (mD', rT', b') \<and> G \<turnstile> X \<preceq> Class C)"
|
|
146 |
(is "?app ST LT = ?P ST LT")
|
|
147 |
proof
|
|
148 |
assume "?P ST LT" thus "?app ST LT" by (auto simp add: min_def list_all2_def)
|
|
149 |
next
|
|
150 |
assume app: "?app ST LT"
|
|
151 |
hence l: "length fpTs < length ST" by simp
|
|
152 |
obtain xs ys where xs: "ST = xs @ ys" "length xs = length fpTs"
|
|
153 |
proof -
|
|
154 |
have "ST = take (length fpTs) ST @ drop (length fpTs) ST" by simp
|
|
155 |
moreover from l have "length (take (length fpTs) ST) = length fpTs"
|
|
156 |
by (simp add: min_def)
|
|
157 |
ultimately show ?thesis ..
|
|
158 |
qed
|
|
159 |
obtain apTs where
|
|
160 |
"ST = (rev apTs) @ ys" and "length apTs = length fpTs"
|
|
161 |
proof -
|
23467
|
162 |
from xs(1) have "ST = rev (rev xs) @ ys" by simp
|
|
163 |
then show thesis by (rule that) (simp add: xs(2))
|
13633
|
164 |
qed
|
|
165 |
moreover
|
|
166 |
from l xs obtain X ST' where "ys = X#ST'" by (auto simp add: neq_Nil_conv)
|
|
167 |
ultimately
|
|
168 |
have "ST = (rev apTs) @ X # ST'" "length apTs = length fpTs" by auto
|
|
169 |
with app
|
|
170 |
show "?P ST LT"
|
|
171 |
apply (clarsimp simp add: list_all2_def min_def)
|
|
172 |
apply ((rule exI)+, (rule conjI)?)+
|
|
173 |
apply auto
|
|
174 |
done
|
|
175 |
qed
|
|
176 |
|
|
177 |
lemma approx_loc_len [simp]:
|
|
178 |
"approx_loc G hp loc LT \<Longrightarrow> length loc = length LT"
|
|
179 |
by (simp add: approx_loc_def list_all2_def)
|
|
180 |
|
|
181 |
lemma approx_stk_len [simp]:
|
|
182 |
"approx_stk G hp stk ST \<Longrightarrow> length stk = length ST"
|
|
183 |
by (simp add: approx_stk_def)
|
|
184 |
|
|
185 |
lemma isRefI [intro, simp]: "G,hp \<turnstile> v ::\<preceq> RefT T \<Longrightarrow> isRef v"
|
|
186 |
apply (drule conf_RefTD)
|
|
187 |
apply (auto simp add: isRef_def)
|
|
188 |
done
|
|
189 |
|
|
190 |
lemma isIntgI [intro, simp]: "G,hp \<turnstile> v ::\<preceq> PrimT Integer \<Longrightarrow> isIntg v"
|
|
191 |
apply (unfold conf_def)
|
|
192 |
apply auto
|
22271
|
193 |
apply (erule widen.cases)
|
13633
|
194 |
apply auto
|
|
195 |
apply (cases v)
|
|
196 |
apply auto
|
|
197 |
done
|
|
198 |
|
|
199 |
lemma list_all2_approx:
|
|
200 |
"\<And>s. list_all2 (approx_val G hp) s (map OK S) =
|
|
201 |
list_all2 (conf G hp) s S"
|
|
202 |
apply (induct S)
|
|
203 |
apply (auto simp add: list_all2_Cons2 approx_val_def)
|
|
204 |
done
|
|
205 |
|
|
206 |
lemma list_all2_conf_widen:
|
|
207 |
"wf_prog mb G \<Longrightarrow>
|
|
208 |
list_all2 (conf G hp) a b \<Longrightarrow>
|
|
209 |
list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) b c \<Longrightarrow>
|
|
210 |
list_all2 (conf G hp) a c"
|
|
211 |
apply (rule list_all2_trans)
|
|
212 |
defer
|
|
213 |
apply assumption
|
|
214 |
apply assumption
|
|
215 |
apply (drule conf_widen, assumption+)
|
|
216 |
done
|
|
217 |
|
|
218 |
|
|
219 |
text {*
|
|
220 |
The main theorem: welltyped programs do not produce type errors if they
|
|
221 |
are started in a conformant state.
|
|
222 |
*}
|
|
223 |
theorem no_type_error:
|
|
224 |
assumes welltyped: "wt_jvm_prog G Phi" and conforms: "G,Phi \<turnstile>JVM s \<surd>"
|
|
225 |
shows "exec_d G (Normal s) \<noteq> TypeError"
|
|
226 |
proof -
|
|
227 |
from welltyped obtain mb where wf: "wf_prog mb G" by (fast dest: wt_jvm_progD)
|
|
228 |
|
|
229 |
obtain xcp hp frs where s [simp]: "s = (xcp, hp, frs)" by (cases s)
|
|
230 |
|
|
231 |
from conforms have "xcp \<noteq> None \<or> frs = [] \<Longrightarrow> check G s"
|
|
232 |
by (unfold correct_state_def check_def) auto
|
|
233 |
moreover {
|
|
234 |
assume "\<not>(xcp \<noteq> None \<or> frs = [])"
|
|
235 |
then obtain stk loc C sig pc frs' where
|
|
236 |
xcp [simp]: "xcp = None" and
|
|
237 |
frs [simp]: "frs = (stk,loc,C,sig,pc)#frs'"
|
|
238 |
by (clarsimp simp add: neq_Nil_conv) fast
|
|
239 |
|
|
240 |
from conforms obtain ST LT rT maxs maxl ins et where
|
|
241 |
hconf: "G \<turnstile>h hp \<surd>" and
|
18551
|
242 |
"class": "is_class G C" and
|
13633
|
243 |
meth: "method (G, C) sig = Some (C, rT, maxs, maxl, ins, et)" and
|
|
244 |
phi: "Phi C sig ! pc = Some (ST,LT)" and
|
|
245 |
frame: "correct_frame G hp (ST,LT) maxl ins (stk,loc,C,sig,pc)" and
|
|
246 |
frames: "correct_frames G hp Phi rT sig frs'"
|
23467
|
247 |
by (auto simp add: correct_state_def) (rule that)
|
13633
|
248 |
|
|
249 |
from frame obtain
|
|
250 |
stk: "approx_stk G hp stk ST" and
|
|
251 |
loc: "approx_loc G hp loc LT" and
|
|
252 |
pc: "pc < length ins" and
|
|
253 |
len: "length loc = length (snd sig) + maxl + 1"
|
|
254 |
by (auto simp add: correct_frame_def)
|
|
255 |
|
|
256 |
note approx_val_def [simp]
|
|
257 |
|
|
258 |
from welltyped meth conforms
|
|
259 |
have "wt_instr (ins!pc) G rT (Phi C sig) maxs (length ins) et pc"
|
|
260 |
by simp (rule wt_jvm_prog_impl_wt_instr_cor)
|
|
261 |
then obtain
|
|
262 |
app': "app (ins!pc) G maxs rT pc et (Phi C sig!pc) " and
|
|
263 |
eff: "\<forall>(pc', s')\<in>set (eff (ins ! pc) G pc et (Phi C sig ! pc)). pc' < length ins"
|
|
264 |
by (simp add: wt_instr_def phi) blast
|
|
265 |
|
|
266 |
from eff
|
|
267 |
have pc': "\<forall>pc' \<in> set (succs (ins!pc) pc). pc' < length ins"
|
|
268 |
by (simp add: eff_def) blast
|
|
269 |
|
|
270 |
from app' phi
|
|
271 |
have app:
|
|
272 |
"xcpt_app (ins!pc) G pc et \<and> app' (ins!pc, G, pc, maxs, rT, (ST,LT))"
|
|
273 |
by (clarsimp simp add: app_def)
|
|
274 |
|
|
275 |
with eff stk loc pc'
|
13822
|
276 |
have "check_instr (ins!pc) G hp stk loc C sig pc maxs frs'"
|
13633
|
277 |
proof (cases "ins!pc")
|
|
278 |
case (Getfield F C)
|
|
279 |
with app stk loc phi obtain v vT stk' where
|
18551
|
280 |
"class": "is_class G C" and
|
13633
|
281 |
field: "field (G, C) F = Some (C, vT)" and
|
|
282 |
stk: "stk = v # stk'" and
|
|
283 |
conf: "G,hp \<turnstile> v ::\<preceq> Class C"
|
|
284 |
apply clarsimp
|
|
285 |
apply (blast dest: conf_widen [OF wf])
|
|
286 |
done
|
|
287 |
from conf have isRef: "isRef v" ..
|
|
288 |
moreover {
|
|
289 |
assume "v \<noteq> Null"
|
|
290 |
with conf field isRef wf
|
|
291 |
have "\<exists>D vs. hp (the_Addr v) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C"
|
|
292 |
by (auto dest!: non_np_objD)
|
|
293 |
}
|
18551
|
294 |
ultimately show ?thesis using Getfield field "class" stk hconf wf
|
13633
|
295 |
apply clarsimp
|
14045
|
296 |
apply (fastsimp intro: wf_prog_ws_prog
|
|
297 |
dest!: hconfD widen_cfs_fields oconf_objD)
|
13633
|
298 |
done
|
|
299 |
next
|
|
300 |
case (Putfield F C)
|
|
301 |
with app stk loc phi obtain v ref vT stk' where
|
18551
|
302 |
"class": "is_class G C" and
|
13633
|
303 |
field: "field (G, C) F = Some (C, vT)" and
|
|
304 |
stk: "stk = v # ref # stk'" and
|
|
305 |
confv: "G,hp \<turnstile> v ::\<preceq> vT" and
|
|
306 |
confr: "G,hp \<turnstile> ref ::\<preceq> Class C"
|
|
307 |
apply clarsimp
|
|
308 |
apply (blast dest: conf_widen [OF wf])
|
|
309 |
done
|
|
310 |
from confr have isRef: "isRef ref" ..
|
|
311 |
moreover {
|
|
312 |
assume "ref \<noteq> Null"
|
|
313 |
with confr field isRef wf
|
|
314 |
have "\<exists>D vs. hp (the_Addr ref) = Some (D,vs) \<and> G \<turnstile> D \<preceq>C C"
|
|
315 |
by (auto dest: non_np_objD)
|
|
316 |
}
|
18551
|
317 |
ultimately show ?thesis using Putfield field "class" stk confv
|
13633
|
318 |
by clarsimp
|
|
319 |
next
|
|
320 |
case (Invoke C mn ps)
|
|
321 |
with app
|
|
322 |
obtain apTs X ST' where
|
|
323 |
ST: "ST = rev apTs @ X # ST'" and
|
|
324 |
ps: "length apTs = length ps" and
|
22271
|
325 |
w: "\<forall>(x, y)\<in>set (zip apTs ps). G \<turnstile> x \<preceq> y" and
|
13633
|
326 |
C: "G \<turnstile> X \<preceq> Class C" and
|
|
327 |
mth: "method (G, C) (mn, ps) \<noteq> None"
|
|
328 |
by (simp del: app'.simps) blast
|
|
329 |
|
|
330 |
from ST stk
|
|
331 |
obtain aps x stk' where
|
|
332 |
stk': "stk = aps @ x # stk'" and
|
|
333 |
aps: "approx_stk G hp aps (rev apTs)" and
|
|
334 |
x: "G,hp \<turnstile> x ::\<preceq> X" and
|
|
335 |
l: "length aps = length apTs"
|
|
336 |
by (auto dest!: approx_stk_append)
|
|
337 |
|
|
338 |
from stk' l ps
|
|
339 |
have [simp]: "stk!length ps = x" by (simp add: nth_append)
|
|
340 |
from stk' l ps
|
|
341 |
have [simp]: "take (length ps) stk = aps" by simp
|
|
342 |
from w ps
|
|
343 |
have widen: "list_all2 (\<lambda>x y. G \<turnstile> x \<preceq> y) apTs ps"
|
|
344 |
by (simp add: list_all2_def)
|
|
345 |
|
|
346 |
from stk' l ps have "length ps < length stk" by simp
|
|
347 |
moreover
|
|
348 |
from wf x C
|
|
349 |
have x: "G,hp \<turnstile> x ::\<preceq> Class C" by (rule conf_widen)
|
|
350 |
hence "isRef x" by simp
|
|
351 |
moreover
|
|
352 |
{ assume "x \<noteq> Null"
|
|
353 |
with x
|
|
354 |
obtain D fs where
|
|
355 |
hp: "hp (the_Addr x) = Some (D,fs)" and
|
|
356 |
D: "G \<turnstile> D \<preceq>C C"
|
|
357 |
by - (drule non_npD, assumption, clarsimp, blast)
|
|
358 |
hence "hp (the_Addr x) \<noteq> None" (is ?P1) by simp
|
|
359 |
moreover
|
|
360 |
from wf mth hp D
|
|
361 |
have "method (G, cname_of hp x) (mn, ps) \<noteq> None" (is ?P2)
|
|
362 |
by (auto dest: subcls_widen_methd)
|
|
363 |
moreover
|
|
364 |
from aps have "list_all2 (conf G hp) aps (rev apTs)"
|
|
365 |
by (simp add: list_all2_approx approx_stk_def approx_loc_def)
|
|
366 |
hence "list_all2 (conf G hp) (rev aps) (rev (rev apTs))"
|
|
367 |
by (simp only: list_all2_rev)
|
|
368 |
hence "list_all2 (conf G hp) (rev aps) apTs" by simp
|
|
369 |
with wf widen
|
|
370 |
have "list_all2 (conf G hp) (rev aps) ps" (is ?P3)
|
|
371 |
by - (rule list_all2_conf_widen)
|
|
372 |
ultimately
|
|
373 |
have "?P1 \<and> ?P2 \<and> ?P3" by blast
|
|
374 |
}
|
|
375 |
moreover
|
|
376 |
note Invoke
|
|
377 |
ultimately
|
|
378 |
show ?thesis by simp
|
|
379 |
next
|
|
380 |
case Return with stk app phi meth frames
|
|
381 |
show ?thesis
|
|
382 |
apply clarsimp
|
|
383 |
apply (drule conf_widen [OF wf], assumption)
|
|
384 |
apply (clarsimp simp add: neq_Nil_conv isRef_def2)
|
|
385 |
done
|
|
386 |
qed auto
|
13822
|
387 |
hence "check G s" by (simp add: check_def meth pc)
|
13633
|
388 |
} ultimately
|
|
389 |
have "check G s" by blast
|
|
390 |
thus "exec_d G (Normal s) \<noteq> TypeError" ..
|
|
391 |
qed
|
|
392 |
|
|
393 |
|
|
394 |
text {*
|
|
395 |
The theorem above tells us that, in welltyped programs, the
|
|
396 |
defensive machine reaches the same result as the aggressive
|
|
397 |
one (after arbitrarily many steps).
|
|
398 |
*}
|
|
399 |
theorem welltyped_aggressive_imp_defensive:
|
|
400 |
"wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd> \<Longrightarrow> G \<turnstile> s -jvm\<rightarrow> t
|
|
401 |
\<Longrightarrow> G \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t)"
|
|
402 |
apply (unfold exec_all_def)
|
|
403 |
apply (erule rtrancl_induct)
|
|
404 |
apply (simp add: exec_all_d_def)
|
|
405 |
apply simp
|
|
406 |
apply (fold exec_all_def)
|
|
407 |
apply (frule BV_correct, assumption+)
|
|
408 |
apply (drule no_type_error, assumption, drule no_type_error_commutes, simp)
|
|
409 |
apply (simp add: exec_all_d_def)
|
|
410 |
apply (rule rtrancl_trans, assumption)
|
|
411 |
apply blast
|
|
412 |
done
|
|
413 |
|
|
414 |
|
13822
|
415 |
lemma neq_TypeError_eq [simp]: "s \<noteq> TypeError = (\<exists>s'. s = Normal s')"
|
|
416 |
by (cases s, auto)
|
|
417 |
|
|
418 |
theorem no_type_errors:
|
|
419 |
"wt_jvm_prog G Phi \<Longrightarrow> G,Phi \<turnstile>JVM s \<surd>
|
|
420 |
\<Longrightarrow> G \<turnstile> (Normal s) -jvmd\<rightarrow> t \<Longrightarrow> t \<noteq> TypeError"
|
|
421 |
apply (unfold exec_all_d_def)
|
|
422 |
apply (erule rtrancl_induct)
|
|
423 |
apply simp
|
|
424 |
apply (fold exec_all_d_def)
|
|
425 |
apply (auto dest: defensive_imp_aggressive BV_correct no_type_error)
|
|
426 |
done
|
|
427 |
|
|
428 |
corollary no_type_errors_initial:
|
|
429 |
fixes G ("\<Gamma>") and Phi ("\<Phi>")
|
23467
|
430 |
assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"
|
|
431 |
assumes is_class: "is_class \<Gamma> C"
|
|
432 |
and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
|
|
433 |
and m: "m \<noteq> init"
|
13822
|
434 |
defines start: "s \<equiv> start_state \<Gamma> C m"
|
|
435 |
|
23467
|
436 |
assumes s: "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> t"
|
13822
|
437 |
shows "t \<noteq> TypeError"
|
|
438 |
proof -
|
23467
|
439 |
from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
|
|
440 |
unfolding start by (rule BV_correct_initial)
|
|
441 |
from wt this s show ?thesis by (rule no_type_errors)
|
13822
|
442 |
qed
|
|
443 |
|
13633
|
444 |
text {*
|
|
445 |
As corollary we get that the aggressive and the defensive machine
|
|
446 |
are equivalent for welltyped programs (if started in a conformant
|
|
447 |
state or in the canonical start state)
|
|
448 |
*}
|
|
449 |
corollary welltyped_commutes:
|
|
450 |
fixes G ("\<Gamma>") and Phi ("\<Phi>")
|
23467
|
451 |
assumes wt: "wt_jvm_prog \<Gamma> \<Phi>" and *: "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
|
13633
|
452 |
shows "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s -jvm\<rightarrow> t"
|
23467
|
453 |
apply rule
|
|
454 |
apply (erule defensive_imp_aggressive, rule welltyped_aggressive_imp_defensive)
|
|
455 |
apply (rule wt)
|
|
456 |
apply (rule *)
|
|
457 |
apply assumption
|
|
458 |
done
|
13633
|
459 |
|
|
460 |
corollary welltyped_initial_commutes:
|
|
461 |
fixes G ("\<Gamma>") and Phi ("\<Phi>")
|
23467
|
462 |
assumes wt: "wt_jvm_prog \<Gamma> \<Phi>"
|
|
463 |
assumes is_class: "is_class \<Gamma> C"
|
|
464 |
and method: "method (\<Gamma>,C) (m,[]) = Some (C, b)"
|
|
465 |
and m: "m \<noteq> init"
|
13633
|
466 |
defines start: "s \<equiv> start_state \<Gamma> C m"
|
|
467 |
shows "\<Gamma> \<turnstile> (Normal s) -jvmd\<rightarrow> (Normal t) = \<Gamma> \<turnstile> s -jvm\<rightarrow> t"
|
|
468 |
proof -
|
23467
|
469 |
from wt is_class method have "\<Gamma>,\<Phi> \<turnstile>JVM s \<surd>"
|
|
470 |
unfolding start by (rule BV_correct_initial)
|
|
471 |
with wt show ?thesis by (rule welltyped_commutes)
|
13633
|
472 |
qed
|
|
473 |
|
|
474 |
end
|