header {* \isaheader{Exceptions} *}
theory Exceptions imports Objects begin
definition NullPointer :: cname
where
"NullPointer ≡ ''NullPointer''"
definition ClassCast :: cname
where
"ClassCast ≡ ''ClassCast''"
definition OutOfMemory :: cname
where
"OutOfMemory ≡ ''OutOfMemory''"
definition sys_xcpts :: "cname set"
where
"sys_xcpts ≡ {NullPointer, ClassCast, OutOfMemory}"
definition addr_of_sys_xcpt :: "cname => addr"
where
"addr_of_sys_xcpt s ≡ if s = NullPointer then 0 else
if s = ClassCast then 1 else
if s = OutOfMemory then 2 else undefined"
definition start_heap :: "'c prog => heap"
where
"start_heap G ≡ empty (addr_of_sys_xcpt NullPointer \<mapsto> blank G NullPointer)
(addr_of_sys_xcpt ClassCast \<mapsto> blank G ClassCast)
(addr_of_sys_xcpt OutOfMemory \<mapsto> blank G OutOfMemory)"
definition preallocated :: "heap => bool"
where
"preallocated h ≡ ∀C ∈ sys_xcpts. ∃fs. h(addr_of_sys_xcpt C) = Some (C,fs)"
section "System exceptions"
lemma [simp]: "NullPointer ∈ sys_xcpts ∧ OutOfMemory ∈ sys_xcpts ∧ ClassCast ∈ sys_xcpts"
by(simp add: sys_xcpts_def)
lemma sys_xcpts_cases [consumes 1, cases set]:
"[| C ∈ sys_xcpts; P NullPointer; P OutOfMemory; P ClassCast|] ==> P C"
by (auto simp add: sys_xcpts_def)
section "@{term preallocated}"
lemma preallocated_dom [simp]:
"[| preallocated h; C ∈ sys_xcpts |] ==> addr_of_sys_xcpt C ∈ dom h"
by (fastforce simp:preallocated_def dom_def)
lemma preallocatedD:
"[| preallocated h; C ∈ sys_xcpts |] ==> ∃fs. h(addr_of_sys_xcpt C) = Some (C, fs)"
by(auto simp add: preallocated_def sys_xcpts_def)
lemma preallocatedE [elim?]:
"[| preallocated h; C ∈ sys_xcpts; !!fs. h(addr_of_sys_xcpt C) = Some(C,fs) ==> P h C|]
==> P h C"
by (fast dest: preallocatedD)
lemma cname_of_xcp [simp]:
"[| preallocated h; C ∈ sys_xcpts |] ==> cname_of h (addr_of_sys_xcpt C) = C"
by (auto elim: preallocatedE)
lemma typeof_ClassCast [simp]:
"preallocated h ==> typeof⇘h⇙ (Addr(addr_of_sys_xcpt ClassCast)) = Some(Class ClassCast)"
by (auto elim: preallocatedE)
lemma typeof_OutOfMemory [simp]:
"preallocated h ==> typeof⇘h⇙ (Addr(addr_of_sys_xcpt OutOfMemory)) = Some(Class OutOfMemory)"
by (auto elim: preallocatedE)
lemma typeof_NullPointer [simp]:
"preallocated h ==> typeof⇘h⇙ (Addr(addr_of_sys_xcpt NullPointer)) = Some(Class NullPointer)"
by (auto elim: preallocatedE)
lemma preallocated_hext:
"[| preallocated h; h \<unlhd> h' |] ==> preallocated h'"
by (simp add: preallocated_def hext_def)
lemmas preallocated_upd_obj = preallocated_hext [OF _ hext_upd_obj]
lemmas preallocated_new = preallocated_hext [OF _ hext_new]
lemma preallocated_start:
"preallocated (start_heap P)"
by (auto simp add: start_heap_def blank_def sys_xcpts_def fun_upd_apply
addr_of_sys_xcpt_def preallocated_def)
end