author  wenzelm 
Mon, 25 Feb 2002 20:48:14 +0100  
changeset 12937  0c4fd7529467 
parent 12925  99131847fb93 
child 13337  f75dfc606ac7 
permissions  rwrr 
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 {* Welltypedness 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 typesafety, 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 
(* welltyped 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 
(* welltyped 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 
(* welltyped 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 
(* welltyped 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 