Theory Exceptions
section ‹Exceptions›
theory Exceptions
imports
Value
begin
definition NullPointer :: cname
where [code_unfold]: "NullPointer = STR ''java/lang/NullPointerException''"
definition ClassCast :: cname
where [code_unfold]: "ClassCast = STR ''java/lang/ClassCastException''"
definition OutOfMemory :: cname
where [code_unfold]: "OutOfMemory = STR ''java/lang/OutOfMemoryError''"
definition ArrayIndexOutOfBounds :: cname
where [code_unfold]: "ArrayIndexOutOfBounds = STR ''java/lang/ArrayIndexOutOfBoundsException''"
definition ArrayStore :: cname
where [code_unfold]: "ArrayStore = STR ''java/lang/ArrayStoreException''"
definition NegativeArraySize :: cname
where [code_unfold]: "NegativeArraySize = STR ''java/lang/NegativeArraySizeException''"
definition ArithmeticException :: cname
where [code_unfold]: "ArithmeticException = STR ''java/lang/ArithmeticException''"
definition IllegalMonitorState :: cname
where [code_unfold]: "IllegalMonitorState = STR ''java/lang/IllegalMonitorStateException''"
definition IllegalThreadState :: cname
where [code_unfold]: "IllegalThreadState = STR ''java/lang/IllegalThreadStateException''"
definition InterruptedException :: cname
where [code_unfold]: "InterruptedException = STR ''java/lang/InterruptedException''"
definition sys_xcpts_list :: "cname list"
where
"sys_xcpts_list =
[NullPointer, ClassCast, OutOfMemory, ArrayIndexOutOfBounds, ArrayStore, NegativeArraySize, ArithmeticException,
IllegalMonitorState, IllegalThreadState, InterruptedException]"
definition sys_xcpts :: "cname set"
where [code_unfold]: "sys_xcpts = set sys_xcpts_list"
definition wf_syscls :: "'m prog ⇒ bool"
where "wf_syscls P ≡ (∀C ∈ {Object, Throwable, Thread}. is_class P C) ∧ (∀C ∈ sys_xcpts. P ⊢ C ≼⇧* Throwable)"
subsection "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 ∧
InterruptedException ∈ sys_xcpts ∧
ArithmeticException ∈ sys_xcpts"
by(simp add: sys_xcpts_def sys_xcpts_list_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 ArithmeticException;
P IllegalMonitorState; P IllegalThreadState; P InterruptedException ⟧
⟹ P C"
by (auto simp add: sys_xcpts_def sys_xcpts_list_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 ArithmeticException_not_Object[simp]: "ArithmeticException ≠ Object"
by(simp add: ArithmeticException_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)
lemma InterruptedException_not_Object[simp]: "InterruptedException ≠ Object"
by(simp add: InterruptedException_def Object_def)
lemma sys_xcpts_neqs_aux:
"NullPointer ≠ ClassCast" "NullPointer ≠ OutOfMemory" "NullPointer ≠ ArrayIndexOutOfBounds"
"NullPointer ≠ ArrayStore" "NullPointer ≠ NegativeArraySize" "NullPointer ≠ IllegalMonitorState"
"NullPointer ≠ IllegalThreadState" "NullPointer ≠ InterruptedException" "NullPointer ≠ ArithmeticException"
"ClassCast ≠ OutOfMemory" "ClassCast ≠ ArrayIndexOutOfBounds"
"ClassCast ≠ ArrayStore" "ClassCast ≠ NegativeArraySize" "ClassCast ≠ IllegalMonitorState"
"ClassCast ≠ IllegalThreadState" "ClassCast ≠ InterruptedException" "ClassCast ≠ ArithmeticException"
"OutOfMemory ≠ ArrayIndexOutOfBounds"
"OutOfMemory ≠ ArrayStore" "OutOfMemory ≠ NegativeArraySize" "OutOfMemory ≠ IllegalMonitorState"
"OutOfMemory ≠ IllegalThreadState" "OutOfMemory ≠ InterruptedException"
"OutOfMemory ≠ ArithmeticException"
"ArrayIndexOutOfBounds ≠ ArrayStore" "ArrayIndexOutOfBounds ≠ NegativeArraySize" "ArrayIndexOutOfBounds ≠ IllegalMonitorState"
"ArrayIndexOutOfBounds ≠ IllegalThreadState" "ArrayIndexOutOfBounds ≠ InterruptedException" "ArrayIndexOutOfBounds ≠ ArithmeticException"
"ArrayStore ≠ NegativeArraySize" "ArrayStore ≠ IllegalMonitorState"
"ArrayStore ≠ IllegalThreadState" "ArrayStore ≠ InterruptedException"
"ArrayStore ≠ ArithmeticException"
"NegativeArraySize ≠ IllegalMonitorState"
"NegativeArraySize ≠ IllegalThreadState" "NegativeArraySize ≠ InterruptedException"
"NegativeArraySize ≠ ArithmeticException"
"IllegalMonitorState ≠ IllegalThreadState" "IllegalMonitorState ≠ InterruptedException"
"IllegalMonitorState ≠ ArithmeticException"
"IllegalThreadState ≠ InterruptedException"
"IllegalThreadState ≠ ArithmeticException"
"InterruptedException ≠ ArithmeticException"
by(simp_all add: NullPointer_def ClassCast_def OutOfMemory_def ArrayIndexOutOfBounds_def ArrayStore_def NegativeArraySize_def IllegalMonitorState_def IllegalThreadState_def InterruptedException_def ArithmeticException_def)
lemmas sys_xcpts_neqs = sys_xcpts_neqs_aux sys_xcpts_neqs_aux[symmetric]
lemma Thread_neq_sys_xcpts_aux:
"Thread ≠ NullPointer"
"Thread ≠ ClassCast"
"Thread ≠ OutOfMemory"
"Thread ≠ ArrayIndexOutOfBounds"
"Thread ≠ ArrayStore"
"Thread ≠ NegativeArraySize"
"Thread ≠ ArithmeticException"
"Thread ≠ IllegalMonitorState"
"Thread ≠ IllegalThreadState"
"Thread ≠ InterruptedException"
by(simp_all add: Thread_def NullPointer_def ClassCast_def OutOfMemory_def ArrayIndexOutOfBounds_def ArrayStore_def NegativeArraySize_def IllegalMonitorState_def IllegalThreadState_def InterruptedException_def ArithmeticException_def)
lemmas Thread_neq_sys_xcpts = Thread_neq_sys_xcpts_aux Thread_neq_sys_xcpts_aux[symmetric]
subsection ‹Well-formedness for system classes and exceptions›
lemma
assumes "wf_syscls P"
shows wf_syscls_class_Object: "∃C fs ms. class P Object = Some (C,fs,ms)"
and wf_syscls_class_Thread: "∃C fs ms. class P Thread = Some (C,fs,ms)"
using assms
by(auto simp: map_of_SomeI wf_syscls_def is_class_def)
lemma [simp]:
assumes "wf_syscls P"
shows wf_syscls_is_class_Object: "is_class P Object"
and wf_syscls_is_class_Thread: "is_class P Thread"
using assms by(simp_all add: is_class_def wf_syscls_class_Object wf_syscls_class_Thread)
lemma wf_syscls_xcpt_subcls_Throwable:
"⟦ C ∈ sys_xcpts; wf_syscls P ⟧ ⟹ P ⊢ C ≼⇧* Throwable"
by(simp add: wf_syscls_def is_class_def class_def)
lemma wf_syscls_is_class_Throwable:
"wf_syscls P ⟹ is_class P Throwable"
by(auto simp add: wf_syscls_def is_class_def class_def map_of_SomeI)
lemma wf_syscls_is_class_sub_Throwable:
"⟦ wf_syscls P; P ⊢ C ≼⇧* Throwable ⟧ ⟹ is_class P C"
by(erule subcls_is_class1)(erule wf_syscls_is_class_Throwable)
lemma wf_syscls_is_class_xcpt:
"⟦ C ∈ sys_xcpts; wf_syscls P ⟧ ⟹ is_class P C"
by(blast intro: wf_syscls_is_class_sub_Throwable wf_syscls_xcpt_subcls_Throwable)
lemma wf_syscls_code [code]:
"wf_syscls P ⟷
(∀C ∈ set [Object, Throwable, Thread]. is_class P C) ∧ (∀C ∈ sys_xcpts. P ⊢ C ≼⇧* Throwable)"
by(simp only: wf_syscls_def) simp
end