-- abstract class MessageDigest


package javacard::security


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


-- abstract
context MessageDigest::getAlgorithm(): JByte
  pre : true
  post: true


-- abstract
context MessageDigest::getLength(): JByte
  pre : true
  post: true


-- abstract
context MessageDigest::doFinal(inBuff: Sequence(JByte),
                               inOffset: JShort,
                               inLength: JShort,
                               outBuff: Sequence(JByte),
                               outOffset: JShort): JShort
  pre : inBuff <> null
        and
        outBuff <> null
        and
        inOffset.asInt() >= 0
        and
        inLength.asInt() >= 0
        and
        inOffset.asInt()+inLength.asInt() <= inBuff->size()
        and
        outOffset.asInt() <= outBuff->size()
  post: true


-- abstract
context MessageDigest::update(inBuff: Sequence(JByte),
                              inOffset: JShort,
                              inLength: JShort)
  pre : inBuff <> null
        and
        inOffset.asInt() >= 0
        and
        inLength.asInt() >= 0
        and
        inOffset.asInt()+inLength.asInt() <= inBuff->size()
  post: true


-- abstract
context MessageDigest::reset()
  pre : true
  post: true


endpackage