-- APDUException


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 APDUException systemInstance;
--   private short reason;


context APDUException def:
   let systemInstance: APDUException  -- static
   let reason: JShort


context APDUException
   inv: APDUException.systemInstance <> null


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


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


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


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


endpackage