Theory 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