-- AID


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.
--
--    byte[] theAID;


context AID def:
   let theAID: Sequence(JByte)


context AID inv: 
   self.theAID <> null
   and
   self.theAID->size() >= 5
   and
   self.theAID->size() <= 16


context AID::AID(bArray: Sequence(JByte),
                 offset: JShort,
                 length: JByte)
  pre : length.asInt() >= 5 
        and
        length.asInt() <= 16
        and
        offset.asInt() >= 0
        and
        bArray <> null
        and
        offset.asInt()+length.asInt() <= bArray->size()
  post: (
           not excThrown(java::lang::Exception)
           and
           self.theAID = bArray->subSequence(offset.asInt()+1, 
                                  offset.asInt()+length.asInt())
        )
        or
        (
           excThrown(TransactionException)
           and
           Transaction.systemInstance.getReason().asInt()
              = Transaction.BUFFER_FULL
        )



context AID::getBytes(dest: Sequence(JByte), offset: JShort): JByte
  pre : true
  post: if
        (
           dest <> null
           and
           dest <> self.theAID     
           -- <> is defined on OclAny. Means 'is a different object than'
           and
           offset.asInt() >= 0
           and
           offset.asInt()+self.theAID->size() <= dest->size()
        )
        then
        (
           (
              not excThrown(java::lang::Exception)
              and
              result.asInt() = self.theAID->size()
              and
              Util.arrayCompare(self.theAID, 0, dest, offset, 
                                  self.theAID->size()) = 0
           )
           or
           (
              excThrown(TransactionException)
              and
              TransactionException.systemInstance.getReason().asInt()
                 = TransactionException.BUFFER_FULL
              and
              JCSystem.getTransactionDepth() = 1
           )
        )
        endif
        and
        (
           not excThrown(java::lang::Exception)
           or
           (
              excThrown(java::lang::NullPointerException)
              and
              dest = null
           )
           or
           (
              excThrown(java::lang::ArrayIndexOutOfBounds)
              and
              dest <> null
              and
              (
                 offset.asInt() < 0
                 or
                 offset.asInt()+self.theAID->size() > dest->size()
              )
           )
           or
           (
              excThrown(TransactionException)
              and
              TransactionException.systemInstance.getReason().asInt()
                 = TransactionException.BUFFER_FULL
              and
              JCSystem.getTransactionDepth() = 1
           )
        ) 



context AID::equals(anObject: Object): Boolean
  pre : true
  post: not excThrown(java::lang::Exception)
        and
        result = (anObject.oclIsKindOf(AID)
                  and
                  anObject.oclAsType(AID).theAID = self.theAID)
        


context AID::equals(bArray: Sequence(JByte), 
                    offset: JShort, 
                    length: JByte): Boolean
  pre : true
  post: if
        (
           bArray = null
           or
           (
              offset.asInt() >= 0 
              and
              length.asInt() >= 0
              and
              offset.asInt()+length.asInt() <= bArray->size()
              and
              offset.asInt()+length.asInt() >= 1
           )
        )
        then
        (
           not excThrown(java::lang::Exception)
           and
           result = 
               (
                  bArray <> null
                  and
                  length.asInt() = self.theAID->size()
                  and
                  Util.arrayCompare(bArray, offset, self.theAID, 
                                         0, length) = 0
               )
        )
        endif
        and
        (
           not excThrown(java::lang::Exception)
           or
           (
              excThrown(java::lang::ArrayIndexOutOfBoundsException)
              and
              (
                 offset.asInt()+length.asInt() < 1
                 or
                 offset.asInt() < 0
                 or
                 length.asInt() < 0
                 or
                 offset.asInt()+length.asInt() > bArray->size()
              )
           )
        )



context AID::partialEquals(bArray: Sequence(JByte),
                           offset: JShort,
                           length: JByte): Boolean
  pre : true
  post: if
        (
           bArray = null
           or
           (
              offset.asInt() >= 0 
              and
              length.asInt() >= 0
              and
              offset.asInt()+length.asInt() <= bArray->size()
           )
        )
        then
        (
           not excThrown(java::lang::Exception)
           and
           result = 
               (
                  bArray <> null
                  and
                  length.asInt() = self.theAID->size()
                  and
                  Util.arrayCompare(bArray, offset, self.theAID, 
                                         0, length) = 0
               )
        )
        endif
        and
        (
           not excThrown(java::lang::Exception)
           or
           (
              excThrown(java::lang::ArrayIndexOutOfBoundsException)
              and
              (
                 offset.asInt() < 0
                 or
                 offset.asInt()+length.asInt() > bArray->size()
              )
           )
        )



context AID::RIDEquals(otherAID: AID): Boolean
  pre : true
  post: not excThrown(java::lang::Exception)
        and
        result =
          Util.arrayCompare(self.theAID, 0, otherAID.theAID, 0, 5) = 0


context AID::getPartialBytes(aidOffset: JShort,
                             dest: Sequence(JByte),
                             oOffset: JShort,
                             oLength: JByte)
  pre : true
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(java::lang::NullPointerException)
           and
           dest = null
        )
        or
        (
           excThrown(java::lang::ArrayIndexOutOfBoundsException)
           and
           (
              oOffset.asInt() < 0
              or
              oOffset.asInt()+oLength.asInt() > dest->size()
              or
              aidOffset.asInt() < 0
              or
              aidOffset.asInt() > theAID->size()
           )
        )
          
       
        
endpackage