Theory Exceptions

Up to index of Isabelle/HOL/Jinja

theory Exceptions = Objects: 
(*  Title:      HOL/MicroJava/J/Exceptions.thy
    ID:         $Id: Exceptions.html 1910 2004-05-19 04:46:04Z kleing $
    Author:     Gerwin Klein, Martin Strecker
    Copyright   2002 Technische Universitaet Muenchen
*)

header {* \isaheader{Exceptions} *}

theory Exceptions = Objects:

constdefs
  NullPointer :: cname
  "NullPointer ≡ ''NullPointer''"

  ClassCast :: cname
  "ClassCast ≡ ''ClassCast''"

  OutOfMemory :: cname
  "OutOfMemory ≡ ''OutOfMemory''"

  sys_xcpts :: "cname set"
  "sys_xcpts  ≡  {NullPointer, ClassCast, OutOfMemory}"

  addr_of_sys_xcpt :: "cname => addr"
  "addr_of_sys_xcpt s ≡ if s = NullPointer then 0 else
                        if s = ClassCast then 1 else
                        if s = OutOfMemory then 2 else arbitrary"

  start_heap :: "'c prog => heap"
  "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)"

  preallocated :: "heap => bool"
  "preallocated h ≡ ∀C ∈ sys_xcpts. ∃fs. h(addr_of_sys_xcpt C) = Some (C,fs)"


section "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)(*>*)


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 (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(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 ==> typeofh (Addr(addr_of_sys_xcpt ClassCast)) = Some(Class ClassCast)" 
(*<*)by (auto elim: preallocatedE)(*>*)


lemma typeof_OutOfMemory [simp]:
  "preallocated h ==> typeofh (Addr(addr_of_sys_xcpt OutOfMemory)) = Some(Class OutOfMemory)" 
(*<*)by (auto elim: preallocatedE)(*>*)


lemma typeof_NullPointer [simp]:
  "preallocated h ==> typeofh (Addr(addr_of_sys_xcpt NullPointer)) = Some(Class NullPointer)" 
(*<*)by (auto elim: preallocatedE)(*>*)


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_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)(*>*)


end

System exceptions

lemma 

  NullPointer : sys_xcpts & OutOfMemory : sys_xcpts & ClassCast : sys_xcpts

lemma sys_xcpts_cases: 

  [| C : sys_xcpts; P NullPointer; P OutOfMemory; P ClassCast |] ==> P C

@{term preallocated}

lemma preallocated_dom: 

  [| preallocated h; C : sys_xcpts |] ==> addr_of_sys_xcpt C : dom h

lemma preallocatedD: 

  [| preallocated h; C : sys_xcpts |]
  ==> EX fs. h (addr_of_sys_xcpt C) = ⌊(C, fs)⌋

lemma preallocatedE: 

  [| preallocated h; C : sys_xcpts;
     !!fs. h (addr_of_sys_xcpt C) = ⌊(C, fs)⌋ ==> P h C |]
  ==> P h C

lemma cname_of_xcp: 

  [| preallocated h; C : sys_xcpts |] ==> cname_of h (addr_of_sys_xcpt C) = C

lemma typeof_ClassCast: 

  preallocated h
  ==> typeofh (Addr (addr_of_sys_xcpt ClassCast)) = ⌊Class ClassCast⌋

lemma typeof_OutOfMemory: 

  preallocated h
  ==> typeofh (Addr (addr_of_sys_xcpt OutOfMemory)) = ⌊Class OutOfMemory⌋

lemma typeof_NullPointer: 

  preallocated h
  ==> typeofh (Addr (addr_of_sys_xcpt NullPointer)) = ⌊Class NullPointer⌋

lemma preallocated_hext: 

  [| preallocated h; h \<unlhd> h' |] ==> preallocated h'

lemmas preallocated_upd_obj: 

  [| preallocated h; h a_1 = ⌊(C_1, fs_1)⌋ |]
  ==> preallocated (h(a_1 |-> (C_1, fs'_1)))

lemmas preallocated_new: 

  [| preallocated h; h a_1 = None |] ==> preallocated (h(a_1 |-> x_1))

lemma preallocated_start: 

  preallocated (start_heap P)