-- interface PIN


package javacard::framework


-- 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 interface is naturally free to represent the system state 
-- with the help of other class and instance fields.
--
--    private byte maxPINSize;
--    private byte maxTries;
--    private boolean isValidated;
--    private byte triesRemaining;
--    private byte[] pin;


context PIN def:
   let maxPINSize: JByte
   let maxTries: JByte
   let isValidated: Boolean
   let triesRemaining: JByte
   let pin: Sequence(JByte)


context PIN inv:
   self.maxPINSize.asInt() > 0
   and
   self.maxTries.asInt() > 0
   and
   self.triesRemaining.asInt() >= 0
   and
   self.triesRemaining.asInt() <= self.maxTries.asInt()
   and
   self.pin <> null
   and
   self.pin->size() <= self.maxPINSize.asInt()


context PIN::getTriesRemaining(): JByte
  pre : true
  post: not excThrown(java::lang::Exception)
        and
        result.asInt() = self.triesRemaining.asInt()


context PIN::isValidated(): Boolean
  pre : true
  post: not excThrown(java::lang::Exception)
        and
        result = self.isValidated


context PIN::reset()
  pre : not self.isValidated
  post: not excThrown(java::lang::Exception)
        and
        not self.isValidated
        and
        self.triesRemaining.asInt() = self.triesRemaining@pre.asInt()


context PIN::check(pin: Sequence(JByte), 
                   offset: JShort,
                   length: JByte): Boolean
  pre : true
  post: (
           if
              self.triesRemaining.asInt() = 0
           then
              result = false
           endif
        )
        and
        (
           if
           (
              self.triesRemaining.asInt() > 0
              and
              pin <> null
              and
              offset.asInt() >= 0
              and
              length.asInt() >= 0
              and
              offset.asInt()+length.asInt() <= pin->size()
              and
              Util.arrayCompare(self.pin, 0, pin, offset, length) = 0
           )
           then
           (
              result = true
              and
              self.isValidated
              and
              self.triesRemaining.asInt() = self.maxTries.asInt()
           )
           endif
        )
        and
        (
           if
           (
              self.triesRemaining.asInt() > 0
              and
              not
              (
                 pin <> null
                 and
                 offset.asInt() >= 0
                 and
                 length.asInt() >= 0
                 and
                 offset.asInt()+length.asInt() <= pin->size()
                 and
                 Util.arrayCompare(self.pin, 0, pin, offset, length) = 0
              )
           )
           then
           (
              not self.isValidated
              and
              self.triesRemaining.asInt() = self.triesRemaining@pre.asInt()-1
              and
              (
                 (
                    not excThrown(java::lang::Exception)
                    and
                    result = false
                 )
                 or
                 excThrown(java::lang::NullPointerException)
                 or
                 excThrown(java::lang::ArrayIndexOutOfBoundsException)
              )
           )
           endif
        )


endpackage