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