-- ISOException


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


context ISOException def:
   let systemInstance: ISOException
   let reason: JShort


context ISOException
   inv: ISOException.systemInstance <> null


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


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


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


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


endpackage