-- abstract class RandomData


package javacard::security


-- static final
context RandomData::getInstance(algorithm: JByte): RandomData
  pre : true
  post: not excThrown(java::lang::Exception)
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt()
              = CryptoException.NO_SUCH_ALGORITHM
        )


-- abstract
context RandomData::generateData(buffer: Sequence(JByte),
                                 offset: JShort,
                                 length: JShort)
  pre : buffer <> null
        and
        offset.asInt() >= 0
        and
        length.asInt() >= 0
        and
        offset.asInt()+length.asInt() <= buffer->size()
  post: true


-- abstract
context RandomData::setSeed(buffer: Sequence(JByte),
                            offset: JShort,
                            length: JShort)
  pre : buffer <> null
        and
        offset.asInt() >= 0
        and
        length.asInt() >= 0
        and
        offset.asInt()+length.asInt() <= buffer->size()
  post: true


endpackage