-- CryptoException


package javacard::security


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


context CryptoException def:
   let systemInstance: CryptoException
   let reason: JShort


context CryptoException
   inv: CryptoException.systemInstance <> null


-- In the JML spec for some reason just:
-- context CryptoException::CryptoException(reason: JShort)
--   pre : true
--   post: true

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

-- In the JML spec for some reason just:
-- context CryptoException::throwIt(reason: JShort)
--   pre : true
--   post: excThrown(CryptoException)
--
-- static         
context CryptoException::throwIt(reason: JShort)
  pre : true
  post: excThrown(CryptoException)
        and
        self.systemInstance.reason.asInt() = reason.asInt()


endpackage