31 |
31 |
32 |
32 |
33 section {* Exceptions *} |
33 section {* Exceptions *} |
34 constdefs |
34 constdefs |
35 raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" |
35 raise_system_xcpt :: "bool \<Rightarrow> xcpt \<Rightarrow> val option" |
36 "raise_system_xcpt b x \<equiv> if b then Some (Addr (XcptRef x)) else None" |
36 "raise_system_xcpt b x \<equiv> raise_if b x None" |
37 |
|
38 -- "redefines State.new\\_Addr:" |
|
39 new_Addr :: "aheap \<Rightarrow> loc \<times> val option" |
|
40 "new_Addr h \<equiv> let (a, x) = State.new_Addr h |
|
41 in (a, raise_system_xcpt (x ~= None) OutOfMemory)" |
|
42 |
|
43 |
37 |
44 section {* Runtime State *} |
38 section {* Runtime State *} |
45 types |
39 types |
46 jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames" |
40 jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames" |
47 |
41 |
48 |
42 |
49 text {* a new, blank object with default values in all fields: *} |
|
50 constdefs |
|
51 blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj" |
|
52 "blank G C \<equiv> (C,init_vars (fields(G,C)))" |
|
53 |
|
54 start_heap :: "'c prog \<Rightarrow> aheap" |
|
55 "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer)) |
|
56 (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast)) |
|
57 (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))" |
|
58 |
|
59 section {* Lemmas *} |
43 section {* Lemmas *} |
60 |
|
61 lemma new_AddrD: |
|
62 assumes new: "new_Addr hp = (ref, xcp)" |
|
63 shows "hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))" |
|
64 proof - |
|
65 from new obtain xcpT where old: "State.new_Addr hp = (ref,xcpT)" |
|
66 by (cases "State.new_Addr hp") (simp add: new_Addr_def) |
|
67 from this [symmetric] |
|
68 have "hp ref = None \<and> xcpT = None \<or> xcpT = Some OutOfMemory" |
|
69 by (rule State.new_AddrD) |
|
70 with new old show ?thesis |
|
71 by (auto simp add: new_Addr_def raise_system_xcpt_def) |
|
72 qed |
|
73 |
|
74 |
44 |
75 lemma new_Addr_OutOfMemory: |
45 lemma new_Addr_OutOfMemory: |
76 "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)" |
46 "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)" |
77 proof - |
47 proof - |
78 obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp") |
48 obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp") |