-- DSAPrivateKey extends PrivateKey, 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[] valueX;
--   private boolean isInitX;


context DSAPrivateKey def:
   let valueX: Sequence(JByte)
   let isInitX: Boolean


context DSAPrivateKey inv:
      self.isInitG
      and
      self.isInitP
      and
      self.isInitQ
      and
      self.isInitX
   implies
      self.isInitialized()


context DSAPrivateKey::setX(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.isInitX
           and
           (
                 not self.oclIsKindOf(javacardx::crypto::KeyEncryption)
                 or
                 self.getKeyCipher() = null
              implies
                 Util.arrayCompare(self.valueX, 0, buffer, offset, length) = 0
           )
        )
        or
        (
           excThrown(CryptoException)
           and
           CryptoException.systemInstance.getReason().asInt() 
              = CryptoException.ILLEGAL_VALUE
        )


context DSAPrivateKey::getX(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.valueX->size()
        and
        Util.arrayCompare(self.valueX, 0, buffer, offset, 
                                       self.valueX->size()) = 0


endpackage