Theory JinjaDCI.SystemClasses

(*  Title:     JinjaDCI/Common/SystemClasses.thy

    Author:     Gerwin Klein, Susannah Mansky
    Copyright   2002 Technische Universitaet Muenchen, 2019-20 UIUC
    
    Based on the Jinja theory Common/SystemClasses.thy by Gerwin Klein
*)

section ‹ System Classes ›

theory SystemClasses
imports Decl Exceptions
begin

text ‹
  This theory provides definitions for the @{text Object} class,
  and the system exceptions.
›

definition ObjectC :: "'m cdecl"
where
  "ObjectC  (Object, (undefined,[],[]))"

definition NullPointerC :: "'m cdecl"
where
  "NullPointerC  (NullPointer, (Object,[],[]))"

definition ClassCastC :: "'m cdecl"
where
  "ClassCastC  (ClassCast, (Object,[],[]))"

definition OutOfMemoryC :: "'m cdecl"
where
  "OutOfMemoryC  (OutOfMemory, (Object,[],[]))"

definition NoClassDefFoundC :: "'m cdecl"
where
  "NoClassDefFoundC  (NoClassDefFoundError, (Object,[],[]))"

definition IncompatibleClassChangeC :: "'m cdecl"
where
  "IncompatibleClassChangeC  (IncompatibleClassChangeError, (Object,[],[]))"

definition NoSuchFieldC :: "'m cdecl"
where
  "NoSuchFieldC  (NoSuchFieldError, (Object,[],[]))"

definition NoSuchMethodC :: "'m cdecl"
where
  "NoSuchMethodC  (NoSuchMethodError, (Object,[],[]))"

definition SystemClasses :: "'m cdecl list"
where
  "SystemClasses  [ObjectC, NullPointerC, ClassCastC, OutOfMemoryC, NoClassDefFoundC,
  IncompatibleClassChangeC, NoSuchFieldC, NoSuchMethodC]"

end