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/Eval.thy 
12854  2 
ID: $Id$ 
3 
Author: David von Oheimb 

12858  4 
License: GPL (GNU GENERAL PUBLIC LICENSE) 
12854  5 
*) 
6 
header {* Operational evaluation (bigstep) semantics of Java expressions and 

7 
statements 

8 
*} 

9 

10 
theory Eval = State + DeclConcepts: 

11 

12 
text {* 

13 

14 
improvements over Java Specification 1.0: 

15 
\begin{itemize} 

16 
\item dynamic method lookup does not need to consider the return type 

17 
(cf.15.11.4.4) 

18 
\item throw raises a NullPointer exception if a null reference is given, and 

19 
each throw of a standard exception yield a fresh exception object 

20 
(was not specified) 

21 
\item if there is not enough memory even to allocate an OutOfMemory exception, 

22 
evaluation/execution fails, i.e. simply stops (was not specified) 

23 
\item array assignment checks lhs (and may throw exceptions) before evaluating 

24 
rhs 

25 
\item fixed exact positions of class initializations 

26 
(immediate at first active use) 

27 
\end{itemize} 

28 

29 
design issues: 

30 
\begin{itemize} 

31 
\item evaluation vs. (singlestep) transition semantics 

32 
evaluation semantics chosen, because: 

33 
\begin{itemize} 

34 
\item[++] less verbose and therefore easier to read (and to handle in proofs) 

35 
\item[+] more abstract 

36 
\item[+] intermediate values (appearing in recursive rules) need not be 

37 
stored explicitly, e.g. no call body construct or stack of invocation 

38 
frames containing local variables and return addresses for method calls 

39 
needed 

40 
\item[+] convenient rule induction for subject reduction theorem 

41 
\item[] no interleaving (for parallelism) can be described 

42 
\item[] stating a property of infinite executions requires the metalevel 

43 
argument that this property holds for any finite prefixes of it 

44 
(e.g. stopped using a counter that is decremented to zero and then 

45 
throwing an exception) 

46 
\end{itemize} 

47 
\item unified evaluation for variables, expressions, expression lists, 

48 
statements 

49 
\item the value entry in statement rules is redundant 

50 
\item the value entry in rules is irrelevant in case of exceptions, but its full 

51 
inclusion helps to make the rule structure independent of exception occurence. 

52 
\item as irrelevant value entries are ignored, it does not matter if they are 

53 
unique. 

54 
For simplicity, (fixed) arbitrary values are preferred over "free" values. 

55 
\item the rule format is such that the start state may contain an exception. 

56 
\begin{itemize} 

57 
\item[++] faciliates exception handling 

58 
\item[+] symmetry 

59 
\end{itemize} 

60 
\item the rules are defined carefully in order to be applicable even in not 

61 
typecorrect situations (yielding undefined values), 

62 
e.g. @{text "the_Addr (Val (Bool b)) = arbitrary"}. 

63 
\begin{itemize} 

64 
\item[++] fewer rules 

65 
\item[] less readable because of auxiliary functions like @{text the_Addr} 

66 
\end{itemize} 

67 
Alternative: "defensive" evaluation throwing some InternalError exception 

68 
in case of (impossible, for correct programs) type mismatches 

69 
\item there is exactly one rule per syntactic construct 

70 
\begin{itemize} 

71 
\item[+] no redundancy in case distinctions 

72 
\end{itemize} 

73 
\item halloc fails iff there is no free heap address. When there is 

74 
only one free heap address left, it returns an OutOfMemory exception. 

75 
In this way it is guaranteed that when an OutOfMemory exception is thrown for 

76 
the first time, there is a free location on the heap to allocate it. 

77 
\item the allocation of objects that represent standard exceptions is deferred 

78 
until execution of any enclosing catch clause, which is transparent to 

79 
the program. 

80 
\begin{itemize} 

81 
\item[] requires an auxiliary execution relation 

82 
\item[++] avoids copies of allocation code and awkward case distinctions 

83 
(whether there is enough memory to allocate the exception) in 

84 
evaluation rules 

85 
\end{itemize} 

86 
\item unfortunately @{text new_Addr} is not directly executable because of 

87 
Hilbert operator. 

88 
\end{itemize} 

89 
simplifications: 

90 
\begin{itemize} 

91 
\item local variables are initialized with default values 

92 
(no definite assignment) 

93 
\item garbage collection not considered, therefore also no finalizers 

94 
\item stack overflow and memory overflow during class initialization not 

95 
modelled 

96 
\item exceptions in initializations not replaced by ExceptionInInitializerError 

97 
\end{itemize} 

98 
*} 

99 

100 
types vvar = "val \<times> (val \<Rightarrow> state \<Rightarrow> state)" 

101 
vals = "(val, vvar, val list) sum3" 

102 
translations 

103 
"vvar" <= (type) "val \<times> (val \<Rightarrow> state \<Rightarrow> state)" 

104 
"vals" <= (type)"(val, vvar, val list) sum3" 

105 

106 
syntax (xsymbols) 

107 
dummy_res :: "vals" ("\<diamondsuit>") 

108 
translations 

109 
"\<diamondsuit>" == "In1 Unit" 

110 

111 
constdefs 

112 
arbitrary3 :: "('al + 'ar, 'b, 'c) sum3 \<Rightarrow> vals" 

113 
"arbitrary3 \<equiv> sum3_case (In1 \<circ> sum_case (\<lambda>x. arbitrary) (\<lambda>x. Unit)) 

114 
(\<lambda>x. In2 arbitrary) (\<lambda>x. In3 arbitrary)" 

115 

116 
lemma [simp]: "arbitrary3 (In1l x) = In1 arbitrary" 

117 
by (simp add: arbitrary3_def) 

118 

119 
lemma [simp]: "arbitrary3 (In1r x) = \<diamondsuit>" 

120 
by (simp add: arbitrary3_def) 

121 

122 
lemma [simp]: "arbitrary3 (In2 x) = In2 arbitrary" 

123 
by (simp add: arbitrary3_def) 

124 

125 
lemma [simp]: "arbitrary3 (In3 x) = In3 arbitrary" 

126 
by (simp add: arbitrary3_def) 

127 

128 

129 
section "exception throwing and catching" 

130 

131 
constdefs 

132 
throw :: "val \<Rightarrow> abopt \<Rightarrow> abopt" 

133 
"throw a' x \<equiv> abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)" 

134 

135 
lemma throw_def2: 

136 
"throw a' x = abrupt_if True (Some (Xcpt (Loc (the_Addr a')))) (np a' x)" 

137 
apply (unfold throw_def) 

138 
apply (simp (no_asm)) 

139 
done 

140 

141 
constdefs 

142 
fits :: "prog \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ty \<Rightarrow> bool" ("_,_\<turnstile>_ fits _"[61,61,61,61]60) 

143 
"G,s\<turnstile>a' fits T \<equiv> (\<exists>rt. T=RefT rt) \<longrightarrow> a'=Null \<or> G\<turnstile>obj_ty(lookup_obj s a')\<preceq>T" 

144 

145 
lemma fits_Null [simp]: "G,s\<turnstile>Null fits T" 

146 
by (simp add: fits_def) 

147 

148 

149 
lemma fits_Addr_RefT [simp]: 

150 
"G,s\<turnstile>Addr a fits RefT t = G\<turnstile>obj_ty (the (heap s a))\<preceq>RefT t" 

151 
by (simp add: fits_def) 

152 

153 
lemma fitsD: "\<And>X. G,s\<turnstile>a' fits T \<Longrightarrow> (\<exists>pt. T = PrimT pt) \<or> 

154 
(\<exists>t. T = RefT t) \<and> a' = Null \<or> 

155 
(\<exists>t. T = RefT t) \<and> a' \<noteq> Null \<and> G\<turnstile>obj_ty (lookup_obj s a')\<preceq>T" 

156 
apply (unfold fits_def) 

157 
apply (case_tac "\<exists>pt. T = PrimT pt") 

158 
apply simp_all 

159 
apply (case_tac "T") 

160 
defer 

161 
apply (case_tac "a' = Null") 

162 
apply simp_all 

163 
done 

164 

165 
constdefs 

166 
catch ::"prog \<Rightarrow> state \<Rightarrow> qtname \<Rightarrow> bool" ("_,_\<turnstile>catch _"[61,61,61]60) 

167 
"G,s\<turnstile>catch C\<equiv>\<exists>xc. abrupt s=Some (Xcpt xc) \<and> 

168 
G,store s\<turnstile>Addr (the_Loc xc) fits Class C" 

169 

170 
lemma catch_Norm [simp]: "\<not>G,Norm s\<turnstile>catch tn" 

171 
apply (unfold catch_def) 

172 
apply (simp (no_asm)) 

173 
done 

174 

175 
lemma catch_XcptLoc [simp]: 

176 
"G,(Some (Xcpt (Loc a)),s)\<turnstile>catch C = G,s\<turnstile>Addr a fits Class C" 

177 
apply (unfold catch_def) 

178 
apply (simp (no_asm)) 

179 
done 

180 

181 
constdefs 

182 
new_xcpt_var :: "vname \<Rightarrow> state \<Rightarrow> state" 

183 
"new_xcpt_var vn \<equiv> 

184 
\<lambda>(x,s). Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)" 

185 

186 
lemma new_xcpt_var_def2 [simp]: 

187 
"new_xcpt_var vn (x,s) = 

188 
Norm (lupd(VName vn\<mapsto>Addr (the_Loc (the_Xcpt (the x)))) s)" 

189 
apply (unfold new_xcpt_var_def) 

190 
apply (simp (no_asm)) 

191 
done 

192 

193 

194 

195 
section "misc" 

196 

197 
constdefs 

198 

199 
assign :: "('a \<Rightarrow> state \<Rightarrow> state) \<Rightarrow> 'a \<Rightarrow> state \<Rightarrow> state" 

200 
"assign f v \<equiv> \<lambda>(x,s). let (x',s') = (if x = None then f v else id) (x,s) 

201 
in (x',if x' = None then s' else s)" 

202 

203 
(* 

204 
lemma assign_Norm_Norm [simp]: 

205 
"f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr> 

206 
\<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=None,store=s'\<rparr>" 

207 
by (simp add: assign_def Let_def) 

208 
*) 

209 

210 
lemma assign_Norm_Norm [simp]: 

211 
"f v (Norm s) = Norm s' \<Longrightarrow> assign f v (Norm s) = Norm s'" 

212 
by (simp add: assign_def Let_def) 

213 

214 
(* 

215 
lemma assign_Norm_Some [simp]: 

216 
"\<lbrakk>abrupt (f v \<lparr>abrupt=None,store=s\<rparr>) = Some y\<rbrakk> 

217 
\<Longrightarrow> assign f v \<lparr>abrupt=None,store=s\<rparr> = \<lparr>abrupt=Some y,store =s\<rparr>" 

218 
by (simp add: assign_def Let_def split_beta) 

219 
*) 

220 

221 
lemma assign_Norm_Some [simp]: 

222 
"\<lbrakk>abrupt (f v (Norm s)) = Some y\<rbrakk> 

223 
\<Longrightarrow> assign f v (Norm s) = (Some y,s)" 

224 
by (simp add: assign_def Let_def split_beta) 

225 

226 

227 
lemma assign_Some [simp]: 

228 
"assign f v (Some x,s) = (Some x,s)" 

229 
by (simp add: assign_def Let_def split_beta) 

230 

231 
lemma assign_supd [simp]: 

232 
"assign (\<lambda>v. supd (f v)) v (x,s) 

233 
= (x, if x = None then f v s else s)" 

234 
apply auto 

235 
done 

236 

237 
lemma assign_raise_if [simp]: 

238 
"assign (\<lambda>v (x,s). ((raise_if (b s v) xcpt) x, f v s)) v (x, s) = 

239 
(raise_if (b s v) xcpt x, if x=None \<and> \<not>b s v then f v s else s)" 

240 
apply (case_tac "x = None") 

241 
apply auto 

242 
done 

243 

244 
(* 

245 
lemma assign_raise_if [simp]: 

246 
"assign (\<lambda>v s. \<lparr>abrupt=(raise_if (b (store s) v) xcpt) (abrupt s), 

247 
store = f v (store s)\<rparr>) v s = 

248 
\<lparr>abrupt=raise_if (b (store s) v) xcpt (abrupt s), 

249 
store= if (abrupt s)=None \<and> \<not>b (store s) v 

250 
then f v (store s) else (store s)\<rparr>" 

251 
apply (case_tac "abrupt s = None") 

252 
apply auto 

253 
done 

254 
*) 

255 

256 
constdefs 

257 

258 
init_comp_ty :: "ty \<Rightarrow> stmt" 

259 
"init_comp_ty T \<equiv> if (\<exists>C. T = Class C) then Init (the_Class T) else Skip" 

260 

261 
lemma init_comp_ty_PrimT [simp]: "init_comp_ty (PrimT pt) = Skip" 

262 
apply (unfold init_comp_ty_def) 

263 
apply (simp (no_asm)) 

264 
done 

265 

266 
constdefs 

267 

268 
(* 

269 
target :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" 

270 
"target m s a' t 

271 
\<equiv> if m = IntVir 

272 
then obj_class (lookup_obj s a') 

273 
else the_Class (RefT t)" 

274 
*) 

275 

276 
invocation_class :: "inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> qtname" 

277 
"invocation_class m s a' statT 

278 
\<equiv> (case m of 

279 
Static \<Rightarrow> if (\<exists> statC. statT = ClassT statC) 

280 
then the_Class (RefT statT) 

281 
else Object 

282 
 SuperM \<Rightarrow> the_Class (RefT statT) 

283 
 IntVir \<Rightarrow> obj_class (lookup_obj s a'))" 

284 

285 
invocation_declclass::"prog \<Rightarrow> inv_mode \<Rightarrow> st \<Rightarrow> val \<Rightarrow> ref_ty \<Rightarrow> sig \<Rightarrow> qtname" 

286 
"invocation_declclass G m s a' statT sig 

287 
\<equiv> declclass (the (dynlookup G statT 

288 
(invocation_class m s a' statT) 

289 
sig))" 

290 

291 
lemma invocation_class_IntVir [simp]: 

292 
"invocation_class IntVir s a' statT = obj_class (lookup_obj s a')" 

293 
by (simp add: invocation_class_def) 

294 

295 
lemma dynclass_SuperM [simp]: 

296 
"invocation_class SuperM s a' statT = the_Class (RefT statT)" 

297 
by (simp add: invocation_class_def) 

298 
(* 

299 
lemma invocation_class_notIntVir [simp]: 

300 
"m \<noteq> IntVir \<Longrightarrow> invocation_class m s a' statT = the_Class (RefT statT)" 

301 
by (simp add: invocation_class_def) 

302 
*) 

303 

304 
lemma invocation_class_Static [simp]: 

305 
"invocation_class Static s a' statT = (if (\<exists> statC. statT = ClassT statC) 

306 
then the_Class (RefT statT) 

307 
else Object)" 

308 
by (simp add: invocation_class_def) 

309 

310 
constdefs 

311 
init_lvars :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> inv_mode \<Rightarrow> val \<Rightarrow> val list \<Rightarrow> 

312 
state \<Rightarrow> state" 

313 
"init_lvars G C sig mode a' pvs 

314 
\<equiv> \<lambda> (x,s). 

315 
let m = mthd (the (methd G C sig)); 

316 
l = \<lambda> k. 

317 
(case k of 

318 
EName e 

319 
\<Rightarrow> (case e of 

320 
VNam v \<Rightarrow> (init_vals (table_of (lcls (mbody m))) 

321 
((pars m)[\<mapsto>]pvs)) v 

322 
 Res \<Rightarrow> Some (default_val (resTy m))) 

323 
 This 

324 
\<Rightarrow> (if mode=Static then None else Some a')) 

325 
in set_lvars l (if mode = Static then x else np a' x,s)" 

326 

327 

328 

329 
lemma init_lvars_def2: "init_lvars G C sig mode a' pvs (x,s) = 

330 
set_lvars 

331 
(\<lambda> k. 

332 
(case k of 

333 
EName e 

334 
\<Rightarrow> (case e of 

335 
VNam v 

336 
\<Rightarrow> (init_vals 

337 
(table_of (lcls (mbody (mthd (the (methd G C sig)))))) 

338 
((pars (mthd (the (methd G C sig))))[\<mapsto>]pvs)) v 

339 
 Res \<Rightarrow> Some (default_val (resTy (mthd (the (methd G C sig)))))) 

340 
 This 

341 
\<Rightarrow> (if mode=Static then None else Some a'))) 

342 
(if mode = Static then x else np a' x,s)" 

343 
apply (unfold init_lvars_def) 

344 
apply (simp (no_asm) add: Let_def) 

345 
done 

346 

347 
constdefs 

348 
body :: "prog \<Rightarrow> qtname \<Rightarrow> sig \<Rightarrow> expr" 

349 
"body G C sig \<equiv> let m = the (methd G C sig) 

350 
in Body (declclass m) (stmt (mbody (mthd m)))" 

351 

352 
lemma body_def2: 

353 
"body G C sig = Body (declclass (the (methd G C sig))) 

354 
(stmt (mbody (mthd (the (methd G C sig)))))" 

355 
apply (unfold body_def Let_def) 

356 
apply auto 

357 
done 

358 

359 
section "variables" 

360 

361 
constdefs 

362 

363 
lvar :: "lname \<Rightarrow> st \<Rightarrow> vvar" 

364 
"lvar vn s \<equiv> (the (locals s vn), \<lambda>v. supd (lupd(vn\<mapsto>v)))" 

365 

366 
fvar :: "qtname \<Rightarrow> bool \<Rightarrow> vname \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" 

367 
"fvar C stat fn a' s 

368 
\<equiv> let (oref,xf) = if stat then (Stat C,id) 

369 
else (Heap (the_Addr a'),np a'); 

370 
n = Inl (fn,C); 

371 
f = (\<lambda>v. supd (upd_gobj oref n v)) 

372 
in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)" 

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

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

374 
"fvar C stat fn a' s 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

375 
\<equiv> let (oref,xf) = if stat then (Stat C,id) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

376 
else (Heap (the_Addr a'),np a'); 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

377 
n = Inl (fn,C); 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

378 
f = (\<lambda>v. supd (upd_gobj oref n v)) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

379 
in ((the (values (the (globs (store s) oref)) n),f),abupd xf s)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

380 
*) 
12854  381 
avar :: "prog \<Rightarrow> val \<Rightarrow> val \<Rightarrow> state \<Rightarrow> vvar \<times> state" 
382 
"avar G i' a' s 

383 
\<equiv> let oref = Heap (the_Addr a'); 

384 
i = the_Intg i'; 

385 
n = Inr i; 

386 
(T,k,cs) = the_Arr (globs (store s) oref); 

387 
f = (\<lambda>v (x,s). (raise_if (\<not>G,s\<turnstile>v fits T) 

388 
ArrStore x 

389 
,upd_gobj oref n v s)) 

390 
in ((the (cs n),f) 

391 
,abupd (raise_if (\<not>i in_bounds k) IndOutBound \<circ> np a') s)" 

392 

393 
lemma fvar_def2: "fvar C stat fn a' s = 

394 
((the 

395 
(values 

396 
(the (globs (store s) (if stat then Stat C else Heap (the_Addr a')))) 

397 
(Inl (fn,C))) 

398 
,(\<lambda>v. supd (upd_gobj (if stat then Stat C else Heap (the_Addr a')) 

399 
(Inl (fn,C)) 

400 
v))) 

401 
,abupd (if stat then id else np a') s) 

402 
" 

403 
apply (unfold fvar_def) 

404 
apply (simp (no_asm) add: Let_def split_beta) 

405 
done 

406 

407 
lemma avar_def2: "avar G i' a' s = 

408 
((the ((snd(snd(the_Arr (globs (store s) (Heap (the_Addr a')))))) 

409 
(Inr (the_Intg i'))) 

410 
,(\<lambda>v (x,s'). (raise_if (\<not>G,s'\<turnstile>v fits (fst(the_Arr (globs (store s) 

411 
(Heap (the_Addr a')))))) 

412 
ArrStore x 

413 
,upd_gobj (Heap (the_Addr a')) 

414 
(Inr (the_Intg i')) v s'))) 

415 
,abupd (raise_if (\<not>(the_Intg i') in_bounds (fst(snd(the_Arr (globs (store s) 

416 
(Heap (the_Addr a'))))))) IndOutBound \<circ> np a') 

417 
s)" 

418 
apply (unfold avar_def) 

419 
apply (simp (no_asm) add: Let_def split_beta) 

420 
done 

421 

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

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

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

424 
"prog \<Rightarrow> qtname \<Rightarrow> qtname \<Rightarrow> vname \<Rightarrow> bool \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

425 
"check_field_access G accC statDeclC fn stat a' s 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

426 
\<equiv> let oref = if stat then Stat statDeclC 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

427 
else Heap (the_Addr a'); 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

428 
dynC = case oref of 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

429 
Heap a \<Rightarrow> obj_class (the (globs (store s) oref)) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

430 
 Stat C \<Rightarrow> C; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

431 
f = (the (table_of (DeclConcepts.fields G dynC) (fn,statDeclC))) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

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

433 
(error_if (\<not> G\<turnstile>Field fn (statDeclC,f) in dynC dyn_accessible_from accC) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

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

435 
s" 
12854  436 

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

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

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

439 
"prog \<Rightarrow> qtname \<Rightarrow> ref_ty \<Rightarrow> inv_mode \<Rightarrow> sig \<Rightarrow> val \<Rightarrow> state \<Rightarrow> state" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

440 
"check_method_access G accC statT mode sig a' s 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

441 
\<equiv> let invC = invocation_class mode (store s) a' statT; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

442 
dynM = the (dynlookup G statT invC sig) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

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

444 
(error_if (\<not> G\<turnstile>Methd sig dynM in invC dyn_accessible_from accC) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

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

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

447 

12854  448 
section "evaluation judgments" 
449 

450 
consts 

451 
eval :: "prog \<Rightarrow> (state \<times> term \<times> vals \<times> state) set" 

452 
halloc:: "prog \<Rightarrow> (state \<times> obj_tag \<times> loc \<times> state) set" 

453 
sxalloc:: "prog \<Rightarrow> (state \<times> state) set" 

454 

455 

456 
syntax 

457 
eval ::"[prog,state,term,vals*state]=>bool"("__ _>> _" [61,61,80, 61]60) 

458 
exec ::"[prog,state,stmt ,state]=>bool"("__ _> _" [61,61,65, 61]60) 

459 
evar ::"[prog,state,var ,vvar,state]=>bool"("__ _=>_> _"[61,61,90,61,61]60) 

460 
eval_::"[prog,state,expr ,val, state]=>bool"("__ _>_> _"[61,61,80,61,61]60) 

461 
evals::"[prog,state,expr list , 

462 
val list ,state]=>bool"("__ _#>_> _"[61,61,61,61,61]60) 

463 
hallo::"[prog,state,obj_tag, 

464 
loc,state]=>bool"("__ halloc _>_> _"[61,61,61,61,61]60) 

465 
sallo::"[prog,state ,state]=>bool"("__ sxalloc> _"[61,61, 61]60) 

466 

467 
syntax (xsymbols) 

468 
eval ::"[prog,state,term,vals\<times>state]\<Rightarrow>bool" ("_\<turnstile>_ \<midarrow>_\<succ>\<rightarrow> _" [61,61,80, 61]60) 

469 
exec ::"[prog,state,stmt ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<rightarrow> _" [61,61,65, 61]60) 

470 
evar ::"[prog,state,var ,vvar,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_=\<succ>_\<rightarrow> _"[61,61,90,61,61]60) 

471 
eval_::"[prog,state,expr ,val ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<succ>_\<rightarrow> _"[61,61,80,61,61]60) 

472 
evals::"[prog,state,expr list , 

473 
val list ,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>_\<doteq>\<succ>_\<rightarrow> _"[61,61,61,61,61]60) 

474 
hallo::"[prog,state,obj_tag, 

475 
loc,state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>halloc _\<succ>_\<rightarrow> _"[61,61,61,61,61]60) 

476 
sallo::"[prog,state, state]\<Rightarrow>bool"("_\<turnstile>_ \<midarrow>sxalloc\<rightarrow> _"[61,61, 61]60) 

477 

478 
translations 

479 
"G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> w___s' " == "(s,t,w___s') \<in> eval G" 

480 
"G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> (w, s')" <= "(s,t,w, s') \<in> eval G" 

481 
"G\<turnstile>s \<midarrow>t \<succ>\<rightarrow> (w,x,s')" <= "(s,t,w,x,s') \<in> eval G" 

482 
"G\<turnstile>s \<midarrow>c \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit>,x,s')" 

483 
"G\<turnstile>s \<midarrow>c \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1r c\<succ>\<rightarrow> (\<diamondsuit> , s')" 

484 
"G\<turnstile>s \<midarrow>e\<succ>v \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v ,x,s')" 

485 
"G\<turnstile>s \<midarrow>e\<succ>v \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In1l e\<succ>\<rightarrow> (In1 v , s')" 

486 
"G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In2 e\<succ>\<rightarrow> (In2 vf,x,s')" 

487 
"G\<turnstile>s \<midarrow>e=\<succ>vf\<rightarrow> s' " == "G\<turnstile>s \<midarrow>In2 e\<succ>\<rightarrow> (In2 vf, s')" 

488 
"G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow> (x,s')" <= "G\<turnstile>s \<midarrow>In3 e\<succ>\<rightarrow> (In3 v ,x,s')" 

489 
"G\<turnstile>s \<midarrow>e\<doteq>\<succ>v \<rightarrow> s' " == "G\<turnstile>s \<midarrow>In3 e\<succ>\<rightarrow> (In3 v , s')" 

490 
"G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,s')" <= "(s,oi,a,x,s') \<in> halloc G" 

491 
"G\<turnstile>s \<midarrow>halloc oi\<succ>a\<rightarrow> s' " == "(s,oi,a, s') \<in> halloc G" 

492 
"G\<turnstile>s \<midarrow>sxalloc\<rightarrow> (x,s')" <= "(s ,x,s') \<in> sxalloc G" 

493 
"G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' " == "(s , s') \<in> sxalloc G" 

494 

495 
inductive "halloc G" intros (* allocating objects on the heap, cf. 12.5 *) 

496 

497 
Abrupt: 

498 
"G\<turnstile>(Some x,s) \<midarrow>halloc oi\<succ>arbitrary\<rightarrow> (Some x,s)" 

499 

500 
New: "\<lbrakk>new_Addr (heap s) = Some a; 

501 
(x,oi') = (if atleast_free (heap s) (Suc (Suc 0)) then (None,oi) 

502 
else (Some (Xcpt (Loc a)),CInst (SXcpt OutOfMemory)))\<rbrakk> 

503 
\<Longrightarrow> 

504 
G\<turnstile>Norm s \<midarrow>halloc oi\<succ>a\<rightarrow> (x,init_obj G oi' (Heap a) s)" 

505 

506 
inductive "sxalloc G" intros (* allocating exception objects for 

507 
standard exceptions (other than OutOfMemory) *) 

508 

509 
Norm: "G\<turnstile> Norm s \<midarrow>sxalloc\<rightarrow> Norm s" 

510 

511 
XcptL: "G\<turnstile>(Some (Xcpt (Loc a) ),s) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s)" 

512 

513 
SXcpt: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>halloc (CInst (SXcpt xn))\<succ>a\<rightarrow> (x,s1)\<rbrakk> \<Longrightarrow> 

514 
G\<turnstile>(Some (Xcpt (Std xn)),s0) \<midarrow>sxalloc\<rightarrow> (Some (Xcpt (Loc a)),s1)" 

515 

516 

517 
inductive "eval G" intros 

518 

519 
(* propagation of abrupt completion *) 

520 

521 
(* cf. 14.1, 15.5 *) 

522 
Abrupt: 

523 
"G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s))" 

524 

525 

526 
(* execution of statements *) 

527 

528 
(* cf. 14.5 *) 

529 
Skip: "G\<turnstile>Norm s \<midarrow>Skip\<rightarrow> Norm s" 

530 

531 
(* cf. 14.7 *) 

532 
Expr: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow> 

533 
G\<turnstile>Norm s0 \<midarrow>Expr e\<rightarrow> s1" 

534 

535 
Lab: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c \<rightarrow> s1\<rbrakk> \<Longrightarrow> 

536 
G\<turnstile>Norm s0 \<midarrow>l\<bullet> c\<rightarrow> abupd (absorb (Break l)) s1" 

537 
(* cf. 14.2 *) 

538 
Comp: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1 \<rightarrow> s1; 

539 
G\<turnstile> s1 \<midarrow>c2 \<rightarrow> s2\<rbrakk> \<Longrightarrow> 

540 
G\<turnstile>Norm s0 \<midarrow>c1;; c2\<rightarrow> s2" 

541 

542 

543 
(* cf. 14.8.2 *) 

544 
If: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>b\<rightarrow> s1; 

545 
G\<turnstile> s1\<midarrow>(if the_Bool b then c1 else c2)\<rightarrow> s2\<rbrakk> \<Longrightarrow> 

546 
G\<turnstile>Norm s0 \<midarrow>If(e) c1 Else c2 \<rightarrow> s2" 

547 

548 
(* cf. 14.10, 14.10.1 *) 

549 
(* G\<turnstile>Norm s0 \<midarrow>If(e) (c;; While(e) c) Else Skip\<rightarrow> s3 *) 

550 
(* A "continue jump" from the while body c is handled by 

551 
this rule. If a continue jump with the proper label was invoked inside c 

552 
this label (Cont l) is deleted out of the abrupt component of the state 

553 
before the iterative evaluation of the while statement. 

554 
A "break jump" is handled by the Lab Statement (Lab l (while\<dots>). 

555 
*) 

556 
Loop: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>b\<rightarrow> s1; 

557 
if normal s1 \<and> the_Bool b 

558 
then (G\<turnstile>s1 \<midarrow>c\<rightarrow> s2 \<and> 

559 
G\<turnstile>(abupd (absorb (Cont l)) s2) \<midarrow>l\<bullet> While(e) c\<rightarrow> s3) 

560 
else s3 = s1\<rbrakk> \<Longrightarrow> 

561 
G\<turnstile>Norm s0 \<midarrow>l\<bullet> While(e) c\<rightarrow> s3" 

562 

563 
Do: "G\<turnstile>Norm s \<midarrow>Do j\<rightarrow> (Some (Jump j), s)" 

564 

565 
(* cf. 14.16 *) 

566 
Throw: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>a'\<rightarrow> s1\<rbrakk> \<Longrightarrow> 

567 
G\<turnstile>Norm s0 \<midarrow>Throw e\<rightarrow> abupd (throw a') s1" 

568 

569 
(* cf. 14.18.1 *) 

570 
Try: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>sxalloc\<rightarrow> s2; 

571 
if G,s2\<turnstile>catch C then G\<turnstile>new_xcpt_var vn s2 \<midarrow>c2\<rightarrow> s3 else s3 = s2\<rbrakk> \<Longrightarrow> 

572 
G\<turnstile>Norm s0 \<midarrow>Try c1 Catch(C vn) c2\<rightarrow> s3" 

573 

574 
(* cf. 14.18.2 *) 

575 
Fin: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>c1\<rightarrow> (x1,s1); 

576 
G\<turnstile>Norm s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow> 

577 
G\<turnstile>Norm s0 \<midarrow>c1 Finally c2\<rightarrow> abupd (abrupt_if (x1\<noteq>None) x1) s2" 

578 

579 
(* cf. 12.4.2, 8.5 *) 

580 
Init: "\<lbrakk>the (class G C) = c; 

581 
if inited C (globs s0) then s3 = Norm s0 

582 
else (G\<turnstile>Norm (init_class_obj G C s0) 

583 
\<midarrow>(if C = Object then Skip else Init (super c))\<rightarrow> s1 \<and> 

584 
G\<turnstile>set_lvars empty s1 \<midarrow>init c\<rightarrow> s2 \<and> s3 = restore_lvars s1 s2)\<rbrakk> 

585 
\<Longrightarrow> 

586 
G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3" 

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

587 
(* This class initialisation rule is a little bit inaccurate. Look at the 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

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

589 
1. The current class object (the static fields) are initialised 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

590 
(init_class_obj) 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

591 
2. Then the superclasses are initialised 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

592 
3. The static initialiser of the current class is invoked 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

593 
More precisely we should expect another ordering, namely 2 1 3. 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

594 
But we can't just naively toggle 1 and 2. By calling init_class_obj 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

595 
before initialising the superclasses we also implicitly record that 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

596 
we have started to initialise the current class (by setting an 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

597 
value for the class object). This becomes 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

598 
crucial for the completeness proof of the axiomatic semantics 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

599 
(AxCompl.thy). Static initialisation requires an induction on the number 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

600 
of classes not yet initialised (or to be more precise, classes where the 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

601 
initialisation has not yet begun). 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

602 
So we could first assign a dummy value to the class before 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

603 
superclass initialisation and afterwards set the correct values. 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

604 
But as long as we don't take memory overflow into account 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

605 
when allocating class objects, and don't model definite assignment in 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

606 
the static initialisers, we can leave things as they are for convenience. 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

607 
*) 
12854  608 
(* evaluation of expressions *) 
609 

610 
(* cf. 15.8.1, 12.4.1 *) 

611 
NewC: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s1; 

612 
G\<turnstile> s1 \<midarrow>halloc (CInst C)\<succ>a\<rightarrow> s2\<rbrakk> \<Longrightarrow> 

613 
G\<turnstile>Norm s0 \<midarrow>NewC C\<succ>Addr a\<rightarrow> s2" 

614 

615 
(* cf. 15.9.1, 12.4.1 *) 

616 
NewA: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>init_comp_ty T\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e\<succ>i'\<rightarrow> s2; 

617 
G\<turnstile>abupd (check_neg i') s2 \<midarrow>halloc (Arr T (the_Intg i'))\<succ>a\<rightarrow> s3\<rbrakk> \<Longrightarrow> 

618 
G\<turnstile>Norm s0 \<midarrow>New T[e]\<succ>Addr a\<rightarrow> s3" 

619 

620 
(* cf. 15.15 *) 

621 
Cast: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<rightarrow> s1; 

622 
s2 = abupd (raise_if (\<not>G,store s1\<turnstile>v fits T) ClassCast) s1\<rbrakk> \<Longrightarrow> 

623 
G\<turnstile>Norm s0 \<midarrow>Cast T e\<succ>v\<rightarrow> s2" 

624 

625 
(* cf. 15.19.2 *) 

626 
Inst: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>v\<rightarrow> s1; 

627 
b = (v\<noteq>Null \<and> G,store s1\<turnstile>v fits RefT T)\<rbrakk> \<Longrightarrow> 

628 
G\<turnstile>Norm s0 \<midarrow>e InstOf T\<succ>Bool b\<rightarrow> s1" 

629 

630 
(* cf. 15.7.1 *) 

631 
Lit: "G\<turnstile>Norm s \<midarrow>Lit v\<succ>v\<rightarrow> Norm s" 

632 

633 

634 

635 
(* cf. 15.10.2 *) 

636 
Super: "G\<turnstile>Norm s \<midarrow>Super\<succ>val_this s\<rightarrow> Norm s" 

637 

638 
(* cf. 15.2 *) 

639 
Acc: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(v,f)\<rightarrow> s1\<rbrakk> \<Longrightarrow> 

640 
G\<turnstile>Norm s0 \<midarrow>Acc va\<succ>v\<rightarrow> s1" 

641 

642 
(* cf. 15.25.1 *) 

643 
Ass: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>va=\<succ>(w,f)\<rightarrow> s1; 

644 
G\<turnstile> s1 \<midarrow>e\<succ>v \<rightarrow> s2\<rbrakk> \<Longrightarrow> 

645 
G\<turnstile>Norm s0 \<midarrow>va:=e\<succ>v\<rightarrow> assign f v s2" 

646 

647 
(* cf. 15.24 *) 

648 
Cond: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e0\<succ>b\<rightarrow> s1; 

649 
G\<turnstile> s1 \<midarrow>(if the_Bool b then e1 else e2)\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow> 

650 
G\<turnstile>Norm s0 \<midarrow>e0 ? e1 : e2\<succ>v\<rightarrow> s2" 

651 

652 

653 
(* cf. 15.11.4.1, 15.11.4.2, 15.11.4.4, 15.11.4.5 *) 

654 
Call: 

655 
"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>args\<doteq>\<succ>vs\<rightarrow> s2; 

656 
D = invocation_declclass G mode (store s2) a' 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:
12919
diff
changeset

657 
s3=init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' vs s2; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

658 
s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

659 
G\<turnstile>s3' \<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>\<succ>v\<rightarrow> s4\<rbrakk> 
12854  660 
\<Longrightarrow> 
12925
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

661 
G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}args)\<succ>v\<rightarrow> (restore_lvars s2 s4)" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

662 
(* The accessibility check is after init_lvars, to keep it simple. Init_lvars 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

663 
already tests for the absence of a nullpointer reference in case of an 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

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

665 
*) 
12854  666 

667 
Methd: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>body G D sig\<succ>v\<rightarrow> s1\<rbrakk> \<Longrightarrow> 

668 
G\<turnstile>Norm s0 \<midarrow>Methd D sig\<succ>v\<rightarrow> s1" 

669 

670 
(* cf. 14.15, 12.4.1 *) 

671 
Body: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init D\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c\<rightarrow> s2\<rbrakk> \<Longrightarrow> 

672 
G\<turnstile>Norm s0 \<midarrow>Body D c \<succ>the (locals (store s2) Result)\<rightarrow>abupd (absorb Ret) s2" 

673 

674 
(* evaluation of variables *) 

675 

676 
(* cf. 15.13.1, 15.7.2 *) 

677 
LVar: "G\<turnstile>Norm s \<midarrow>LVar vn=\<succ>lvar vn s\<rightarrow> Norm s" 

678 

679 
(* cf. 15.10.1, 12.4.1 *) 

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

680 
FVar: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>Init statDeclC\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e\<succ>a\<rightarrow> s2; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

681 
(v,s2') = fvar statDeclC stat fn a s2; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

682 
s3 = check_field_access G accC statDeclC fn stat a s2' \<rbrakk> \<Longrightarrow> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

683 
G\<turnstile>Norm s0 \<midarrow>{accC,statDeclC,stat}e..fn=\<succ>v\<rightarrow> s3" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

684 
(* The accessibility check is after fvar, to keep it simple. Fvar already 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

685 
tests for the absence of a nullpointer reference in case of an instance 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

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

687 
*) 
12854  688 

689 
(* cf. 15.12.1, 15.25.1 *) 

690 
AVar: "\<lbrakk>G\<turnstile> Norm s0 \<midarrow>e1\<succ>a\<rightarrow> s1; G\<turnstile>s1 \<midarrow>e2\<succ>i\<rightarrow> s2; 

691 
(v,s2') = avar G i a s2\<rbrakk> \<Longrightarrow> 

692 
G\<turnstile>Norm s0 \<midarrow>e1.[e2]=\<succ>v\<rightarrow> s2'" 

693 

694 

695 
(* evaluation of expression lists *) 

696 

697 
(* cf. 15.11.4.2 *) 

698 
Nil: 

699 
"G\<turnstile>Norm s0 \<midarrow>[]\<doteq>\<succ>[]\<rightarrow> Norm s0" 

700 

701 
(* cf. 15.6.4 *) 

702 
Cons: "\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e \<succ> v \<rightarrow> s1; 

703 
G\<turnstile> s1 \<midarrow>es\<doteq>\<succ>vs\<rightarrow> s2\<rbrakk> \<Longrightarrow> 

704 
G\<turnstile>Norm s0 \<midarrow>e#es\<doteq>\<succ>v#vs\<rightarrow> s2" 

705 

706 
(* Rearrangement of premisses: 

707 
[0,1(Abrupt),2(Skip),8(Do),4(Lab),28(Nil),29(Cons),25(LVar),15(Cast),16(Inst), 

708 
17(Lit),18(Super),19(Acc),3(Expr),5(Comp),23(Methd),24(Body),21(Cond),6(If), 

709 
7(Loop),11(Fin),9(Throw),13(NewC),14(NewA),12(Init),20(Ass),10(Try),26(FVar), 

710 
27(AVar),22(Call)] 

711 
*) 

712 
ML {* 

713 
bind_thm ("eval_induct_", rearrange_prems 

714 
[0,1,2,8,4,28,29,25,15,16, 

715 
17,18,19,3,5,23,24,21,6, 

716 
7,11,9,13,14,12,20,10,26, 

717 
27,22] (thm "eval.induct")) 

718 
*} 

719 

720 
lemmas eval_induct = eval_induct_ [split_format and and and and and and and and 

721 
and and and and s1 (* Acc *) and and s2 (* Comp *) and and and and and and 

722 
s2 (* Fin *) and and s2 (* NewC *)] 

723 

724 
declare split_if [split del] split_if_asm [split del] 

725 
option.split [split del] option.split_asm [split del] 

726 
inductive_cases halloc_elim_cases: 

727 
"G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'" 

728 
"G\<turnstile>(Norm s) \<midarrow>halloc oi\<succ>a\<rightarrow> s'" 

729 

730 
inductive_cases sxalloc_elim_cases: 

731 
"G\<turnstile> Norm s \<midarrow>sxalloc\<rightarrow> s'" 

732 
"G\<turnstile>(Some (Xcpt (Loc a )),s) \<midarrow>sxalloc\<rightarrow> s'" 

733 
"G\<turnstile>(Some (Xcpt (Std xn)),s) \<midarrow>sxalloc\<rightarrow> s'" 

734 
inductive_cases sxalloc_cases: "G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'" 

735 

736 
lemma sxalloc_elim_cases2: "\<lbrakk>G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'; 

737 
\<And>s. \<lbrakk>s' = Norm s\<rbrakk> \<Longrightarrow> P; 

738 
\<And>a s. \<lbrakk>s' = (Some (Xcpt (Loc a)),s)\<rbrakk> \<Longrightarrow> P 

739 
\<rbrakk> \<Longrightarrow> P" 

740 
apply cut_tac 

741 
apply (erule sxalloc_cases) 

742 
apply blast+ 

743 
done 

744 

745 
declare not_None_eq [simp del] (* IntDef.Zero_def [simp del] *) 

746 
declare split_paired_All [simp del] split_paired_Ex [simp del] 

747 
ML_setup {* 

748 
simpset_ref() := simpset() delloop "split_all_tac" 

749 
*} 

750 
inductive_cases eval_cases: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'" 

751 

752 
inductive_cases eval_elim_cases: 

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

753 
"G\<turnstile>(Some xc,s) \<midarrow>t \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

754 
"G\<turnstile>Norm s \<midarrow>In1r Skip \<succ>\<rightarrow> xs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

755 
"G\<turnstile>Norm s \<midarrow>In1r (Do j) \<succ>\<rightarrow> xs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

756 
"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> c) \<succ>\<rightarrow> xs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

757 
"G\<turnstile>Norm s \<midarrow>In3 ([]) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

758 
"G\<turnstile>Norm s \<midarrow>In3 (e#es) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

759 
"G\<turnstile>Norm s \<midarrow>In1l (Lit w) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

760 
"G\<turnstile>Norm s \<midarrow>In2 (LVar vn) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

761 
"G\<turnstile>Norm s \<midarrow>In1l (Cast T e) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

762 
"G\<turnstile>Norm s \<midarrow>In1l (e InstOf T) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

763 
"G\<turnstile>Norm s \<midarrow>In1l (Super) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

764 
"G\<turnstile>Norm s \<midarrow>In1l (Acc va) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

765 
"G\<turnstile>Norm s \<midarrow>In1r (Expr e) \<succ>\<rightarrow> xs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

766 
"G\<turnstile>Norm s \<midarrow>In1r (c1;; c2) \<succ>\<rightarrow> xs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

767 
"G\<turnstile>Norm s \<midarrow>In1l (Methd C sig) \<succ>\<rightarrow> xs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

768 
"G\<turnstile>Norm s \<midarrow>In1l (Body D c) \<succ>\<rightarrow> xs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

769 
"G\<turnstile>Norm s \<midarrow>In1l (e0 ? e1 : e2) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

770 
"G\<turnstile>Norm s \<midarrow>In1r (If(e) c1 Else c2) \<succ>\<rightarrow> xs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

771 
"G\<turnstile>Norm s \<midarrow>In1r (l\<bullet> While(e) c) \<succ>\<rightarrow> xs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

772 
"G\<turnstile>Norm s \<midarrow>In1r (c1 Finally c2) \<succ>\<rightarrow> xs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

773 
"G\<turnstile>Norm s \<midarrow>In1r (Throw e) \<succ>\<rightarrow> xs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

774 
"G\<turnstile>Norm s \<midarrow>In1l (NewC C) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

775 
"G\<turnstile>Norm s \<midarrow>In1l (New T[e]) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

776 
"G\<turnstile>Norm s \<midarrow>In1l (Ass va e) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

777 
"G\<turnstile>Norm s \<midarrow>In1r (Try c1 Catch(tn vn) c2) \<succ>\<rightarrow> xs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

778 
"G\<turnstile>Norm s \<midarrow>In2 ({accC,statDeclC,stat}e..fn) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

779 
"G\<turnstile>Norm s \<midarrow>In2 (e1.[e2]) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

780 
"G\<turnstile>Norm s \<midarrow>In1l ({accC,statT,mode}e\<cdot>mn({pT}p)) \<succ>\<rightarrow> vs'" 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

781 
"G\<turnstile>Norm s \<midarrow>In1r (Init C) \<succ>\<rightarrow> xs'" 
12854  782 
declare not_None_eq [simp] (* IntDef.Zero_def [simp] *) 
783 
declare split_paired_All [simp] split_paired_Ex [simp] 

784 
ML_setup {* 

785 
simpset_ref() := simpset() addloop ("split_all_tac", split_all_tac) 

786 
*} 

787 
declare split_if [split] split_if_asm [split] 

788 
option.split [split] option.split_asm [split] 

789 

790 
lemma eval_Inj_elim: 

791 
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') 

792 
\<Longrightarrow> case t of 

793 
In1 ec \<Rightarrow> (case ec of 

794 
Inl e \<Rightarrow> (\<exists>v. w = In1 v) 

795 
 Inr c \<Rightarrow> w = \<diamondsuit>) 

796 
 In2 e \<Rightarrow> (\<exists>v. w = In2 v) 

797 
 In3 e \<Rightarrow> (\<exists>v. w = In3 v)" 

798 
apply (erule eval_cases) 

799 
apply auto 

800 
apply (induct_tac "t") 

801 
apply (induct_tac "a") 

802 
apply auto 

803 
done 

804 

805 
ML_setup {* 

806 
fun eval_fun nam inj rhs = 

807 
let 

808 
val name = "eval_" ^ nam ^ "_eq" 

809 
val lhs = "G\<turnstile>s \<midarrow>" ^ inj ^ " t\<succ>\<rightarrow> (w, s')" 

810 
val () = qed_goal name (the_context()) (lhs ^ " = (" ^ rhs ^ ")") 

811 
(K [Auto_tac, ALLGOALS (ftac (thm "eval_Inj_elim")) THEN Auto_tac]) 

812 
fun is_Inj (Const (inj,_) $ _) = true 

813 
 is_Inj _ = false 

814 
fun pred (_ $ (Const ("Pair",_) $ _ $ 

815 
(Const ("Pair", _) $ _ $ (Const ("Pair", _) $ x $ _ ))) $ _ ) = is_Inj x 

816 
in 

817 
make_simproc name lhs pred (thm name) 

818 
end 

819 

820 
val eval_expr_proc =eval_fun "expr" "In1l" "\<exists>v. w=In1 v \<and> G\<turnstile>s \<midarrow>t\<succ>v \<rightarrow> s'" 

821 
val eval_var_proc =eval_fun "var" "In2" "\<exists>vf. w=In2 vf \<and> G\<turnstile>s \<midarrow>t=\<succ>vf\<rightarrow> s'" 

822 
val eval_exprs_proc=eval_fun "exprs""In3" "\<exists>vs. w=In3 vs \<and> G\<turnstile>s \<midarrow>t\<doteq>\<succ>vs\<rightarrow> s'" 

823 
val eval_stmt_proc =eval_fun "stmt" "In1r" " w=\<diamondsuit> \<and> G\<turnstile>s \<midarrow>t \<rightarrow> s'"; 

824 
Addsimprocs [eval_expr_proc,eval_var_proc,eval_exprs_proc,eval_stmt_proc]; 

825 
bind_thms ("AbruptIs", sum3_instantiate (thm "eval.Abrupt")) 

826 
*} 

827 

828 
declare halloc.Abrupt [intro!] eval.Abrupt [intro!] AbruptIs [intro!] 

829 

830 

831 
lemma eval_no_abrupt_lemma: 

832 
"\<And>s s'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> normal s' \<longrightarrow> normal s" 

833 
by (erule eval_cases, auto) 

834 

835 
lemma eval_no_abrupt: 

836 
"G\<turnstile>(x,s) \<midarrow>t\<succ>\<rightarrow> (w,Norm s') = 

837 
(x = None \<and> G\<turnstile>Norm s \<midarrow>t\<succ>\<rightarrow> (w,Norm s'))" 

838 
apply auto 

839 
apply (frule eval_no_abrupt_lemma, auto)+ 

840 
done 

841 

842 
ML {* 

843 
local 

12919  844 
fun is_None (Const ("Datatype.option.None",_)) = true 
12854  845 
 is_None _ = false 
846 
fun pred (t as (_ $ (Const ("Pair",_) $ 

847 
(Const ("Pair", _) $ x $ _) $ _ ) $ _)) = is_None x 

848 
in 

849 
val eval_no_abrupt_proc = 

850 
make_simproc "eval_no_abrupt" "G\<turnstile>(x,s) \<midarrow>e\<succ>\<rightarrow> (w,Norm s')" pred 

851 
(thm "eval_no_abrupt") 

852 
end; 

853 
Addsimprocs [eval_no_abrupt_proc] 

854 
*} 

855 

856 

857 
lemma eval_abrupt_lemma: 

858 
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (v,s') \<Longrightarrow> abrupt s=Some xc \<longrightarrow> s'= s \<and> v = arbitrary3 t" 

859 
by (erule eval_cases, auto) 

860 

861 
lemma eval_abrupt: 

862 
" G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (w,s') = 

863 
(s'=(Some xc,s) \<and> w=arbitrary3 t \<and> 

864 
G\<turnstile>(Some xc,s) \<midarrow>t\<succ>\<rightarrow> (arbitrary3 t,(Some xc,s)))" 

865 
apply auto 

866 
apply (frule eval_abrupt_lemma, auto)+ 

867 
done 

868 

869 
ML {* 

870 
local 

12919  871 
fun is_Some (Const ("Pair",_) $ (Const ("Datatype.option.Some",_) $ _)$ _) =true 
12854  872 
 is_Some _ = false 
873 
fun pred (_ $ (Const ("Pair",_) $ 

874 
_ $ (Const ("Pair", _) $ _ $ (Const ("Pair", _) $ _ $ 

875 
x))) $ _ ) = is_Some x 

876 
in 

877 
val eval_abrupt_proc = 

878 
make_simproc "eval_abrupt" 

879 
"G\<turnstile>(Some xc,s) \<midarrow>e\<succ>\<rightarrow> (w,s')" pred (thm "eval_abrupt") 

880 
end; 

881 
Addsimprocs [eval_abrupt_proc] 

882 
*} 

883 

884 

885 
lemma LitI: "G\<turnstile>s \<midarrow>Lit v\<succ>(if normal s then v else arbitrary)\<rightarrow> s" 

886 
apply (case_tac "s", case_tac "a = None") 

887 
by (auto intro!: eval.Lit) 

888 

889 
lemma SkipI [intro!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s" 

890 
apply (case_tac "s", case_tac "a = None") 

891 
by (auto intro!: eval.Skip) 

892 

893 
lemma ExprI: "G\<turnstile>s \<midarrow>e\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Expr e\<rightarrow> s'" 

894 
apply (case_tac "s", case_tac "a = None") 

895 
by (auto intro!: eval.Expr) 

896 

897 
lemma CompI: "\<lbrakk>G\<turnstile>s \<midarrow>c1\<rightarrow> s1; G\<turnstile>s1 \<midarrow>c2\<rightarrow> s2\<rbrakk> \<Longrightarrow> G\<turnstile>s \<midarrow>c1;; c2\<rightarrow> s2" 

898 
apply (case_tac "s", case_tac "a = None") 

899 
by (auto intro!: eval.Comp) 

900 

901 
lemma CondI: 

902 
"\<And>s1. \<lbrakk>G\<turnstile>s \<midarrow>e\<succ>b\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool b then e1 else e2)\<succ>v\<rightarrow> s2\<rbrakk> \<Longrightarrow> 

903 
G\<turnstile>s \<midarrow>e ? e1 : e2\<succ>(if normal s1 then v else arbitrary)\<rightarrow> s2" 

904 
apply (case_tac "s", case_tac "a = None") 

905 
by (auto intro!: eval.Cond) 

906 

907 
lemma IfI: "\<lbrakk>G\<turnstile>s \<midarrow>e\<succ>v\<rightarrow> s1; G\<turnstile>s1 \<midarrow>(if the_Bool v then c1 else c2)\<rightarrow> s2\<rbrakk> 

908 
\<Longrightarrow> G\<turnstile>s \<midarrow>If(e) c1 Else c2\<rightarrow> s2" 

909 
apply (case_tac "s", case_tac "a = None") 

910 
by (auto intro!: eval.If) 

911 

912 
lemma MethdI: "G\<turnstile>s \<midarrow>body G C sig\<succ>v\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>Methd C sig\<succ>v\<rightarrow> s'" 

913 
apply (case_tac "s", case_tac "a = None") 

914 
by (auto intro!: eval.Methd) 

915 

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

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

917 
"\<lbrakk>G\<turnstile>Norm s0 \<midarrow>e\<succ>a'\<rightarrow> s1; G\<turnstile>s1 \<midarrow>ps\<doteq>\<succ>pvs\<rightarrow> s2; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

918 
D = invocation_declclass G mode (store s2) a' statT \<lparr>name=mn,parTs=pTs\<rparr>; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

919 
s3 = init_lvars G D \<lparr>name=mn,parTs=pTs\<rparr> mode a' pvs s2; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

920 
s3' = check_method_access G accC statT mode \<lparr>name=mn,parTs=pTs\<rparr> a' s3; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

921 
G\<turnstile>s3'\<midarrow>Methd D \<lparr>name=mn,parTs=pTs\<rparr>\<succ> v\<rightarrow> s4; 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

922 
s4' = restore_lvars s2 s4\<rbrakk> \<Longrightarrow> 
99131847fb93
Added check for field/method access to operational semantics and proved the acesses valid.
schirmer
parents:
12919
diff
changeset

923 
G\<turnstile>Norm s0 \<midarrow>{accC,statT,mode}e\<cdot>mn({pTs}ps)\<succ>v\<rightarrow> s4'" 
12854  924 
apply (drule eval.Call, assumption) 
925 
apply (rule HOL.refl) 

926 
apply simp+ 

927 
done 

928 

929 
lemma eval_Init: 

930 
"\<lbrakk>if inited C (globs s0) then s3 = Norm s0 

931 
else G\<turnstile>Norm (init_class_obj G C s0) 

932 
\<midarrow>(if C = Object then Skip else Init (super (the (class G C))))\<rightarrow> s1 \<and> 

933 
G\<turnstile>set_lvars empty s1 \<midarrow>(init (the (class G C)))\<rightarrow> s2 \<and> 

934 
s3 = restore_lvars s1 s2\<rbrakk> \<Longrightarrow> 

935 
G\<turnstile>Norm s0 \<midarrow>Init C\<rightarrow> s3" 

936 
apply (rule eval.Init) 

937 
apply auto 

938 
done 

939 

940 
lemma init_done: "initd C s \<Longrightarrow> G\<turnstile>s \<midarrow>Init C\<rightarrow> s" 

941 
apply (case_tac "s", simp) 

942 
apply (case_tac "a") 

943 
apply safe 

944 
apply (rule eval_Init) 

945 
apply auto 

946 
done 

947 

948 
lemma eval_StatRef: 

949 
"G\<turnstile>s \<midarrow>StatRef rt\<succ>(if abrupt s=None then Null else arbitrary)\<rightarrow> s" 

950 
apply (case_tac "s", simp) 

951 
apply (case_tac "a = None") 

952 
apply (auto del: eval.Abrupt intro!: eval.intros) 

953 
done 

954 

955 

956 
lemma SkipD [dest!]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' \<Longrightarrow> s' = s" 

957 
apply (erule eval_cases) 

958 
by auto 

959 

960 
lemma Skip_eq [simp]: "G\<turnstile>s \<midarrow>Skip\<rightarrow> s' = (s = s')" 

961 
by auto 

962 

963 
(*unused*) 

964 
lemma init_retains_locals [rule_format (no_asm)]: "G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> (w,s') \<Longrightarrow> 

965 
(\<forall>C. t=In1r (Init C) \<longrightarrow> locals (store s) = locals (store s'))" 

966 
apply (erule eval.induct) 

967 
apply (simp (no_asm_use) split del: split_if_asm option.split_asm)+ 

968 
apply auto 

969 
done 

970 

971 
lemma halloc_xcpt [dest!]: 

972 
"\<And>s'. G\<turnstile>(Some xc,s) \<midarrow>halloc oi\<succ>a\<rightarrow> s' \<Longrightarrow> s'=(Some xc,s)" 

973 
apply (erule_tac halloc_elim_cases) 

974 
by auto 

975 

976 
(* 

977 
G\<turnstile>(x,(h,l)) \<midarrow>e\<succ>v\<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This" 

978 
G\<turnstile>(x,(h,l)) \<midarrow>s \<rightarrow> (x',(h',l'))) \<Longrightarrow> l This = l' This" 

979 
*) 

980 

981 
lemma eval_Methd: 

982 
"G\<turnstile>s \<midarrow>In1l(body G C sig)\<succ>\<rightarrow> (w,s') \<Longrightarrow> G\<turnstile>s \<midarrow>In1l(Methd C sig)\<succ>\<rightarrow> (w,s')" 

983 
apply (case_tac "s") 

984 
apply (case_tac "a") 

985 
apply clarsimp+ 

986 
apply (erule eval.Methd) 

987 
apply (drule eval_abrupt_lemma) 

988 
apply force 

989 
done 

990 

991 

992 
section "single valued" 

993 

994 
lemma unique_halloc [rule_format (no_asm)]: 

995 
"\<And>s as as'. (s,oi,as)\<in>halloc G \<Longrightarrow> (s,oi,as')\<in>halloc G \<longrightarrow> as'=as" 

996 
apply (simp (no_asm_simp) only: split_tupled_all) 

997 
apply (erule halloc.induct) 

998 
apply (auto elim!: halloc_elim_cases split del: split_if split_if_asm) 

999 
apply (drule trans [THEN sym], erule sym) 

1000 
defer 

1001 
apply (drule trans [THEN sym], erule sym) 

1002 
apply auto 

1003 
done 

1004 

1005 

1006 
lemma single_valued_halloc: 

1007 
"single_valued {((s,oi),(a,s')). G\<turnstile>s \<midarrow>halloc oi\<succ>a \<rightarrow> s'}" 

1008 
apply (unfold single_valued_def) 

1009 
by (clarsimp, drule (1) unique_halloc, auto) 

1010 

1011 

1012 
lemma unique_sxalloc [rule_format (no_asm)]: 

1013 
"\<And>s s'. G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s' \<Longrightarrow> G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'' \<longrightarrow> s'' = s'" 

1014 
apply (simp (no_asm_simp) only: split_tupled_all) 

1015 
apply (erule sxalloc.induct) 

1016 
apply (auto dest: unique_halloc elim!: sxalloc_elim_cases 

1017 
split del: split_if split_if_asm) 

1018 
done 

1019 

1020 
lemma single_valued_sxalloc: "single_valued {(s,s'). G\<turnstile>s \<midarrow>sxalloc\<rightarrow> s'}" 

1021 
apply (unfold single_valued_def) 

1022 
apply (blast dest: unique_sxalloc) 

1023 
done 

1024 

1025 
lemma split_pairD: "(x,y) = p \<Longrightarrow> x = fst p & y = snd p" 

1026 
by auto 

1027 

1028 
lemma unique_eval [rule_format (no_asm)]: 

1029 
"G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws \<Longrightarrow> (\<forall>ws'. G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> ws' \<longrightarrow> ws' = ws)" 

1030 
apply (case_tac "ws") 

1031 
apply (simp only:) 

1032 
apply (erule thin_rl) 

1033 
apply (erule eval_induct) 

1034 
apply (tactic {* ALLGOALS (EVERY' 

1035 
[strip_tac, rotate_tac ~1, eresolve_tac (thms "eval_elim_cases")]) *}) 

1036 
(* 29 subgoals *) 

1037 
prefer 26 (* Try *) 

1038 
apply (simp (no_asm_use) only: split add: split_if_asm) 

1039 
(* 32 subgoals *) 

1040 
prefer 28 (* Init *) 

1041 
apply (case_tac "inited C (globs s0)", (simp only: if_True if_False)+) 

1042 
prefer 24 (* While *) 

1043 
apply (simp (no_asm_use) only: split add: split_if_asm, blast) 

1044 
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp) 

1045 
apply (drule_tac x="(In1 bb, s1a)" in spec, drule (1) mp, simp) 

1046 
apply blast 

1047 
(* 31 subgoals *) 

1048 
apply (blast dest: unique_sxalloc unique_halloc split_pairD)+ 

1049 
done 

1050 

1051 
(* unused *) 

1052 
lemma single_valued_eval: 

1053 
"single_valued {((s,t),vs'). G\<turnstile>s \<midarrow>t\<succ>\<rightarrow> vs'}" 

1054 
apply (unfold single_valued_def) 

1055 
by (clarify, drule (1) unique_eval, auto) 

1056 

1057 
end 