-- CardRuntimeException

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


context CardRuntimeException def:
   let systemInstance: CardRuntimeException
   let reason: JShort


context CardRuntimeException
   inv: CardRuntimeException.systemInstance <> null


context CardRuntimeException::CardRuntimeException(reason: JShort)
  pre : true
  post: self.getReason().asInt() = reason.asInt()


context CardRuntimeException::getReason(): JShort
  pre : true
  post: result.asInt() = self.reason.asInt()


context CardRuntimeException::setReason(reason: JShort)
  pre : true
  post: self.getReason().asInt() = reason.asInt()


context CardRuntimeException::throwIt(reason: JShort)
  pre : true
  post: excThrown(CardRuntimeException)
        and
        self.systemInstance.getReason().asInt() = reason.asInt()


endpackage