author | haftmann |
Sat, 05 Jul 2014 11:01:53 +0200 | |
changeset 57514 | bdc2c6b40bf2 |
parent 46226 | e88e980ed735 |
child 58886 | 8a6cac7c7247 |
permissions | -rw-r--r-- |
12516 | 1 |
(* Title: HOL/MicroJava/BV/JVM.thy |
2 |
Author: Tobias Nipkow, Gerwin Klein |
|
10592 | 3 |
Copyright 2000 TUM |
4 |
*) |
|
5 |
||
12911 | 6 |
header {* \isaheader{Kildall for the JVM}\label{sec:JVM} *} |
10592 | 7 |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33639
diff
changeset
|
8 |
theory JVM |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33639
diff
changeset
|
9 |
imports Typing_Framework_JVM |
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33639
diff
changeset
|
10 |
begin |
10592 | 11 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
12 |
definition kiljvm :: "jvm_prog \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> ty \<Rightarrow> exception_table \<Rightarrow> |
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
13 |
instr list \<Rightarrow> JVMType.state list \<Rightarrow> JVMType.state list" where |
12516 | 14 |
"kiljvm G maxs maxr rT et bs == |
15 |
kildall (JVMType.le G maxs maxr) (JVMType.sup G maxs maxr) (exec G maxs rT et bs)" |
|
10592 | 16 |
|
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
17 |
definition wt_kil :: "jvm_prog \<Rightarrow> cname \<Rightarrow> ty list \<Rightarrow> ty \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> |
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
18 |
exception_table \<Rightarrow> instr list \<Rightarrow> bool" where |
12516 | 19 |
"wt_kil G C pTs rT mxs mxl et ins == |
13066 | 20 |
check_bounded ins et \<and> 0 < size ins \<and> |
10637 | 21 |
(let first = Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err)); |
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11299
diff
changeset
|
22 |
start = OK first#(replicate (size ins - 1) (OK None)); |
12516 | 23 |
result = kiljvm G mxs (1+size pTs+mxl) rT et ins start |
10637 | 24 |
in \<forall>n < size ins. result!n \<noteq> Err)" |
25 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
33954
diff
changeset
|
26 |
definition wt_jvm_prog_kildall :: "jvm_prog \<Rightarrow> bool" where |
10637 | 27 |
"wt_jvm_prog_kildall G == |
12516 | 28 |
wf_prog (\<lambda>G C (sig,rT,(maxs,maxl,b,et)). wt_kil G C (snd sig) rT maxs maxl et b) G" |
10592 | 29 |
|
30 |
theorem is_bcv_kiljvm: |
|
13066 | 31 |
"\<lbrakk> wf_prog wf_mb G; bounded (exec G maxs rT et bs) (size bs) \<rbrakk> \<Longrightarrow> |
12516 | 32 |
is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) |
33 |
(size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)" |
|
10592 | 34 |
apply (unfold kiljvm_def sl_triple_conv) |
35 |
apply (rule is_bcv_kildall) |
|
36 |
apply (simp (no_asm) add: sl_triple_conv [symmetric]) |
|
14045 | 37 |
apply (force intro!: semilat_JVM_slI dest: wf_acyclic |
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
26450
diff
changeset
|
38 |
simp add: symmetric sl_triple_conv) |
10592 | 39 |
apply (simp (no_asm) add: JVM_le_unfold) |
40 |
apply (blast intro!: order_widen wf_converse_subcls1_impl_acc_subtype |
|
33954
1bc3b688548c
backported parts of abstract byte code verifier from AFP/Jinja
haftmann
parents:
33639
diff
changeset
|
41 |
dest: wf_subcls1 wf_acyclic wf_prog_ws_prog) |
10592 | 42 |
apply (simp add: JVM_le_unfold) |
43 |
apply (erule exec_pres_type) |
|
13066 | 44 |
apply assumption |
14045 | 45 |
apply (drule wf_prog_ws_prog, erule exec_mono, assumption) |
10592 | 46 |
done |
47 |
||
13224 | 48 |
lemma subset_replicate: "set (replicate n x) \<subseteq> {x}" |
49 |
by (induct n) auto |
|
50 |
||
51 |
lemma in_set_replicate: |
|
52 |
"x \<in> set (replicate n y) \<Longrightarrow> x = y" |
|
53 |
proof - |
|
54 |
assume "x \<in> set (replicate n y)" |
|
55 |
also have "set (replicate n y) \<subseteq> {y}" by (rule subset_replicate) |
|
56 |
finally have "x \<in> {y}" . |
|
57 |
thus ?thesis by simp |
|
58 |
qed |
|
10637 | 59 |
|
60 |
theorem wt_kil_correct: |
|
13224 | 61 |
assumes wf: "wf_prog wf_mb G" |
62 |
assumes C: "is_class G C" |
|
63 |
assumes pTs: "set pTs \<subseteq> types G" |
|
64 |
||
65 |
assumes wtk: "wt_kil G C pTs rT maxs mxl et bs" |
|
66 |
||
67 |
shows "\<exists>phi. wt_method G C pTs rT maxs mxl bs et phi" |
|
10592 | 68 |
proof - |
69 |
let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11299
diff
changeset
|
70 |
#(replicate (size bs - 1) (OK None))" |
10592 | 71 |
|
13224 | 72 |
from wtk obtain maxr r where |
13066 | 73 |
bounded: "check_bounded bs et" and |
12516 | 74 |
result: "r = kiljvm G maxs maxr rT et bs ?start" and |
10637 | 75 |
success: "\<forall>n < size bs. r!n \<noteq> Err" and |
76 |
instrs: "0 < size bs" and |
|
77 |
maxr: "maxr = Suc (length pTs + mxl)" |
|
78 |
by (unfold wt_kil_def) simp |
|
10592 | 79 |
|
13066 | 80 |
from bounded have "bounded (exec G maxs rT et bs) (size bs)" |
81 |
by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded) |
|
82 |
with wf have bcv: |
|
12516 | 83 |
"is_bcv (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) |
13066 | 84 |
(size bs) (states G maxs maxr) (kiljvm G maxs maxr rT et bs)" |
10592 | 85 |
by (rule is_bcv_kiljvm) |
13066 | 86 |
|
13224 | 87 |
from C pTs instrs maxr |
10592 | 88 |
have "?start \<in> list (length bs) (states G maxs maxr)" |
13224 | 89 |
apply (unfold JVM_states_unfold) |
90 |
apply (rule listI) |
|
91 |
apply (auto intro: list_appendI dest!: in_set_replicate) |
|
92 |
apply force |
|
93 |
done |
|
94 |
||
12516 | 95 |
with bcv success result have |
10592 | 96 |
"\<exists>ts\<in>list (length bs) (states G maxs maxr). |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
97 |
?start <=[JVMType.le G maxs maxr] ts \<and> |
12516 | 98 |
wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) ts" |
10592 | 99 |
by (unfold is_bcv_def) auto |
100 |
then obtain phi' where |
|
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
101 |
phi': "phi' \<in> list (length bs) (states G maxs maxr)" and |
10812
ead84e90bfeb
merged semilattice orders with <=' from Convert.thy (now defined in JVMType.thy)
kleing
parents:
10657
diff
changeset
|
102 |
s: "?start <=[JVMType.le G maxs maxr] phi'" and |
12516 | 103 |
w: "wt_step (JVMType.le G maxs maxr) Err (exec G maxs rT et bs) phi'" |
10592 | 104 |
by blast |
13066 | 105 |
hence wt_err_step: |
106 |
"wt_err_step (sup_state_opt G) (exec G maxs rT et bs) phi'" |
|
107 |
by (simp add: wt_err_step_def exec_def JVM_le_Err_conv) |
|
10592 | 108 |
|
12516 | 109 |
from s have le: "JVMType.le G maxs maxr (?start ! 0) (phi'!0)" |
10592 | 110 |
by (drule_tac p=0 in le_listD) (simp add: lesub_def)+ |
111 |
||
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
112 |
from phi' have l: "size phi' = size bs" by simp |
12516 | 113 |
with instrs w have "phi' ! 0 \<noteq> Err" by (unfold wt_step_def) simp |
114 |
with instrs l have phi0: "OK (map ok_val phi' ! 0) = phi' ! 0" |
|
46226 | 115 |
by auto |
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
116 |
|
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
117 |
from phi' have "check_types G maxs maxr phi'" by(simp add: check_types_def) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
118 |
also from w have "phi' = map OK (map ok_val phi')" |
46226 | 119 |
by (auto simp add: wt_step_def intro!: nth_equalityI) |
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
120 |
finally |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
121 |
have check_types: |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
122 |
"check_types G maxs maxr (map OK (map ok_val phi'))" . |
10592 | 123 |
|
12516 | 124 |
from l bounded |
13067 | 125 |
have "bounded (\<lambda>pc. eff (bs!pc) G pc et) (length phi')" |
13066 | 126 |
by (simp add: exec_def check_bounded_is_bounded) |
13067 | 127 |
hence bounded': "bounded (exec G maxs rT et bs) (length bs)" |
128 |
by (auto intro: bounded_lift simp add: exec_def l) |
|
13066 | 129 |
with wt_err_step |
130 |
have "wt_app_eff (sup_state_opt G) (\<lambda>pc. app (bs!pc) G maxs rT pc et) |
|
131 |
(\<lambda>pc. eff (bs!pc) G pc et) (map ok_val phi')" |
|
13067 | 132 |
by (auto intro: wt_err_imp_wt_app_eff simp add: l exec_def) |
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
133 |
with instrs l le bounded bounded' check_types maxr |
12516 | 134 |
have "wt_method G C pTs rT maxs mxl bs et (map ok_val phi')" |
13066 | 135 |
apply (unfold wt_method_def wt_app_eff_def) |
10592 | 136 |
apply simp |
137 |
apply (rule conjI) |
|
138 |
apply (unfold wt_start_def) |
|
139 |
apply (rule JVM_le_convert [THEN iffD1]) |
|
140 |
apply (simp (no_asm) add: phi0) |
|
141 |
apply clarify |
|
142 |
apply (erule allE, erule impE, assumption) |
|
143 |
apply (elim conjE) |
|
144 |
apply (clarsimp simp add: lesub_def wt_instr_def) |
|
13067 | 145 |
apply (simp add: exec_def) |
146 |
apply (drule bounded_err_stepD, assumption+) |
|
147 |
apply blast |
|
10592 | 148 |
done |
149 |
||
150 |
thus ?thesis by blast |
|
151 |
qed |
|
152 |
||
10651 | 153 |
|
154 |
theorem wt_kil_complete: |
|
13224 | 155 |
assumes wf: "wf_prog wf_mb G" |
156 |
assumes C: "is_class G C" |
|
157 |
assumes pTs: "set pTs \<subseteq> types G" |
|
158 |
||
159 |
assumes wtm: "wt_method G C pTs rT maxs mxl bs et phi" |
|
160 |
||
161 |
shows "wt_kil G C pTs rT maxs mxl et bs" |
|
10651 | 162 |
proof - |
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
163 |
let ?mxr = "1+size pTs+mxl" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
164 |
|
13224 | 165 |
from wtm obtain |
10651 | 166 |
instrs: "0 < length bs" and |
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
167 |
len: "length phi = length bs" and |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
168 |
bounded: "check_bounded bs et" and |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
169 |
ck_types: "check_types G maxs ?mxr (map OK phi)" and |
10651 | 170 |
wt_start: "wt_start G C pTs mxl phi" and |
171 |
wt_ins: "\<forall>pc. pc < length bs \<longrightarrow> |
|
12516 | 172 |
wt_instr (bs ! pc) G rT phi maxs (length bs) et pc" |
10651 | 173 |
by (unfold wt_method_def) simp |
174 |
||
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
175 |
from ck_types len |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
176 |
have istype_phi: |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
177 |
"map OK phi \<in> list (length bs) (states G maxs (1+size pTs+mxl))" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
178 |
by (auto simp add: check_types_def intro!: listI) |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
179 |
|
12516 | 180 |
let ?eff = "\<lambda>pc. eff (bs!pc) G pc et" |
181 |
let ?app = "\<lambda>pc. app (bs!pc) G maxs rT pc et" |
|
10651 | 182 |
|
13066 | 183 |
from bounded |
184 |
have bounded_exec: "bounded (exec G maxs rT et bs) (size bs)" |
|
185 |
by (unfold exec_def) (intro bounded_lift check_bounded_is_bounded) |
|
12516 | 186 |
|
10651 | 187 |
from wt_ins |
13066 | 188 |
have "wt_app_eff (sup_state_opt G) ?app ?eff phi" |
189 |
apply (unfold wt_app_eff_def wt_instr_def lesub_def) |
|
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
190 |
apply (simp (no_asm) only: len) |
10651 | 191 |
apply blast |
192 |
done |
|
13066 | 193 |
with bounded_exec |
194 |
have "wt_err_step (sup_state_opt G) (err_step (size phi) ?app ?eff) (map OK phi)" |
|
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
195 |
by - (erule wt_app_eff_imp_wt_err,simp add: exec_def len) |
13066 | 196 |
hence wt_err: |
197 |
"wt_err_step (sup_state_opt G) (exec G maxs rT et bs) (map OK phi)" |
|
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
198 |
by (unfold exec_def) (simp add: len) |
10651 | 199 |
|
12516 | 200 |
from wf bounded_exec |
10651 | 201 |
have is_bcv: |
13224 | 202 |
"is_bcv (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs) |
203 |
(size bs) (states G maxs ?mxr) (kiljvm G maxs ?mxr rT et bs)" |
|
10651 | 204 |
by (rule is_bcv_kiljvm) |
205 |
||
206 |
let ?start = "OK (Some ([],(OK (Class C))#((map OK pTs))@(replicate mxl Err))) |
|
11701
3d51fbf81c17
sane numerals (stage 1): added generic 1, removed 1' and 2 on nat,
wenzelm
parents:
11299
diff
changeset
|
207 |
#(replicate (size bs - 1) (OK None))" |
10651 | 208 |
|
13224 | 209 |
from C pTs instrs |
210 |
have start: "?start \<in> list (length bs) (states G maxs ?mxr)" |
|
211 |
apply (unfold JVM_states_unfold) |
|
212 |
apply (rule listI) |
|
213 |
apply (auto intro!: list_appendI dest!: in_set_replicate) |
|
214 |
apply force |
|
215 |
done |
|
10651 | 216 |
|
12516 | 217 |
let ?phi = "map OK phi" |
13224 | 218 |
have less_phi: "?start <=[JVMType.le G maxs ?mxr] ?phi" |
10657 | 219 |
proof - |
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
220 |
from len instrs |
12516 | 221 |
have "length ?start = length (map OK phi)" by simp |
222 |
moreover |
|
10657 | 223 |
{ fix n |
224 |
from wt_start |
|
225 |
have "G \<turnstile> ok_val (?start!0) <=' phi!0" |
|
226 |
by (simp add: wt_start_def) |
|
227 |
moreover |
|
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
228 |
from instrs len |
10657 | 229 |
have "0 < length phi" by simp |
230 |
ultimately |
|
13224 | 231 |
have "JVMType.le G maxs ?mxr (?start!0) (?phi!0)" |
10657 | 232 |
by (simp add: JVM_le_Err_conv Err.le_def lesub_def) |
233 |
moreover |
|
234 |
{ fix n' |
|
13224 | 235 |
have "JVMType.le G maxs ?mxr (OK None) (?phi!n)" |
10657 | 236 |
by (auto simp add: JVM_le_Err_conv Err.le_def lesub_def |
237 |
split: err.splits) |
|
13006 | 238 |
hence "\<lbrakk> n = Suc n'; n < length ?start \<rbrakk> |
13224 | 239 |
\<Longrightarrow> JVMType.le G maxs ?mxr (?start!n) (?phi!n)" |
10657 | 240 |
by simp |
241 |
} |
|
242 |
ultimately |
|
13224 | 243 |
have "n < length ?start \<Longrightarrow> (?start!n) <=_(JVMType.le G maxs ?mxr) (?phi!n)" |
12516 | 244 |
by (unfold lesub_def) (cases n, blast+) |
245 |
} |
|
246 |
ultimately show ?thesis by (rule le_listI) |
|
10657 | 247 |
qed |
10651 | 248 |
|
13066 | 249 |
from wt_err |
13224 | 250 |
have "wt_step (JVMType.le G maxs ?mxr) Err (exec G maxs rT et bs) ?phi" |
13066 | 251 |
by (simp add: wt_err_step_def JVM_le_Err_conv) |
12516 | 252 |
with start istype_phi less_phi is_bcv |
13224 | 253 |
have "\<forall>p. p < length bs \<longrightarrow> kiljvm G maxs ?mxr rT et bs ?start ! p \<noteq> Err" |
12516 | 254 |
by (unfold is_bcv_def) auto |
13066 | 255 |
with bounded instrs |
12516 | 256 |
show "wt_kil G C pTs rT maxs mxl et bs" by (unfold wt_kil_def) simp |
257 |
qed |
|
10651 | 258 |
|
10637 | 259 |
|
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
260 |
theorem jvm_kildall_sound_complete: |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
261 |
"wt_jvm_prog_kildall G = (\<exists>Phi. wt_jvm_prog G Phi)" |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
262 |
proof |
12516 | 263 |
let ?Phi = "\<lambda>C sig. let (C,rT,(maxs,maxl,ins,et)) = the (method (G,C) sig) in |
264 |
SOME phi. wt_method G C (snd sig) rT maxs maxl ins et phi" |
|
13224 | 265 |
|
266 |
assume "wt_jvm_prog_kildall G" |
|
267 |
hence "wt_jvm_prog G ?Phi" |
|
268 |
apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def) |
|
269 |
apply (erule jvm_prog_lift) |
|
270 |
apply (auto dest!: wt_kil_correct intro: someI) |
|
10637 | 271 |
done |
13224 | 272 |
thus "\<exists>Phi. wt_jvm_prog G Phi" by fast |
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
273 |
next |
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
274 |
assume "\<exists>Phi. wt_jvm_prog G Phi" |
13224 | 275 |
thus "wt_jvm_prog_kildall G" |
276 |
apply (clarify) |
|
277 |
apply (unfold wt_jvm_prog_def wt_jvm_prog_kildall_def) |
|
278 |
apply (erule jvm_prog_lift) |
|
279 |
apply (auto intro: wt_kil_complete) |
|
13214
2aa33ed5f526
wt_method now checks bounded+types ==> wt_kildall <=> wt_method
kleing
parents:
13074
diff
changeset
|
280 |
done |
10637 | 281 |
qed |
282 |
||
10592 | 283 |
end |