Theory Exceptions

(*  Title:       CoreC++
    Author:      Gerwin Klein, Martin Strecker, Daniel Wasserrab
    Maintainer:  Daniel Wasserrab <wasserra at fmi.uni-passau.de>
*)

section ‹Exceptions›

theory Exceptions imports Objects begin

subsection ‹Exceptions›


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 :: "prog ⇒ heap" where
  "start_heap P ≡ Map.empty (addr_of_sys_xcpt NullPointer ↦ blank P NullPointer,
                        addr_of_sys_xcpt ClassCast ↦ blank P ClassCast,
                        addr_of_sys_xcpt OutOfMemory ↦ blank P OutOfMemory)"

definition preallocated :: "heap ⇒ bool" where
  "preallocated h ≡ ∀C ∈ sys_xcpts. ∃S. h (addr_of_sys_xcpt C) = Some (C,S)"


subsection "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)


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 ⟧ ⟹ ∃S. h (addr_of_sys_xcpt C) = Some (C,S)"
by(auto simp add: preallocated_def sys_xcpts_def)


lemma preallocatedE [elim?]:
  "⟦ preallocated h;  C ∈ sys_xcpts; ⋀S. h (addr_of_sys_xcpt C) = Some(C,S) ⟹ 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 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)



subsection "@{term start_heap}"

lemma start_Subobj:
"⟦start_heap P a = Some(C, S); (Cs,fs) ∈ S⟧ ⟹ Subobjs P C Cs"
by (fastforce elim:init_obj.cases simp:start_heap_def blank_def 
                                    fun_upd_apply split:if_split_asm)

lemma start_SuboSet:
"⟦start_heap P a = Some(C, S); Subobjs P C Cs⟧ ⟹ ∃fs. (Cs,fs) ∈ S"
by (fastforce intro:init_obj.intros simp:start_heap_def blank_def
                split:if_split_asm)

lemma start_init_obj: "start_heap P a = Some(C,S) ⟹ S = Collect (init_obj P C)"
by (auto simp:start_heap_def blank_def split:if_split_asm)

lemma start_subobj:
  "⟦start_heap P a = Some(C, S); ∃fs. (Cs, fs) ∈ S⟧ ⟹ Subobjs P C Cs"
by (fastforce elim:init_obj.cases simp:start_heap_def blank_def
                  split:if_split_asm)

end