author  wenzelm 
Mon, 25 Feb 2002 20:48:14 +0100  
changeset 12937  0c4fd7529467 
parent 12925  99131847fb93 
child 12962  a24ffe84a06a 
permissions  rwrr 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1 
(* Title: HOL/Bali/DeclConcepts.thy 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

2 
ID: $Id$ 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

3 
Author: Norbert Schirmer 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

5 
*) 
12854  6 
header {* Advanced concepts on Java declarations like overriding, inheritance, 
7 
dynamic method lookup*} 

8 

9 
theory DeclConcepts = TypeRel: 

10 

11 
section "access control (cf. 6.6), overriding and hiding (cf. 8.4.6.1)" 

12 

13 
constdefs 

14 
is_public :: "prog \<Rightarrow> qtname \<Rightarrow> bool" 

15 
"is_public G qn \<equiv> (case class G qn of 

16 
None \<Rightarrow> (case iface G qn of 

17 
None \<Rightarrow> False 

18 
 Some iface \<Rightarrow> access iface = Public) 

19 
 Some class \<Rightarrow> access class = Public)" 

20 

21 
subsection "accessibility of types (cf. 6.6.1)" 

22 
text {* 

23 
Primitive types are always accessible, interfaces and classes are accessible 

24 
in their package or if they are defined public, an array type is accessible if 

25 
its element type is accessible *} 

26 

27 
consts accessible_in :: "prog \<Rightarrow> ty \<Rightarrow> pname \<Rightarrow> bool" 

28 
("_ \<turnstile> _ accessible'_in _" [61,61,61] 60) 

29 
rt_accessible_in:: "prog \<Rightarrow> ref_ty \<Rightarrow> pname \<Rightarrow> bool" 

30 
("_ \<turnstile> _ accessible'_in' _" [61,61,61] 60) 

31 
primrec 

32 
"G\<turnstile>(PrimT p) accessible_in pack = True" 

33 
accessible_in_RefT_simp: 

34 
"G\<turnstile>(RefT r) accessible_in pack = G\<turnstile>r accessible_in' pack" 

35 

36 
"G\<turnstile>(NullT) accessible_in' pack = True" 

37 
"G\<turnstile>(IfaceT I) accessible_in' pack = ((pid I = pack) \<or> is_public G I)" 

38 
"G\<turnstile>(ClassT C) accessible_in' pack = ((pid C = pack) \<or> is_public G C)" 

39 
"G\<turnstile>(ArrayT ty) accessible_in' pack = G\<turnstile>ty accessible_in pack" 

40 

41 
declare accessible_in_RefT_simp [simp del] 

42 

43 
constdefs 

44 
is_acc_class :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" 

45 
"is_acc_class G P C \<equiv> is_class G C \<and> G\<turnstile>(Class C) accessible_in P" 

46 
is_acc_iface :: "prog \<Rightarrow> pname \<Rightarrow> qtname \<Rightarrow> bool" 

47 
"is_acc_iface G P I \<equiv> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P" 

48 
is_acc_type :: "prog \<Rightarrow> pname \<Rightarrow> ty \<Rightarrow> bool" 

49 
"is_acc_type G P T \<equiv> is_type G T \<and> G\<turnstile>T accessible_in P" 

50 
is_acc_reftype :: "prog \<Rightarrow> pname \<Rightarrow> ref_ty \<Rightarrow> bool" 

51 
"is_acc_reftype G P T \<equiv> isrtype G T \<and> G\<turnstile>T accessible_in' P" 

52 

53 
lemma is_acc_classD: 

54 
"is_acc_class G P C \<Longrightarrow> is_class G C \<and> G\<turnstile>(Class C) accessible_in P" 

55 
by (simp add: is_acc_class_def) 

56 

57 
lemma is_acc_class_is_class: "is_acc_class G P C \<Longrightarrow> is_class G C" 

58 
by (auto simp add: is_acc_class_def) 

59 

60 
lemma is_acc_ifaceD: 

61 
"is_acc_iface G P I \<Longrightarrow> is_iface G I \<and> G\<turnstile>(Iface I) accessible_in P" 

62 
by (simp add: is_acc_iface_def) 

63 

64 
lemma is_acc_typeD: 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

65 
"is_acc_type G P T \<Longrightarrow> is_type G T \<and> G\<turnstile>T accessible_in P" 
12854  66 
by (simp add: is_acc_type_def) 
67 

68 
lemma is_acc_reftypeD: 

69 
"is_acc_reftype G P T \<Longrightarrow> isrtype G T \<and> G\<turnstile>T accessible_in' P" 

70 
by (simp add: is_acc_reftype_def) 

71 

72 
subsection "accessibility of members" 

73 
text {* 

74 
The accessibility of members is more involved as the accessibility of types. 

75 
We have to distinguish several cases to model the different effects of 

76 
accessibility during inheritance, overriding and ordinary member access 

77 
*} 

78 

79 
subsubsection {* Various technical conversion and selection functions *} 

80 

81 
text {* overloaded selector @{text accmodi} to select the access modifier 

82 
out of various HOL types *} 

83 

84 
axclass has_accmodi < "type" 

85 
consts accmodi:: "'a::has_accmodi \<Rightarrow> acc_modi" 

86 

12859  87 
instance acc_modi::has_accmodi .. 
12854  88 

89 
defs (overloaded) 

90 
acc_modi_accmodi_def: "accmodi (a::acc_modi) \<equiv> a" 

91 

92 
lemma acc_modi_accmodi_simp[simp]: "accmodi (a::acc_modi) = a" 

93 
by (simp add: acc_modi_accmodi_def) 

94 

12859  95 
instance access_field_type:: ("type","type") has_accmodi .. 
12854  96 

97 
defs (overloaded) 

98 
decl_acc_modi_def: "accmodi (d::('a:: type) decl_scheme) \<equiv> access d" 

99 

100 

101 
lemma decl_acc_modi_simp[simp]: "accmodi (d::('a::type) decl_scheme) = access d" 

102 
by (simp add: decl_acc_modi_def) 

103 

12859  104 
instance * :: ("type",has_accmodi) has_accmodi .. 
12854  105 

106 
defs (overloaded) 

107 
pair_acc_modi_def: "accmodi p \<equiv> (accmodi (snd p))" 

108 

109 
lemma pair_acc_modi_simp[simp]: "accmodi (x,a) = (accmodi a)" 

110 
by (simp add: pair_acc_modi_def) 

111 

12859  112 
instance memberdecl :: has_accmodi .. 
12854  113 

114 
defs (overloaded) 

115 
memberdecl_acc_modi_def: "accmodi m \<equiv> (case m of 

116 
fdecl f \<Rightarrow> accmodi f 

117 
 mdecl m \<Rightarrow> accmodi m)" 

118 

119 
lemma memberdecl_fdecl_acc_modi_simp[simp]: 

120 
"accmodi (fdecl m) = accmodi m" 

121 
by (simp add: memberdecl_acc_modi_def) 

122 

123 
lemma memberdecl_mdecl_acc_modi_simp[simp]: 

124 
"accmodi (mdecl m) = accmodi m" 

125 
by (simp add: memberdecl_acc_modi_def) 

126 

127 
text {* overloaded selector @{text declclass} to select the declaring class 

128 
out of various HOL types *} 

129 

130 
axclass has_declclass < "type" 

131 
consts declclass:: "'a::has_declclass \<Rightarrow> qtname" 

132 

12859  133 
instance pid_field_type::("type","type") has_declclass .. 
12854  134 

135 
defs (overloaded) 

136 
qtname_declclass_def: "declclass (q::qtname) \<equiv> q" 

137 

138 
lemma qtname_declclass_simp[simp]: "declclass (q::qtname) = q" 

139 
by (simp add: qtname_declclass_def) 

140 

12859  141 
instance * :: ("has_declclass","type") has_declclass .. 
12854  142 

143 
defs (overloaded) 

144 
pair_declclass_def: "declclass p \<equiv> declclass (fst p)" 

145 

146 
lemma pair_declclass_simp[simp]: "declclass (c,x) = declclass c" 

147 
by (simp add: pair_declclass_def) 

148 

149 
text {* overloaded selector @{text is_static} to select the static modifier 

150 
out of various HOL types *} 

151 

152 

153 
axclass has_static < "type" 

154 
consts is_static :: "'a::has_static \<Rightarrow> bool" 

155 

156 
(* 

157 
consts is_static :: "'a \<Rightarrow> bool" 

158 
*) 

159 

12859  160 
instance access_field_type :: ("type","has_static") has_static .. 
12854  161 

162 
defs (overloaded) 

163 
decl_is_static_def: 

164 
"is_static (m::('a::has_static) decl_scheme) \<equiv> is_static (Decl.decl.more m)" 

165 

12859  166 
instance static_field_type :: ("type","type") has_static .. 
12854  167 

168 
defs (overloaded) 

169 
static_field_type_is_static_def: 

170 
"is_static (m::(bool,'b::type) static_field_type) \<equiv> static_val m" 

171 

172 
lemma member_is_static_simp: "is_static (m::'a member_scheme) = static m" 

173 
apply (cases m) 

174 
apply (simp add: static_field_type_is_static_def 

175 
decl_is_static_def Decl.member.dest_convs) 

176 
done 

177 

12859  178 
instance * :: ("type","has_static") has_static .. 
12854  179 

180 
defs (overloaded) 

181 
pair_is_static_def: "is_static p \<equiv> is_static (snd p)" 

182 

183 
lemma pair_is_static_simp [simp]: "is_static (x,s) = is_static s" 

184 
by (simp add: pair_is_static_def) 

185 

186 
lemma pair_is_static_simp1: "is_static p = is_static (snd p)" 

187 
by (simp add: pair_is_static_def) 

188 

12859  189 
instance memberdecl:: has_static .. 
12854  190 

191 
defs (overloaded) 

192 
memberdecl_is_static_def: 

193 
"is_static m \<equiv> (case m of 

194 
fdecl f \<Rightarrow> is_static f 

195 
 mdecl m \<Rightarrow> is_static m)" 

196 

197 
lemma memberdecl_is_static_fdecl_simp[simp]: 

198 
"is_static (fdecl f) = is_static f" 

199 
by (simp add: memberdecl_is_static_def) 

200 

201 
lemma memberdecl_is_static_mdecl_simp[simp]: 

202 
"is_static (mdecl m) = is_static m" 

203 
by (simp add: memberdecl_is_static_def) 

204 

205 
lemma mhead_static_simp [simp]: "is_static (mhead m) = is_static m" 

206 
by (cases m) (simp add: mhead_def member_is_static_simp) 

207 

208 
constdefs (* some mnemotic selectors for (qtname \<times> ('a::more) decl_scheme) 

209 
* the first component is a class or interface name 

210 
* the second component is a method, field or method head *) 

211 
(* "declclass":: "(qtname \<times> ('a::more) decl_scheme) \<Rightarrow> qtname"*) 

212 
(* "declclass \<equiv> fst" *) (* get the class component *) 

213 

214 
"decliface":: "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> qtname" 

215 
"decliface \<equiv> fst" (* get the interface component *) 

216 

217 
(* 

218 
"member":: "(qtname \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme" 

219 
*) 

220 
"mbr":: "(qtname \<times> memberdecl) \<Rightarrow> memberdecl" 

221 
"mbr \<equiv> snd" (* get the memberdecl component *) 

222 

223 
"mthd":: "('b \<times> 'a) \<Rightarrow> 'a" 

224 
(* also used for mdecl,mhead *) 

225 
"mthd \<equiv> snd" (* get the method component *) 

226 

227 
"fld":: "('b \<times> ('a::type) decl_scheme) \<Rightarrow> ('a::type) decl_scheme" 

228 
(* also used for ((vname \<times> qtname)\<times> field) *) 

229 
"fld \<equiv> snd" (* get the field component *) 

230 

231 
(* "accmodi" :: "('b \<times> ('a::type) decl_scheme) \<Rightarrow> acc_modi"*) 

232 
(* also used for mdecl *) 

233 
(* "accmodi \<equiv> access \<circ> snd"*) (* get the access modifier *) 

234 
(* 

235 
"is_static" ::"('b \<times> ('a::type) member_scheme) \<Rightarrow> bool" *) 

236 
(* also defined for emhead cf. WellType *) 

237 
(*"is_static \<equiv> static \<circ> snd"*) (* get the static modifier *) 

238 

239 
constdefs (* some mnemotic selectors for (vname \<times> qtname) *) 

240 
fname:: "(vname \<times> 'a) \<Rightarrow> vname" (* also used for fdecl *) 

241 
"fname \<equiv> fst" 

242 

243 
declclassf:: "(vname \<times> qtname) \<Rightarrow> qtname" 

244 
"declclassf \<equiv> snd" 

245 

246 
(* 

247 
lemma declclass_simp[simp]: "declclass (C,m) = C" 

248 
by (simp add: declclass_def) 

249 
*) 

250 

251 
lemma decliface_simp[simp]: "decliface (I,m) = I" 

252 
by (simp add: decliface_def) 

253 

254 
lemma mbr_simp[simp]: "mbr (C,m) = m" 

255 
by (simp add: mbr_def) 

256 

257 
lemma access_mbr_simp [simp]: "(accmodi (mbr m)) = accmodi m" 

258 
by (cases m) (simp add: mbr_def) 

259 

260 
lemma mthd_simp[simp]: "mthd (C,m) = m" 

261 
by (simp add: mthd_def) 

262 

263 
lemma fld_simp[simp]: "fld (C,f) = f" 

264 
by (simp add: fld_def) 

265 

266 
lemma accmodi_simp[simp]: "accmodi (C,m) = access m" 

267 
by (simp ) 

268 

269 
lemma access_mthd_simp [simp]: "(access (mthd m)) = accmodi m" 

270 
by (cases m) (simp add: mthd_def) 

271 

272 
lemma access_fld_simp [simp]: "(access (fld f)) = accmodi f" 

273 
by (cases f) (simp add: fld_def) 

274 

275 
(* 

276 
lemma is_static_simp[simp]: "is_static (C,m) = static m" 

277 
by (simp add: is_static_def) 

278 
*) 

279 

280 
lemma static_mthd_simp[simp]: "static (mthd m) = is_static m" 

281 
by (cases m) (simp add: mthd_def member_is_static_simp) 

282 

283 
lemma mthd_is_static_simp [simp]: "is_static (mthd m) = is_static m" 

284 
by (cases m) simp 

285 

286 
lemma static_fld_simp[simp]: "static (fld f) = is_static f" 

287 
by (cases f) (simp add: fld_def member_is_static_simp) 

288 

289 
lemma ext_field_simp [simp]: "(declclass f,fld f) = f" 

290 
by (cases f) (simp add: fld_def) 

291 

292 
lemma ext_method_simp [simp]: "(declclass m,mthd m) = m" 

293 
by (cases m) (simp add: mthd_def) 

294 

295 
lemma ext_mbr_simp [simp]: "(declclass m,mbr m) = m" 

296 
by (cases m) (simp add: mbr_def) 

297 

298 
lemma fname_simp[simp]:"fname (n,c) = n" 

299 
by (simp add: fname_def) 

300 

301 
lemma declclassf_simp[simp]:"declclassf (n,c) = c" 

302 
by (simp add: declclassf_def) 

303 

304 
constdefs (* some mnemotic selectors for (vname \<times> qtname) *) 

305 
"fldname" :: "(vname \<times> qtname) \<Rightarrow> vname" 

306 
"fldname \<equiv> fst" 

307 

308 
"fldclass" :: "(vname \<times> qtname) \<Rightarrow> qtname" 

309 
"fldclass \<equiv> snd" 

310 

311 
lemma fldname_simp[simp]: "fldname (n,c) = n" 

312 
by (simp add: fldname_def) 

313 

314 
lemma fldclass_simp[simp]: "fldclass (n,c) = c" 

315 
by (simp add: fldclass_def) 

316 

317 
lemma ext_fieldname_simp[simp]: "(fldname f,fldclass f) = f" 

318 
by (simp add: fldname_def fldclass_def) 

319 

320 
text {* Convert a qualified method declaration (qualified with its declaring 

321 
class) to a qualified member declaration: @{text methdMembr} *} 

322 

323 
constdefs 

324 
methdMembr :: "(qtname \<times> mdecl) \<Rightarrow> (qtname \<times> memberdecl)" 

325 
"methdMembr m \<equiv> (fst m,mdecl (snd m))" 

326 

327 
lemma methdMembr_simp[simp]: "methdMembr (c,m) = (c,mdecl m)" 

328 
by (simp add: methdMembr_def) 

329 

330 
lemma accmodi_methdMembr_simp[simp]: "accmodi (methdMembr m) = accmodi m" 

331 
by (cases m) (simp add: methdMembr_def) 

332 

333 
lemma is_static_methdMembr_simp[simp]: "is_static (methdMembr m) = is_static m" 

334 
by (cases m) (simp add: methdMembr_def) 

335 

336 
lemma declclass_methdMembr_simp[simp]: "declclass (methdMembr m) = declclass m" 

337 
by (cases m) (simp add: methdMembr_def) 

338 

339 
text {* Convert a qualified method (qualified with its declaring 

340 
class) to a qualified member declaration: @{text method} *} 

341 

342 
constdefs 

343 
method :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> memberdecl)" 

344 
"method sig m \<equiv> (declclass m, mdecl (sig, mthd m))" 

345 

346 
lemma method_simp[simp]: "method sig (C,m) = (C,mdecl (sig,m))" 

347 
by (simp add: method_def) 

348 

349 
lemma accmodi_method_simp[simp]: "accmodi (method sig m) = accmodi m" 

350 
by (simp add: method_def) 

351 

352 
lemma declclass_method_simp[simp]: "declclass (method sig m) = declclass m" 

353 
by (simp add: method_def) 

354 

355 
lemma is_static_method_simp[simp]: "is_static (method sig m) = is_static m" 

356 
by (cases m) (simp add: method_def) 

357 

358 
lemma mbr_method_simp[simp]: "mbr (method sig m) = mdecl (sig,mthd m)" 

359 
by (simp add: mbr_def method_def) 

360 

361 
lemma memberid_method_simp[simp]: "memberid (method sig m) = mid sig" 

362 
by (simp add: method_def) 

363 

364 
constdefs 

365 
fieldm :: "vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> (qtname \<times> memberdecl)" 

366 
"fieldm n f \<equiv> (declclass f, fdecl (n, fld f))" 

367 

368 
lemma fieldm_simp[simp]: "fieldm n (C,f) = (C,fdecl (n,f))" 

369 
by (simp add: fieldm_def) 

370 

371 
lemma accmodi_fieldm_simp[simp]: "accmodi (fieldm n f) = accmodi f" 

372 
by (simp add: fieldm_def) 

373 

374 
lemma declclass_fieldm_simp[simp]: "declclass (fieldm n f) = declclass f" 

375 
by (simp add: fieldm_def) 

376 

377 
lemma is_static_fieldm_simp[simp]: "is_static (fieldm n f) = is_static f" 

378 
by (cases f) (simp add: fieldm_def) 

379 

380 
lemma mbr_fieldm_simp[simp]: "mbr (fieldm n f) = fdecl (n,fld f)" 

381 
by (simp add: mbr_def fieldm_def) 

382 

383 
lemma memberid_fieldm_simp[simp]: "memberid (fieldm n f) = fid n" 

384 
by (simp add: fieldm_def) 

385 

386 
text {* Select the signature out of a qualified method declaration: 

387 
@{text msig} *} 

388 

389 
constdefs msig:: "(qtname \<times> mdecl) \<Rightarrow> sig" 

390 
"msig m \<equiv> fst (snd m)" 

391 

392 
lemma msig_simp[simp]: "msig (c,(s,m)) = s" 

393 
by (simp add: msig_def) 

394 

395 
text {* Convert a qualified method (qualified with its declaring 

396 
class) to a qualified method declaration: @{text qmdecl} *} 

397 

398 
constdefs qmdecl :: "sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> mdecl)" 

399 
"qmdecl sig m \<equiv> (declclass m, (sig,mthd m))" 

400 

401 
lemma qmdecl_simp[simp]: "qmdecl sig (C,m) = (C,(sig,m))" 

402 
by (simp add: qmdecl_def) 

403 

404 
lemma declclass_qmdecl_simp[simp]: "declclass (qmdecl sig m) = declclass m" 

405 
by (simp add: qmdecl_def) 

406 

407 
lemma accmodi_qmdecl_simp[simp]: "accmodi (qmdecl sig m) = accmodi m" 

408 
by (simp add: qmdecl_def) 

409 

410 
lemma is_static_qmdecl_simp[simp]: "is_static (qmdecl sig m) = is_static m" 

411 
by (cases m) (simp add: qmdecl_def) 

412 

413 
lemma msig_qmdecl_simp[simp]: "msig (qmdecl sig m) = sig" 

414 
by (simp add: qmdecl_def) 

415 

416 
lemma mdecl_qmdecl_simp[simp]: 

417 
"mdecl (mthd (qmdecl sig new)) = mdecl (sig, mthd new)" 

418 
by (simp add: qmdecl_def) 

419 

420 
lemma methdMembr_qmdecl_simp [simp]: 

421 
"methdMembr (qmdecl sig old) = method sig old" 

422 
by (simp add: methdMembr_def qmdecl_def method_def) 

423 

424 
text {* overloaded selector @{text resTy} to select the result type 

425 
out of various HOL types *} 

426 

427 
axclass has_resTy < "type" 

428 
consts resTy:: "'a::has_resTy \<Rightarrow> ty" 

429 

12859  430 
instance access_field_type :: ("type","has_resTy") has_resTy .. 
12854  431 

432 
defs (overloaded) 

433 
decl_resTy_def: 

434 
"resTy (m::('a::has_resTy) decl_scheme) \<equiv> resTy (Decl.decl.more m)" 

435 

12859  436 
instance static_field_type :: ("type","has_resTy") has_resTy .. 
12854  437 

438 
defs (overloaded) 

439 
static_field_type_resTy_def: 

440 
"resTy (m::(bool,'b::has_resTy) static_field_type) 

441 
\<equiv> resTy (static_more m)" 

442 

12859  443 
instance pars_field_type :: ("type","has_resTy") has_resTy .. 
12854  444 

445 
defs (overloaded) 

446 
pars_field_type_resTy_def: 

447 
"resTy (m::(vname list,'b::has_resTy) pars_field_type) 

448 
\<equiv> resTy (pars_more m)" 

449 

12859  450 
instance resT_field_type :: ("type","type") has_resTy .. 
12854  451 

452 
defs (overloaded) 

453 
resT_field_type_resTy_def: 

454 
"resTy (m::(ty,'b::type) resT_field_type) 

455 
\<equiv> resT_val m" 

456 

457 
lemma mhead_resTy_simp: "resTy (m::'a mhead_scheme) = resT m" 

458 
apply (cases m) 

459 
apply (simp add: decl_resTy_def static_field_type_resTy_def 

460 
pars_field_type_resTy_def resT_field_type_resTy_def 

461 
member.dest_convs mhead.dest_convs) 

462 
done 

463 

464 
lemma resTy_mhead [simp]:"resTy (mhead m) = resTy m" 

465 
by (simp add: mhead_def mhead_resTy_simp) 

466 

12859  467 
instance * :: ("type","has_resTy") has_resTy .. 
12854  468 

469 
defs (overloaded) 

470 
pair_resTy_def: "resTy p \<equiv> resTy (snd p)" 

471 

472 
lemma pair_resTy_simp[simp]: "resTy (x,m) = resTy m" 

473 
by (simp add: pair_resTy_def) 

474 

475 
lemma qmdecl_resTy_simp [simp]: "resTy (qmdecl sig m) = resTy m" 

476 
by (cases m) (simp) 

477 

478 
lemma resTy_mthd [simp]:"resTy (mthd m) = resTy m" 

479 
by (cases m) (simp add: mthd_def ) 

480 

481 
subsubsection "inheritablein" 

482 
text {* 

483 
@{text "G\<turnstile>m inheritable_in P"}: m can be inherited by 

484 
classes in package P if: 

485 
\begin{itemize} 

486 
\item the declaration class of m is accessible in P and 

487 
\item the member m is declared with protected or public access or if it is 

488 
declared with default (package) access, the package of the declaration 

489 
class of m is also P. If the member m is declared with private access 

490 
it is not accessible for inheritance at all. 

491 
\end{itemize} 

492 
*} 

493 
constdefs 

494 
inheritable_in:: 

495 
"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> pname \<Rightarrow> bool" 

496 
("_ \<turnstile> _ inheritable'_in _" [61,61,61] 60) 

497 
"G\<turnstile>membr inheritable_in pack 

498 
\<equiv> (case (accmodi membr) of 

499 
Private \<Rightarrow> False 

500 
 Package \<Rightarrow> (pid (declclass membr)) = pack 

501 
 Protected \<Rightarrow> True 

502 
 Public \<Rightarrow> True)" 

503 

504 
syntax 

505 
Method_inheritable_in:: 

506 
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> pname \<Rightarrow> bool" 

507 
("_ \<turnstile>Method _ inheritable'_in _ " [61,61,61] 60) 

508 

509 
translations 

510 
"G\<turnstile>Method m inheritable_in p" == "G\<turnstile>methdMembr m inheritable_in p" 

511 

512 
syntax 

513 
Methd_inheritable_in:: 

514 
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> pname \<Rightarrow> bool" 

515 
("_ \<turnstile>Methd _ _ inheritable'_in _ " [61,61,61,61] 60) 

516 

517 
translations 

518 
"G\<turnstile>Methd s m inheritable_in p" == "G\<turnstile>(method s m) inheritable_in p" 

519 

520 
subsubsection "declaredin/undeclaredin" 

521 

522 
constdefs cdeclaredmethd:: "prog \<Rightarrow> qtname \<Rightarrow> (sig,methd) table" 

523 
"cdeclaredmethd G C 

524 
\<equiv> (case class G C of 

525 
None \<Rightarrow> \<lambda> sig. None 

526 
 Some c \<Rightarrow> table_of (methods c) 

527 
)" 

528 

529 
constdefs 

530 
cdeclaredfield:: "prog \<Rightarrow> qtname \<Rightarrow> (vname,field) table" 

531 
"cdeclaredfield G C 

532 
\<equiv> (case class G C of 

533 
None \<Rightarrow> \<lambda> sig. None 

534 
 Some c \<Rightarrow> table_of (cfields c) 

535 
)" 

536 

537 

538 
constdefs 

539 
declared_in:: "prog \<Rightarrow> memberdecl \<Rightarrow> qtname \<Rightarrow> bool" 

540 
("_\<turnstile> _ declared'_in _" [61,61,61] 60) 

541 
"G\<turnstile>m declared_in C \<equiv> (case m of 

542 
fdecl (fn,f ) \<Rightarrow> cdeclaredfield G C fn = Some f 

543 
 mdecl (sig,m) \<Rightarrow> cdeclaredmethd G C sig = Some m)" 

544 

545 
syntax 

546 
method_declared_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool" 

547 
("_\<turnstile>Method _ declared'_in _" [61,61,61] 60) 

548 
translations 

549 
"G\<turnstile>Method m declared_in C" == "G\<turnstile>mdecl (mthd m) declared_in C" 

550 

551 
syntax 

552 
methd_declared_in:: "prog \<Rightarrow> sig \<Rightarrow>(qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool" 

553 
("_\<turnstile>Methd _ _ declared'_in _" [61,61,61,61] 60) 

554 
translations 

555 
"G\<turnstile>Methd s m declared_in C" == "G\<turnstile>mdecl (s,mthd m) declared_in C" 

556 

557 
lemma declared_in_classD: 

558 
"G\<turnstile>m declared_in C \<Longrightarrow> is_class G C" 

559 
by (cases m) 

560 
(auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def) 

561 

562 
constdefs 

563 
undeclared_in:: "prog \<Rightarrow> memberid \<Rightarrow> qtname \<Rightarrow> bool" 

564 
("_\<turnstile> _ undeclared'_in _" [61,61,61] 60) 

565 

566 
"G\<turnstile>m undeclared_in C \<equiv> (case m of 

567 
fid fn \<Rightarrow> cdeclaredfield G C fn = None 

568 
 mid sig \<Rightarrow> cdeclaredmethd G C sig = None)" 

569 

570 
lemma method_declared_inI: 

571 
"\<lbrakk>class G C = Some c; table_of (methods c) sig = Some m\<rbrakk> 

572 
\<Longrightarrow> G\<turnstile>mdecl (sig,m) declared_in C" 

573 
by (auto simp add: declared_in_def cdeclaredmethd_def) 

574 

575 

576 
subsubsection "members" 

577 

578 
consts 

579 
members:: "prog \<Rightarrow> (qtname \<times> (qtname \<times> memberdecl)) set" 

580 
(* Can't just take a function: prog \<Rightarrow> qtname \<Rightarrow> memberdecl set because 

581 
the class qtname changes to the superclass in the inductive definition 

582 
below 

583 
*) 

584 

585 
syntax 

586 
member_of:: "prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" 

587 
("_ \<turnstile> _ member'_of _" [61,61,61] 60) 

588 

589 
translations 

590 
"G\<turnstile>m member_of C" \<rightleftharpoons> "(C,m) \<in> members G" 

591 

592 
inductive "members G" intros 

593 

594 
Immediate: "\<lbrakk>G\<turnstile>mbr m declared_in C;declclass m = C\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C" 

595 
Inherited: "\<lbrakk>G\<turnstile>m inheritable_in (pid C); G\<turnstile>memberid m undeclared_in C; 

596 
G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S; G\<turnstile>(Class S) accessible_in (pid C);G\<turnstile>m member_of S 

597 
\<rbrakk> \<Longrightarrow> G\<turnstile>m member_of C" 

598 
text {* Note that in the case of an inherited member only the members of the 

599 
direct superclass are concerned. If a member of a superclass of the direct 

600 
superclass isn't inherited in the direct superclass (not member of the 

601 
direct superclass) than it can't be a member of the class. E.g. If a 

602 
member of a class A is defined with package access it isn't member of a 

603 
subclass S if S isn't in the same package as A. Any further subclasses 

604 
of S will not inherit the member, regardless if they are in the same 

605 
package as A or not.*} 

606 

607 
syntax 

608 
method_member_of:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool" 

609 
("_ \<turnstile>Method _ member'_of _" [61,61,61] 60) 

610 

611 
translations 

612 
"G\<turnstile>Method m member_of C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_of C" 

613 

614 
syntax 

615 
methd_member_of:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool" 

616 
("_ \<turnstile>Methd _ _ member'_of _" [61,61,61,61] 60) 

617 

618 
translations 

619 
"G\<turnstile>Methd s m member_of C" \<rightleftharpoons> "G\<turnstile>(method s m) member_of C" 

620 

621 
syntax 

622 
fieldm_member_of:: "prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> bool" 

623 
("_ \<turnstile>Field _ _ member'_of _" [61,61,61] 60) 

624 

625 
translations 

626 
"G\<turnstile>Field n f member_of C" \<rightleftharpoons> "G\<turnstile>fieldm n f member_of C" 

627 

628 
constdefs 

629 
inherits:: "prog \<Rightarrow> qtname \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> bool" 

630 
("_ \<turnstile> _ inherits _" [61,61,61] 60) 

631 
"G\<turnstile>C inherits m 

632 
\<equiv> G\<turnstile>m inheritable_in (pid C) \<and> G\<turnstile>memberid m undeclared_in C \<and> 

633 
(\<exists> S. G\<turnstile>C \<prec>\<^sub>C\<^sub>1 S \<and> G\<turnstile>(Class S) accessible_in (pid C) \<and> G\<turnstile>m member_of S)" 

634 

635 
lemma inherits_member: "G\<turnstile>C inherits m \<Longrightarrow> G\<turnstile>m member_of C" 

636 
by (auto simp add: inherits_def intro: members.Inherited) 

637 

638 

639 
constdefs member_in::"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> bool" 

640 
("_ \<turnstile> _ member'_in _" [61,61,61] 60) 

641 
"G\<turnstile>m member_in C \<equiv> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC" 

642 
text {* A member is in a class if it is member of the class or a superclass. 

643 
If a member is in a class we can select this member. This additional notion 

644 
is necessary since not all members are inherited to subclasses. So such 

645 
members are not memberof the subclass but memberin the subclass.*} 

646 

647 
syntax 

648 
method_member_in:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> bool" 

649 
("_ \<turnstile>Method _ member'_in _" [61,61,61] 60) 

650 

651 
translations 

652 
"G\<turnstile>Method m member_in C" \<rightleftharpoons> "G\<turnstile>(methdMembr m) member_in C" 

653 

654 
syntax 

655 
methd_member_in:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> bool" 

656 
("_ \<turnstile>Methd _ _ member'_in _" [61,61,61,61] 60) 

657 

658 
translations 

659 
"G\<turnstile>Methd s m member_in C" \<rightleftharpoons> "G\<turnstile>(method s m) member_in C" 

660 

661 
consts stat_overridesR:: 

662 
"prog \<Rightarrow> ((qtname \<times> mdecl) \<times> (qtname \<times> mdecl)) set" 

663 

664 
lemma member_inD: "G\<turnstile>m member_in C 

665 
\<Longrightarrow> \<exists> provC. G\<turnstile> C \<preceq>\<^sub>C provC \<and> G \<turnstile> m member_of provC" 

666 
by (auto simp add: member_in_def) 

667 

668 
lemma member_inI: "\<lbrakk>G \<turnstile> m member_of provC;G\<turnstile> C \<preceq>\<^sub>C provC\<rbrakk> \<Longrightarrow> G\<turnstile>m member_in C" 

669 
by (auto simp add: member_in_def) 

670 

671 
lemma member_of_to_member_in: "G \<turnstile> m member_of C \<Longrightarrow> G \<turnstile>m member_in C" 

672 
by (auto intro: member_inI) 

673 

674 

675 
subsubsection "overriding" 

676 

677 
text {* Unfortunately the static notion of overriding (used during the 

678 
typecheck of the compiler) and the dynamic notion of overriding (used during 

679 
execution in the JVM) are not exactly the same. 

680 
*} 

681 

682 
text {* Static overriding (used during the typecheck of the compiler) *} 

683 
syntax 

684 
stat_overrides:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 

685 
("_ \<turnstile> _ overrides\<^sub>S _" [61,61,61] 60) 

686 
translations 

687 
"G\<turnstile>new overrides\<^sub>S old" == "(new,old) \<in> stat_overridesR G " 

688 

689 
inductive "stat_overridesR G" intros 

690 

691 
Direct: "\<lbrakk>\<not> is_static new; msig new = msig old; 

692 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old); 

693 
G\<turnstile>Method new declared_in (declclass new); 

694 
G\<turnstile>Method old declared_in (declclass old); 

695 
G\<turnstile>Method old inheritable_in pid (declclass new); 

696 
G\<turnstile>(declclass new) \<prec>\<^sub>C\<^sub>1 superNew; 

697 
G \<turnstile>Method old member_of superNew 

698 
\<rbrakk> \<Longrightarrow> G\<turnstile>new overrides\<^sub>S old" 

699 

700 
Indirect: "\<lbrakk>G\<turnstile>new overrides\<^sub>S inter; G\<turnstile>inter overrides\<^sub>S old\<rbrakk> 

701 
\<Longrightarrow> G\<turnstile>new overrides\<^sub>S old" 

702 

703 
text {* Dynamic overriding (used during the typecheck of the compiler) *} 

704 
consts overridesR:: 

705 
"prog \<Rightarrow> ((qtname \<times> mdecl) \<times> (qtname \<times> mdecl)) set" 

706 

707 

708 
overrides:: "prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 

709 
("_ \<turnstile> _ overrides _" [61,61,61] 60) 

710 
translations 

711 
"G\<turnstile>new overrides old" == "(new,old) \<in> overridesR G " 

712 

713 
inductive "overridesR G" intros 

714 

715 
Direct: "\<lbrakk>\<not> is_static new; \<not> is_static old; accmodi new \<noteq> Private; 

716 
msig new = msig old; 

717 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old); 

718 
G\<turnstile>Method new declared_in (declclass new); 

719 
G\<turnstile>Method old declared_in (declclass old); 

720 
G\<turnstile>Method old inheritable_in pid (declclass new); 

721 
G\<turnstile>resTy new \<preceq> resTy old 

722 
\<rbrakk> \<Longrightarrow> G\<turnstile>new overrides old" 

723 

724 
Indirect: "\<lbrakk>G\<turnstile>new overrides inter; G\<turnstile>inter overrides old\<rbrakk> 

725 
\<Longrightarrow> G\<turnstile>new overrides old" 

726 

727 
syntax 

728 
sig_stat_overrides:: 

729 
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 

730 
("_,_\<turnstile> _ overrides\<^sub>S _" [61,61,61,61] 60) 

731 
translations 

732 
"G,s\<turnstile>new overrides\<^sub>S old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides\<^sub>S (qmdecl s old)" 

733 

734 
syntax 

735 
sig_overrides:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 

736 
("_,_\<turnstile> _ overrides _" [61,61,61,61] 60) 

737 
translations 

738 
"G,s\<turnstile>new overrides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) overrides (qmdecl s old)" 

739 

740 
subsubsection "Hiding" 

741 

742 
constdefs hides:: 

743 
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 

744 
("_\<turnstile> _ hides _" [61,61,61] 60) 

745 
"G\<turnstile>new hides old 

746 
\<equiv> is_static new \<and> msig new = msig old \<and> 

747 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> 

748 
G\<turnstile>Method new declared_in (declclass new) \<and> 

749 
G\<turnstile>Method old declared_in (declclass old) \<and> 

750 
G\<turnstile>Method old inheritable_in pid (declclass new)" 

751 

752 
syntax 

753 
sig_hides:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> bool" 

754 
("_,_\<turnstile> _ hides _" [61,61,61,61] 60) 

755 
translations 

756 
"G,s\<turnstile>new hides old" \<rightharpoonup> "G\<turnstile>(qmdecl s new) hides (qmdecl s old)" 

757 

758 
lemma hidesI: 

759 
"\<lbrakk>is_static new; msig new = msig old; 

760 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old); 

761 
G\<turnstile>Method new declared_in (declclass new); 

762 
G\<turnstile>Method old declared_in (declclass old); 

763 
G\<turnstile>Method old inheritable_in pid (declclass new) 

764 
\<rbrakk> \<Longrightarrow> G\<turnstile>new hides old" 

765 
by (auto simp add: hides_def) 

766 

767 
lemma hidesD: 

768 
"\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow> 

769 
declclass new \<noteq> Object \<and> is_static new \<and> msig new = msig old \<and> 

770 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> 

771 
G\<turnstile>Method new declared_in (declclass new) \<and> 

772 
G\<turnstile>Method old declared_in (declclass old)" 

773 
by (auto simp add: hides_def) 

774 

775 
lemma overrides_commonD: 

776 
"\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> 

777 
declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and> 

778 
accmodi new \<noteq> Private \<and> 

779 
msig new = msig old \<and> 

780 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> 

781 
G\<turnstile>Method new declared_in (declclass new) \<and> 

782 
G\<turnstile>Method old declared_in (declclass old)" 

783 
by (induct set: overridesR) (auto intro: trancl_trans) 

784 

785 
lemma ws_overrides_commonD: 

786 
"\<lbrakk>G\<turnstile>new overrides old;ws_prog G\<rbrakk> \<Longrightarrow> 

787 
declclass new \<noteq> Object \<and> \<not> is_static new \<and> \<not> is_static old \<and> 

788 
accmodi new \<noteq> Private \<and> G\<turnstile>resTy new \<preceq> resTy old \<and> 

789 
msig new = msig old \<and> 

790 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> 

791 
G\<turnstile>Method new declared_in (declclass new) \<and> 

792 
G\<turnstile>Method old declared_in (declclass old)" 

793 
by (induct set: overridesR) (auto intro: trancl_trans ws_widen_trans) 

794 

795 
lemma stat_overrides_commonD: 

796 
"\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> 

797 
declclass new \<noteq> Object \<and> \<not> is_static new \<and> msig new = msig old \<and> 

798 
G\<turnstile>(declclass new) \<prec>\<^sub>C (declclass old) \<and> 

799 
G\<turnstile>Method new declared_in (declclass new) \<and> 

800 
G\<turnstile>Method old declared_in (declclass old)" 

801 
by (induct set: stat_overridesR) (auto intro: trancl_trans) 

802 

803 
lemma overrides_eq_sigD: 

804 
"\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> msig old=msig new" 

805 
by (auto dest: overrides_commonD) 

806 

807 
lemma hides_eq_sigD: 

808 
"\<lbrakk>G\<turnstile>new hides old\<rbrakk> \<Longrightarrow> msig old=msig new" 

809 
by (auto simp add: hides_def) 

810 

811 
subsubsection "permits access" 

812 
constdefs 

813 
permits_acc:: 

814 
"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

815 
("_ \<turnstile> _ in _ permits'_acc'_to _" [61,61,61,61] 60) 

816 

817 
"G\<turnstile>membr in class permits_acc_to accclass 

818 
\<equiv> (case (accmodi membr) of 

819 
Private \<Rightarrow> (declclass membr = accclass) 

820 
 Package \<Rightarrow> (pid (declclass membr) = pid accclass) 

821 
 Protected \<Rightarrow> (pid (declclass membr) = pid accclass) 

822 
\<or> 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

823 
(G\<turnstile>accclass \<prec>\<^sub>C declclass membr 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

824 
\<and> (G\<turnstile>class \<preceq>\<^sub>C accclass \<or> is_static membr)) 
12854  825 
 Public \<Rightarrow> True)" 
826 
text {* 

827 
The subcondition of the @{term "Protected"} case: 

828 
@{term "G\<turnstile>accclass \<prec>\<^sub>C declclass membr"} could also be relaxed to: 

829 
@{term "G\<turnstile>accclass \<preceq>\<^sub>C declclass membr"} since in case both classes are the 

830 
same the other condition @{term "(pid (declclass membr) = pid accclass)"} 

831 
holds anyway. 

832 
*} 

833 

834 
text {* Like in case of overriding, the static and dynamic accessibility 

835 
of members is not uniform. 

836 
\begin{itemize} 

837 
\item Statically the class/interface of the member must be accessible for the 

838 
member to be accessible. During runtime this is not necessary. For 

839 
Example, if a class is accessible and we are allowed to access a member 

840 
of this class (statically) we expect that we can access this member in 

841 
an arbitrary subclass (during runtime). It's not intended to restrict 

842 
the access to accessible subclasses during runtime. 

843 
\item Statically the member we want to access must be "member of" the class. 

844 
Dynamically it must only be "member in" the class. 

845 
\end{itemize} 

846 
*} 

847 

848 

849 
consts 

850 
accessible_fromR:: 

851 
"prog \<Rightarrow> qtname \<Rightarrow> ((qtname \<times> memberdecl) \<times> qtname) set" 

852 

853 
syntax 

854 
accessible_from:: 

855 
"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

856 
("_ \<turnstile> _ of _ accessible'_from _" [61,61,61,61] 60) 

857 

858 
translations 

859 
"G\<turnstile>membr of cls accessible_from accclass" 

860 
\<rightleftharpoons> "(membr,cls) \<in> accessible_fromR G accclass" 

861 

862 
syntax 

863 
method_accessible_from:: 

864 
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

865 
("_ \<turnstile>Method _ of _ accessible'_from _" [61,61,61,61] 60) 

866 

867 
translations 

868 
"G\<turnstile>Method m of cls accessible_from accclass" 

869 
\<rightleftharpoons> "G\<turnstile>methdMembr m of cls accessible_from accclass" 

870 

871 
syntax 

872 
methd_accessible_from:: 

873 
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

874 
("_ \<turnstile>Methd _ _ of _ accessible'_from _" [61,61,61,61,61] 60) 

875 

876 
translations 

877 
"G\<turnstile>Methd s m of cls accessible_from accclass" 

878 
\<rightleftharpoons> "G\<turnstile>(method s m) of cls accessible_from accclass" 

879 

880 
syntax 

881 
field_accessible_from:: 

882 
"prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

883 
("_ \<turnstile>Field _ _ of _ accessible'_from _" [61,61,61,61,61] 60) 

884 

885 
translations 

886 
"G\<turnstile>Field fn f of C accessible_from accclass" 

887 
\<rightleftharpoons> "G\<turnstile>(fieldm fn f) of C accessible_from accclass" 

888 

889 
inductive "accessible_fromR G accclass" intros 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

890 
Immediate: "\<lbrakk>G\<turnstile>membr member_of class; 
12854  891 
G\<turnstile>(Class class) accessible_in (pid accclass); 
892 
G\<turnstile>membr in class permits_acc_to accclass 

893 
\<rbrakk> \<Longrightarrow> G\<turnstile>membr of class accessible_from accclass" 

894 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

895 
Overriding: "\<lbrakk>G\<turnstile>membr member_of class; 
12854  896 
G\<turnstile>(Class class) accessible_in (pid accclass); 
897 
membr=(C,mdecl new); 

898 
G\<turnstile>(C,new) overrides\<^sub>S old; 

899 
G\<turnstile>class \<prec>\<^sub>C sup; 

900 
G\<turnstile>Method old of sup accessible_from accclass 

901 
\<rbrakk>\<Longrightarrow> G\<turnstile>membr of class accessible_from accclass" 

902 

903 
consts 

904 
dyn_accessible_fromR:: 

905 
"prog \<Rightarrow> qtname \<Rightarrow> ((qtname \<times> memberdecl) \<times> qtname) set" 

906 

907 
syntax 

908 
dyn_accessible_from:: 

909 
"prog \<Rightarrow> (qtname \<times> memberdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

910 
("_ \<turnstile> _ in _ dyn'_accessible'_from _" [61,61,61,61] 60) 

911 

912 
translations 

913 
"G\<turnstile>membr in C dyn_accessible_from accC" 

914 
\<rightleftharpoons> "(membr,C) \<in> dyn_accessible_fromR G accC" 

915 

916 
syntax 

917 
method_dyn_accessible_from:: 

918 
"prog \<Rightarrow> (qtname \<times> mdecl) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

919 
("_ \<turnstile>Method _ in _ dyn'_accessible'_from _" [61,61,61,61] 60) 

920 

921 
translations 

922 
"G\<turnstile>Method m in C dyn_accessible_from accC" 

923 
\<rightleftharpoons> "G\<turnstile>methdMembr m in C dyn_accessible_from accC" 

924 

925 
syntax 

926 
methd_dyn_accessible_from:: 

927 
"prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

928 
("_ \<turnstile>Methd _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60) 

929 

930 
translations 

931 
"G\<turnstile>Methd s m in C dyn_accessible_from accC" 

932 
\<rightleftharpoons> "G\<turnstile>(method s m) in C dyn_accessible_from accC" 

933 

934 
syntax 

935 
field_dyn_accessible_from:: 

936 
"prog \<Rightarrow> vname \<Rightarrow> (qtname \<times> field) \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> bool" 

937 
("_ \<turnstile>Field _ _ in _ dyn'_accessible'_from _" [61,61,61,61,61] 60) 

938 

939 
translations 

940 
"G\<turnstile>Field fn f in dynC dyn_accessible_from accC" 

941 
\<rightleftharpoons> "G\<turnstile>(fieldm fn f) in dynC dyn_accessible_from accC" 

942 

943 
inductive "dyn_accessible_fromR G accclass" intros 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

944 
Immediate: "\<lbrakk>G\<turnstile>membr member_in class; 
12854  945 
G\<turnstile>membr in class permits_acc_to accclass 
946 
\<rbrakk> \<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass" 

947 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

948 
Overriding: "\<lbrakk>G\<turnstile>membr member_in class; 
12854  949 
membr=(C,mdecl new); 
950 
G\<turnstile>(C,new) overrides old; 

951 
G\<turnstile>class \<prec>\<^sub>C sup; 

952 
G\<turnstile>Method old in sup dyn_accessible_from accclass 

953 
\<rbrakk>\<Longrightarrow> G\<turnstile>membr in class dyn_accessible_from accclass" 

954 

955 

956 
lemma accessible_from_commonD: "G\<turnstile>m of C accessible_from S 

957 
\<Longrightarrow> G\<turnstile>m member_of C \<and> G\<turnstile>(Class C) accessible_in (pid S)" 

958 
by (auto elim: accessible_fromR.induct) 

959 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

960 
lemma unique_declaration: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

961 
"\<lbrakk>G\<turnstile>m declared_in C; G\<turnstile>n declared_in C; memberid m = memberid n \<rbrakk> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

962 
\<Longrightarrow> m = n" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

963 
apply (cases m) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

964 
apply (cases n, 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

965 
auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def)+ 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

966 
done 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

967 

12854  968 
lemma declared_not_undeclared: 
969 
"G\<turnstile>m declared_in C \<Longrightarrow> \<not> G\<turnstile> memberid m undeclared_in C" 

970 
by (cases m) (auto simp add: declared_in_def undeclared_in_def) 

971 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

972 
lemma undeclared_not_declared: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

973 
"G\<turnstile> memberid m undeclared_in C \<Longrightarrow> \<not> G\<turnstile> m declared_in C" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

974 
by (cases m) (auto simp add: declared_in_def undeclared_in_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

975 

12854  976 
lemma not_undeclared_declared: 
977 
"\<not> G\<turnstile> membr_id undeclared_in C \<Longrightarrow> (\<exists> m. G\<turnstile>m declared_in C \<and> 

978 
membr_id = memberid m)" 

979 
proof  

980 
assume not_undecl:"\<not> G\<turnstile> membr_id undeclared_in C" 

981 
show ?thesis (is "?P membr_id") 

982 
proof (cases membr_id) 

983 
case (fid vname) 

984 
with not_undecl 

985 
obtain fld where 

986 
"G\<turnstile>fdecl (vname,fld) declared_in C" 

987 
by (auto simp add: undeclared_in_def declared_in_def 

988 
cdeclaredfield_def) 

989 
with fid show ?thesis 

990 
by auto 

991 
next 

992 
case (mid sig) 

993 
with not_undecl 

994 
obtain mthd where 

995 
"G\<turnstile>mdecl (sig,mthd) declared_in C" 

996 
by (auto simp add: undeclared_in_def declared_in_def 

997 
cdeclaredmethd_def) 

998 
with mid show ?thesis 

999 
by auto 

1000 
qed 

1001 
qed 

1002 

1003 
lemma unique_declared_in: 

1004 
"\<lbrakk>G\<turnstile>m declared_in C; G\<turnstile>n declared_in C; memberid m = memberid n\<rbrakk> 

1005 
\<Longrightarrow> m = n" 

1006 
by (auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def 

1007 
split: memberdecl.splits) 

1008 

1009 
lemma unique_member_of: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1010 
assumes n: "G\<turnstile>n member_of C" and 
12854  1011 
m: "G\<turnstile>m member_of C" and 
1012 
eqid: "memberid n = memberid m" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1013 
shows "n=m" 
12854  1014 
proof  
1015 
from n m eqid 

1016 
show "n=m" 

1017 
proof (induct) 

1018 
case (Immediate C n) 

1019 
assume member_n: "G\<turnstile> mbr n declared_in C" "declclass n = C" 

1020 
assume eqid: "memberid n = memberid m" 

1021 
assume "G \<turnstile> m member_of C" 

1022 
then show "n=m" 

1023 
proof (cases) 

1024 
case (Immediate _ m') 

1025 
with eqid 

1026 
have "m=m'" 

1027 
"memberid n = memberid m" 

1028 
"G\<turnstile> mbr m declared_in C" 

1029 
"declclass m = C" 

1030 
by auto 

1031 
with member_n 

1032 
show ?thesis 

1033 
by (cases n, cases m) 

1034 
(auto simp add: declared_in_def 

1035 
cdeclaredmethd_def cdeclaredfield_def 

1036 
split: memberdecl.splits) 

1037 
next 

1038 
case (Inherited _ _ m') 

1039 
then have "G\<turnstile> memberid m undeclared_in C" 

1040 
by simp 

1041 
with eqid member_n 

1042 
show ?thesis 

1043 
by (cases n) (auto dest: declared_not_undeclared) 

1044 
qed 

1045 
next 

1046 
case (Inherited C S n) 

1047 
assume undecl: "G\<turnstile> memberid n undeclared_in C" 

1048 
assume super: "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S" 

1049 
assume hyp: "\<lbrakk>G \<turnstile> m member_of S; memberid n = memberid m\<rbrakk> \<Longrightarrow> n = m" 

1050 
assume eqid: "memberid n = memberid m" 

1051 
assume "G \<turnstile> m member_of C" 

1052 
then show "n=m" 

1053 
proof (cases) 

1054 
case Immediate 

1055 
then have "G\<turnstile> mbr m declared_in C" by simp 

1056 
with eqid undecl 

1057 
show ?thesis 

1058 
by (cases m) (auto dest: declared_not_undeclared) 

1059 
next 

1060 
case Inherited 

1061 
with super have "G \<turnstile> m member_of S" 

1062 
by (auto dest!: subcls1D) 

1063 
with eqid hyp 

1064 
show ?thesis 

1065 
by blast 

1066 
qed 

1067 
qed 

1068 
qed 

1069 

1070 
lemma member_of_is_classD: "G\<turnstile>m member_of C \<Longrightarrow> is_class G C" 

1071 
proof (induct set: members) 

1072 
case (Immediate C m) 

1073 
assume "G\<turnstile> mbr m declared_in C" 

1074 
then show "is_class G C" 

1075 
by (cases "mbr m") 

1076 
(auto simp add: declared_in_def cdeclaredmethd_def cdeclaredfield_def) 

1077 
next 

1078 
case (Inherited C S m) 

1079 
assume "G\<turnstile>C\<prec>\<^sub>C\<^sub>1S" and "is_class G S" 

1080 
then show "is_class G C" 

1081 
by  (rule subcls_is_class2,auto) 

1082 
qed 

1083 

1084 
lemma member_of_declC: 

1085 
"G\<turnstile>m member_of C 

1086 
\<Longrightarrow> G\<turnstile>mbr m declared_in (declclass m)" 

1087 
by (induct set: members) auto 

1088 

1089 
lemma member_of_member_of_declC: 

1090 
"G\<turnstile>m member_of C 

1091 
\<Longrightarrow> G\<turnstile>m member_of (declclass m)" 

1092 
by (auto dest: member_of_declC intro: members.Immediate) 

1093 

1094 
lemma member_of_class_relation: 

1095 
"G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m" 

1096 
proof (induct set: members) 

1097 
case (Immediate C m) 

1098 
then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" by simp 

1099 
next 

1100 
case (Inherited C S m) 

1101 
then show "G\<turnstile>C \<preceq>\<^sub>C declclass m" 

1102 
by (auto dest: r_into_rtrancl intro: rtrancl_trans) 

1103 
qed 

1104 

1105 
lemma member_in_class_relation: 

1106 
"G\<turnstile>m member_in C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m" 

1107 
by (auto dest: member_inD member_of_class_relation 

1108 
intro: rtrancl_trans) 

1109 

1110 
lemma member_of_Package: 

1111 
"\<lbrakk>G\<turnstile>m member_of C; accmodi m = Package\<rbrakk> 

1112 
\<Longrightarrow> pid (declclass m) = pid C" 

1113 
proof  

1114 
assume member: "G\<turnstile>m member_of C" 

1115 
then show " accmodi m = Package \<Longrightarrow> ?thesis" (is "PROP ?P m C") 

1116 
proof (induct rule: members.induct) 

1117 
fix C m 

1118 
assume C: "declclass m = C" 

1119 
then show "pid (declclass m) = pid C" 

1120 
by simp 

1121 
next 

1122 
fix C S m 

1123 
assume inheritable: "G \<turnstile> m inheritable_in pid C" 

1124 
assume hyp: "PROP ?P m S" and 

1125 
package_acc: "accmodi m = Package" 

1126 
with inheritable package_acc hyp 

1127 
show "pid (declclass m) = pid C" 

1128 
by (auto simp add: inheritable_in_def) 

1129 
qed 

1130 
qed 

1131 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1132 
lemma member_in_declC: "G\<turnstile>m member_in C\<Longrightarrow> G\<turnstile>m member_in (declclass m)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1133 
proof  
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1134 
assume member_in_C: "G\<turnstile>m member_in C" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1135 
from member_in_C 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1136 
obtain provC where 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1137 
subclseq_C_provC: "G\<turnstile> C \<preceq>\<^sub>C provC" and 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1138 
member_of_provC: "G \<turnstile> m member_of provC" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1139 
by (auto simp add: member_in_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1140 
from member_of_provC 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1141 
have "G \<turnstile> m member_of declclass m" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1142 
by (rule member_of_member_of_declC) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1143 
moreover 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1144 
from member_in_C 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1145 
have "G\<turnstile>C \<preceq>\<^sub>C declclass m" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1146 
by (rule member_in_class_relation) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1147 
ultimately 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1148 
show ?thesis 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1149 
by (auto simp add: member_in_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1150 
qed 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1151 

12854  1152 
lemma dyn_accessible_from_commonD: "G\<turnstile>m in C dyn_accessible_from S 
1153 
\<Longrightarrow> G\<turnstile>m member_in C" 

1154 
by (auto elim: dyn_accessible_fromR.induct) 

1155 

1156 
lemma no_Private_stat_override: 

1157 
"\<lbrakk>G\<turnstile>new overrides\<^sub>S old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private" 

1158 
by (induct set: stat_overridesR) (auto simp add: inheritable_in_def) 

1159 

1160 
lemma no_Private_override: "\<lbrakk>G\<turnstile>new overrides old\<rbrakk> \<Longrightarrow> accmodi old \<noteq> Private" 

1161 
by (induct set: overridesR) (auto simp add: inheritable_in_def) 

1162 

1163 
lemma permits_acc_inheritance: 

1164 
"\<lbrakk>G\<turnstile>m in statC permits_acc_to accC; G\<turnstile>dynC \<preceq>\<^sub>C statC 

1165 
\<rbrakk> \<Longrightarrow> G\<turnstile>m in dynC permits_acc_to accC" 

1166 
by (cases "accmodi m") 

1167 
(auto simp add: permits_acc_def 

1168 
intro: subclseq_trans) 

1169 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1170 
lemma permits_acc_static_declC: 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1171 
"\<lbrakk>G\<turnstile>m in C permits_acc_to accC; G\<turnstile>m member_in C; is_static m 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1172 
\<rbrakk> \<Longrightarrow> G\<turnstile>m in (declclass m) permits_acc_to accC" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1173 
by (cases "accmodi m") (auto simp add: permits_acc_def) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1174 

99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1175 
lemma dyn_accessible_from_static_declC: 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1176 
assumes acc_C: "G\<turnstile>m in C dyn_accessible_from accC" and 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1177 
static: "is_static m" 
12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1178 
shows "G\<turnstile>m in (declclass m) dyn_accessible_from accC" 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1179 
proof  
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1180 
from acc_C static 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1181 
show "G\<turnstile>m in (declclass m) dyn_accessible_from accC" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1182 
proof (induct) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1183 
case (Immediate C m) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1184 
then show ?case 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1185 
by (auto intro!: dyn_accessible_fromR.Immediate 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1186 
dest: member_in_declC permits_acc_static_declC) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1187 
next 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1188 
case (Overriding declCNew C m new old sup) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1189 
then have "\<not> is_static m" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1190 
by (auto dest: overrides_commonD) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1191 
moreover 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1192 
assume "is_static m" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1193 
ultimately show ?case 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1194 
by contradiction 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1195 
qed 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1196 
qed 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1197 

12854  1198 
lemma field_accessible_fromD: 
1199 
"\<lbrakk>G\<turnstile>membr of C accessible_from accC;is_field membr\<rbrakk> 

1200 
\<Longrightarrow> G\<turnstile>membr member_of C \<and> 

1201 
G\<turnstile>(Class C) accessible_in (pid accC) \<and> 

1202 
G\<turnstile>membr in C permits_acc_to accC" 

1203 
by (cases set: accessible_fromR) 

1204 
(auto simp add: is_field_def split: memberdecl.splits) 

1205 

1206 
lemma field_accessible_from_permits_acc_inheritance: 

1207 
"\<lbrakk>G\<turnstile>membr of statC accessible_from accC; is_field membr; G \<turnstile> dynC \<preceq>\<^sub>C statC\<rbrakk> 

1208 
\<Longrightarrow> G\<turnstile>membr in dynC permits_acc_to accC" 

1209 
by (auto dest: field_accessible_fromD intro: permits_acc_inheritance) 

1210 

1211 

1212 
(* 

1213 
lemma accessible_Package: 

1214 
"\<lbrakk>G \<turnstile> m of C accessible_from S;accmodi m = Package; 

1215 
\<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new\<rbrakk> 

1216 
\<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)" 

1217 
proof  

1218 
assume wf: "\<And> new old. G\<turnstile>new overrides\<^sub>S old \<Longrightarrow> accmodi old \<le> accmodi new" 

1219 
assume "G \<turnstile> m of C accessible_from S" 

1220 
then show "accmodi m = Package \<Longrightarrow> pid S = pid C \<and> pid C = pid (declclass m)" 

1221 
(is "?Pack m \<Longrightarrow> ?P C m") 

1222 
proof (induct rule: accessible_fromR.induct) 

1223 
fix C m 

1224 
assume "G\<turnstile>m member_of C" 

1225 
"G \<turnstile> m in C permits_acc_to S" 

1226 
"accmodi m = Package" 

1227 
then show "?P C m" 

1228 
by (auto dest: member_of_Package simp add: permits_acc_def) 

1229 
next 

1230 
fix declC C new newm old Sup 

1231 
assume member_new: "G \<turnstile> new member_of C" and 

1232 
acc_C: "G \<turnstile> Class C accessible_in pid S" and 

1233 
new: "new = (declC, mdecl newm)" and 

1234 
override: "G \<turnstile> (declC, newm) overrides\<^sub>S old" and 

1235 
subcls_C_Sup: "G\<turnstile>C \<prec>\<^sub>C Sup" and 

1236 
acc_old: "G \<turnstile> methdMembr old of Sup accessible_from S" and 

1237 
hyp: "?Pack (methdMembr old) \<Longrightarrow> ?P Sup (methdMembr old)" and 

1238 
accmodi_new: "accmodi new = Package" 

1239 
from override wf 

1240 
have accmodi_weaken: "accmodi old \<le> accmodi newm" 

1241 
by (cases old,cases newm) auto 

1242 
from override new 

1243 
have "accmodi old \<noteq> Private" 

1244 
by (simp add: no_Private_stat_override) 

1245 
with accmodi_weaken accmodi_new new 

1246 
have accmodi_old: "accmodi old = Package" 

1247 
by (cases "accmodi old") (auto simp add: le_acc_def less_acc_def) 

1248 
with hyp 

1249 
have P_sup: "?P Sup (methdMembr old)" 

1250 
by (simp) 

1251 
from wf override new accmodi_old accmodi_new 

1252 
have eq_pid_new_old: "pid (declclass new) = pid (declclass old)" 

1253 
by (auto dest: stat_override_Package) 

1254 
from member_new accmodi_new 

1255 
have "pid (declclass new) = pid C" 

1256 
by (auto dest: member_of_Package) 

1257 
with eq_pid_new_old P_sup show "?P C new" 

1258 
by auto 

1259 
qed 

1260 
qed 

1261 
*) 

1262 
lemma accessible_fieldD: 

1263 
"\<lbrakk>G\<turnstile>membr of C accessible_from accC; is_field membr\<rbrakk> 

1264 
\<Longrightarrow> G\<turnstile>membr member_of C \<and> 

1265 
G\<turnstile>(Class C) accessible_in (pid accC) \<and> 

1266 
G\<turnstile>membr in C permits_acc_to accC" 

1267 
by (induct rule: accessible_fromR.induct) (auto dest: is_fieldD) 

1268 

1269 
(* lemmata: 

1270 
Wegen G\<turnstile>Super accessible_in (pid C) folgt: 

1271 
G\<turnstile>m declared_in C; G\<turnstile>m member_of D; accmodi m = Package (G\<turnstile>D \<preceq>\<^sub>C C) 

1272 
\<Longrightarrow> pid C = pid D 

1273 

1274 
C package 

1275 
m public in C 

1276 
für alle anderen D: G\<turnstile>m undeclared_in C 

1277 
m wird in alle subklassen vererbt, auch aus dem Package heraus! 

1278 

1279 
G\<turnstile>m member_of C \<Longrightarrow> \<exists> D. G\<turnstile>C \<preceq>\<^sub>C D \<and> G\<turnstile>m declared_in D 

1280 
*) 

1281 

1282 
(* Begriff (C,m) overrides (D,m) 

1283 
3 Fälle: Direkt, 

1284 
Indirekt über eine Zwischenklasse (ohne weiteres override) 

1285 
Indirekt über override 

1286 
*) 

1287 

1288 
(* 

1289 
"G\<turnstile>m member_of C \<equiv> 

1290 
constdefs declares_method:: "prog \<Rightarrow> sig \<Rightarrow> qtname \<Rightarrow> methd \<Rightarrow> bool" 

1291 
("_,_\<turnstile> _ declares'_method _" [61,61,61,61] 60) 

1292 
"G,sig\<turnstile>C declares_method m \<equiv> cdeclaredmethd G C sig = Some m" 

1293 

1294 
constdefs is_declared:: "prog \<Rightarrow> sig \<Rightarrow> (qtname \<times> methd) \<Rightarrow> bool" 

1295 
"is_declared G sig em \<equiv> G,sig\<turnstile>declclass em declares_method mthd em" 

1296 
*) 

1297 

1298 
lemma member_of_Private: 

1299 
"\<lbrakk>G\<turnstile>m member_of C; accmodi m = Private\<rbrakk> \<Longrightarrow> declclass m = C" 

1300 
by (induct set: members) (auto simp add: inheritable_in_def) 

1301 

1302 
lemma member_of_subclseq_declC: 

1303 
"G\<turnstile>m member_of C \<Longrightarrow> G\<turnstile>C \<preceq>\<^sub>C declclass m" 

1304 
by (induct set: members) (auto dest: r_into_rtrancl intro: rtrancl_trans) 

1305 

1306 
lemma member_of_inheritance: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1307 
assumes m: "G\<turnstile>m member_of D" and 
12854  1308 
subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and 
1309 
subclseq_C_m: "G\<turnstile>C \<preceq>\<^sub>C declclass m" and 

1310 
ws: "ws_prog G" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1311 
shows "G\<turnstile>m member_of C" 
12854  1312 
proof  
1313 
from m subclseq_D_C subclseq_C_m 

1314 
show ?thesis 

1315 
proof (induct) 

1316 
case (Immediate D m) 

1317 
assume "declclass m = D" and 

1318 
"G\<turnstile>D\<preceq>\<^sub>C C" and "G\<turnstile>C\<preceq>\<^sub>C declclass m" 

1319 
with ws have "D=C" 

1320 
by (auto intro: subclseq_acyclic) 

1321 
with Immediate 

1322 
show "G\<turnstile>m member_of C" 

1323 
by (auto intro: members.Immediate) 

1324 
next 

1325 
case (Inherited D S m) 

1326 
assume member_of_D_props: 

1327 
"G \<turnstile> m inheritable_in pid D" 

1328 
"G\<turnstile> memberid m undeclared_in D" 

1329 
"G \<turnstile> Class S accessible_in pid D" 

1330 
"G \<turnstile> m member_of S" 

1331 
assume super: "G\<turnstile>D\<prec>\<^sub>C\<^sub>1S" 

1332 
assume hyp: "\<lbrakk>G\<turnstile>S\<preceq>\<^sub>C C; G\<turnstile>C\<preceq>\<^sub>C declclass m\<rbrakk> \<Longrightarrow> G \<turnstile> m member_of C" 

1333 
assume subclseq_C_m: "G\<turnstile>C\<preceq>\<^sub>C declclass m" 

1334 
assume "G\<turnstile>D\<preceq>\<^sub>C C" 

1335 
then show "G\<turnstile>m member_of C" 

1336 
proof (cases rule: subclseq_cases) 

1337 
case Eq 

1338 
assume "D=C" 

1339 
with super member_of_D_props 

1340 
show ?thesis 

1341 
by (auto intro: members.Inherited) 

1342 
next 

1343 
case Subcls 

1344 
assume "G\<turnstile>D\<prec>\<^sub>C C" 

1345 
with super 

1346 
have "G\<turnstile>S\<preceq>\<^sub>C C" 

1347 
by (auto dest: subcls1D subcls_superD) 

1348 
with subclseq_C_m hyp show ?thesis 

1349 
by blast 

1350 
qed 

1351 
qed 

1352 
qed 

1353 

1354 
lemma member_of_subcls: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1355 
assumes old: "G\<turnstile>old member_of C" and 
12854  1356 
new: "G\<turnstile>new member_of D" and 
1357 
eqid: "memberid new = memberid old" and 

1358 
subclseq_D_C: "G\<turnstile>D \<preceq>\<^sub>C C" and 

1359 
subcls_new_old: "G\<turnstile>declclass new \<prec>\<^sub>C declclass old" and 

1360 
ws: "ws_prog G" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1361 
shows "G\<turnstile>D \<prec>\<^sub>C C" 
12854  1362 
proof  
1363 
from old 

1364 
have subclseq_C_old: "G\<turnstile>C \<preceq>\<^sub>C declclass old" 

1365 
by (auto dest: member_of_subclseq_declC) 

1366 
from new 

1367 
have subclseq_D_new: "G\<turnstile>D \<preceq>\<^sub>C declclass new" 

1368 
by (auto dest: member_of_subclseq_declC) 

1369 
from subcls_new_old ws 

1370 
have neq_new_old: "new\<noteq>old" 

1371 
by (cases new,cases old) (auto dest: subcls_irrefl) 

1372 
from subclseq_D_new subclseq_D_C 

1373 
have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C \<or> G\<turnstile>C \<preceq>\<^sub>C (declclass new)" 

1374 
by (rule subcls_compareable) 

1375 
then have "G\<turnstile>(declclass new) \<preceq>\<^sub>C C" 

1376 
proof 

1377 
assume "G\<turnstile>declclass new\<preceq>\<^sub>C C" then show ?thesis . 

1378 
next 

1379 
assume "G\<turnstile>C \<preceq>\<^sub>C (declclass new)" 

1380 
with new subclseq_D_C ws 

1381 
have "G\<turnstile>new member_of C" 

1382 
by (blast intro: member_of_inheritance) 

1383 
with eqid old 

1384 
have "new=old" 

1385 
by (blast intro: unique_member_of) 

1386 
with neq_new_old 

1387 
show ?thesis 

1388 
by contradiction 

1389 
qed 

1390 
then show ?thesis 

1391 
proof (cases rule: subclseq_cases) 

1392 
case Eq 

1393 
assume "declclass new = C" 

1394 
with new have "G\<turnstile>new member_of C" 

1395 
by (auto dest: member_of_member_of_declC) 

1396 
with eqid old 

1397 
have "new=old" 

1398 
by (blast intro: unique_member_of) 

1399 
with neq_new_old 

1400 
show ?thesis 

1401 
by contradiction 

1402 
next 

1403 
case Subcls 

1404 
assume "G\<turnstile>declclass new\<prec>\<^sub>C C" 

1405 
with subclseq_D_new 

1406 
show "G\<turnstile>D\<prec>\<^sub>C C" 

1407 
by (rule rtrancl_trancl_trancl) 

1408 
qed 

1409 
qed 

1410 

1411 
corollary member_of_overrides_subcls: 

1412 
"\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C; 

1413 
G,sig\<turnstile>new overrides old; ws_prog G\<rbrakk> 

1414 
\<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C" 

1415 
by (drule overrides_commonD) (auto intro: member_of_subcls) 

1416 

1417 
corollary member_of_stat_overrides_subcls: 

1418 
"\<lbrakk>G\<turnstile>Methd sig old member_of C; G\<turnstile>Methd sig new member_of D;G\<turnstile>D \<preceq>\<^sub>C C; 

1419 
G,sig\<turnstile>new overrides\<^sub>S old; ws_prog G\<rbrakk> 

1420 
\<Longrightarrow> G\<turnstile>D \<prec>\<^sub>C C" 

1421 
by (drule stat_overrides_commonD) (auto intro: member_of_subcls) 

1422 

1423 

1424 

1425 
lemma inherited_field_access: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1426 
assumes stat_acc: "G\<turnstile>membr of statC accessible_from accC" and 
12854  1427 
is_field: "is_field membr" and 
1428 
subclseq: "G \<turnstile> dynC \<preceq>\<^sub>C statC" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1429 
shows "G\<turnstile>membr in dynC dyn_accessible_from accC" 
12854  1430 
proof  
1431 
from stat_acc is_field subclseq 

1432 
show ?thesis 

1433 
by (auto dest: accessible_fieldD 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1434 
intro: dyn_accessible_fromR.Immediate 
12854  1435 
member_inI 
1436 
permits_acc_inheritance) 

1437 
qed 

1438 

1439 
lemma accessible_inheritance: 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1440 
assumes stat_acc: "G\<turnstile>m of statC accessible_from accC" and 
12854  1441 
subclseq: "G\<turnstile>dynC \<preceq>\<^sub>C statC" and 
1442 
member_dynC: "G\<turnstile>m member_of dynC" and 

1443 
dynC_acc: "G\<turnstile>(Class dynC) accessible_in (pid accC)" 

12937
0c4fd7529467
clarified syntax of ``long'' statements: fixes/assumes/shows;
wenzelm
parents:
12925
diff
changeset

1444 
shows "G\<turnstile>m of dynC accessible_from accC" 
12854  1445 
proof  
1446 
from stat_acc 

1447 
have member_statC: "G\<turnstile>m member_of statC" 

1448 
by (auto dest: accessible_from_commonD) 

1449 
from stat_acc 

1450 
show ?thesis 

1451 
proof (cases) 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1452 
case Immediate 
12854  1453 
with member_dynC member_statC subclseq dynC_acc 
1454 
show ?thesis 

12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1455 
by (auto intro: accessible_fromR.Immediate permits_acc_inheritance) 
12854  1456 
next 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12859
diff
changeset

1457 
case Overriding 
12854
