Theory Exceptions
section ‹ Exceptions ›
theory Exceptions imports Objects begin
definition ErrorCl :: "string" where "ErrorCl = ''Error''"
definition ThrowCl :: "string" where "ThrowCl = ''Throwable''"
definition NullPointer :: cname
where
"NullPointer ≡ ''NullPointer''"
definition ClassCast :: cname
where
"ClassCast ≡ ''ClassCast''"
definition OutOfMemory :: cname
where
"OutOfMemory ≡ ''OutOfMemory''"
definition NoClassDefFoundError :: cname
where
"NoClassDefFoundError ≡ ''NoClassDefFoundError''"
definition IncompatibleClassChangeError :: cname
where
"IncompatibleClassChangeError ≡ ''IncompatibleClassChangeError''"
definition NoSuchFieldError :: cname
where
"NoSuchFieldError ≡ ''NoSuchFieldError''"
definition NoSuchMethodError :: cname
where
"NoSuchMethodError ≡ ''NoSuchMethodError''"
definition sys_xcpts :: "cname set"
where
"sys_xcpts ≡ {NullPointer, ClassCast, OutOfMemory, NoClassDefFoundError,
IncompatibleClassChangeError,
NoSuchFieldError, NoSuchMethodError}"
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
if s = NoClassDefFoundError then 3 else
if s = IncompatibleClassChangeError then 4 else
if s = NoSuchFieldError then 5 else
if s = NoSuchMethodError then 6 else undefined"
lemmas sys_xcpts_defs = NullPointer_def ClassCast_def OutOfMemory_def NoClassDefFoundError_def
IncompatibleClassChangeError_def NoSuchFieldError_def NoSuchMethodError_def
lemma Start_nsys_xcpts: "Start ∉ sys_xcpts"
by(simp add: Start_def sys_xcpts_def sys_xcpts_defs)
lemma Start_nsys_xcpts1 [simp]: "Start ≠ NullPointer" "Start ≠ ClassCast"
"Start ≠ OutOfMemory" "Start ≠ NoClassDefFoundError"
"Start ≠ IncompatibleClassChangeError" "Start ≠ NoSuchFieldError"
"Start ≠ NoSuchMethodError"
using Start_nsys_xcpts by(auto simp: sys_xcpts_def)
lemma Start_nsys_xcpts2 [simp]: "NullPointer ≠ Start" "ClassCast ≠ Start"
"OutOfMemory ≠ Start" "NoClassDefFoundError ≠ Start"
"IncompatibleClassChangeError ≠ Start" "NoSuchFieldError ≠ Start"
"NoSuchMethodError ≠ Start"
using Start_nsys_xcpts by(auto simp: sys_xcpts_def dest: sym)
definition start_heap :: "'c prog ⇒ heap"
where
"start_heap G ≡ Map.empty (addr_of_sys_xcpt NullPointer ↦ blank G NullPointer,
addr_of_sys_xcpt ClassCast ↦ blank G ClassCast,
addr_of_sys_xcpt OutOfMemory ↦ blank G OutOfMemory,
addr_of_sys_xcpt NoClassDefFoundError ↦ blank G NoClassDefFoundError,
addr_of_sys_xcpt IncompatibleClassChangeError ↦ blank G IncompatibleClassChangeError,
addr_of_sys_xcpt NoSuchFieldError ↦ blank G NoSuchFieldError,
addr_of_sys_xcpt NoSuchMethodError ↦ blank G NoSuchMethodError)"
definition preallocated :: "heap ⇒ bool"
where
"preallocated h ≡ ∀C ∈ sys_xcpts. ∃fs. h(addr_of_sys_xcpt C) = Some (C,fs)"
subsection "System exceptions"
lemma sys_xcpts_incl [simp]: "NullPointer ∈ sys_xcpts ∧ OutOfMemory ∈ sys_xcpts
∧ ClassCast ∈ sys_xcpts ∧ NoClassDefFoundError ∈ sys_xcpts
∧ IncompatibleClassChangeError ∈ sys_xcpts ∧ NoSuchFieldError ∈ sys_xcpts
∧ NoSuchMethodError ∈ 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 NoClassDefFoundError;
P IncompatibleClassChangeError; P NoSuchFieldError;
P NoSuchMethodError ⟧ ⟹ P C"
by (auto simp: sys_xcpts_def)
subsection "Starting heap"
lemma start_heap_sys_xcpts:
assumes "C ∈ sys_xcpts"
shows "start_heap P (addr_of_sys_xcpt C) = Some(blank P C)"
by(rule sys_xcpts_cases[OF assms])
(auto simp add: start_heap_def sys_xcpts_def addr_of_sys_xcpt_def sys_xcpts_defs)
lemma start_heap_classes:
"start_heap P a = Some(C,fs) ⟹ C ∈ sys_xcpts"
by(simp add: start_heap_def blank_def split: if_split_asm)
lemma start_heap_nStart: "start_heap P a = Some obj ⟹ fst(obj) ≠ Start"
by(cases obj, auto dest!: start_heap_classes simp: Start_nsys_xcpts)
subsection "@{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: 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 typeof_NoClassDefFoundError [simp]:
"preallocated h ⟹ typeof⇘h⇙ (Addr(addr_of_sys_xcpt NoClassDefFoundError)) = Some(Class NoClassDefFoundError)"
by (auto elim: preallocatedE)
lemma typeof_IncompatibleClassChangeError [simp]:
"preallocated h ⟹ typeof⇘h⇙ (Addr(addr_of_sys_xcpt IncompatibleClassChangeError)) = Some(Class IncompatibleClassChangeError)"
by (auto elim: preallocatedE)
lemma typeof_NoSuchFieldError [simp]:
"preallocated h ⟹ typeof⇘h⇙ (Addr(addr_of_sys_xcpt NoSuchFieldError)) = Some(Class NoSuchFieldError)"
by (auto elim: preallocatedE)
lemma typeof_NoSuchMethodError [simp]:
"preallocated h ⟹ typeof⇘h⇙ (Addr(addr_of_sys_xcpt NoSuchMethodError)) = Some(Class NoSuchMethodError)"
by (auto elim: preallocatedE)
lemma preallocated_hext:
"⟦ preallocated h; h ⊴ 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: start_heap_sys_xcpts blank_def preallocated_def)
end