-- Key


package javacard::security


context Key::isInitialized(): Boolean
  pre : true
  post: true


context Key::clearKey()
  pre : true
  post: not self.isInitialized()


context Key::getType(): JByte
  pre : self.isInitialized()
  post: true


context Key::getSize(): JShort
  pre : self.isInitialized()
  post: true


endpackage