01: package javacard.framework;
02:
03: public class TransactionException extends CardRuntimeException {
04:
05: /*@ static invariant \is_initialized(TransactionException); @*/
06: /*@ static invariant _systemInstance != null; @*/
07: private static TransactionException _systemInstance;
08:
09: public final static short IN_PROGRESS = (short) 1;
10: public final static short NOT_IN_PROGRESS = (short) 2;
11: public final static short BUFFER_FULL = (short) 3;
12: public final static short INTERNAL_FAILURE = (short) 4;
13:
14: /*@ exceptional_behavior
15: requires true;
16: signals (TransactionException te) te == _systemInstance && te._reason[0] == reason ;
17: assignable _systemInstance._reason[0] ;
18: @*/
19: public static void throwIt(short reason)
20: throws TransactionException {
21: _systemInstance.setReason(reason);
22: throw _systemInstance;
23: }
24:
25: }
|