-- CardException


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


context CardException def:
   let systemInstance: CardException
   let reason: JShort


context CardException
   inv: CardException.systemInstance <> null


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


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


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


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


endpackage