-- Util


package javacard::framework


-- static final native
context Util::arrayCopy(src: Sequence(JByte), 
			srcOff: JShort,
			dest: Sequence(JByte),
			destOff: JShort,
			length: JShort): JShort
  pre : true
  post: -- not assignable
        (
            destOff.asInt() >= 1
          implies 
            dest->subSequence(1, destOff.asInt()) 
               = dest@pre->subSequence(1, destOff.asInt())
        )
        and
        (
            destOff.asInt()+length.asInt()+1 <= dest->size() 
          implies
            dest->subSequence(destOff.asInt()+length.asInt()+1, dest->size()) 
             = dest@pre->subSequence(destOff.asInt()+length.asInt()+1, dest->size())
        )
        --
        and 
        (
           if
           (
              src <> null
              and
              srcOff.asInt() >= 0
              and
              srcOff.asInt()+length.asInt() <= src->size()
              and
              dest <> null
              and
              destOff.asInt() >= 0
              and
              destOff.asInt()+length.asInt() <= dest->size()
              and
              length.asInt() >= 0
           )
           then
           (
              (
                 not excThrown(java::lang::Exception)
                 and
                 src@pre->subSequence(srcOff.asInt()+1, srcOff.asInt()+length.asInt()) 
                    = dest->subSequence(destOff.asInt()+1, destOff.asInt()+length.asInt())
              )
              or
              (
                 excThrown(TransactionException)
                 and
                 TransactionException.systemInstance.getReason().asInt()
                    = TransactionException.BUFFER_FULL
                 and
                 JCSystem.getTransactionDepth().asInt() = 1
              )
           )
           endif
        )   
        and
        (
           if
              true
           then
           (
              not excThrown(java::lang::Exception)
              or
              (
                 excThrown(java::lang::NullPointerException)
                 and
                 (
                    src = null
                    or
                    dest = null
                 )
              )
              or
              (
                 excThrown(java::lang::ArrayIndexOutOfBoundsException)
                 and
                 (
                    srcOff.asInt() < 0
                    or
                    destOff.asInt() < 0
                    or
                    srcOff.asInt()+length.asInt() > src->size()
                    or
                    destOff.asInt()+length.asInt() > dest->size()
                    or
                    length.asInt() < 0
                 )
              )
              or
              (
                 excThrown(TransactionException)
                 and
                 TransactionException.systemInstance.getReason().asInt()
                    = TransactionException.BUFFER_FULL
                 and
                 JCSystem.getTransactionDepth().asInt() = 1
              )
           )
           endif
        )



-- static final native
context Util::arrayCopyNonAtomic(src: Sequence(JByte), 
			         srcOff: JShort,
			         dest: Sequence(JByte),
			         destOff: JShort,
			         length: JShort): JShort
  pre : true
  post: -- not assignable
        (
            destOff.asInt() >= 1
          implies 
            dest->subSequence(1, destOff.asInt()) 
               = dest@pre->subSequence(1, destOff.asInt())
        )
        and
        (
            destOff.asInt()+length.asInt()+1 <= dest->size() 
          implies
            dest->subSequence(destOff.asInt()+length.asInt()+1, dest->size()) 
             = dest@pre->subSequence(destOff.asInt()+length.asInt()+1, dest->size())
        )
        --
        and 
        (
           if
           (
              src <> null
              and
              srcOff.asInt() >= 0
              and
              srcOff.asInt()+length.asInt() <= src->size()
              and
              dest <> null
              and
              destOff.asInt() >= 0
              and
              destOff.asInt()+length.asInt() <= dest->size()
              and
              length.asInt() >= 0
           )
           then
           (
              not excThrown(java::lang::Exception)
              and
              src@pre->subSequence(srcOff.asInt()+1, srcOff.asInt()+length.asInt()) 
                 = dest->subSequence(destOff.asInt()+1, destOff.asInt()+length.asInt())
           )
           endif
        )   
        and
        ( 
           if
              true
           then
           (
              not excThrown(java::lang::Exception)
              or
              (
                 excThrown(NullPointerException)
                 and
                 (
                    src = null
                    or
                    dest = null
                 )
              )
              or
              (
                 excThrown(java::lang::ArrayIndexOutOfBoundsException)
                 and
                 (
                    srcOff.asInt() < 0
                    or
                    destOff.asInt() < 0
                    or
                    srcOff.asInt()+length.asInt() > src->size()
                    or
                    destOff.asInt()+length.asInt() > dest->size()
                    or
                    length.asInt() < 0
                 )
              )
           )
           endif
        )



-- static final native
context Util::arrayFillNonAtomic(bArray: Sequence(JByte), 
			         bOff: JShort,
			         bLen: JShort,
			         bValue: JByte): JShort
  pre : true
  post: -- not assignable
        (
            bOff.asInt() >= 1
          implies 
            bArray->subSequence(1, bOff.asInt()) 
               = bArray@pre->subSequence(1, bOff.asInt())
        )
        and
        (
            bOff.asInt()+bLen.asInt()+1 <= bArray->size() 
          implies
            bArray->subSequence(bOff.asInt()+bLen.asInt()+1, bArray->size()) 
             = bArray@pre->subSequence(bOff.asInt()+bLen.asInt()+1, bArray->size())
        )
        --
        and 
        (
           if
           (
              bArray <> null
              and
              bOff.asInt() >= 0
              and
              bLen.asInt() >= 0
              and
              bOff.asInt()+bLen.asInt() <= bArray->size()
           )
           then
           (
              not excThrown(java::lang::Exception)
              and
              Sequence{1..bLen.asInt()}->forAll(i: Integer|
                 bArray->at(bOff+i).asInt() = bValue.asInt())
           )
           endif
        )   
        and
        (
           if
              true
           then
           (
              not excThrown(java::lang::Exception)
              or
              (
                 excThrown(java::lang::NullPointerException)
                 and
                 bArray = null
              )
              or
              (
                 excThrown(java::lang::ArrayIndexOutOfBoundsException)
                 and
                 (
                    bOff.asInt()+bLen.asInt() < 0
                    or
                    bOff.asInt()+bLen.asInt() > bArray->size()
                 )
              )
           )
           endif
        )
        


-- static final native
context Util::arrayCompare(src: Sequence(JByte),
                           srcOff: JShort,
                           dest: Sequence(JByte),
                           destOff: JShort,
                           length: JShort): JByte
  pre : true
  post: (
           if
           (
              src <> null  
              and
              srcOff.asInt() >= 0
              and
              srcOff.asInt()+length.asInt() <= src->size()
              and
              dest <> null
              and
              destOff.asInt() >= 0
              and
              destOff.asInt()+length.asInt() <= dest->size()
              and
              length.asInt() >= 0
           )
           then
           (
              not excThrown(java::lang::Exception)
              and
              (
                 result.asInt() = -1
                 or
                 result.asInt() = 0
                 or
                 result.asInt() = 1
              )
              and
              (
                    src->subSequence(srcOff.asInt()+1, srcOff.asInt()+length.asInt())
                       = dest->subSequence(destOff.asInt()+1, 
                                           destOff.asInt()+length.asInt())
                 implies
                    result.asInt() = 0
              )
              and
              (
                    Sequence{1..length.asInt()}->exists(i: Integer|
                          (
                             src->at(srcOff.asInt()+i) < dest->at(destOff.asInt()+i) 
                             and 
                             Sequence{1..i-1}->forAll(j: Integer|
                                src->at(srcOff.asInt()+j) = dest->at(destOff.asInt()+j))
                          )
                 implies
                    result.asInt() = -1
              )
              and
              (
                    Sequence{1..length.asInt()}->exists(i: Integer|
                          (
                             src->at(srcOff.asInt()+i) > dest->at(destOff.asInt()+i) 
                             and 
                             Sequence{1..i-1}->forAll(j: Integer|
                                src->at(srcOff.asInt()+j) = dest->at(destOff.asInt()+j))
                          )
                 implies
                    result.asInt() = 1
              )
           )
           endif
        )
        and
        (
           if
              true
           then
           (
              not excThrown(java::lang::Exception)
              or
              (
                 excThrown(java::lang::NullPointerException)
                 and
                 (
                    src = null
                    or
                    dest = null
                 )
              )
              or
              ( 
                 excThrown(java::lang::ArrayIndexOutOfBoundsException)
                 and
                 (
                    srcOff.asInt() < 0
                    or
                    destOff.asInt() < 0
                    or
                    length.asInt() < 0
                    or
                    srcOff.asInt()+length.asInt() > src->size()
                    or
                    destOff.asInt()+length.asInt() > dest->size()
                 )
              )
           )
           endif
        )
        


-- static final 
context Util::makeShort(b1: JByte, b2: JByte): JShort
  pre : true
  post: result.asInt() = (b1.asInt()*2*2*2*2*2*2*2*2) + b2.asInt()



-- static final 
context Util::getShort(bArray: Sequence(JByte), bOff: JShort): JShort
  pre : true
  post: (
           if
           ( 
              bArray <> null
              and
              bOff.asInt() >= 0
              and
              bOff.asInt()+1 < bArray->size()
           )
           then
           (
              not excThrown(java::lang::Exception)
              and
              result.asInt() 
                 = self.makeShort(bArray->at(bOff.asInt()+1), 
                                  bArray->at(bOff.asInt()+2)).asInt()
           )
           endif
        )
        and
        (
           if 
              true
           then
           (
              (
                 excThrown(java::lang::NullPointerException)
                 and
                 bArray = null
              )
              or
              (
                 excThrown(java::lang::ArrayIndexOutOfBoundsException)
                 and
                 bOff.asInt() < 0
                 or
                 bOff.asInt()+1 > bArray->size()  
              )
           )
           endif
        ) 



-- static final native
context Util::setShort(bArray: Sequence(JByte), 
                       bOff: JShort,
                       sValue: JShort): JShort
  pre : true
  post: -- not assignable
        (
            bOff.asInt() >= 1 
          implies 
            bArray->subSequence(1, bOff.asInt()) 
               = bArray@pre->subSequence(1, bOff.asInt())
        )
        and
        (
            bOff+3 <= bArray->size() 
          implies
            bArray->subSequence(bOff.asInt()+3, bArray->size()) 
             = bArray@pre->subSequence(bOff.asInt()+3, bArray->size())
        )
        ------
        and
        (
           if
           ( 
              bArray <> null
              and
              bOff.asInt() >= 0
              and
              bOff.asInt()+1 < bArray->size()
           )
           then
           (
              (
                 not excThrown(java::lang::Exception)
                 and
                 result.asInt() = bOff.asInt()+2
                 and
                 self.getShort(bArray, bOff).asInt() = sValue.asInt()
              )
              or
              (
                 excThrown(TransactionException)
                 and
                 TransactionException.systemInstance.getReason().asInt()
                    = TransactionException.BUFFER_FULL
                 and
                 JCSystem.getTransactionDepth().asInt() = 1
              )
           )
           endif
        )
        and
        (
           if 
              true
           then
           (
              (
                 excThrown(java::lang::NullPointerException)
                 and
                 bArray = null
              )
              or
              (
                 excThrown(java::lang::ArrayIndexOutOfBoundsException)
                 and
                 bOff.asInt() < 0
                 or
                 bOff.asInt()+1 > bArray->size()  
              )
              or
              (
                 excThrown(TransactionException)
                 and
                 TransactionException.systemInstance.getReason().asInt()
                    = TransactionException.BUFFER_FULL
                 and
                 JCSystem.getTransactionDepth().asInt() = 1
              )
           )
           endif
        )


endpackage