-- DSAPublicKey extends PublicKey, DSAKey


package javacard::security


-- 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.
--
--   private byte[] valueY;
--   private boolean isInitY;


context DSAPublicKey def:
   let valueY: Sequence(JByte)
   let isInitY: Boolean


context DSAPublicKey inv:
      self.isInitG
      and
      self.isInitP
      and
      self.isInitQ
      and
      self.isInitY
   implies
      self.isInitialized()


context DSAPublicKey::setY(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: (
           not excThrown(java::lang::Exception)
           and
           self.isInitY
           and
           (
                 not self.oclIsKindOf(javacardx::crypto::KeyEncryption)
                 or
                 self.getKeyCipher() = null
              implies
                 Util.arrayCompare(self.valueY, 0, buffer, offset, length) = 0
           )
        )
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt() 
              = CryptoException.ILLEGAL_VALUE
        )


context DSAPublicKey::getY(buffer: Sequence(JByte),
                           offset: JShort): JShort
  pre : buffer <> null
        and
        offset.asInt() >= 0
        and
        offset.asInt() < buffer->size()
        and
        self.isInitialized()
  post: result.asInt() = self.valueY->size()
        and
        Util.arrayCompare(self.valueY, 0, buffer, offset, 
                                       self.valueY->size()) = 0


endpackage