author | schirmer |
Fri, 22 Feb 2002 11:26:44 +0100 | |
changeset 12925 | 99131847fb93 |
parent 12858 | 6214f03d6d27 |
child 13337 | f75dfc606ac7 |
permissions | -rw-r--r-- |
12857 | 1 |
(* Title: HOL/Bali/WellType.thy |
12854 | 2 |
ID: $Id$ |
3 |
Author: David von Oheimb |
|
12858 | 4 |
License: GPL (GNU GENERAL PUBLIC LICENSE) |
12854 | 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" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
156 |
"invmode m e \<equiv> if is_static m |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
157 |
then Static |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
158 |
else if e=Super then SuperM else IntVir" |
12854 | 159 |
|
160 |
lemma invmode_nonstatic [simp]: |
|
161 |
"invmode \<lparr>access=a,static=False,\<dots>=x\<rparr> (Acc (LVar e)) = IntVir" |
|
162 |
apply (unfold invmode_def) |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
163 |
apply (simp (no_asm) add: member_is_static_simp) |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
164 |
done |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
165 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
166 |
|
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
167 |
lemma invmode_Static_eq [simp]: "(invmode m e = Static) = is_static m" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
168 |
apply (unfold invmode_def) |
12854 | 169 |
apply (simp (no_asm)) |
170 |
done |
|
171 |
||
172 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
173 |
lemma invmode_IntVir_eq: "(invmode m e = IntVir) = (\<not>(is_static m) \<and> e\<noteq>Super)" |
12854 | 174 |
apply (unfold invmode_def) |
175 |
apply (simp (no_asm)) |
|
176 |
done |
|
177 |
||
178 |
lemma Null_staticD: |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
179 |
"a'=Null \<longrightarrow> (is_static m) \<Longrightarrow> invmode m e = IntVir \<longrightarrow> a' \<noteq> Null" |
12854 | 180 |
apply (clarsimp simp add: invmode_IntVir_eq) |
181 |
done |
|
182 |
||
183 |
||
184 |
types tys = "ty + ty list" |
|
185 |
translations |
|
186 |
"tys" <= (type) "ty + ty list" |
|
187 |
||
188 |
consts |
|
189 |
wt :: "(env\<spacespace> \<times> dyn_ty\<spacespace> \<times> term \<times> tys) set" |
|
190 |
(*wt :: " env \<Rightarrow> dyn_ty \<Rightarrow> (term \<times> tys) set" not feasible because of |
|
191 |
\<spacespace> changing env in Try stmt *) |
|
192 |
||
193 |
syntax |
|
194 |
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_|=_::_" [51,51,51,51] 50) |
|
195 |
wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_|=_:<>" [51,51,51 ] 50) |
|
196 |
ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_|=_:-_" [51,51,51,51] 50) |
|
197 |
ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_|=_:=_" [51,51,51,51] 50) |
|
198 |
ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, |
|
199 |
\<spacespace> \<spacespace> ty list] \<Rightarrow> bool" ("_,_|=_:#_" [51,51,51,51] 50) |
|
200 |
||
201 |
syntax (xsymbols) |
|
202 |
wt :: "env \<Rightarrow> dyn_ty \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>_" [51,51,51,51] 50) |
|
203 |
wt_stmt :: "env \<Rightarrow> dyn_ty \<Rightarrow> stmt \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>\<surd>" [51,51,51 ] 50) |
|
204 |
ty_expr :: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>-_" [51,51,51,51] 50) |
|
205 |
ty_var :: "env \<Rightarrow> dyn_ty \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_,_\<Turnstile>_\<Colon>=_" [51,51,51,51] 50) |
|
206 |
ty_exprs:: "env \<Rightarrow> dyn_ty \<Rightarrow> [expr list, |
|
207 |
\<spacespace> \<spacespace> ty list] \<Rightarrow> bool"("_,_\<Turnstile>_\<Colon>\<doteq>_" [51,51,51,51] 50) |
|
208 |
||
209 |
translations |
|
210 |
"E,dt\<Turnstile>t\<Colon>T" == "(E,dt,t,T) \<in> wt" |
|
211 |
"E,dt\<Turnstile>s\<Colon>\<surd>" == "E,dt\<Turnstile>In1r s\<Colon>Inl (PrimT Void)" |
|
212 |
"E,dt\<Turnstile>e\<Colon>-T" == "E,dt\<Turnstile>In1l e\<Colon>Inl T" |
|
213 |
"E,dt\<Turnstile>e\<Colon>=T" == "E,dt\<Turnstile>In2 e\<Colon>Inl T" |
|
214 |
"E,dt\<Turnstile>e\<Colon>\<doteq>T" == "E,dt\<Turnstile>In3 e\<Colon>Inr T" |
|
215 |
||
216 |
syntax (* for purely static typing *) |
|
217 |
wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_|-_::_" [51,51,51] 50) |
|
218 |
wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_|-_:<>" [51,51 ] 50) |
|
219 |
ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_|-_:-_" [51,51,51] 50) |
|
220 |
ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_|-_:=_" [51,51,51] 50) |
|
221 |
ty_exprs_:: "env \<Rightarrow> [expr list, |
|
222 |
\<spacespace> ty list] \<Rightarrow> bool" ("_|-_:#_" [51,51,51] 50) |
|
223 |
||
224 |
syntax (xsymbols) |
|
225 |
wt_ :: "env \<Rightarrow> [term,tys] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>_" [51,51,51] 50) |
|
226 |
wt_stmt_ :: "env \<Rightarrow> stmt \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<surd>" [51,51 ] 50) |
|
227 |
ty_expr_ :: "env \<Rightarrow> [expr ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>-_" [51,51,51] 50) |
|
228 |
ty_var_ :: "env \<Rightarrow> [var ,ty ] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>=_" [51,51,51] 50) |
|
229 |
ty_exprs_ :: "env \<Rightarrow> [expr list, |
|
230 |
\<spacespace> ty list] \<Rightarrow> bool" ("_\<turnstile>_\<Colon>\<doteq>_" [51,51,51] 50) |
|
231 |
||
232 |
translations |
|
233 |
"E\<turnstile>t\<Colon> T" == "E,empty_dt\<Turnstile>t\<Colon> T" |
|
234 |
"E\<turnstile>s\<Colon>\<surd>" == "E,empty_dt\<Turnstile>s\<Colon>\<surd>" |
|
235 |
"E\<turnstile>e\<Colon>-T" == "E,empty_dt\<Turnstile>e\<Colon>-T" |
|
236 |
"E\<turnstile>e\<Colon>=T" == "E,empty_dt\<Turnstile>e\<Colon>=T" |
|
237 |
"E\<turnstile>e\<Colon>\<doteq>T" == "E,empty_dt\<Turnstile>e\<Colon>\<doteq>T" |
|
238 |
||
239 |
||
240 |
inductive wt intros |
|
241 |
||
242 |
||
243 |
(* well-typed statements *) |
|
244 |
||
245 |
Skip: "E,dt\<Turnstile>Skip\<Colon>\<surd>" |
|
246 |
||
247 |
Expr: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T\<rbrakk> \<Longrightarrow> |
|
248 |
E,dt\<Turnstile>Expr e\<Colon>\<surd>" |
|
249 |
(* cf. 14.6 *) |
|
250 |
Lab: "E,dt\<Turnstile>c\<Colon>\<surd> \<Longrightarrow> |
|
251 |
E,dt\<Turnstile>l\<bullet> c\<Colon>\<surd>" |
|
252 |
||
253 |
Comp: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; |
|
254 |
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> |
|
255 |
E,dt\<Turnstile>c1;; c2\<Colon>\<surd>" |
|
256 |
||
257 |
(* cf. 14.8 *) |
|
258 |
If: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean; |
|
259 |
E,dt\<Turnstile>c1\<Colon>\<surd>; |
|
260 |
E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> |
|
261 |
E,dt\<Turnstile>If(e) c1 Else c2\<Colon>\<surd>" |
|
262 |
||
263 |
(* cf. 14.10 *) |
|
264 |
Loop: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-PrimT Boolean; |
|
265 |
E,dt\<Turnstile>c\<Colon>\<surd>\<rbrakk> \<Longrightarrow> |
|
266 |
E,dt\<Turnstile>l\<bullet> While(e) c\<Colon>\<surd>" |
|
267 |
(* cf. 14.13, 14.15, 14.16 *) |
|
268 |
Do: "E,dt\<Turnstile>Do jump\<Colon>\<surd>" |
|
269 |
||
270 |
(* cf. 14.16 *) |
|
271 |
Throw: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class tn; |
|
272 |
prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable\<rbrakk> \<Longrightarrow> |
|
273 |
E,dt\<Turnstile>Throw e\<Colon>\<surd>" |
|
274 |
(* cf. 14.18 *) |
|
275 |
Try: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; prg E\<turnstile>tn\<preceq>\<^sub>C SXcpt Throwable; |
|
276 |
lcl E (VName vn)=None; E \<lparr>lcl := lcl E(VName vn\<mapsto>Class tn)\<rparr>,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> |
|
277 |
\<Longrightarrow> |
|
278 |
E,dt\<Turnstile>Try c1 Catch(tn vn) c2\<Colon>\<surd>" |
|
279 |
||
280 |
(* cf. 14.18 *) |
|
281 |
Fin: "\<lbrakk>E,dt\<Turnstile>c1\<Colon>\<surd>; E,dt\<Turnstile>c2\<Colon>\<surd>\<rbrakk> \<Longrightarrow> |
|
282 |
E,dt\<Turnstile>c1 Finally c2\<Colon>\<surd>" |
|
283 |
||
284 |
Init: "\<lbrakk>is_class (prg E) C\<rbrakk> \<Longrightarrow> |
|
285 |
E,dt\<Turnstile>Init C\<Colon>\<surd>" |
|
286 |
(* Init is created on the fly during evaluation (see Eval.thy). The class |
|
287 |
* isn't necessarily accessible from the points Init is called. Therefor |
|
288 |
* we only demand is_class and not is_acc_class here |
|
289 |
*) |
|
290 |
||
291 |
(* well-typed expressions *) |
|
292 |
||
293 |
(* cf. 15.8 *) |
|
294 |
NewC: "\<lbrakk>is_acc_class (prg E) (pkg E) C\<rbrakk> \<Longrightarrow> |
|
295 |
E,dt\<Turnstile>NewC C\<Colon>-Class C" |
|
296 |
(* cf. 15.9 *) |
|
297 |
NewA: "\<lbrakk>is_acc_type (prg E) (pkg E) T; |
|
298 |
E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow> |
|
299 |
E,dt\<Turnstile>New T[i]\<Colon>-T.[]" |
|
300 |
||
301 |
(* cf. 15.15 *) |
|
302 |
Cast: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T; is_acc_type (prg E) (pkg E) T'; |
|
303 |
prg E\<turnstile>T\<preceq>? T'\<rbrakk> \<Longrightarrow> |
|
304 |
E,dt\<Turnstile>Cast T' e\<Colon>-T'" |
|
305 |
||
306 |
(* cf. 15.19.2 *) |
|
307 |
Inst: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT T; is_acc_type (prg E) (pkg E) (RefT T'); |
|
308 |
prg E\<turnstile>RefT T\<preceq>? RefT T'\<rbrakk> \<Longrightarrow> |
|
309 |
E,dt\<Turnstile>e InstOf T'\<Colon>-PrimT Boolean" |
|
310 |
||
311 |
(* cf. 15.7.1 *) |
|
312 |
Lit: "\<lbrakk>typeof dt x = Some T\<rbrakk> \<Longrightarrow> |
|
313 |
E,dt\<Turnstile>Lit x\<Colon>-T" |
|
314 |
||
315 |
(* cf. 15.10.2, 15.11.1 *) |
|
316 |
Super: "\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; |
|
317 |
class (prg E) C = Some c\<rbrakk> \<Longrightarrow> |
|
318 |
E,dt\<Turnstile>Super\<Colon>-Class (super c)" |
|
319 |
||
320 |
(* cf. 15.13.1, 15.10.1, 15.12 *) |
|
321 |
Acc: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T\<rbrakk> \<Longrightarrow> |
|
322 |
E,dt\<Turnstile>Acc va\<Colon>-T" |
|
323 |
||
324 |
(* cf. 15.25, 15.25.1 *) |
|
325 |
Ass: "\<lbrakk>E,dt\<Turnstile>va\<Colon>=T; va \<noteq> LVar This; |
|
326 |
E,dt\<Turnstile>v \<Colon>-T'; |
|
327 |
prg E\<turnstile>T'\<preceq>T\<rbrakk> \<Longrightarrow> |
|
328 |
E,dt\<Turnstile>va:=v\<Colon>-T'" |
|
329 |
||
330 |
(* cf. 15.24 *) |
|
331 |
Cond: "\<lbrakk>E,dt\<Turnstile>e0\<Colon>-PrimT Boolean; |
|
332 |
E,dt\<Turnstile>e1\<Colon>-T1; E,dt\<Turnstile>e2\<Colon>-T2; |
|
333 |
prg E\<turnstile>T1\<preceq>T2 \<and> T = T2 \<or> prg E\<turnstile>T2\<preceq>T1 \<and> T = T1\<rbrakk> \<Longrightarrow> |
|
334 |
E,dt\<Turnstile>e0 ? e1 : e2\<Colon>-T" |
|
335 |
||
336 |
(* cf. 15.11.1, 15.11.2, 15.11.3 *) |
|
337 |
Call: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; |
|
338 |
E,dt\<Turnstile>ps\<Colon>\<doteq>pTs; |
|
339 |
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> |
|
340 |
= {((statDeclT,m),pTs')} |
|
341 |
\<rbrakk> \<Longrightarrow> |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
342 |
E,dt\<Turnstile>{cls E,statT,invmode m e}e\<cdot>mn({pTs'}ps)\<Colon>-(resTy m)" |
12854 | 343 |
|
344 |
Methd: "\<lbrakk>is_class (prg E) C; |
|
345 |
methd (prg E) C sig = Some m; |
|
346 |
E,dt\<Turnstile>Body (declclass m) (stmt (mbody (mthd m)))\<Colon>-T\<rbrakk> \<Longrightarrow> |
|
347 |
E,dt\<Turnstile>Methd C sig\<Colon>-T" |
|
348 |
(* The class C is the dynamic class of the method call (cf. Eval.thy). |
|
349 |
* It hasn't got to be directly accessible from the current package (pkg E). |
|
350 |
* Only the static class must be accessible (enshured indirectly by Call). |
|
351 |
*) |
|
352 |
||
353 |
Body: "\<lbrakk>is_class (prg E) D; |
|
354 |
E,dt\<Turnstile>blk\<Colon>\<surd>; |
|
355 |
(lcl E) Result = Some T; |
|
356 |
is_type (prg E) T\<rbrakk> \<Longrightarrow> |
|
357 |
E,dt\<Turnstile>Body D blk\<Colon>-T" |
|
358 |
(* the class D implementing the method must not directly be accessible |
|
359 |
* from the current package (pkg E), but can also be indirectly accessible |
|
360 |
* due to inheritance (enshured in Call) |
|
361 |
* The result type hasn't got to be accessible in Java! (If it is not |
|
362 |
* accessible you can only assign it to Object) |
|
363 |
*) |
|
364 |
||
365 |
(* well-typed variables *) |
|
366 |
||
367 |
(* cf. 15.13.1 *) |
|
368 |
LVar: "\<lbrakk>lcl E vn = Some T; is_acc_type (prg E) (pkg E) T\<rbrakk> \<Longrightarrow> |
|
369 |
E,dt\<Turnstile>LVar vn\<Colon>=T" |
|
370 |
(* cf. 15.10.1 *) |
|
371 |
FVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
372 |
accfield (prg E) (cls E) C fn = Some (statDeclC,f)\<rbrakk> \<Longrightarrow> |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
373 |
E,dt\<Turnstile>{cls E,statDeclC,is_static f}e..fn\<Colon>=(type f)" |
12854 | 374 |
(* cf. 15.12 *) |
375 |
AVar: "\<lbrakk>E,dt\<Turnstile>e\<Colon>-T.[]; |
|
376 |
E,dt\<Turnstile>i\<Colon>-PrimT Integer\<rbrakk> \<Longrightarrow> |
|
377 |
E,dt\<Turnstile>e.[i]\<Colon>=T" |
|
378 |
||
379 |
||
380 |
(* well-typed expression lists *) |
|
381 |
||
382 |
(* cf. 15.11.??? *) |
|
383 |
Nil: "E,dt\<Turnstile>[]\<Colon>\<doteq>[]" |
|
384 |
||
385 |
(* cf. 15.11.??? *) |
|
386 |
Cons: "\<lbrakk>E,dt\<Turnstile>e \<Colon>-T; |
|
387 |
E,dt\<Turnstile>es\<Colon>\<doteq>Ts\<rbrakk> \<Longrightarrow> |
|
388 |
E,dt\<Turnstile>e#es\<Colon>\<doteq>T#Ts" |
|
389 |
||
390 |
||
391 |
declare not_None_eq [simp del] |
|
392 |
declare split_if [split del] split_if_asm [split del] |
|
393 |
declare split_paired_All [simp del] split_paired_Ex [simp del] |
|
394 |
ML_setup {* |
|
395 |
simpset_ref() := simpset() delloop "split_all_tac" |
|
396 |
*} |
|
397 |
inductive_cases wt_stmt_cases: "E,dt\<Turnstile>c\<Colon>\<surd>" |
|
398 |
inductive_cases wt_elim_cases: |
|
399 |
"E,dt\<Turnstile>In2 (LVar vn) \<Colon>T" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
400 |
"E,dt\<Turnstile>In2 ({accC,statDeclC,s}e..fn)\<Colon>T" |
12854 | 401 |
"E,dt\<Turnstile>In2 (e.[i]) \<Colon>T" |
402 |
"E,dt\<Turnstile>In1l (NewC C) \<Colon>T" |
|
403 |
"E,dt\<Turnstile>In1l (New T'[i]) \<Colon>T" |
|
404 |
"E,dt\<Turnstile>In1l (Cast T' e) \<Colon>T" |
|
405 |
"E,dt\<Turnstile>In1l (e InstOf T') \<Colon>T" |
|
406 |
"E,dt\<Turnstile>In1l (Lit x) \<Colon>T" |
|
407 |
"E,dt\<Turnstile>In1l (Super) \<Colon>T" |
|
408 |
"E,dt\<Turnstile>In1l (Acc va) \<Colon>T" |
|
409 |
"E,dt\<Turnstile>In1l (Ass va v) \<Colon>T" |
|
410 |
"E,dt\<Turnstile>In1l (e0 ? e1 : e2) \<Colon>T" |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
411 |
"E,dt\<Turnstile>In1l ({accC,statT,mode}e\<cdot>mn({pT'}p))\<Colon>T" |
12854 | 412 |
"E,dt\<Turnstile>In1l (Methd C sig) \<Colon>T" |
413 |
"E,dt\<Turnstile>In1l (Body D blk) \<Colon>T" |
|
414 |
"E,dt\<Turnstile>In3 ([]) \<Colon>Ts" |
|
415 |
"E,dt\<Turnstile>In3 (e#es) \<Colon>Ts" |
|
416 |
"E,dt\<Turnstile>In1r Skip \<Colon>x" |
|
417 |
"E,dt\<Turnstile>In1r (Expr e) \<Colon>x" |
|
418 |
"E,dt\<Turnstile>In1r (c1;; c2) \<Colon>x" |
|
419 |
"E,dt\<Turnstile>In1r (l\<bullet> c) \<Colon>x" |
|
420 |
"E,dt\<Turnstile>In1r (If(e) c1 Else c2) \<Colon>x" |
|
421 |
"E,dt\<Turnstile>In1r (l\<bullet> While(e) c) \<Colon>x" |
|
422 |
"E,dt\<Turnstile>In1r (Do jump) \<Colon>x" |
|
423 |
"E,dt\<Turnstile>In1r (Throw e) \<Colon>x" |
|
424 |
"E,dt\<Turnstile>In1r (Try c1 Catch(tn vn) c2)\<Colon>x" |
|
425 |
"E,dt\<Turnstile>In1r (c1 Finally c2) \<Colon>x" |
|
426 |
"E,dt\<Turnstile>In1r (Init C) \<Colon>x" |
|
427 |
declare not_None_eq [simp] |
|
428 |
declare split_if [split] split_if_asm [split] |
|
429 |
declare split_paired_All [simp] split_paired_Ex [simp] |
|
430 |
ML_setup {* |
|
431 |
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) |
|
432 |
*} |
|
433 |
||
434 |
lemma is_acc_class_is_accessible: |
|
435 |
"is_acc_class G P C \<Longrightarrow> G\<turnstile>(Class C) accessible_in P" |
|
436 |
by (auto simp add: is_acc_class_def) |
|
437 |
||
438 |
lemma is_acc_iface_is_iface: "is_acc_iface G P I \<Longrightarrow> is_iface G I" |
|
439 |
by (auto simp add: is_acc_iface_def) |
|
440 |
||
441 |
lemma is_acc_iface_is_accessible: |
|
442 |
"is_acc_iface G P I \<Longrightarrow> G\<turnstile>(Iface I) accessible_in P" |
|
443 |
by (auto simp add: is_acc_iface_def) |
|
444 |
||
445 |
lemma is_acc_type_is_type: "is_acc_type G P T \<Longrightarrow> is_type G T" |
|
446 |
by (auto simp add: is_acc_type_def) |
|
447 |
||
448 |
lemma is_acc_iface_is_accessible: "is_acc_type G P T \<Longrightarrow> G\<turnstile>T accessible_in P" |
|
449 |
by (auto simp add: is_acc_type_def) |
|
450 |
||
451 |
lemma wt_Methd_is_methd: |
|
452 |
"E\<turnstile>In1l (Methd C sig)\<Colon>T \<Longrightarrow> is_methd (prg E) C sig" |
|
453 |
apply (erule_tac wt_elim_cases) |
|
454 |
apply clarsimp |
|
455 |
apply (erule is_methdI, assumption) |
|
456 |
done |
|
457 |
||
458 |
(* Special versions of some typing rules, better suited to pattern match the |
|
459 |
* conclusion (no selectors in the conclusion\<dots>) |
|
460 |
*) |
|
461 |
||
462 |
lemma wt_Super: |
|
463 |
"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; |
|
464 |
class (prg E) C = Some c;D=super c\<rbrakk> |
|
465 |
\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D" |
|
466 |
by (auto elim: wt.Super) |
|
467 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
468 |
|
12854 | 469 |
lemma wt_Call: |
470 |
"\<lbrakk>E,dt\<Turnstile>e\<Colon>-RefT statT; E,dt\<Turnstile>ps\<Colon>\<doteq>pTs; |
|
471 |
max_spec (prg E) (cls E) statT \<lparr>name=mn,parTs=pTs\<rparr> |
|
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
472 |
= {((statDeclC,m),pTs')};rT=(resTy m);accC=cls E; |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
473 |
mode = invmode m e\<rbrakk> \<Longrightarrow> E,dt\<Turnstile>{accC,statT,mode}e\<cdot>mn({pTs'}ps)\<Colon>-rT" |
12854 | 474 |
by (auto elim: wt.Call) |
475 |
||
476 |
||
477 |
lemma invocationTypeExpr_noClassD: |
|
478 |
"\<lbrakk> E\<turnstile>e\<Colon>-RefT statT\<rbrakk> |
|
479 |
\<Longrightarrow> (\<forall> statC. statT \<noteq> ClassT statC) \<longrightarrow> invmode m e \<noteq> SuperM" |
|
480 |
proof - |
|
481 |
assume wt: "E\<turnstile>e\<Colon>-RefT statT" |
|
482 |
show ?thesis |
|
483 |
proof (cases "e=Super") |
|
484 |
case True |
|
485 |
with wt obtain "C" where "statT = ClassT C" by (blast elim: wt_elim_cases) |
|
486 |
then show ?thesis by blast |
|
487 |
next |
|
488 |
case False then show ?thesis |
|
489 |
by (auto simp add: invmode_def split: split_if_asm) |
|
490 |
qed |
|
491 |
qed |
|
492 |
||
493 |
lemma wt_Super: |
|
494 |
"\<lbrakk>lcl E This = Some (Class C); C \<noteq> Object; class (prg E) C = Some c; D=super c\<rbrakk> |
|
495 |
\<Longrightarrow> E,dt\<Turnstile>Super\<Colon>-Class D" |
|
496 |
by (auto elim: wt.Super) |
|
497 |
||
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
498 |
lemma wt_FVar: |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
499 |
"\<lbrakk>E,dt\<Turnstile>e\<Colon>-Class C; accfield (prg E) (cls E) C fn = Some (statDeclC,f); |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
500 |
sf=is_static f; fT=(type f); accC=cls E\<rbrakk> |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
501 |
\<Longrightarrow> E,dt\<Turnstile>{accC,statDeclC,sf}e..fn\<Colon>=fT" |
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12858
diff
changeset
|
502 |
by (auto dest: wt.FVar) |
12854 | 503 |
|
504 |
||
505 |
lemma wt_init [iff]: "E,dt\<Turnstile>Init C\<Colon>\<surd> = is_class (prg E) C" |
|
506 |
by (auto elim: wt_elim_cases intro: "wt.Init") |
|
507 |
||
508 |
declare wt.Skip [iff] |
|
509 |
||
510 |
lemma wt_StatRef: |
|
511 |
"is_acc_type (prg E) (pkg E) (RefT rt) \<Longrightarrow> E\<turnstile>StatRef rt\<Colon>-RefT rt" |
|
512 |
apply (rule wt.Cast) |
|
513 |
apply (rule wt.Lit) |
|
514 |
apply (simp (no_asm)) |
|
515 |
apply (simp (no_asm_simp)) |
|
516 |
apply (rule cast.widen) |
|
517 |
apply (simp (no_asm)) |
|
518 |
done |
|
519 |
||
520 |
lemma wt_Inj_elim: |
|
521 |
"\<And>E. E,dt\<Turnstile>t\<Colon>U \<Longrightarrow> case t of |
|
522 |
In1 ec \<Rightarrow> (case ec of |
|
523 |
Inl e \<Rightarrow> \<exists>T. U=Inl T |
|
524 |
| Inr s \<Rightarrow> U=Inl (PrimT Void)) |
|
525 |
| In2 e \<Rightarrow> (\<exists>T. U=Inl T) |
|
526 |
| In3 e \<Rightarrow> (\<exists>T. U=Inr T)" |
|
527 |
apply (erule wt.induct) |
|
528 |
apply auto |
|
529 |
done |
|
530 |
||
531 |
ML {* |
|
532 |
fun wt_fun name inj rhs = |
|
533 |
let |
|
534 |
val lhs = "E,dt\<Turnstile>" ^ inj ^ " t\<Colon>U" |
|
535 |
val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") |
|
536 |
(K [Auto_tac, ALLGOALS (ftac (thm "wt_Inj_elim")) THEN Auto_tac]) |
|
537 |
fun is_Inj (Const (inj,_) $ _) = true |
|
538 |
| is_Inj _ = false |
|
539 |
fun pred (t as (_ $ (Const ("Pair",_) $ |
|
540 |
_ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $ |
|
541 |
x))) $ _ )) = is_Inj x |
|
542 |
in |
|
543 |
make_simproc name lhs pred (thm name) |
|
544 |
end |
|
545 |
||
546 |
val wt_expr_proc = wt_fun "wt_expr_eq" "In1l" "\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>-T" |
|
547 |
val wt_var_proc = wt_fun "wt_var_eq" "In2" "\<exists>T. U=Inl T \<and> E,dt\<Turnstile>t\<Colon>=T" |
|
548 |
val wt_exprs_proc = wt_fun "wt_exprs_eq" "In3" "\<exists>Ts. U=Inr Ts \<and> E,dt\<Turnstile>t\<Colon>\<doteq>Ts" |
|
549 |
val wt_stmt_proc = wt_fun "wt_stmt_eq" "In1r" "U=Inl(PrimT Void)\<and>E,dt\<Turnstile>t\<Colon>\<surd>" |
|
550 |
*} |
|
551 |
||
552 |
ML {* |
|
553 |
Addsimprocs [wt_expr_proc,wt_var_proc,wt_exprs_proc,wt_stmt_proc] |
|
554 |
*} |
|
555 |
||
556 |
lemma Inj_eq_lemma [simp]: |
|
557 |
"(\<forall>T. (\<exists>T'. T = Inj T' \<and> P T') \<longrightarrow> Q T) = (\<forall>T'. P T' \<longrightarrow> Q (Inj T'))" |
|
558 |
by auto |
|
559 |
||
560 |
(* unused *) |
|
561 |
lemma single_valued_tys_lemma [rule_format (no_asm)]: |
|
562 |
"\<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> |
|
563 |
G = prg E \<longrightarrow> (\<forall>T'. E,dt\<Turnstile>t\<Colon>T' \<longrightarrow> T = T')" |
|
564 |
apply (cases "E", erule wt.induct) |
|
565 |
apply (safe del: disjE) |
|
566 |
apply (simp_all (no_asm_use) split del: split_if_asm) |
|
567 |
apply (safe del: disjE) |
|
568 |
(* 17 subgoals *) |
|
569 |
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) *}) |
|
570 |
(*apply (safe del: disjE elim!: wt_elim_cases)*) |
|
571 |
apply (tactic {*ALLGOALS (eresolve_tac (thms "wt_elim_cases"))*}) |
|
572 |
apply (simp_all (no_asm_use) split del: split_if_asm) |
|
573 |
apply (erule_tac [10] V = "All ?P" in thin_rl) (* Call *) |
|
574 |
apply ((blast del: equalityCE dest: sym [THEN trans])+) |
|
575 |
done |
|
576 |
||
577 |
(* unused *) |
|
578 |
lemma single_valued_tys: |
|
579 |
"ws_prog (prg E) \<Longrightarrow> single_valued {(t,T). E,dt\<Turnstile>t\<Colon>T}" |
|
580 |
apply (unfold single_valued_def) |
|
581 |
apply clarsimp |
|
582 |
apply (rule single_valued_tys_lemma) |
|
583 |
apply (auto intro!: widen_antisym) |
|
584 |
done |
|
585 |
||
586 |
lemma typeof_empty_is_type [rule_format (no_asm)]: |
|
587 |
"typeof (\<lambda>a. None) v = Some T \<longrightarrow> is_type G T" |
|
588 |
apply (rule val.induct) |
|
589 |
apply auto |
|
590 |
done |
|
591 |
||
592 |
(* unused *) |
|
593 |
lemma typeof_is_type [rule_format (no_asm)]: |
|
594 |
"(\<forall>a. v \<noteq> Addr a) \<longrightarrow> (\<exists>T. typeof dt v = Some T \<and> is_type G T)" |
|
595 |
apply (rule val.induct) |
|
596 |
prefer 5 |
|
597 |
apply fast |
|
598 |
apply (simp_all (no_asm)) |
|
599 |
done |
|
600 |
||
601 |
end |