-- OCL spec for javacard.framework.TransactionException


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


context TransactionException def:
   let systemInstance: TransactionException
   let reason: JShort


context TransactionException
   inv: TransactionException.systemInstance <> null


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

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


endpackage