-- APDU


package javacard::framework


-- PUBLIC FIELDS:
--    public static final byte STATE_INITIAL;
--    public static final byte STATE_PARTIAL_INCOMING;
--    public static final byte STATE_FULL_INCOMING;
--    public static final byte STATE_OUTGOING;
--    public static final byte STATE_OUTGOING_LENGTH_KNOWN;
--    public static final byte STATE_PARTIAL_OUTGOING;
--    public static final byte STATE_FULL_OUTGOING;
--    public static final byte STATE_ERROR_NO_T0_GETRESPONSE;
--    public static final byte STATE_ERROR_T1_IFD_ABORT;
--    public static final byte STATE_ERROR_IO;
--    public static final byte STATE_ERROR_NO_T0_REISSUE;	
--    public static final byte PROTOCOL_MEDIA_MASK;
--    public static final byte PROTOCOL_TYPE_MASK;
--    public static final byte PROTOCOL_T0; 
--    public static final byte PROTOCOL_T1; 
--    public static final byte PROTOCOL_MEDIA_DEFAULT;
--    public static final byte PROTOCOL_MEDIA_CONTACTLESS_TYPE_A
--    public static final byte PROTOCOL_MEDIA_CONTACTLESS_TYPE_B;
--    public static final byte PROTOCOL_MEDIA_USB;
--
--
-- 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.
--
--    //model fields in the JML spec
--    private short Lc; // incoming command length
--    private short Lr; // response length
--    private short Le; // terminal expected length
--    //////////////////////////////
--   
--    private static final short BUFFERSIZE = 37;
--    private byte[] buffer;
--    private byte APDU_state;


context APDU def:
   let Lc: JShort
   let Lr: JShort
   let Le: JShort
   let BUFFERSIZE: JShort  -- static final
   let buffer: Sequence(JByte)
   let APDU_state: JByte


context APDU inv:
   self.buffer <> null
   and
   APDU.BUFFER_SIZE.asInt() >= 37
   and
   self.buffer->size() = APDU.BUFFER_SIZE.asInt()
   and
   APDU.PROTOCOL_T0 = 0
   and
   APDU.PROTOCOL_T1 = 1
   and
   self.getCurrentState().asInt() >= APDU.STATE_INITIAL
   and
   self.getCurrentState().asInt() <= APDU.STATE_FULL_OUTGOING
   and
   self.Lc.asInt() >= 0
   and
   self.Lc.asInt() < 256
   and
   self.Lr.asInt() >= 0
   and
   self.Lr.asInt() <= 256
   and
   self.Le.asInt() >= 0
   and
   self.Le.asInt() <= 256



context APDU::getBuffer(): Sequence(JByte)
  pre : true
  post: result = self.buffer


-- static
context APDU::getInBlockSize(): JShort
  pre : true
  post: result.asInt() > 0
        and
        result.asInt() <= APDU.BUFFERSIZE.asInt()
        and
        (
              self.getProtocol().asInt() = APDU.PROTOCOL_T0
           implies
              result.asInt() = 1
        )


-- static
context APDU::getOutBlockSize(): JShort
  pre : true
  post: result.asInt() > 0
        and
        result.asInt() <= APDU.BUFFERSIZE.asInt()
        and
        (
              self.getProtocol().asInt() = APDU.PROTOCOL_T0
           implies
              result.asInt() = 258
        )


-- static
context APDU::getProtocol(): JByte
  pre : true
  post: result.asInt() = APDU.PROTOCOL_T0
        or
        result.asInt() = APDU.PROTOCOL_T1


context APDU::getNAD(): JByte
  pre : true
  post:    self.getProtocol().asInt() = APDU.PROTOCOL_T0
        implies
           result.asInt() = 0



context APDU::setIncomingAndReceive(): JShort
  pre : self.APDU_state = 1
        -- and
        -- 'self.Lc bytes still to be received'
  post: (
           not excThrown(java::lang::Exception)
           and
           self.APDU_state = 2
           and
           result.asInt() >= 0
           and
           result.asInt() <= self.Lc@pre
           and
           self.Lc = self.Lc@pre - result.asInt()
           and
           result.asInt()+5 <= APDU.BUFFERSIZE
           -- and
           -- 'self.Lc bytes still to be received'
           -- and
           -- 'data received in self.buffer->subSequence(6, 
           --                                  6+result.asInt()-1)'
        )
        or
        (
           excThrown(APDUException)
           and
           (
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.IO_ERROR
              or
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.T1_IFD_ABORT
           )
        )



context APDU::receiveBytes(bOff: JShort): JShort
  pre : self.getCurrentState().asInt() = APDU.STATE_PARTIAL_INCOMING
        and
        bOff.asInt() >= 0
        and
        bOff.asInt()+self.getInBlockSize().asInt() 
           <= APDU.BUFFERSIZE.asInt()
        -- and
        -- 'self.Lc.asInt() bytes still to be received'
  post: (
           not excThrown(java::lang::Exception)
           and
           (
              self.getCurrentState().asInt() = APDU.STATE_PARTIAL_INCOMING
              or
              self.getCurrentState().asInt() = APDU.STATE_FULL_INCOMING
           )
           and
           result.asInt() >= 0
           and
           result.asInt() <= self.Lc@pre.asInt()
           and
           self.Lc.asInt() = self.Lc@pre.asInt() - result.asInt()
           and
           result.asInt()+bOff.asInt() <= APDU.BUFFERSIZE.asInt()
           -- and
           -- 'self.Lc.asInt() bytes still to be received'
           -- and
           -- 'data received in self.buffer->subSequence(bOff.asInt()+1, 
           --                            bOff.asInt()+1+result.asInt()-1)'
        )
        or
        (
           excThrown(APDUException)
           (
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.IO_ERROR
              or
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.T1_IFD_ABORT
           )
        )



context APDU::setOutgoing(): JShort
  pre : self.getCurrentState().asInt() = APDU::STATE_INITIAL
        or
        (
           self.getCurrentState().asInt() = APDU::STATE_FULL_INCOMING
           and
           self.Lc.asInt() = 0
        )
  post: (
           not excThrown(java::lang::Exception)
           and
           self.getCurrentState().asInt() = APDU::STATE_OUTGOING
           and
           result.asInt() = self.Le.asInt()
           -- and
           -- 'self.Le.asInt() is the terminal expected response length'
        )
        or
        (
           excThrown(APDUException)
           and
           APDUException.systemInstance.getReason().asInt()
              = APDUException.IO_ERROR
        )



context APDU::setOutgoingNoChaining(): JShort
  pre : self.getCurrentState().asInt() = APDU.STATE_INITIAL
        or
        (
           self.getCurrentState().asInt() = APDU.STATE_FULL_INCOMING
           and
           self.Lc.asInt() = 0
        )
  post: (
           not excThrown(java::lang::Exception)
           and
           self.getCurrentState().asInt() = APDU::STATE_OUTGOING
           and
           result.asInt() = self.Le.asInt()
           -- and
           -- 'self.Le.asInt() is the terminal expected response length'
        )
        or
        (
           excThrown(APDUException)
           and
           APDUException.systemInstance.getReason().asInt()
              = APDUException.IO_ERROR
        )



context APDU::setOutgoingLength(len: JShort)
  pre : (
           self.getCurrentState().asInt() = APDU.STATE_OUTGOING
           and
           len.asInt() >= 0
           and
           len.asInt() <= 256
        )
  post: (
           not excThrown(java::lang::Exception)
           and
           self.getCurrentState().asInt() 
              = APDU.STATE_OUTGOING_LENGTH_KNOWN
           and
           self.Lr.asInt() = len.asInt()
           -- and
           -- 'self.Lr.asInt() bytes will be sent'
        )
        or
        (
           excThrown(APDUException)
           and
           APDUException.systemInstance.getReason().asInt()
              = APDUException.IO_ERROR
        )



context APDU::sendBytes(bOff: JShort, len: JShort)
  pre : (
           self.getCurrentState().asInt() 
              = APDU::STATE_OUTGOING_LENGTH_KNOWN
           or
           self.getCurrentState().asInt() = APDU.STATE_PARTIAL_OUTGOING
        )
        and
        len.asInt() >= 0
        and
        len.asInt() <= self.Lr.asInt()
        and
        bOff.asInt()+len.asInt() <= APDU.BUFFERSIZE.asInt()
  post: (
           not excThrown(java::lang::Exception)
           and
           (
              self.getCurrentState().asInt() 
                 = APDU.STATE_PARTIAL_OUTGOING
              or
              self.getCurrentState().asInt() = APDU.STATE_FULL_OUTGOING
           )
           and
           self.Lr.asInt() = self.Lr@pre.asInt()-len.asInt()
           -- and
           -- (
           --       self.Lr.asInt() >= 0
           --    implies
           --       'self.buffer->subSequence(bOff.asInt()+1, 
           --        bOff.asInt()+1+len.asInt()-1) sent'
           -- )
           -- and
           -- (
           --       self.Lr.asInt() = 0
           --    implies
           --       'self.buffer->subSequence(bOff.asInt()+1, 
           --        bOff.asInt()+1+len.asInt()-1) will
           --        be sent later! Namely at end of current 
           --                    process invocation.
           --        so self.buffer->subSequence(bOff.asInt()+1, 
           --        bOff.asInt()+1+len.asInt()-1) shouldn't be altered.'
           -- )
           -- and
           -- 'self.Lr.asInt() bytes still to be sent'
        )
        or
        (
           excThrown(APDUException)
           and
           (
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.ILLEGAL_USE
              or
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.IO_ERROR
              or
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.NO_T0_GETRESPONSE
              or
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.T1_IFD_ABORT
              or
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.NO_T0_REISSUE
              or
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.BUFFER_BOUNDS
           )
        )



context APDU::sendBytesLong(outData: Sequence(JByte), 
                            bOff: JShort, 
                            len: JShort)
  pre : (
           self.getCurrentState().asInt() 
              = APDU.STATE_OUTGOING_LENGTH_KNOWN
           or
           self.getCurrentState().asInt() = APDU.STATE_PARTIAL_OUTGOING
        )
        and
        len.asInt() >= 0
        and
        len.asInt() <= self.Lr.asInt()
        and
        bOff.asInt()+len.asInt() <= outData->size()
  post: (
           not excThrown(java::lang::Exception)
           and
           (
              self.getCurrentState().asInt() 
                 = APDU.STATE_PARTIAL_OUTGOING
              or
              self.getCurrentState().asInt() = APDU.STATE_FULL_OUTGOING
           )
           and
           self.Lr.asInt() = self.Lr@pre.asInt()-len.asInt()
           -- and
           -- (
           --       self.Lr.asInt() >= 0
           --    implies
           --       'outData->subSequence(bOff.asInt()+1, 
           --        bOff.asInt()+1+len.asInt()-1) sent'
           -- )
           -- and
           -- (
           --       self.Lr.asInt() = 0
           --    implies
           --       'outData->subSequence(bOff.asInt()+1, 
           --        bOff.asInt()+1+len.asInt()-1) will
           --        be sent later! Namely at end of current 
           --                                   process invocation.
           --        so buffer[*] shouldn't be altered.'
           -- )
           -- and
           -- 'self.Lr.asInt() bytes still to be sent'
        )
        or
        (
           excThrown(APDUException)
           and
           (
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.ILLEGAL_USE
              or
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.IO_ERROR
              or
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.NO_T0_GETRESPONSE
              or
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.T1_IFD_ABORT
              or
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.NO_T0_REISSUE
              or
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.BUFFER_BOUNDS
           )
        )
        or
        (
           excThrown(java::lang::SecurityException)
           -- and
           -- 'outData not accesible in callers context'
        )



context APDU::setOutgoingAndSend(bOff: JShort, len: JShort)
  pre : self.getCurrentState().asInt() = APDU.STATE_INITIAL
        or
        (
           self.getCurrentState().asInt() = APDU.STATE_FULL_INCOMING
           and
           self.Lc.asInt() = 0
        )
        and
        bOff.asInt() >= 0
        and
        len.asInt() >= 0
        and
        bOff.asInt()+len.asInt() <= APDU.BUFFERSIZE.asInt()
  post: (
           not excThrown(java::lang::Exception)
           and
           self.getCurrentState().asInt() = APDU.STATE_FULL_OUTGOING
           and
           self.Lr.asInt() = 0
           -- and
           -- 'self.buffer->subSequence(bOff.asInt()+1, 
           --  bOff.asInt()+1+len.asInt()-1) sent'
        )
        or
        (
           excThrown(APDUException)
           and
           (
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.ILLEGAL_USE
              or
              APDUException.systemInstance.getReason().asInt()
                 = APDUException.IO_ERROR
           )
        )



context APDU::getCurrentState(): JByte
  pre : true
  post: result.asInt() = self.APDU_state.asInt()



-- static
context APDU::getCurrentAPDU(): APDU
  pre : true
  post: true



-- static
context APDU::getCurrentAPDUBuffer(): Sequence(JByte)
  pre : true
  post: true



-- static
context APDU::getCLAChannel(): JByte
  pre : true
  post: true



-- static
context APDU::waitExtension()
  pre : true
  post: true
        


endpackage