12854
|
1 |
(* Title: isabelle/Bali/WellType.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: David von Oheimb
|
|
4 |
Copyright 1997 Technische Universitaet Muenchen
|
|
5 |
*)
|
|
6 |
header {* Well-typedness of Java programs *}
|
|
7 |
|
|
8 |
theory WellType = DeclConcepts:
|
|
9 |
|
|
10 |
text {*
|
|
11 |
improvements over Java Specification 1.0:
|
|
12 |
\begin{itemize}
|
|
13 |
\item methods of Object can be called upon references of interface or array type
|
|
14 |
\end{itemize}
|
|
15 |
simplifications:
|
|
16 |
\begin{itemize}
|
|
17 |
\item the type rules include all static checks on statements and expressions,
|
|
18 |
e.g. definedness of names (of parameters, locals, fields, methods)
|
|
19 |
\end{itemize}
|
|
20 |
design issues:
|
|
21 |
\begin{itemize}
|
|
22 |
\item unified type judgment for statements, variables, expressions,
|
|
23 |
expression lists
|
|
24 |
\item statements are typed like expressions with dummy type Void
|
|
25 |
\item the typing rules take an extra argument that is capable of determining
|
|
26 |
the dynamic type of objects. Therefore, they can be used for both
|
|
27 |
checking static types and determining runtime types in transition semantics.
|
|
28 |
\end{itemize}
|
|
29 |
*}
|
|
30 |
|
|
31 |
types lenv
|
|
32 |
= "(lname, ty) table" (* local variables, including This and Result *)
|
|
33 |
|
|
34 |
record env =
|
|
35 |
prg:: "prog" (* program *)
|
|
36 |
cls:: "qtname" (* current package and class name *)
|
|
37 |
lcl:: "lenv" (* local environment *)
|
|
38 |
|
|
39 |
translations
|
|
40 |
"lenv" <= (type) "(lname, ty) table"
|
|
41 |
"lenv" <= (type) "lname \<Rightarrow> ty option"
|
|
42 |
"env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv\<rparr>"
|
|
43 |
"env" <= (type) "\<lparr>prg::prog,cls::qtname,lcl::lenv,\<dots>::'a\<rparr>"
|
|
44 |
|
|
45 |
|
|
46 |
|
|
47 |
syntax
|
|
48 |
pkg :: "env \<Rightarrow> pname" (* select the current package from an environment *)
|
|
49 |
translations
|
|
50 |
"pkg e" == "pid (cls e)"
|
|
51 |
|
|
52 |
section "Static overloading: maximally specific methods "
|
|
53 |
|
|
54 |
types
|
|
55 |
emhead = "ref_ty \<times> mhead"
|
|
56 |
|
|
57 |
(* Some mnemotic selectors for emhead *)
|
|
58 |
constdefs
|
|
59 |
"declrefT" :: "emhead \<Rightarrow> ref_ty"
|
|
60 |
"declrefT \<equiv> fst"
|
|
61 |
|
|
62 |
"mhd" :: "emhead \<Rightarrow> mhead"
|
|
63 |
"mhd \<equiv> snd"
|
|
64 |
|
|
65 |
lemma declrefT_simp[simp]:"declrefT (r,m) = r"
|
|
66 |
by (simp add: declrefT_def)
|
|
67 |
|
|
68 |
lemma mhd_simp[simp]:"mhd (r,m) = m"
|
|
69 |
by (simp add: mhd_def)
|
|
70 |
|
|
71 |
lemma static_mhd_simp[simp]: "static (mhd m) = is_static m"
|
|
72 |
by (cases m) (simp add: member_is_static_simp mhd_def)
|
|
73 |
|
|
74 |
lemma mhd_resTy_simp [simp]: "resTy (mhd m) = resTy m"
|
|
75 |
by (cases m) simp
|
|
76 |
|
|
77 |
lemma mhd_is_static_simp [simp]: "is_static (mhd m) = is_static m"
|
|
78 |
by (cases m) simp
|
|
79 |
|
|
80 |
lemma mhd_accmodi_simp [simp]: "accmodi (mhd m) = accmodi m"
|
|
81 |
by (cases m) simp
|
|
82 |
|
|
83 |
consts
|
|
84 |
cmheads :: "prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
|
|
85 |
Objectmheads :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> emhead set"
|
|
86 |
accObjectmheads:: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
|
|
87 |
mheads :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> emhead set"
|
|
88 |
defs
|
|
89 |
cmheads_def:
|
|
90 |
"cmheads G S C
|
|
91 |
\<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd))) ` o2s (accmethd G S C sig)"
|
|
92 |
Objectmheads_def:
|
|
93 |
"Objectmheads G S
|
|
94 |
\<equiv> \<lambda>sig. (\<lambda>(Cls,mthd). (ClassT Cls,(mhead mthd)))
|
|
95 |
` o2s (filter_tab (\<lambda>sig m. accmodi m \<noteq> Private) (accmethd G S Object) sig)"
|
|
96 |
accObjectmheads_def:
|
|
97 |
"accObjectmheads G S T
|
|
98 |
\<equiv> if G\<turnstile>RefT T accessible_in (pid S)
|
|
99 |
then Objectmheads G S
|
|
100 |
else \<lambda>sig. {}"
|
|
101 |
primrec
|
|
102 |
"mheads G S NullT = (\<lambda>sig. {})"
|
|
103 |
"mheads G S (IfaceT I) = (\<lambda>sig. (\<lambda>(I,h).(IfaceT I,h))
|
|
104 |
` accimethds G (pid S) I sig \<union>
|
|
105 |
accObjectmheads G S (IfaceT I) sig)"
|
|
106 |
"mheads G S (ClassT C) = cmheads G S C"
|
|
107 |
"mheads G S (ArrayT T) = accObjectmheads G S (ArrayT T)"
|
|
108 |
|
|
109 |
|
|
110 |
(* more detailed than necessary for type-safety, see below. *)
|
|
111 |
constdefs
|
|
112 |
(* applicable methods, cf. 15.11.2.1 *)
|
|
113 |
appl_methds :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
|
|
114 |
"appl_methds G S rt \<equiv> \<lambda> sig.
|
|
115 |
{(mh,pTs') |mh pTs'. mh \<in> mheads G S rt \<lparr>name=name sig,parTs=pTs'\<rparr> \<and>
|
|
116 |
G\<turnstile>(parTs sig)[\<preceq>]pTs'}"
|
|
117 |
|
|
118 |
(* more specific methods, cf. 15.11.2.2 *)
|
|
119 |
more_spec :: "prog \<Rightarrow> emhead \<times> ty list \<Rightarrow> emhead \<times> ty list \<Rightarrow> bool"
|
|
120 |
"more_spec G \<equiv> \<lambda>(mh,pTs). \<lambda>(mh',pTs'). G\<turnstile>pTs[\<preceq>]pTs'"
|
|
121 |
(*more_spec G \<equiv>\<lambda>((d,h),pTs). \<lambda>((d',h'),pTs'). G\<turnstile>RefT d\<preceq>RefT d'\<and>G\<turnstile>pTs[\<preceq>]pTs'*)
|
|
122 |
|
|
123 |
(* maximally specific methods, cf. 15.11.2.2 *)
|
|
124 |
max_spec :: "prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> (emhead \<times> ty list)\<spacespace> set"
|
|
125 |
|
|
126 |
"max_spec G S rt sig \<equiv>{m. m \<in>appl_methds G S rt sig \<and>
|
|
127 |
(\<forall>m'\<in>appl_methds G S rt sig. more_spec G m' m \<longrightarrow> m'=m)}"
|
|
128 |
(*
|
|
129 |
rules (* all properties of more_spec, appl_methods and max_spec we actually need
|
|
130 |
these can easily be proven from the above definitions *)
|
|
131 |
|
|
132 |
max_spec2mheads "max_spec G S rt (mn, pTs) = insert (mh, pTs') A \<Longrightarrow>
|
|
133 |
mh\<in>mheads G S rt (mn, pTs') \<and> G\<turnstile>pTs[\<preceq>]pTs'"
|
|
134 |
*)
|
|
135 |
|
|
136 |
lemma max_spec2appl_meths:
|
|
137 |
"x \<in> max_spec G S T sig \<Longrightarrow> x \<in> appl_methds G S T sig"
|
|
138 |
by (auto simp: max_spec_def)
|
|
139 |
|
|
140 |
lemma appl_methsD: "(mh,pTs')\<in>appl_methds G S T \<lparr>name=mn,parTs=pTs\<rparr> \<Longrightarrow>
|
|
141 |
mh \<in> mheads G S T \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
|
|
142 |
by (auto simp: appl_methds_def)
|
|
143 |
|
|
144 |
lemma max_spec2mheads:
|
|
145 |
"max_spec G S rt \<lparr>name=mn,parTs=pTs\<rparr> = insert (mh, pTs') A
|
|
146 |
\<Longrightarrow> mh \<in> mheads G S rt \<lparr>name=mn,parTs=pTs'\<rparr> \<and> G\<turnstile>pTs[\<preceq>]pTs'"
|
|
147 |
apply (auto dest: equalityD2 subsetD max_spec2appl_meths appl_methsD)
|
|
148 |
done
|
|
149 |
|
|
150 |
|
|
151 |
constdefs
|
|
152 |
empty_dt :: "dyn_ty"
|
|
153 |
"empty_dt \<equiv> \<lambda>a. None"
|
|
154 |
|
|
155 |
invmode :: "('a::type)member_scheme \<Rightarrow> expr \<Rightarrow> inv_mode"
|
|
156 |
"invmode m e \<equiv> if static m then Static else if e=Super then SuperM else IntVir"
|
|
157 |
|
|
158 |
lemma invmode_nonstatic [simp]:
|
|
159 |
"invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir"
|
|
160 |
apply (unfold invmode_def)
|
|
161 |
apply (simp (no_asm))
|
|
162 |
done
|
|
163 |
|
|
164 |
|
|
165 |
lemma invmode_Static_eq [simp]: "(invmode m e = Static) = static m"
|
|
166 |
apply (unfold invmode_def)
|
|
167 |
apply (simp (no_asm))
|
|
168 |
done
|
|
169 |
|
|
170 |
|
|
171 |
lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(static m) \<and> e\<noteq>Super)"
|
|
172 |
apply (unfold invmode_def)
|
|
173 |
apply (simp (no_asm))
|
|
174 |
done
|
|
175 |
|
|
176 |
lemma Null_staticD:
|
|
177 |
"a'=Null \<longrightarrow> (static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null"
|
|
178 |
apply (clarsimp simp add: invmode_IntVir_eq)
|
|
179 |
done
|
|
180 |
|
|
181 |
|
|
182 |
types tys = "ty + ty list"
|
|
183 |
translations
|
|
184 |
"tys" <= (type) "ty + ty list"
|
|
185 |
|
|
186 |
consts
|
|
187 |
wt :: "(env\<spacespace> \<times> dyn_ty\<spacespace> \<times> term \<times> tys) set"
|
|
188 |
(*wt :: " env \<Rightarrow> dyn_ty \<Rightarrow> (term \<times> tys) set" not feasible because of
|
|
189 |
\<spacespace> changing env in Try stmt *)
|
|
190 |
|
|
191 |
syntax
|
|
192 |
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_|=_::_" [51,51,51,51] 50)
|
|
193 |
wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_|=_:<>" [51,51,51 ] 50)
|
|
194 |
ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_|=_:-_" [51,51,51,51] 50)
|
|
195 |
ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_|=_:=_" [51,51,51,51] 50)
|
|
196 |
ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
|
|
197 |
\<spacespace> \<spacespace> ty list] \<Rightarrow> bool" ("_,_|=_:#_" [51,51,51,51] 50)
|
|
198 |
|
|
199 |
syntax (xsymbols)
|
|
200 |
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50)
|
|
201 |
wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>" [51,51,51 ] 50)
|
|
202 |
ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50)
|
|
203 |
ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50)
|
|
204 |
ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list,
|
|
205 |
\<spacespace> \<spacespace> ty list] \<Rightarrow> bool"("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50)
|
|
206 |
|
|
207 |
translations
|
|
208 |
"E,dt\<Turnstile>t\<Colon>T" == "(E,dt,t,T) \<in> wt"
|
|
209 |
"E,dt\<Turnstile>s\<Colon>\<surd>" == "E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)"
|
|
210 |
"E,dt\<Turnstile>e\<Colon>-T" == "E,dt\<Turnstile>In1l e\<Colon>Inl T"
|
|
211 |
"E,dt\<Turnstile>e\<Colon>=T" == "E,dt\<Turnstile>In2 e\<Colon>Inl T"
|
|
212 |
"E,dt\<Turnstile>e\<Colon>\<doteq>T" == "E,dt\<Turnstile>In3 e\<Colon>Inr T"
|
|
213 |
|
|
214 |
syntax (* for purely static typing *)
|
|
215 |
wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50)
|
|
216 |
wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50)
|
|
217 |
ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50)
|
|
218 |
ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50)
|
|
219 |
ty_exprs_:: "env \<Rightarrow> [expr list,
|
|
220 |
\<spacespace> ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50)
|
|
221 |
|
|
222 |
syntax (xsymbols)
|
|
223 |
wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50)
|
|
224 |
wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50)
|
|
225 |
ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50)
|
|
226 |
ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50)
|
|
227 |
ty_exprs_ :: "env \<Rightarrow> [expr list,
|
|
228 |
\<spacespace> ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50)
|
|
229 |
|
|
230 |
translations
|
|
231 |
"E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T"
|
|
232 |
"E\<turnstile>s\<Colon>\<surd>" == "E,empty_dt\<Turnstile>s\<Colon>\<surd>"
|
|
233 |
"E\<turnstile>e\<Colon>-T" == "E,empty_dt\<Turnstile>e\<Colon>-T"
|
|
234 |
"E\<turnstile>e\<Colon>=T" == "E,empty_dt\<Turnstile>e\<Colon>=T"
|
|
235 |
"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T"
|
|
236 |
|
|
237 |
|
|
238 |
inductive wt intros
|
|
239 |
|
|
240 |
|
|
241 |
(* well-typed statements *)
|
|
242 |
|
|
243 |
Skip: "E,dt\<Turnstile>Skip\<Colon>\<surd>"
|
|
244 |
|
|
245 |
Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow>
|
|
246 |
E,dt\<Turnstile>Expr e\<Colon>\<surd>"
|
|
247 |
(* cf. 14.6 *)
|
|
248 |
Lab: "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow>
|
|
249 |
E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>"
|
|
250 |
|
|
251 |
Comp: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>;
|
|
252 |
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
|
|
253 |
E,dt\<Turnstile>c1;; c2\<Colon>\<surd>"
|
|
254 |
|
|
255 |
(* cf. 14.8 *)
|
|
256 |
If: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
|
|
257 |
E,dt\<Turnstile>c1\<Colon>\<surd>;
|
|
258 |
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
|
|
259 |
E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>"
|
|
260 |
|
|
261 |
(* cf. 14.10 *)
|
|
262 |
Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean;
|
|
263 |
E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
|
|
264 |
E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>"
|
|
265 |
(* cf. 14.13, 14.15, 14.16 *)
|
|
266 |
Do: "E,dt\<Turnstile>Do jump\<Colon>\<surd>"
|
|
267 |
|
|
268 |
(* cf. 14.16 *)
|
|
269 |
Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn;
|
|
270 |
prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow>
|
|
271 |
E,dt\<Turnstile>Throw e\<Colon>\<surd>"
|
|
272 |
(* cf. 14.18 *)
|
|
273 |
Try: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable;
|
|
274 |
lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk>
|
|
275 |
\<Longrightarrow>
|
|
276 |
E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>"
|
|
277 |
|
|
278 |
(* cf. 14.18 *)
|
|
279 |
Fin: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow>
|
|
280 |
E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>"
|
|
281 |
|
|
282 |
Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow>
|
|
283 |
E,dt\<Turnstile>Init C\<Colon>\<surd>"
|
|
284 |
(* Init is created on the fly during evaluation (see Eval.thy). The class
|
|
285 |
* isn't necessarily accessible from the points Init is called. Therefor
|
|
286 |
* we only demand is_class and not is_acc_class here
|
|
287 |
*)
|
|
288 |
|
|
289 |
(* well-typed expressions *)
|
|
290 |
|
|
291 |
(* cf. 15.8 *)
|
|
292 |
NewC: "\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow>
|
|
293 |
E,dt\<Turnstile>NewC C\<Colon>-Class C"
|
|
294 |
(* cf. 15.9 *)
|
|
295 |
NewA: "\<lbrakk>is_acc_type (prg E) (pkg E) T;
|
|
296 |
E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
|
|
297 |
E,dt\<Turnstile>New T[i]\<Colon>-T.[]"
|
|
298 |
|
|
299 |
(* cf. 15.15 *)
|
|
300 |
Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T';
|
|
301 |
prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow>
|
|
302 |
E,dt\<Turnstile>Cast T' e\<Colon>-T'"
|
|
303 |
|
|
304 |
(* cf. 15.19.2 *)
|
|
305 |
Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T');
|
|
306 |
prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow>
|
|
307 |
E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean"
|
|
308 |
|
|
309 |
(* cf. 15.7.1 *)
|
|
310 |
Lit: "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow>
|
|
311 |
E,dt\<Turnstile>Lit x\<Colon>-T"
|
|
312 |
|
|
313 |
(* cf. 15.10.2, 15.11.1 *)
|
|
314 |
Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
|
|
315 |
class (prg E) C = Some c\<rbrakk> \<Longrightarrow>
|
|
316 |
E,dt\<Turnstile>Super\<Colon>-Class (super c)"
|
|
317 |
|
|
318 |
(* cf. 15.13.1, 15.10.1, 15.12 *)
|
|
319 |
Acc: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow>
|
|
320 |
E,dt\<Turnstile>Acc va\<Colon>-T"
|
|
321 |
|
|
322 |
(* cf. 15.25, 15.25.1 *)
|
|
323 |
Ass: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This;
|
|
324 |
E,dt\<Turnstile>v \<Colon>-T';
|
|
325 |
prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow>
|
|
326 |
E,dt\<Turnstile>va:=v\<Colon>-T'"
|
|
327 |
|
|
328 |
(* cf. 15.24 *)
|
|
329 |
Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean;
|
|
330 |
E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2;
|
|
331 |
prg E\<turnstile>T1\<preceq>T2 \<and> T = T2 \<or> prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow>
|
|
332 |
E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T"
|
|
333 |
|
|
334 |
(* cf. 15.11.1, 15.11.2, 15.11.3 *)
|
|
335 |
Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT;
|
|
336 |
E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
|
|
337 |
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr>
|
|
338 |
= {((statDeclT,m),pTs')}
|
|
339 |
\<rbrakk> \<Longrightarrow>
|
|
340 |
E,dt\<Turnstile>{statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)"
|
|
341 |
|
|
342 |
Methd: "\<lbrakk>is_class (prg E) C;
|
|
343 |
methd (prg E) C sig = Some m;
|
|
344 |
E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow>
|
|
345 |
E,dt\<Turnstile>Methd C sig\<Colon>-T"
|
|
346 |
(* The class C is the dynamic class of the method call (cf. Eval.thy).
|
|
347 |
* It hasn't got to be directly accessible from the current package (pkg E).
|
|
348 |
* Only the static class must be accessible (enshured indirectly by Call).
|
|
349 |
*)
|
|
350 |
|
|
351 |
Body: "\<lbrakk>is_class (prg E) D;
|
|
352 |
E,dt\<Turnstile>blk\<Colon>\<surd>;
|
|
353 |
(lcl E) Result = Some T;
|
|
354 |
is_type (prg E) T\<rbrakk> \<Longrightarrow>
|
|
355 |
E,dt\<Turnstile>Body D blk\<Colon>-T"
|
|
356 |
(* the class D implementing the method must not directly be accessible
|
|
357 |
* from the current package (pkg E), but can also be indirectly accessible
|
|
358 |
* due to inheritance (enshured in Call)
|
|
359 |
* The result type hasn't got to be accessible in Java! (If it is not
|
|
360 |
* accessible you can only assign it to Object)
|
|
361 |
*)
|
|
362 |
|
|
363 |
(* well-typed variables *)
|
|
364 |
|
|
365 |
(* cf. 15.13.1 *)
|
|
366 |
LVar: "\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow>
|
|
367 |
E,dt\<Turnstile>LVar vn\<Colon>=T"
|
|
368 |
(* cf. 15.10.1 *)
|
|
369 |
FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C;
|
|
370 |
accfield (prg E) (cls E) C fn = Some (fd,f)\<rbrakk> \<Longrightarrow>
|
|
371 |
E,dt\<Turnstile>{fd,static f}e..fn\<Colon>=(type f)"
|
|
372 |
(* cf. 15.12 *)
|
|
373 |
AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[];
|
|
374 |
E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow>
|
|
375 |
E,dt\<Turnstile>e.[i]\<Colon>=T"
|
|
376 |
|
|
377 |
|
|
378 |
(* well-typed expression lists *)
|
|
379 |
|
|
380 |
(* cf. 15.11.??? *)
|
|
381 |
Nil: "E,dt\<Turnstile>[]\<Colon>\<doteq>[]"
|
|
382 |
|
|
383 |
(* cf. 15.11.??? *)
|
|
384 |
Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>-T;
|
|
385 |
E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow>
|
|
386 |
E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts"
|
|
387 |
|
|
388 |
|
|
389 |
declare not_None_eq [simp del]
|
|
390 |
declare split_if [split del] split_if_asm [split del]
|
|
391 |
declare split_paired_All [simp del] split_paired_Ex [simp del]
|
|
392 |
ML_setup {*
|
|
393 |
simpset_ref() := simpset() delloop "split_all_tac"
|
|
394 |
*}
|
|
395 |
inductive_cases wt_stmt_cases: "E,dt\<Turnstile>c\<Colon>\<surd>"
|
|
396 |
inductive_cases wt_elim_cases:
|
|
397 |
"E,dt\<Turnstile>In2 (LVar vn) \<Colon>T"
|
|
398 |
"E,dt\<Turnstile>In2 ({fd,s}e..fn) \<Colon>T"
|
|
399 |
"E,dt\<Turnstile>In2 (e.[i]) \<Colon>T"
|
|
400 |
"E,dt\<Turnstile>In1l (NewC C) \<Colon>T"
|
|
401 |
"E,dt\<Turnstile>In1l (New T'[i]) \<Colon>T"
|
|
402 |
"E,dt\<Turnstile>In1l (Cast T' e) \<Colon>T"
|
|
403 |
"E,dt\<Turnstile>In1l (e InstOf T') \<Colon>T"
|
|
404 |
"E,dt\<Turnstile>In1l (Lit x) \<Colon>T"
|
|
405 |
"E,dt\<Turnstile>In1l (Super) \<Colon>T"
|
|
406 |
"E,dt\<Turnstile>In1l (Acc va) \<Colon>T"
|
|
407 |
"E,dt\<Turnstile>In1l (Ass va v) \<Colon>T"
|
|
408 |
"E,dt\<Turnstile>In1l (e0 ? e1 : e2) \<Colon>T"
|
|
409 |
"E,dt\<Turnstile>In1l ({statT,mode}e\<cdot>mn({pT'}p))\<Colon>T"
|
|
410 |
"E,dt\<Turnstile>In1l (Methd C sig) \<Colon>T"
|
|
411 |
"E,dt\<Turnstile>In1l (Body D blk) \<Colon>T"
|
|
412 |
"E,dt\<Turnstile>In3 ([]) \<Colon>Ts"
|
|
413 |
"E,dt\<Turnstile>In3 (e#es) \<Colon>Ts"
|
|
414 |
"E,dt\<Turnstile>In1r Skip \<Colon>x"
|
|
415 |
"E,dt\<Turnstile>In1r (Expr e) \<Colon>x"
|
|
416 |
"E,dt\<Turnstile>In1r (c1;; c2) \<Colon>x"
|
|
417 |
"E,dt\<Turnstile>In1r (l\<bullet> c) \<Colon>x"
|
|
418 |
"E,dt\<Turnstile>In1r (If(e) c1 Else c2) \<Colon>x"
|
|
419 |
"E,dt\<Turnstile>In1r (l\<bullet> While(e) c) \<Colon>x"
|
|
420 |
"E,dt\<Turnstile>In1r (Do jump) \<Colon>x"
|
|
421 |
"E,dt\<Turnstile>In1r (Throw e) \<Colon>x"
|
|
422 |
"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x"
|
|
423 |
"E,dt\<Turnstile>In1r (c1 Finally c2) \<Colon>x"
|
|
424 |
"E,dt\<Turnstile>In1r (Init C) \<Colon>x"
|
|
425 |
declare not_None_eq [simp]
|
|
426 |
declare split_if [split] split_if_asm [split]
|
|
427 |
declare split_paired_All [simp] split_paired_Ex [simp]
|
|
428 |
ML_setup {*
|
|
429 |
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac)
|
|
430 |
*}
|
|
431 |
|
|
432 |
lemma is_acc_class_is_accessible:
|
|
433 |
"is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P"
|
|
434 |
by (auto simp add: is_acc_class_def)
|
|
435 |
|
|
436 |
lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I"
|
|
437 |
by (auto simp add: is_acc_iface_def)
|
|
438 |
|
|
439 |
lemma is_acc_iface_is_accessible:
|
|
440 |
"is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P"
|
|
441 |
by (auto simp add: is_acc_iface_def)
|
|
442 |
|
|
443 |
lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T"
|
|
444 |
by (auto simp add: is_acc_type_def)
|
|
445 |
|
|
446 |
lemma is_acc_iface_is_accessible: "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P"
|
|
447 |
by (auto simp add: is_acc_type_def)
|
|
448 |
|
|
449 |
lemma wt_Methd_is_methd:
|
|
450 |
"E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig"
|
|
451 |
apply (erule_tac wt_elim_cases)
|
|
452 |
apply clarsimp
|
|
453 |
apply (erule is_methdI, assumption)
|
|
454 |
done
|
|
455 |
|
|
456 |
(* Special versions of some typing rules, better suited to pattern match the
|
|
457 |
* conclusion (no selectors in the conclusion\<dots>)
|
|
458 |
*)
|
|
459 |
|
|
460 |
lemma wt_Super:
|
|
461 |
"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object;
|
|
462 |
class (prg E) C = Some c;D=super c\<rbrakk>
|
|
463 |
\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
|
|
464 |
by (auto elim: wt.Super)
|
|
465 |
|
|
466 |
lemma wt_Call:
|
|
467 |
"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs;
|
|
468 |
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr>
|
|
469 |
= {((statDeclC,m),pTs')};rT=(resTy m);
|
|
470 |
mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT"
|
|
471 |
by (auto elim: wt.Call)
|
|
472 |
|
|
473 |
|
|
474 |
|
|
475 |
lemma invocationTypeExpr_noClassD:
|
|
476 |
"\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk>
|
|
477 |
\<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM"
|
|
478 |
proof -
|
|
479 |
assume wt: "E\<turnstile>e\<Colon>-RefT statT"
|
|
480 |
show ?thesis
|
|
481 |
proof (cases "e=Super")
|
|
482 |
case True
|
|
483 |
with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases)
|
|
484 |
then show ?thesis by blast
|
|
485 |
next
|
|
486 |
case False then show ?thesis
|
|
487 |
by (auto simp add: invmode_def split: split_if_asm)
|
|
488 |
qed
|
|
489 |
qed
|
|
490 |
|
|
491 |
lemma wt_Super:
|
|
492 |
"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk>
|
|
493 |
\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D"
|
|
494 |
by (auto elim: wt.Super)
|
|
495 |
|
|
496 |
|
|
497 |
lemma wt_FVar:
|
|
498 |
"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (fd,f);
|
|
499 |
sf=static f; fT=(type f)\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{fd,sf}e..fn\<Colon>=fT"
|
|
500 |
by (auto elim: wt.FVar)
|
|
501 |
|
|
502 |
lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C"
|
|
503 |
by (auto elim: wt_elim_cases intro: "wt.Init")
|
|
504 |
|
|
505 |
declare wt.Skip [iff]
|
|
506 |
|
|
507 |
lemma wt_StatRef:
|
|
508 |
"is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt"
|
|
509 |
apply (rule wt.Cast)
|
|
510 |
apply (rule wt.Lit)
|
|
511 |
apply (simp (no_asm))
|
|
512 |
apply (simp (no_asm_simp))
|
|
513 |
apply (rule cast.widen)
|
|
514 |
apply (simp (no_asm))
|
|
515 |
done
|
|
516 |
|
|
517 |
lemma wt_Inj_elim:
|
|
518 |
"\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of
|
|
519 |
In1 ec \<Rightarrow> (case ec of
|
|
520 |
Inl e \<Rightarrow> \<exists>T. U=Inl T
|
|
521 |
| Inr s \<Rightarrow> U=Inl (PrimT Void))
|
|
522 |
| In2 e \<Rightarrow> (\<exists>T. U=Inl T)
|
|
523 |
| In3 e \<Rightarrow> (\<exists>T. U=Inr T)"
|
|
524 |
apply (erule wt.induct)
|
|
525 |
apply auto
|
|
526 |
done
|
|
527 |
|
|
528 |
ML {*
|
|
529 |
fun wt_fun name inj rhs =
|
|
530 |
let
|
|
531 |
val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U"
|
|
532 |
val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")")
|
|
533 |
(K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac])
|
|
534 |
fun is_Inj (Const (inj,_) $ _) = true
|
|
535 |
| is_Inj _ = false
|
|
536 |
fun pred (t as (_ $ (Const ("Pair",_) $
|
|
537 |
_ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $
|
|
538 |
x))) $ _ )) = is_Inj x
|
|
539 |
in
|
|
540 |
make_simproc name lhs pred (thm name)
|
|
541 |
end
|
|
542 |
|
|
543 |
val wt_expr_proc = wt_fun "wt_expr_eq" "In1l" "\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T"
|
|
544 |
val wt_var_proc = wt_fun "wt_var_eq" "In2" "\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T"
|
|
545 |
val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3" "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts"
|
|
546 |
val wt_stmt_proc = wt_fun "wt_stmt_eq" "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>"
|
|
547 |
*}
|
|
548 |
|
|
549 |
ML {*
|
|
550 |
Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc]
|
|
551 |
*}
|
|
552 |
|
|
553 |
lemma Inj_eq_lemma [simp]:
|
|
554 |
"(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))"
|
|
555 |
by auto
|
|
556 |
|
|
557 |
(* unused *)
|
|
558 |
lemma single_valued_tys_lemma [rule_format (no_asm)]:
|
|
559 |
"\<forall>S T. G\<turnstile>S\<preceq>T \<longrightarrow> G\<turnstile>T\<preceq>S \<longrightarrow> S = T \<Longrightarrow> E,dt\<Turnstile>t\<Colon>T \<Longrightarrow>
|
|
560 |
G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T = T')"
|
|
561 |
apply (cases "E", erule wt.induct)
|
|
562 |
apply (safe del: disjE)
|
|
563 |
apply (simp_all (no_asm_use) split del: split_if_asm)
|
|
564 |
apply (safe del: disjE)
|
|
565 |
(* 17 subgoals *)
|
|
566 |
apply (tactic {* ALLGOALS (fn i => if i = 9 then EVERY'[thin_tac "?E,dt\<Turnstile>e0\<Colon>-PrimT Boolean", thin_tac "?E,dt\<Turnstile>e1\<Colon>-?T1", thin_tac "?E,dt\<Turnstile>e2\<Colon>-?T2"] i else thin_tac "All ?P" i) *})
|
|
567 |
(*apply (safe del: disjE elim!: wt_elim_cases)*)
|
|
568 |
apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*})
|
|
569 |
apply (simp_all (no_asm_use) split del: split_if_asm)
|
|
570 |
apply (erule_tac [10] V = "All ?P" in thin_rl) (* Call *)
|
|
571 |
apply ((blast del: equalityCE dest: sym [THEN trans])+)
|
|
572 |
done
|
|
573 |
|
|
574 |
(* unused *)
|
|
575 |
lemma single_valued_tys:
|
|
576 |
"ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}"
|
|
577 |
apply (unfold single_valued_def)
|
|
578 |
apply clarsimp
|
|
579 |
apply (rule single_valued_tys_lemma)
|
|
580 |
apply (auto intro!: widen_antisym)
|
|
581 |
done
|
|
582 |
|
|
583 |
lemma typeof_empty_is_type [rule_format (no_asm)]:
|
|
584 |
"typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T"
|
|
585 |
apply (rule val.induct)
|
|
586 |
apply auto
|
|
587 |
done
|
|
588 |
|
|
589 |
(* unused *)
|
|
590 |
lemma typeof_is_type [rule_format (no_asm)]:
|
|
591 |
"(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)"
|
|
592 |
apply (rule val.induct)
|
|
593 |
prefer 5
|
|
594 |
apply fast
|
|
595 |
apply (simp_all (no_asm))
|
|
596 |
done
|
|
597 |
|
|
598 |
end
|