-- SystemException


package javacard::framework


-- PRIVATE FIELDS
-- The variables below are not part of the informal specification given by SUN.
-- They are given a name, a type and a meaning that reflects a part of the 
-- system state, in order to be able to make a meaningful specification. An 
-- implementer of this class is naturally free to represent the system state 
-- with the help of other class and instance fields.
--
--   private static SystemException systemInstance;
--   private short reason;


context SystemException def:
   let systemInstance: SystemException
   let reason: JShort


context SystemException
   inv: SystemException.systemInstance <> null


context SystemException::SystemException(reason: JShort)
  pre : true
  post: not excThrown(java::lang::Exception)
        and
        self.getReason().asInt() = reason.asInt()
        

-- static
context SystemException::throwIt(reason: JShort)
  pre : true
  post: excThrown(SystemException)
        and
        SystemException.systemInstance.getReason().asInt() = reason.asInt()


endpackage