Theory SystemClasses

Up to index of Isabelle/HOL/arrays

(*  Title:      HOL/MicroJava/J/SystemClasses.thy
    ID:         $Id: SystemClasses.html,v 1.1 2002/11/28 16:11:18 kleing Exp $
    Author:     Gerwin Klein
    Copyright   2002 Technische Universitaet Muenchen
*)

header {* \isaheader{System Classes} *}

theory SystemClasses = Decl:

text {*
  This theory provides definitions for the @{text Object} class,
  and the system exceptions. It leaves methods empty (to be instantiated
  later).
*}

constdefs
  ObjectC_decl :: "'c mdecl list \<Rightarrow> 'c cdecl"
  "ObjectC_decl ms \<equiv> (Object, (arbitrary,[],ms))"

  NullPointerC_decl :: "'c mdecl list \<Rightarrow> 'c cdecl"
  "NullPointerC_decl ms \<equiv> (Xcpt NullPointer, (Object,[],ms))"

  ClassCastC_decl :: "'c mdecl list \<Rightarrow> 'c cdecl"
  "ClassCastC_decl ms \<equiv> (Xcpt ClassCast, (Object,[],ms))"

  OutOfMemoryC_decl :: "'c mdecl list \<Rightarrow> 'c cdecl"
  "OutOfMemoryC_decl ms \<equiv> (Xcpt OutOfMemory, (Object,[],ms))"
  
  ArrayIndexOutOfBoundsC_decl :: "'c mdecl list \<Rightarrow> 'c cdecl"
  "ArrayIndexOutOfBoundsC_decl ms \<equiv> (Xcpt ArrayIndexOutOfBounds, (Object,[],ms))"

  NegativeArraySizeC_decl :: "'c mdecl list \<Rightarrow> 'c cdecl"
  "NegativeArraySizeC_decl ms \<equiv> (Xcpt NegativeArraySize, (Object,[],ms))"

  ArrayStoreC_decl :: "'c mdecl list \<Rightarrow> 'c cdecl"
  "ArrayStoreC_decl ms \<equiv> (Xcpt ArrayStore, (Object,[],ms))"

  SystemClasses :: "cname list"
  "SystemClasses \<equiv> [Object, Xcpt NullPointer, Xcpt ClassCast, Xcpt OutOfMemory, 
                    Xcpt ArrayIndexOutOfBounds, Xcpt NegativeArraySize,
                    Xcpt ArrayStore]"


lemmas SystemClass_decl_defs = ObjectC_decl_def NullPointerC_decl_def 
                               ClassCastC_decl_def OutOfMemoryC_decl_def
                               ArrayIndexOutOfBoundsC_decl_def 
                               NegativeArraySizeC_decl_def
                               ArrayStoreC_decl_def

end

lemmas SystemClass_decl_defs:

  ObjectC_decl ms == (Object, arbitrary, [], ms)

  NullPointerC_decl ms == (Xcpt NullPointer, Object, [], ms)

  ClassCastC_decl ms == (Xcpt ClassCast, Object, [], ms)

  OutOfMemoryC_decl ms == (Xcpt OutOfMemory, Object, [], ms)

  ArrayIndexOutOfBoundsC_decl ms == (Xcpt ArrayIndexOutOfBounds, Object, [], ms)

  NegativeArraySizeC_decl ms == (Xcpt NegativeArraySize, Object, [], ms)

  ArrayStoreC_decl ms == (Xcpt ArrayStore, Object, [], ms)