header {* \isaheader{Exceptions} *}
theory Exceptions imports Objects begin
definition NullPointer :: cname
where [code_inline]: "NullPointer = STR ''NullPointer''"
definition ClassCast :: cname
where [code_inline]: "ClassCast = STR ''ClassCast''"
definition OutOfMemory :: cname
where [code_inline]: "OutOfMemory = STR ''OutOfMemory''"
definition ArrayIndexOutOfBounds :: cname
where [code_inline]: "ArrayIndexOutOfBounds = STR ''ArrayIndexOutOfBounds''"
definition ArrayStore :: cname
where [code_inline]: "ArrayStore = STR ''ArrayStore''"
definition NegativeArraySize :: cname
where [code_inline]: "NegativeArraySize = STR ''NegativeArraySize''"
definition IllegalMonitorState :: cname
where [code_inline]: "IllegalMonitorState = STR ''IllegalMonitorState''"
definition IllegalThreadState :: cname
where [code_inline]: "IllegalThreadState = STR ''IllegalThreadState''"
definition sys_xcpts :: "cname set"
where [code_inline]: "sys_xcpts = {NullPointer, ClassCast, OutOfMemory, ArrayIndexOutOfBounds,
ArrayStore, NegativeArraySize, IllegalMonitorState, IllegalThreadState}"
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 = ArrayIndexOutOfBounds then 3 else
if s = ArrayStore then 4 else
if s = NegativeArraySize then 5 else
if s = IllegalMonitorState then 6 else
if s = IllegalThreadState then 7 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)
(addr_of_sys_xcpt ArrayIndexOutOfBounds \<mapsto> blank G ArrayIndexOutOfBounds)
(addr_of_sys_xcpt ArrayStore \<mapsto> blank G ArrayStore)
(addr_of_sys_xcpt NegativeArraySize \<mapsto> blank G NegativeArraySize)
(addr_of_sys_xcpt IllegalMonitorState \<mapsto> blank G IllegalMonitorState)
(addr_of_sys_xcpt IllegalThreadState \<mapsto> blank G IllegalThreadState)"
definition preallocated :: "heap => bool"
where "preallocated h ≡ ∀C ∈ sys_xcpts. ∃fs. h(addr_of_sys_xcpt C) = Some (Obj C fs)"
lemma sys_xcpts_code [code_inline]:
"sys_xcpts = set [NullPointer, ClassCast, OutOfMemory, ArrayIndexOutOfBounds, ArrayStore,
NegativeArraySize, IllegalMonitorState, IllegalThreadState]"
by(simp add: sys_xcpts_def)
section "System exceptions"
lemma [simp]:
"NullPointer ∈ sys_xcpts ∧
OutOfMemory ∈ sys_xcpts ∧
ClassCast ∈ sys_xcpts ∧
ArrayIndexOutOfBounds ∈ sys_xcpts ∧
ArrayStore ∈ sys_xcpts ∧
NegativeArraySize ∈ sys_xcpts ∧
IllegalMonitorState ∈ sys_xcpts ∧
IllegalThreadState ∈ 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 ArrayIndexOutOfBounds; P ArrayStore; P NegativeArraySize;
P IllegalMonitorState; P IllegalThreadState |] ==> P C"
by (auto simp add: sys_xcpts_def)
lemma OutOfMemory_not_Object[simp]: "OutOfMemory ≠ Object"
by(simp add: OutOfMemory_def Object_def)
lemma ClassCast_not_Object[simp]: "ClassCast ≠ Object"
by(simp add: ClassCast_def Object_def)
lemma NullPointer_not_Object[simp]: "NullPointer ≠ Object"
by(simp add: NullPointer_def Object_def)
lemma ArrayIndexOutOfBounds_not_Object[simp]: "ArrayIndexOutOfBounds ≠ Object"
by(simp add: ArrayIndexOutOfBounds_def Object_def)
lemma ArrayStore_not_Object[simp]: "ArrayStore ≠ Object"
by(simp add: ArrayStore_def Object_def)
lemma NegativeArraySize_not_Object[simp]: "NegativeArraySize ≠ Object"
by(simp add: NegativeArraySize_def Object_def)
lemma IllegalMonitorState_not_Object[simp]: "IllegalMonitorState ≠ Object"
by(simp add: IllegalMonitorState_def Object_def)
lemma IllegalThreadState_not_Object[simp]: "IllegalThreadState ≠ Object"
by(simp add: IllegalThreadState_def Object_def)
section "@{term preallocated}"
lemma preallocated_dom [simp]:
"[| preallocated h; C ∈ sys_xcpts |] ==> addr_of_sys_xcpt C ∈ dom h"
by (fastsimp simp:preallocated_def dom_def)
lemma preallocatedD:
"[| preallocated h; C ∈ sys_xcpts |]
==> ∃fs. h(addr_of_sys_xcpt C) = Some (Obj 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 (Obj 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"
apply(erule preallocatedE)
apply(auto elim: preallocatedE)
done
lemma typeof_ClassCast [simp]:
"preallocated h ==>
typeofh (Addr(addr_of_sys_xcpt ClassCast)) = Some(Class ClassCast)"
by(erule preallocatedE, auto split:heapobj.split if_splits simp add: addr_of_sys_xcpt_def preallocated_def)
lemma typeof_OutOfMemory [simp]:
"preallocated h ==> typeofh (Addr(addr_of_sys_xcpt OutOfMemory)) = Some(Class OutOfMemory)"
by(erule preallocatedE, auto split:heapobj.split if_splits simp add: addr_of_sys_xcpt_def preallocated_def)
lemma typeof_NullPointer [simp]:
"preallocated h ==> typeofh (Addr(addr_of_sys_xcpt NullPointer)) = Some(Class NullPointer)"
by(erule preallocatedE, auto split:heapobj.split if_splits simp add: addr_of_sys_xcpt_def preallocated_def)
lemma typeof_ArrayIndexOutOfBounds [simp]:
"preallocated h ==> typeofh (Addr(addr_of_sys_xcpt ArrayIndexOutOfBounds)) = Some(Class ArrayIndexOutOfBounds)"
by(erule preallocatedE, auto split:heapobj.split if_splits simp add: addr_of_sys_xcpt_def preallocated_def)
lemma typeof_ArrayStore [simp]:
"preallocated h ==> typeofh (Addr(addr_of_sys_xcpt ArrayStore)) = Some(Class ArrayStore)"
by(erule preallocatedE, auto split:heapobj.split if_splits simp add: addr_of_sys_xcpt_def preallocated_def)
lemma typeof_NegativeArraySize [simp]:
"preallocated h ==> typeofh (Addr(addr_of_sys_xcpt NegativeArraySize)) = Some(Class NegativeArraySize)"
by(erule preallocatedE, auto split:heapobj.split if_splits simp add: addr_of_sys_xcpt_def preallocated_def)
lemma typeof_IllegalMonitorState [simp]:
"preallocated h ==> typeofh (Addr(addr_of_sys_xcpt IllegalMonitorState)) = Some(Class IllegalMonitorState)"
by(erule preallocatedE, auto split:heapobj.split if_splits simp add: addr_of_sys_xcpt_def preallocated_def)
lemma typeof_IllegalThreadState [simp]:
"preallocated h ==> typeofh (Addr(addr_of_sys_xcpt IllegalThreadState)) = Some(Class IllegalThreadState)"
by(erule preallocatedE, auto split:heapobj.split if_splits simp add: addr_of_sys_xcpt_def preallocated_def)
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_upd_arr:
"[| preallocated h; h a = ⌊Arr T el⌋ |] ==> preallocated (h(a \<mapsto> Arr T el'))"
by(auto simp add: preallocated_def)
lemma addrNullPointer: "addr_of_sys_xcpt NullPointer = 0"
by (simp add: addr_of_sys_xcpt_def)
lemma addrClassCast: "addr_of_sys_xcpt ClassCast = 1"
by (simp add: addr_of_sys_xcpt_def ClassCast_def NullPointer_def)
lemma addrOutOfMemory: "addr_of_sys_xcpt OutOfMemory = 2"
by (simp add: addr_of_sys_xcpt_def ClassCast_def NullPointer_def OutOfMemory_def)
lemma addrArrayIndex: "addr_of_sys_xcpt ArrayIndexOutOfBounds = 3"
by (simp add: addr_of_sys_xcpt_def ClassCast_def NullPointer_def OutOfMemory_def ArrayIndexOutOfBounds_def)
lemma addrArrayStore: "addr_of_sys_xcpt ArrayStore = 4"
by (simp add: addr_of_sys_xcpt_def ClassCast_def NullPointer_def OutOfMemory_def ArrayIndexOutOfBounds_def ArrayStore_def)
lemma addrNegativeArray: "addr_of_sys_xcpt NegativeArraySize = 5"
by (simp add: addr_of_sys_xcpt_def ClassCast_def NullPointer_def OutOfMemory_def ArrayIndexOutOfBounds_def ArrayStore_def NegativeArraySize_def)
lemma addrIllegalMonitorState: "addr_of_sys_xcpt IllegalMonitorState = 6"
by (simp add: addr_of_sys_xcpt_def ClassCast_def NullPointer_def OutOfMemory_def ArrayIndexOutOfBounds_def ArrayStore_def NegativeArraySize_def IllegalMonitorState_def)
lemma addrIllegalThreadState: "addr_of_sys_xcpt IllegalThreadState = 7"
by (simp add: addr_of_sys_xcpt_def ClassCast_def NullPointer_def OutOfMemory_def ArrayIndexOutOfBounds_def ArrayStore_def NegativeArraySize_def IllegalMonitorState_def IllegalThreadState_def)
lemma preallocated_start:
"preallocated (start_heap P)"
apply(clarsimp simp add: preallocated_def)
apply(erule sys_xcpts_cases)
apply(simp, simp only: addrNullPointer addrClassCast addrOutOfMemory addrArrayIndex addrArrayStore addrNegativeArray addrIllegalMonitorState addrIllegalThreadState start_heap_def fun_upd_apply addr_of_sys_xcpt_def, simp only: NegativeArraySize_def NullPointer_def ClassCast_def OutOfMemory_def ArrayIndexOutOfBounds_def NegativeArraySize_def ArrayStore_def IllegalMonitorState_def IllegalThreadState_def, simp add: blank_def)+
done
end