4 *) |
4 *) |
5 |
5 |
6 theory Exceptions imports State begin |
6 theory Exceptions imports State begin |
7 |
7 |
8 text {* a new, blank object with default values in all fields: *} |
8 text {* a new, blank object with default values in all fields: *} |
9 constdefs |
9 definition blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj" where |
10 blank :: "'c prog \<Rightarrow> cname \<Rightarrow> obj" |
|
11 "blank G C \<equiv> (C,init_vars (fields(G,C)))" |
10 "blank G C \<equiv> (C,init_vars (fields(G,C)))" |
12 |
11 |
13 start_heap :: "'c prog \<Rightarrow> aheap" |
12 definition start_heap :: "'c prog \<Rightarrow> aheap" where |
14 "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer)) |
13 "start_heap G \<equiv> empty (XcptRef NullPointer \<mapsto> blank G (Xcpt NullPointer)) |
15 (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast)) |
14 (XcptRef ClassCast \<mapsto> blank G (Xcpt ClassCast)) |
16 (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))" |
15 (XcptRef OutOfMemory \<mapsto> blank G (Xcpt OutOfMemory))" |
17 |
16 |
18 |
17 |
19 abbreviation |
18 abbreviation |
20 cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname" |
19 cname_of :: "aheap \<Rightarrow> val \<Rightarrow> cname" |
21 where "cname_of hp v == fst (the (hp (the_Addr v)))" |
20 where "cname_of hp v == fst (the (hp (the_Addr v)))" |
22 |
21 |
23 |
22 |
24 constdefs |
23 definition preallocated :: "aheap \<Rightarrow> bool" where |
25 preallocated :: "aheap \<Rightarrow> bool" |
|
26 "preallocated hp \<equiv> \<forall>x. \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)" |
24 "preallocated hp \<equiv> \<forall>x. \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)" |
27 |
25 |
28 lemma preallocatedD: |
26 lemma preallocatedD: |
29 "preallocated hp \<Longrightarrow> \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)" |
27 "preallocated hp \<Longrightarrow> \<exists>fs. hp (XcptRef x) = Some (Xcpt x, fs)" |
30 by (unfold preallocated_def) fast |
28 by (unfold preallocated_def) fast |