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 == if b then Some (Addr (XcptRef x)) else None" |
36 "raise_system_xcpt b x \<equiv> if b then Some (Addr (XcptRef x)) else None" |
37 |
37 |
38 -- "redefines State.new\\_Addr:" |
38 -- "redefines State.new\\_Addr:" |
39 new_Addr :: "aheap => loc \<times> val option" |
39 new_Addr :: "aheap \<Rightarrow> loc \<times> val option" |
40 "new_Addr h == SOME (a,x). (h a = None \<and> x = None) | |
40 "new_Addr h \<equiv> let (a, x) = State.new_Addr h |
41 x = raise_system_xcpt True OutOfMemory" |
41 in (a, raise_system_xcpt (x ~= None) OutOfMemory)" |
42 |
42 |
43 |
43 |
44 section {* Runtime State *} |
44 section {* Runtime State *} |
45 types |
45 types |
46 jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames" |
46 jvm_state = "val option \<times> aheap \<times> frame list" -- "exception flag, heap, frames" |
51 blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj" |
51 blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj" |
52 "blank G C \<equiv> (C,init_vars (fields(G,C)))" |
52 "blank G C \<equiv> (C,init_vars (fields(G,C)))" |
53 |
53 |
54 start_heap :: "'c prog \<Rightarrow> aheap" |
54 start_heap :: "'c prog \<Rightarrow> aheap" |
55 "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer)) |
55 "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer)) |
56 (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast)) |
56 (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast)) |
57 (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))" |
57 (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))" |
58 |
58 |
59 section {* Lemmas *} |
59 section {* Lemmas *} |
60 |
60 |
61 lemma new_AddrD: |
61 lemma new_AddrD: |
62 "new_Addr hp = (ref, xcp) \<Longrightarrow> hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))" |
62 assumes new: "new_Addr hp = (ref, xcp)" |
63 apply (drule sym) |
63 shows "hp ref = None \<and> xcp = None \<or> xcp = Some (Addr (XcptRef OutOfMemory))" |
64 apply (unfold new_Addr_def) |
64 proof - |
65 apply (simp add: raise_system_xcpt_def) |
65 from new obtain xcpT where old: "State.new_Addr hp = (ref,xcpT)" |
66 apply (simp add: Pair_fst_snd_eq Eps_split) |
66 by (cases "State.new_Addr hp") (simp add: new_Addr_def) |
67 apply (rule someI) |
67 from this [symmetric] |
68 apply (rule disjI2) |
68 have "hp ref = None \<and> xcpT = None \<or> xcpT = Some OutOfMemory" |
69 apply (rule_tac "r" = "snd (?a,Some (Addr (XcptRef OutOfMemory)))" in trans) |
69 by (rule State.new_AddrD) |
70 apply auto |
70 with new old show ?thesis |
71 done |
71 by (auto simp add: new_Addr_def raise_system_xcpt_def) |
|
72 qed |
|
73 |
72 |
74 |
73 lemma new_Addr_OutOfMemory: |
75 lemma new_Addr_OutOfMemory: |
74 "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)" |
76 "snd (new_Addr hp) = Some xcp \<Longrightarrow> xcp = Addr (XcptRef OutOfMemory)" |
75 proof - |
77 proof - |
76 obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp") |
78 obtain ref xp where "new_Addr hp = (ref, xp)" by (cases "new_Addr hp") |