-- JCSystem


package javacard::framework


-- PUBLIC FIELDS
--    public static final byte CLEAR_ON_DESELECT;
--    public static final byte CLEAR_ON_RESET;
--    public static final byte NOT_A_TRANSIENT_OBJECT;
--
--    
-- 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. 
-- 
-- In the context of JCSystem, there are further complications. JCSystem does  
-- not provide a piece of functionality that provides an addition to the bare  
-- JCVM and that can be understood in isolation. The parts of the system state 
-- that are represented by the variables below, can be changed by normal Java 
-- Card statements, i.e. as 'side effects' of certain virtual machine instructions. 
-- For instance, the variable activeContext may need to be changed at every method 
-- invocation. All this means that ultimately a specification of the Java Card API 
-- cannot be considered on its own, but has to be considered together with a 
-- formalisation of the Java Card language itself.
--
--    //The amount of free (i.e. unallocated) transient memory
--    private static int freeTransient;
--
--    private static byte previousContext;
--    private static byte selectedContext;
--    private static byte activeContext;
--
--    private static byte transactionDepth;
--
--    //registeredAIDs is the domain of appletTable
--    //the objects in registeredAIDs are of type AID
--    //appletTable is a partial function from AIDs to applets
--    private static Set registeredAIDs;
--    private static Map appletTable;
--
--    private static byte JCRE_CONTEXT;


context JCSystem def:
   let freeTransient: Integer
   let previousContext: JByte
   let selectedContext: JByte
   let activeContext: JByte
   let transactionDepth: JByte
   let registeredAIDs: Set
   let appletTable: (Map)
   let JCRE_CONTEXT: JByte



context JCSystem inv:
      JCSystem.NOT_A_TRANSIENT_OBJECT = 0
      and
      JCSystem.CLEAR_ON_RESET = 1 
      and
      JCSystem.CLEAR_ON_DESELECT = 2
      and
      (
         JCSystem.transactionDepth.asInt() = 0
         or
         JCSystem.transactionDepth.asInt() = 1
      )



-------- TRANSIENT MEMORY ----------------------------------------

-- static
context JCSystem::isTransient(theObj: OclAny): JByte
  pre : true
  post: result.asInt() = JCSystem.NOT_A_TRANSIENT_OBJECT
        or
        result.asInt() = JCSystem.CLEAR_ON_RESET
        or
        result.asInt() = JCSystem.CLEAR_ON_DESELECT



-- static
context JCSystem::makeTransientBooleanArray(length: JShort,
                                            event: JByte): Sequence(Boolean)
  pre : true
  post: if
        (
           length.asInt() >= 0
           and
           length.asInt() <= JCSystem.freeTransient@pre
           and
           (
              event.asInt() = JCSystem.CLEAR_ON_RESET
              or
              event.asInt() = JCSystem.CLEAR_ON_DESELECT
           )
           and
           (
              event.asInt() = JCSystem.CLEAR_ON_DESELECT
                 implies
              JCSystem.selectedContext.asInt() = JCSystem.activeContext.asInt()
           )
        )
        then
        (
           not excThrown(java::lang::Exception)
           and
           not (result = null)
           and
           result->size() = length.asInt()
           and
           result.oclIsNew()
           and
           JCSystem.isTransient(result).asInt() = event.asInt()
           and
           JCSystem.freeTransient
              = JCSystem.freeTransient@pre-length.asInt()
           and
           result->forAll(b: Boolean|b = false)
        )
        endif
        and
        if
           true
        then
        (
           not excThrown(java::lang::Exception)
           or
           (
              excThrown(java::lang::NegativeArraySizeException)
              and
              length.asInt() < 0
           )
           or
           (
              excThrown(SystemException)
              and
              (
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.ILLEGAL_VALUE
                    and
                    event.asInt() <> JCSystem.CLEAR_ON_RESET
                    and
                    event.asInt() <> JCSystem.CLEAR_ON_DESELECT
                 )
                 or
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.NO_TRANSIENT_SPACE
                    and
                    JCSystem.freeTransient < length.asInt()
                 )
                 or
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.ILLEGAL_TRANSIENT
                    and
                    event.asInt() = JCSystem.CLEAR_ON_DESELECT
                    and
                    JCSystem.selectedContext.asInt() <> JCSystem.activeContext.asInt()
                 )
              )
           )
        )
        endif




-- static
context JCSystem::makeTransientByteArray(length: JShort,
                                         event: JByte): Sequence(JByte)
  pre : true
  post: if
        (
           length.asInt() >= 0
           and
           length.asInt() <= JCSystem.freeTransient@pre
           and
           (
              event.asInt() = JCSystem.CLEAR_ON_RESET
              or
              event.asInt() = JCSystem.CLEAR_ON_DESELECT
           )
           and
           (
              event.asInt() = JCSystem.CLEAR_ON_DESELECT
                 implies
              JCSystem.selectedContext.asInt() = JCSystem.activeContext.asInt()
           )
        )
        then
        (
           not excThrown(java::lang::Exception)
           and
           not (result = null)
           and
           result->size() = length.asInt()
           and
           result.oclIsNew()
           and
           JCSystem.isTransient(result).asInt() = event.asInt()
           and
           JCSystem.freeTransient
              = JCSystem.freeTransient@pre-length.asInt()
           and
           result->forAll(b: JByte|b.asInt() = 0)
        )
        endif
        and
        if
           true
        then
        (
           not excThrown(java::lang::Exception)
           or
           (
              excThrown(java::lang::NegativeArraySizeException)
              and
              length.asInt() < 0
           )
           or
           (
              excThrown(SystemException)
              and
              (
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.ILLEGAL_VALUE
                    and
                    event.asInt() <> JCSystem.CLEAR_ON_RESET
                    and
                    event.asInt() <> JCSystem.CLEAR_ON_DESELECT
                 )
                 or
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.NO_TRANSIENT_SPACE
                    and
                    JCSystem.freeTransient < length.asInt()
                 )
                 or
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.ILLEGAL_TRANSIENT
                    and
                    event.asInt() = JCSystem.CLEAR_ON_DESELECT
                    and
                    JCSystem.selectedContext.asInt() <> JCSystem.activeContext.asInt()
                 )
              )
           )
        )
        endif




-- static
context JCSystem::makeTransientShortArray(length: JShort,
                                          event: JByte): Sequence(JShort)
  pre : true
  post: if
        (
           length.asInt() >= 0
           and
           length.asInt() <= JCSystem.freeTransient@pre
           and
           (
              event.asInt() = JCSystem.CLEAR_ON_RESET
              or
              event.asInt() = JCSystem.CLEAR_ON_DESELECT
           )
           and
           (
              event.asInt() = JCSystem.CLEAR_ON_DESELECT
                 implies
              JCSystem.selectedContext.asInt() = JCSystem.activeContext.asInt()
           )
        )
        then
        (
           not excThrown(java::lang::Exception)
           and
           not (result = null)
           and
           result->size() = length.asInt()
           and
           result.oclIsNew()
           and
           JCSystem.isTransient(result).asInt() = event.asInt()
           and
           JCSystem.freeTransient
              = JCSystem.freeTransient@pre-length.asInt()
           and
           result->forAll(s: JShort|s.asInt() = 0)
        )
        endif
        and
        if
           true
        then
        (
           not excThrown(java::lang::Exception)
           or
           (
              excThrown(java::lang::NegativeArraySizeException)
              and
              length.asInt() < 0
           )
           or
           (
              excThrown(SystemException)
              and
              (
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.ILLEGAL_VALUE
                    and
                    event.asInt() <> JCSystem.CLEAR_ON_RESET
                    and
                    event.asInt() <> JCSystem.CLEAR_ON_DESELECT
                 )
                 or
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.NO_TRANSIENT_SPACE
                    and
                    JCSystem.freeTransient < length.asInt()
                 )
                 or
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.ILLEGAL_TRANSIENT
                    and
                    event.asInt() = JCSystem.CLEAR_ON_DESELECT
                    and
                    JCSystem.selectedContext.asInt() <> JCSystem.activeContext.asInt()
                 )
              )
           )
        )
        endif



-- static
context JCSystem::makeTransientObjectArray(length: JShort,
                                           event: JByte): Sequence(Object)
  pre : true
  post: if
        (
           length.asInt() >= 0
           and
           length.asInt() <= JCSystem.freeTransient@pre
           and
           (
              event.asInt() = JCSystem.CLEAR_ON_RESET
              or
              event.asInt() = JCSystem.CLEAR_ON_DESELECT
           )
           and
           (
              event.asInt() = JCSystem.CLEAR_ON_DESELECT
                 implies
              JCSystem.selectedContext.asInt() = JCSystem.activeContext.asInt()
           )
        )
        then
        (
           not excThrown(java::lang::Exception)
           and
           not (result = null)
           and
           result->size() = length.asInt()
           and
           result.oclIsNew()
           and
           JCSystem.isTransient(result).asInt() = event.asInt()
           and
           JCSystem.freeTransient
              = JCSystem.freeTransient@pre-length.asInt()
           and
           result->forAll(o: Object|o = null)
        )
        endif
        and
        if
           true
        then
        (
           not excThrown(java::lang::Exception)
           or
           (
              excThrown(java::lang::NegativeArraySizeException)
              and
              length.asInt() < 0
           )
           or
           (
              excThrown(SystemException)
              and
              (
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.ILLEGAL_VALUE
                    and
                    event.asInt() <> JCSystem.CLEAR_ON_RESET
                    and
                    event.asInt() <> JCSystem.CLEAR_ON_DESELECT
                 )
                 or
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.NO_TRANSIENT_SPACE
                    and
                    JCSystem.freeTransient < length.asInt()
                 )
                 or
                 (
                    SystemException.systemInstance.getReason().asInt()
                       = SystemException.ILLEGAL_TRANSIENT
                    and
                    event.asInt() = JCSystem.CLEAR_ON_DESELECT
                    and
                    JCSystem.selectedContext.asInt() <> JCSystem.activeContext.asInt()
                 )
              )
           )
        )
        endif



-- static
context JCSystem::getVersion(): JShort
  pre : true
  post: result.asInt() = JCSystem.API_VERSION



-------- TRANSACTIONS ----------------------------------------

-- static
context JCSystem::beginTransaction()
  pre : true
  post: if
           JCSystem.transactionDepth.asInt@pre() = 0
        then
        (
           not excThrown(java::lang::Exception)
           and
           JCSystem.transactionDepth.asInt() = 1
        )
        endif
        and
        if
           JCSystem.transactionDepth.asInt@pre() = 1
        then
        (
           excThrown(TransactionException)
           and
           TransactionException.systemInstance.getReason().asInt()
              = TransactionException.IN_PROGRESS
        )
        endif



-- static
context JCSystem::abortTransaction()
  pre : true
  post: if
           JCSystem.transactionDepth.asInt@pre() = 1
        then
        (
           not excThrown(java::lang::Exception)
           and
           JCSystem.transactionDepth.asInt() = 0
        )
        endif
        and
        if
           JCSystem.transactionDepth.asInt@pre() = 0
        then
        (
           excThrown(TransactionException)
           and
           TransactionException.systemInstance.getReason().asInt()
              = TransactionException.NOT_IN_PROGRESS
        )
        endif



-- static
context JCSystem::commitTransaction()
  pre : true
  post: if
           JCSystem.transactionDepth.asInt@pre() = 1
        then
        (
           not excThrown(java::lang::Exception)
           and
           JCSystem.transactionDepth.asInt() = 0
        )
        endif
        and
        if
           JCSystem.transactionDepth.asInt@pre() = 0
        then
        (
           excThrown(TransactionException)
           and
           TransactionException.systemInstance.getReason().asInt()
              = TransactionException.NOT_IN_PROGRESS
        )
        endif




-- static
context JCSystem::getTransactionDepth(): JByte
  pre : true
  post: result.asInt() = JCSystem.transactionDepth.asInt()



-- static
context JCSystem::getUnusedCommitCapacity(): JShort
  pre : true
  post: result.asInt() <= JCSystem.getMaxCommitCapacity().asInt()



-- static
context JCSystem::getMaxCommitCapacity(): JShort
  pre : true
  post: true



-------- THE FIREWALL ----------------------------------------

-- static
context JCSystem::getAID(): AID
  pre : true
  post: true



-- static
context JCSystem::getPreviousContextAID(): AID
  pre : true
  post: true



-- static
context JCSystem::lookupAID(buffer: Sequence(JByte),
                            offset: JShort,
                            length: JByte): AID
  pre : true
  post: if
        (
           not (buffer = null)
           and
           offset.asInt() >= 0
           and
           length.asInt() >= 0
           and
           offset.asInt()+length.asInt() <= buffer->size()
        )
        then
        (
           not excThrown(java::lang::Exception)
           and
           (
                 not (result = null)
              implies
                 result.equals(buffer, offset, length)
           )
        )
        endif
        and
        (
           not excThrown(java::lang::Exception)
           or
           (
              excThrown(java::lang::NullPointerException)
              and
              buffer = null
           )
           or
           (
              excThrown(java::lang::ArrayIndexOutOfBoundsException)
              and
              (
                 offset.asInt() < 0
                 or
                 length.asInt() < 0
                 or
                 offset.asInt()+length.asInt() > buffer->size()
              )
           )
        )
      



-- static
context JCSystem::getAppletShareableInterfaceObject(serverAID: AID,
                                            parameter: JByte): Shareable
  pre : true
  post: if
           not (serverAID = null)
        then
           not excThrown(java::lang::Exception)
        endif
        and
        if
        (
           not (serverAID = null)
           and
           JCSystem.previousContext.asInt() = JCSystem.JCRE_CONTEXT.asInt()
           and
           JCSystem.registeredAIDs.has(serverAID)
        )
        then
        (
           not excThrown(java::lang::Exception)
           and
           result = 
              JCSystem.appletTable.apply(serverAID).oclAsType(Applet).                     
                 getShareableInterfaceObject(null, parameter)
        )
        endif
        and
        if
        (
           JCSystem.previousContext.asInt() <> JCSystem.JCRE_CONTEXT.asInt()
           and
           JCSystem.registeredAIDs.has(serverAID)
        )
        then
        (
           not excThrown(java::lang::Exception)
           and
           result = 
              JCSystem.appletTable.apply(serverAID).oclAsType(Applet).                     
                 getShareableInterfaceObject(
                    JCSystem.getPreviousContextAID(), parameter)
        )
        endif
        and
        if
        (
           not (serverAID = null)
           and
           not JCSystem.registeredAIDs.has(serverAID)
        )
        then
        (
           not excThrown(java::lang::Exception)
           and
           result = null
        )
        endif



endpackage