author | haftmann |
Tue, 24 Nov 2009 14:37:23 +0100 | |
changeset 33954 | 1bc3b688548c |
parent 31998 | 2c7a24f74db9 |
child 35102 | cc7a0b9f938c |
permissions | -rwxr-xr-x |
12951 | 1 |
(* Title: HOL/MicroJava/BV/BVExample.thy |
2 |
Author: Gerwin Klein |
|
3 |
*) |
|
4 |
||
12972 | 5 |
header {* \isaheader{Example Welltypings}\label{sec:BVExample} *} |
12951 | 6 |
|
23022
9872ef956276
added qualification for ambiguous definition names
haftmann
parents:
22271
diff
changeset
|
7 |
theory BVExample |
24351 | 8 |
imports "../JVM/JVMListExample" BVSpecTypeSafe JVM Executable_Set |
23022
9872ef956276
added qualification for ambiguous definition names
haftmann
parents:
22271
diff
changeset
|
9 |
begin |
12951 | 10 |
|
12972 | 11 |
text {* |
12 |
This theory shows type correctness of the example program in section |
|
13 |
\ref{sec:JVMListExample} (p. \pageref{sec:JVMListExample}) by |
|
14 |
explicitly providing a welltyping. It also shows that the start |
|
15 |
state of the program conforms to the welltyping; hence type safe |
|
16 |
execution is guaranteed. |
|
17 |
*} |
|
18 |
||
12951 | 19 |
section "Setup" |
20 |
text {* |
|
21 |
Since the types @{typ cnam}, @{text vnam}, and @{text mname} are |
|
22 |
anonymous, we describe distinctness of names in the example by axioms: |
|
23 |
*} |
|
24 |
axioms |
|
25 |
distinct_classes: "list_nam \<noteq> test_nam" |
|
26 |
distinct_fields: "val_nam \<noteq> next_nam" |
|
27 |
||
13101 | 28 |
text {* Abbreviations for definitions we will have to use often in the |
12951 | 29 |
proofs below: *} |
13101 | 30 |
lemmas name_defs = list_name_def test_name_def val_name_def next_name_def |
12951 | 31 |
lemmas system_defs = SystemClasses_def ObjectC_def NullPointerC_def |
32 |
OutOfMemoryC_def ClassCastC_def |
|
33 |
lemmas class_defs = list_class_def test_class_def |
|
34 |
||
35 |
text {* These auxiliary proofs are for efficiency: class lookup, |
|
36 |
subclass relation, method and field lookup are computed only once: |
|
37 |
*} |
|
38 |
lemma class_Object [simp]: |
|
28520 | 39 |
"class E Object = Some (undefined, [],[])" |
12951 | 40 |
by (simp add: class_def system_defs E_def) |
41 |
||
42 |
lemma class_NullPointer [simp]: |
|
43 |
"class E (Xcpt NullPointer) = Some (Object, [], [])" |
|
44 |
by (simp add: class_def system_defs E_def) |
|
45 |
||
46 |
lemma class_OutOfMemory [simp]: |
|
47 |
"class E (Xcpt OutOfMemory) = Some (Object, [], [])" |
|
48 |
by (simp add: class_def system_defs E_def) |
|
49 |
||
50 |
lemma class_ClassCast [simp]: |
|
51 |
"class E (Xcpt ClassCast) = Some (Object, [], [])" |
|
52 |
by (simp add: class_def system_defs E_def) |
|
53 |
||
54 |
lemma class_list [simp]: |
|
55 |
"class E list_name = Some list_class" |
|
56 |
by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric]) |
|
57 |
||
58 |
lemma class_test [simp]: |
|
59 |
"class E test_name = Some test_class" |
|
60 |
by (simp add: class_def system_defs E_def name_defs distinct_classes [symmetric]) |
|
61 |
||
62 |
lemma E_classes [simp]: |
|
63 |
"{C. is_class E C} = {list_name, test_name, Xcpt NullPointer, |
|
64 |
Xcpt ClassCast, Xcpt OutOfMemory, Object}" |
|
65 |
by (auto simp add: is_class_def class_def system_defs E_def name_defs class_defs) |
|
66 |
||
67 |
text {* The subclass releation spelled out: *} |
|
68 |
lemma subcls1: |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
69 |
"subcls1 E = {(list_name,Object), (test_name,Object), (Xcpt NullPointer, Object), |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
70 |
(Xcpt ClassCast, Object), (Xcpt OutOfMemory, Object)}" |
31197
c1c163ec6c44
fine-tuned elimination of comprehensions involving x=t.
nipkow
parents:
31168
diff
changeset
|
71 |
apply (simp add: subcls1_def2) |
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
28520
diff
changeset
|
72 |
apply (simp add: name_defs class_defs system_defs E_def class_def) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
73 |
apply (simp add: Sigma_def) |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
74 |
apply auto |
31166
a90fe83f58ea
"{x. P x & x=t & Q x}" is now rewritten to "if P t & Q t then {t} else {}"
nipkow
parents:
28520
diff
changeset
|
75 |
done |
12951 | 76 |
|
77 |
text {* The subclass relation is acyclic; hence its converse is well founded: *} |
|
78 |
lemma notin_rtrancl: |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
79 |
"(a, b) \<in> r\<^sup>* \<Longrightarrow> a \<noteq> b \<Longrightarrow> (\<And>y. (a, y) \<notin> r) \<Longrightarrow> False" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
80 |
by (auto elim: converse_rtranclE) |
12951 | 81 |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
82 |
lemma acyclic_subcls1_E: "acyclic (subcls1 E)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
83 |
apply (rule acyclicI) |
12951 | 84 |
apply (simp add: subcls1) |
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
85 |
apply (auto dest!: tranclD) |
12951 | 86 |
apply (auto elim!: notin_rtrancl simp add: name_defs distinct_classes) |
87 |
done |
|
88 |
||
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
89 |
lemma wf_subcls1_E: "wf ((subcls1 E)\<inverse>)" |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
31998
diff
changeset
|
90 |
apply (rule finite_acyclic_wf_converse) |
23757 | 91 |
apply (simp add: subcls1 del: insert_iff) |
12951 | 92 |
apply (rule acyclic_subcls1_E) |
93 |
done |
|
94 |
||
95 |
text {* Method and field lookup: *} |
|
96 |
lemma method_Object [simp]: |
|
31852
a16bb835e97d
explicit Set constructor for code generated for sets
haftmann
parents:
31197
diff
changeset
|
97 |
"method (E, Object) = Map.empty" |
12951 | 98 |
by (simp add: method_rec_lemma [OF class_Object wf_subcls1_E]) |
99 |
||
100 |
lemma method_append [simp]: |
|
101 |
"method (E, list_name) (append_name, [Class list_name]) = |
|
102 |
Some (list_name, PrimT Void, 3, 0, append_ins, [(1, 2, 8, Xcpt NullPointer)])" |
|
103 |
apply (insert class_list) |
|
104 |
apply (unfold list_class_def) |
|
105 |
apply (drule method_rec_lemma [OF _ wf_subcls1_E]) |
|
106 |
apply simp |
|
107 |
done |
|
108 |
||
109 |
lemma method_makelist [simp]: |
|
110 |
"method (E, test_name) (makelist_name, []) = |
|
111 |
Some (test_name, PrimT Void, 3, 2, make_list_ins, [])" |
|
112 |
apply (insert class_test) |
|
113 |
apply (unfold test_class_def) |
|
114 |
apply (drule method_rec_lemma [OF _ wf_subcls1_E]) |
|
115 |
apply simp |
|
116 |
done |
|
117 |
||
118 |
lemma field_val [simp]: |
|
119 |
"field (E, list_name) val_name = Some (list_name, PrimT Integer)" |
|
23022
9872ef956276
added qualification for ambiguous definition names
haftmann
parents:
22271
diff
changeset
|
120 |
apply (unfold TypeRel.field_def) |
12951 | 121 |
apply (insert class_list) |
122 |
apply (unfold list_class_def) |
|
123 |
apply (drule fields_rec_lemma [OF _ wf_subcls1_E]) |
|
124 |
apply simp |
|
125 |
done |
|
126 |
||
127 |
lemma field_next [simp]: |
|
128 |
"field (E, list_name) next_name = Some (list_name, Class list_name)" |
|
23022
9872ef956276
added qualification for ambiguous definition names
haftmann
parents:
22271
diff
changeset
|
129 |
apply (unfold TypeRel.field_def) |
12951 | 130 |
apply (insert class_list) |
131 |
apply (unfold list_class_def) |
|
132 |
apply (drule fields_rec_lemma [OF _ wf_subcls1_E]) |
|
133 |
apply (simp add: name_defs distinct_fields [symmetric]) |
|
134 |
done |
|
135 |
||
136 |
lemma [simp]: "fields (E, Object) = []" |
|
137 |
by (simp add: fields_rec_lemma [OF class_Object wf_subcls1_E]) |
|
138 |
||
139 |
lemma [simp]: "fields (E, Xcpt NullPointer) = []" |
|
140 |
by (simp add: fields_rec_lemma [OF class_NullPointer wf_subcls1_E]) |
|
141 |
||
142 |
lemma [simp]: "fields (E, Xcpt ClassCast) = []" |
|
143 |
by (simp add: fields_rec_lemma [OF class_ClassCast wf_subcls1_E]) |
|
144 |
||
145 |
lemma [simp]: "fields (E, Xcpt OutOfMemory) = []" |
|
146 |
by (simp add: fields_rec_lemma [OF class_OutOfMemory wf_subcls1_E]) |
|
147 |
||
148 |
lemma [simp]: "fields (E, test_name) = []" |
|
149 |
apply (insert class_test) |
|
150 |
apply (unfold test_class_def) |
|
151 |
apply (drule fields_rec_lemma [OF _ wf_subcls1_E]) |
|
152 |
apply simp |
|
153 |
done |
|
154 |
||
155 |
lemmas [simp] = is_class_def |
|
156 |
||
157 |
text {* |
|
158 |
The next definition and three proof rules implement an algorithm to |
|
159 |
enumarate natural numbers. The command @{text "apply (elim pc_end pc_next pc_0"} |
|
160 |
transforms a goal of the form |
|
161 |
@{prop [display] "pc < n \<Longrightarrow> P pc"} |
|
162 |
into a series of goals |
|
163 |
@{prop [display] "P 0"} |
|
164 |
@{prop [display] "P (Suc 0)"} |
|
165 |
||
166 |
@{text "\<dots>"} |
|
167 |
||
168 |
@{prop [display] "P n"} |
|
169 |
*} |
|
170 |
constdefs |
|
171 |
intervall :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> bool" ("_ \<in> [_, _')") |
|
172 |
"x \<in> [a, b) \<equiv> a \<le> x \<and> x < b" |
|
173 |
||
174 |
lemma pc_0: "x < n \<Longrightarrow> (x \<in> [0, n) \<Longrightarrow> P x) \<Longrightarrow> P x" |
|
175 |
by (simp add: intervall_def) |
|
176 |
||
177 |
lemma pc_next: "x \<in> [n0, n) \<Longrightarrow> P n0 \<Longrightarrow> (x \<in> [Suc n0, n) \<Longrightarrow> P x) \<Longrightarrow> P x" |
|
178 |
apply (cases "x=n0") |
|
13187 | 179 |
apply (auto simp add: intervall_def) |
12951 | 180 |
done |
181 |
||
182 |
lemma pc_end: "x \<in> [n,n) \<Longrightarrow> P x" |
|
183 |
by (unfold intervall_def) arith |
|
184 |
||
185 |
||
186 |
section "Program structure" |
|
187 |
||
188 |
text {* |
|
189 |
The program is structurally wellformed: |
|
190 |
*} |
|
14045 | 191 |
|
12951 | 192 |
lemma wf_struct: |
193 |
"wf_prog (\<lambda>G C mb. True) E" (is "wf_prog ?mb E") |
|
194 |
proof - |
|
195 |
have "unique E" |
|
196 |
by (simp add: system_defs E_def class_defs name_defs distinct_classes) |
|
197 |
moreover |
|
198 |
have "set SystemClasses \<subseteq> set E" by (simp add: system_defs E_def) |
|
199 |
hence "wf_syscls E" by (rule wf_syscls) |
|
200 |
moreover |
|
201 |
have "wf_cdecl ?mb E ObjectC" by (simp add: wf_cdecl_def ObjectC_def) |
|
202 |
moreover |
|
203 |
have "wf_cdecl ?mb E NullPointerC" |
|
204 |
by (auto elim: notin_rtrancl |
|
205 |
simp add: wf_cdecl_def name_defs NullPointerC_def subcls1) |
|
206 |
moreover |
|
207 |
have "wf_cdecl ?mb E ClassCastC" |
|
208 |
by (auto elim: notin_rtrancl |
|
209 |
simp add: wf_cdecl_def name_defs ClassCastC_def subcls1) |
|
210 |
moreover |
|
211 |
have "wf_cdecl ?mb E OutOfMemoryC" |
|
212 |
by (auto elim: notin_rtrancl |
|
213 |
simp add: wf_cdecl_def name_defs OutOfMemoryC_def subcls1) |
|
214 |
moreover |
|
215 |
have "wf_cdecl ?mb E (list_name, list_class)" |
|
216 |
apply (auto elim!: notin_rtrancl |
|
217 |
simp add: wf_cdecl_def wf_fdecl_def list_class_def |
|
218 |
wf_mdecl_def wf_mhead_def subcls1) |
|
219 |
apply (auto simp add: name_defs distinct_classes distinct_fields) |
|
220 |
done |
|
221 |
moreover |
|
222 |
have "wf_cdecl ?mb E (test_name, test_class)" |
|
223 |
apply (auto elim!: notin_rtrancl |
|
224 |
simp add: wf_cdecl_def wf_fdecl_def test_class_def |
|
225 |
wf_mdecl_def wf_mhead_def subcls1) |
|
226 |
apply (auto simp add: name_defs distinct_classes distinct_fields) |
|
227 |
done |
|
228 |
ultimately |
|
14045 | 229 |
show ?thesis |
230 |
by (simp add: wf_prog_def ws_prog_def wf_cdecl_mrT_cdecl_mdecl E_def SystemClasses_def) |
|
12951 | 231 |
qed |
232 |
||
233 |
section "Welltypings" |
|
234 |
text {* |
|
235 |
We show welltypings of the methods @{term append_name} in class @{term list_name}, |
|
236 |
and @{term makelist_name} in class @{term test_name}: |
|
237 |
*} |
|
238 |
lemmas eff_simps [simp] = eff_def norm_eff_def xcpt_eff_def |
|
239 |
declare appInvoke [simp del] |
|
240 |
||
241 |
constdefs |
|
242 |
phi_append :: method_type ("\<phi>\<^sub>a") |
|
243 |
"\<phi>\<^sub>a \<equiv> map (\<lambda>(x,y). Some (x, map OK y)) [ |
|
244 |
( [], [Class list_name, Class list_name]), |
|
245 |
( [Class list_name], [Class list_name, Class list_name]), |
|
246 |
( [Class list_name], [Class list_name, Class list_name]), |
|
247 |
( [Class list_name, Class list_name], [Class list_name, Class list_name]), |
|
248 |
([NT, Class list_name, Class list_name], [Class list_name, Class list_name]), |
|
249 |
( [Class list_name], [Class list_name, Class list_name]), |
|
250 |
( [Class list_name, Class list_name], [Class list_name, Class list_name]), |
|
251 |
( [PrimT Void], [Class list_name, Class list_name]), |
|
252 |
( [Class Object], [Class list_name, Class list_name]), |
|
253 |
( [], [Class list_name, Class list_name]), |
|
254 |
( [Class list_name], [Class list_name, Class list_name]), |
|
255 |
( [Class list_name, Class list_name], [Class list_name, Class list_name]), |
|
256 |
( [], [Class list_name, Class list_name]), |
|
257 |
( [PrimT Void], [Class list_name, Class list_name])]" |
|
258 |
||
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
259 |
|
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
260 |
lemma bounded_append [simp]: |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
261 |
"check_bounded append_ins [(Suc 0, 2, 8, Xcpt NullPointer)]" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
262 |
apply (simp add: check_bounded_def) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
263 |
apply (simp add: nat_number append_ins_def) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
264 |
apply (rule allI, rule impI) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
265 |
apply (elim pc_end pc_next pc_0) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
266 |
apply auto |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
267 |
done |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
268 |
|
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
269 |
lemma types_append [simp]: "check_types E 3 (Suc (Suc 0)) (map OK \<phi>\<^sub>a)" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
270 |
apply (auto simp add: check_types_def phi_append_def JVM_states_unfold) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
271 |
apply (unfold list_def) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
272 |
apply auto |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
273 |
done |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
274 |
|
12951 | 275 |
lemma wt_append [simp]: |
276 |
"wt_method E list_name [Class list_name] (PrimT Void) 3 0 append_ins |
|
277 |
[(Suc 0, 2, 8, Xcpt NullPointer)] \<phi>\<^sub>a" |
|
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
278 |
apply (simp add: wt_method_def wt_start_def wt_instr_def) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
279 |
apply (simp add: phi_append_def append_ins_def) |
12951 | 280 |
apply clarify |
281 |
apply (elim pc_end pc_next pc_0) |
|
282 |
apply simp |
|
283 |
apply (fastsimp simp add: match_exception_entry_def sup_state_conv subcls1) |
|
284 |
apply simp |
|
285 |
apply simp |
|
286 |
apply (fastsimp simp add: sup_state_conv subcls1) |
|
287 |
apply simp |
|
288 |
apply (simp add: app_def xcpt_app_def) |
|
289 |
apply simp |
|
290 |
apply simp |
|
291 |
apply simp |
|
292 |
apply (simp add: match_exception_entry_def) |
|
293 |
apply (simp add: match_exception_entry_def) |
|
294 |
apply simp |
|
295 |
apply simp |
|
296 |
done |
|
297 |
||
13006 | 298 |
text {* Some abbreviations for readability *} |
12951 | 299 |
syntax |
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
300 |
Clist :: ty |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
301 |
Ctest :: ty |
12951 | 302 |
translations |
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
303 |
"Clist" == "Class list_name" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
304 |
"Ctest" == "Class test_name" |
12951 | 305 |
|
306 |
constdefs |
|
307 |
phi_makelist :: method_type ("\<phi>\<^sub>m") |
|
308 |
"\<phi>\<^sub>m \<equiv> map (\<lambda>(x,y). Some (x, y)) [ |
|
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
309 |
( [], [OK Ctest, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
310 |
( [Clist], [OK Ctest, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
311 |
( [Clist, Clist], [OK Ctest, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
312 |
( [Clist], [OK Clist, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
313 |
( [PrimT Integer, Clist], [OK Clist, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
314 |
( [], [OK Clist, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
315 |
( [Clist], [OK Clist, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
316 |
( [Clist, Clist], [OK Clist, Err , Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
317 |
( [Clist], [OK Clist, OK Clist, Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
318 |
( [PrimT Integer, Clist], [OK Clist, OK Clist, Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
319 |
( [], [OK Clist, OK Clist, Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
320 |
( [Clist], [OK Clist, OK Clist, Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
321 |
( [Clist, Clist], [OK Clist, OK Clist, Err ]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
322 |
( [Clist], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
323 |
( [PrimT Integer, Clist], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
324 |
( [], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
325 |
( [Clist], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
326 |
( [Clist, Clist], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
327 |
( [PrimT Void], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
328 |
( [], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
329 |
( [Clist], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
330 |
( [Clist, Clist], [OK Clist, OK Clist, OK Clist]), |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
331 |
( [PrimT Void], [OK Clist, OK Clist, OK Clist])]" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
332 |
|
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
333 |
lemma bounded_makelist [simp]: "check_bounded make_list_ins []" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
334 |
apply (simp add: check_bounded_def) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
335 |
apply (simp add: nat_number make_list_ins_def) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
336 |
apply (rule allI, rule impI) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
337 |
apply (elim pc_end pc_next pc_0) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
338 |
apply auto |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
339 |
done |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
340 |
|
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
341 |
lemma types_makelist [simp]: "check_types E 3 (Suc (Suc (Suc 0))) (map OK \<phi>\<^sub>m)" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
342 |
apply (auto simp add: check_types_def phi_makelist_def JVM_states_unfold) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
343 |
apply (unfold list_def) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
344 |
apply auto |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
345 |
done |
12951 | 346 |
|
347 |
lemma wt_makelist [simp]: |
|
348 |
"wt_method E test_name [] (PrimT Void) 3 2 make_list_ins [] \<phi>\<^sub>m" |
|
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
349 |
apply (simp add: wt_method_def) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13187
diff
changeset
|
350 |
apply (simp add: make_list_ins_def phi_makelist_def) |
13043
ad1828b479b7
renamed nat_number_of to nat_number (avoid clash with separate theorem);
wenzelm
parents:
13006
diff
changeset
|
351 |
apply (simp add: wt_start_def nat_number) |
12951 | 352 |
apply (simp add: wt_instr_def) |
353 |
apply clarify |
|
354 |
apply (elim pc_end pc_next pc_0) |
|
355 |
apply (simp add: match_exception_entry_def) |
|
356 |
apply simp |
|
357 |
apply simp |
|
358 |
apply simp |
|
359 |
apply (simp add: match_exception_entry_def) |
|
360 |
apply (simp add: match_exception_entry_def) |
|
361 |
apply simp |
|
362 |
apply simp |
|
363 |
apply simp |
|
364 |
apply (simp add: match_exception_entry_def) |
|
365 |
apply (simp add: match_exception_entry_def) |
|
366 |
apply simp |
|
367 |
apply simp |
|
368 |
apply simp |
|
369 |
apply (simp add: match_exception_entry_def) |
|
370 |
apply (simp add: match_exception_entry_def) |
|
371 |
apply simp |
|
372 |
apply (simp add: app_def xcpt_app_def) |
|
13101 | 373 |
apply simp |
12951 | 374 |
apply simp |
375 |
apply simp |
|
13101 | 376 |
apply (simp add: app_def xcpt_app_def) |
12951 | 377 |
apply simp |
378 |
done |
|
379 |
||
380 |
text {* The whole program is welltyped: *} |
|
381 |
constdefs |
|
382 |
Phi :: prog_type ("\<Phi>") |
|
13101 | 383 |
"\<Phi> C sg \<equiv> if C = test_name \<and> sg = (makelist_name, []) then \<phi>\<^sub>m else |
384 |
if C = list_name \<and> sg = (append_name, [Class list_name]) then \<phi>\<^sub>a else []" |
|
13139 | 385 |
|
12951 | 386 |
lemma wf_prog: |
13101 | 387 |
"wt_jvm_prog E \<Phi>" |
12951 | 388 |
apply (unfold wt_jvm_prog_def) |
389 |
apply (rule wf_mb'E [OF wf_struct]) |
|
390 |
apply (simp add: E_def) |
|
391 |
apply clarify |
|
392 |
apply (fold E_def) |
|
13101 | 393 |
apply (simp add: system_defs class_defs Phi_def) |
12951 | 394 |
apply auto |
13101 | 395 |
done |
12951 | 396 |
|
397 |
||
398 |
section "Conformance" |
|
399 |
text {* Execution of the program will be typesafe, because its |
|
400 |
start state conforms to the welltyping: *} |
|
401 |
||
13052 | 402 |
lemma "E,\<Phi> \<turnstile>JVM start_state E test_name makelist_name \<surd>" |
403 |
apply (rule BV_correct_initial) |
|
404 |
apply (rule wf_prog) |
|
405 |
apply simp |
|
406 |
apply simp |
|
12951 | 407 |
done |
408 |
||
13092 | 409 |
|
410 |
section "Example for code generation: inferring method types" |
|
411 |
||
28520 | 412 |
definition test_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> |
413 |
exception_table \<Rightarrow> instr list \<Rightarrow> JVMType.state list" where |
|
414 |
"test_kil G C pTs rT mxs mxl et instr = |
|
13092 | 415 |
(let first = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)); |
416 |
start = OK first#(replicate (size instr - 1) (OK None)) |
|
417 |
in kiljvm G mxs (1+size pTs+mxl) rT et instr start)" |
|
418 |
||
419 |
lemma [code]: |
|
15045 | 420 |
"unstables r step ss = (UN p:{..<size ss}. if \<not>stable r step ss p then {p} else {})" |
13092 | 421 |
apply (unfold unstables_def) |
422 |
apply (rule equalityI) |
|
423 |
apply (rule subsetI) |
|
424 |
apply (erule CollectE) |
|
425 |
apply (erule conjE) |
|
426 |
apply (rule UN_I) |
|
427 |
apply simp |
|
428 |
apply simp |
|
429 |
apply (rule subsetI) |
|
430 |
apply (erule UN_E) |
|
431 |
apply (case_tac "\<not> stable r step ss p") |
|
432 |
apply simp+ |
|
433 |
done |
|
434 |
||
28520 | 435 |
definition some_elem :: "'a set \<Rightarrow> 'a" where |
436 |
"some_elem = (%S. SOME x. x : S)" |
|
13092 | 437 |
|
438 |
consts_code |
|
31852
a16bb835e97d
explicit Set constructor for code generated for sets
haftmann
parents:
31197
diff
changeset
|
439 |
"some_elem" ("(case/ _ of/ {*Set*}/ xs/ =>/ hd/ xs)") |
13092 | 440 |
|
28520 | 441 |
text {* This code setup is just a demonstration and \emph{not} sound! *} |
442 |
||
443 |
lemma False |
|
444 |
proof - |
|
445 |
have "some_elem (set [False, True]) = False" |
|
446 |
by evaluation |
|
447 |
moreover have "some_elem (set [True, False]) = True" |
|
448 |
by evaluation |
|
449 |
ultimately show False |
|
450 |
by (simp add: some_elem_def) |
|
451 |
qed |
|
452 |
||
453 |
lemma [code]: |
|
31867 | 454 |
"iter f step ss w = while (\<lambda>(ss, w). \<not> is_empty w) |
28520 | 455 |
(\<lambda>(ss, w). |
456 |
let p = some_elem w in propa f (step p (ss ! p)) ss (w - {p})) |
|
457 |
(ss, w)" |
|
31852
a16bb835e97d
explicit Set constructor for code generated for sets
haftmann
parents:
31197
diff
changeset
|
458 |
unfolding iter_def List_Set.is_empty_def some_elem_def .. |
20593 | 459 |
|
13092 | 460 |
lemma JVM_sup_unfold [code]: |
461 |
"JVMType.sup S m n = lift2 (Opt.sup |
|
462 |
(Product.sup (Listn.sup (JType.sup S)) |
|
463 |
(\<lambda>x y. OK (map2 (lift2 (JType.sup S)) x y))))" |
|
464 |
apply (unfold JVMType.sup_def JVMType.sl_def Opt.esl_def Err.sl_def |
|
465 |
stk_esl_def reg_sl_def Product.esl_def |
|
466 |
Listn.sl_def upto_esl_def JType.esl_def Err.esl_def) |
|
467 |
by simp |
|
468 |
||
28520 | 469 |
lemmas [code] = JType.sup_def [unfolded exec_lub_def] JVM_le_unfold |
13092 | 470 |
|
31998
2c7a24f74db9
code attributes use common underscore convention
haftmann
parents:
31867
diff
changeset
|
471 |
lemmas [code_ind] = rtranclp.rtrancl_refl converse_rtranclp_into_rtranclp |
13092 | 472 |
|
17145 | 473 |
code_module BV |
474 |
contains |
|
13092 | 475 |
test1 = "test_kil E list_name [Class list_name] (PrimT Void) 3 0 |
476 |
[(Suc 0, 2, 8, Xcpt NullPointer)] append_ins" |
|
477 |
test2 = "test_kil E test_name [] (PrimT Void) 3 2 [] make_list_ins" |
|
17145 | 478 |
ML BV.test1 |
479 |
ML BV.test2 |
|
13092 | 480 |
|
13006 | 481 |
end |