[Abstract syntax]

OCLf ([Pack (PackName (PathN ([PN (Ident "javacard"); PN (Ident "framework")])), Constraints ([Constr (CDClassif (CC (Ident "OwnerPIN")), [CBDef ([LENoParam (Ident "tryCounter", EExplPropCall (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "triesLeft")]), NoTE, NoQual, NoPCP)), PArrow, PCall (PathN ([PN (Ident "at")]), NoTE, NoQual, PCPs (PCPConcrete (ELit (LitNum (NumInt (1))), [])))))]); CB (Inv, OCLExp (EOpRel (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "maxPINSize")]), NoTE, NoQual, NoPCP)), RGT, ELit (LitNum (NumInt (0)))))); CB (Inv, OCLExp (EOpRel (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "maxTries")]), NoTE, NoQual, NoPCP)), RGT, ELit (LitNum (NumInt (0)))))); CB (Inv, OCLExp (EOpRel (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "tryCounter")]), NoTE, NoQual, NoPCP)), RGTE, ELit (LitNum (NumInt (0)))))); CB (Inv, OCLExp (EOpRel (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "tryCounter")]), NoTE, NoQual, NoPCP)), RLTE, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "maxTries")]), NoTE, NoQual, NoPCP))))); CB (Inv, OCLExp (EOpEq (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP)), ENEq, ENull))); CB (Inv, OCLExp (EOpRel (EExplPropCall (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP)), PArrow, PCall (PathN ([PN (Ident "size")]), NoTE, NoQual, PCPs (PCPNoDeclNoParam))), RLTE, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "maxPINSize")]), NoTE, NoQual, NoPCP)))))]); Constr (CDOper (OpC (Ident "OwnerPIN", OpName (Ident "OwnerPIN"), [FP (Ident "tryLimit", TSsimple (STSpec (PathN ([PN (Ident "Integer")])))); FP (Ident "maxPINSize", TSsimple (STSpec (PathN ([PN (Ident "Integer")]))))])), [CB (Pre, OCLExp (EOpRel (EImplPropCall (PCall (PathN ([PN (Ident "maxPINSize")]), NoTE, NoQual, NoPCP)), RGT, ELit (LitNum (NumInt (0)))))); CB (Pre, OCLExp (EOpRel (EImplPropCall (PCall (PathN ([PN (Ident "tryLimit")]), NoTE, NoQual, NoPCP)), RGT, ELit (LitNum (NumInt (0)))))); CB (Post, OCLExp (EOpUn (UNot, EImplPropCall (PCall (PathN ([PN (Ident "excThrown")]), NoTE, NoQual, PCPs (PCPConcrete (EImplPropCall (PCall (PathN ([PN (Ident "java"); PN (Ident "lang"); PN (Ident "Exception")]), NoTE, NoQual, NoPCP)), []))))))); CB (Post, OCLExp (EOpEq (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "maxPINSize")]), NoTE, NoQual, NoPCP)), EEq, EImplPropCall (PCall (PathN ([PN (Ident "maxPINSize")]), NoTE, NoQual, NoPCP))))); CB (Post, OCLExp (EOpEq (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "maxTries")]), NoTE, NoQual, NoPCP)), EEq, EImplPropCall (PCall (PathN ([PN (Ident "tryLimit")]), NoTE, NoQual, NoPCP))))); CB (Post, OCLExp (EOpEq (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "tryCounter")]), NoTE, NoQual, NoPCP)), EEq, EImplPropCall (PCall (PathN ([PN (Ident "tryLimit")]), NoTE, NoQual, NoPCP))))); CB (Post, OCLExp (EOpUn (UNot, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "isValidated")]), NoTE, NoQual, PCPs (PCPNoDeclNoParam))))))]); Constr (CDOper (OpC (Ident "OwnerPIN", OpName (Ident "update"), [FP (Ident "pin", TScoll (CT (Sequence, STSpec (PathN ([PN (Ident "Integer")]))))); FP (Ident "offset", TSsimple (STSpec (PathN ([PN (Ident "Integer")])))); FP (Ident "length", TSsimple (STSpec (PathN ([PN (Ident "Integer")]))))])), [CB (Pre, OCLExp (EOpEq (EImplPropCall (PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP)), ENEq, ENull))); CB (Pre, OCLExp (EOpRel (EImplPropCall (PCall (PathN ([PN (Ident "offset")]), NoTE, NoQual, NoPCP)), RGTE, ELit (LitNum (NumInt (0)))))); CB (Pre, OCLExp (EOpRel (EOpAdd (EImplPropCall (PCall (PathN ([PN (Ident "offset")]), NoTE, NoQual, NoPCP)), AAdd, EImplPropCall (PCall (PathN ([PN (Ident "length")]), NoTE, NoQual, NoPCP))), RLTE, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP)), PArrow, PCall (PathN ([PN (Ident "size")]), NoTE, NoQual, PCPs (PCPNoDeclNoParam)))))); CB (Pre, OCLExp (EOpRel (EImplPropCall (PCall (PathN ([PN (Ident "length")]), NoTE, NoQual, NoPCP)), RGTE, ELit (LitNum (NumInt (0)))))); CB (Post, OCLExp (EOpLog (EOpLog (EOpLog (EOpUn (UNot, EImplPropCall (PCall (PathN ([PN (Ident "excThrown")]), NoTE, NoQual, PCPs (PCPConcrete (EImplPropCall (PCall (PathN ([PN (Ident "java"); PN (Ident "lang"); PN (Ident "Exception")]), NoTE, NoQual, NoPCP)), []))))), LAnd, EOpEq (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "Util")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "arrayCompare")]), NoTE, NoQual, PCPs (PCPConcrete (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP)), [PCPComma (ELit (LitNum (NumInt (0)))); PCPComma (EImplPropCall (PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP))); PCPComma (EImplPropCall (PCall (PathN ([PN (Ident "offset")]), NoTE, NoQual, NoPCP))); PCPComma (EImplPropCall (PCall (PathN ([PN (Ident "length")]), NoTE, NoQual, NoPCP)))])))), EEq, ELit (LitNum (NumInt (0))))), LOr, EOpLog (EImplPropCall (PCall (PathN ([PN (Ident "excThrown")]), NoTE, NoQual, PCPs (PCPConcrete (EImplPropCall (PCall (PathN ([PN (Ident "PINException")]), NoTE, NoQual, NoPCP)), [])))), LAnd, EOpRel (EImplPropCall (PCall (PathN ([PN (Ident "length")]), NoTE, NoQual, NoPCP)), RGT, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "maxPINSize")]), NoTE, NoQual, NoPCP))))), LOr, EOpLog (EImplPropCall (PCall (PathN ([PN (Ident "excThrown")]), NoTE, NoQual, PCPs (PCPConcrete (EImplPropCall (PCall (PathN ([PN (Ident "TransactionException")]), NoTE, NoQual, NoPCP)), [])))), LAnd, EOpEq (EExplPropCall (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "TransactionException")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "systemInstance")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "getReason")]), NoTE, NoQual, PCPs (PCPNoDeclNoParam))), EEq, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "TransactionException")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "BUFFER_FULL")]), NoTE, NoQual, NoPCP)))))))]); Constr (CDOper (OpC (Ident "OwnerPIN", OpName (Ident "resetAndUnblock"), [])), [CB (Post, OCLExp (EOpUn (UNot, EImplPropCall (PCall (PathN ([PN (Ident "excThrown")]), NoTE, NoQual, PCPs (PCPConcrete (EImplPropCall (PCall (PathN ([PN (Ident "java"); PN (Ident "lang"); PN (Ident "Exception")]), NoTE, NoQual, NoPCP)), []))))))); CB (Post, OCLExp (EOpUn (UNot, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "isValidated")]), NoTE, NoQual, PCPs (PCPNoDeclNoParam)))))); CB (Post, OCLExp (EOpEq (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "tryCounter")]), NoTE, NoQual, NoPCP)), EEq, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "maxTries")]), NoTE, NoQual, NoPCP)))))]); Constr (CDOper (OpCRT (Ident "OwnerPIN", OpName (Ident "isValidated"), [], RT (TSsimple (STSpec (PathN ([PN (Ident "Boolean")])))))), [CB (Post, OCLExp (EOpUn (UNot, EImplPropCall (PCall (PathN ([PN (Ident "excThrown")]), NoTE, NoQual, PCPs (PCPConcrete (EImplPropCall (PCall (PathN ([PN (Ident "java"); PN (Ident "lang"); PN (Ident "Exception")]), NoTE, NoQual, NoPCP)), []))))))); CB (Post, OCLExp (EOpEq (EImplPropCall (PCall (PathN ([PN (Ident "result")]), NoTE, NoQual, NoPCP)), EEq, ELit (LitBoolTrue))))]); Constr (CDOper (OpCRT (Ident "OwnerPIN", OpName (Ident "getTriesRemaining"), [], RT (TSsimple (STSpec (PathN ([PN (Ident "Integer")])))))), [CB (Post, OCLExp (EOpUn (UNot, EImplPropCall (PCall (PathN ([PN (Ident "excThrown")]), NoTE, NoQual, PCPs (PCPConcrete (EImplPropCall (PCall (PathN ([PN (Ident "java"); PN (Ident "lang"); PN (Ident "Exception")]), NoTE, NoQual, NoPCP)), []))))))); CB (Post, OCLExp (EOpEq (EImplPropCall (PCall (PathN ([PN (Ident "result")]), NoTE, NoQual, NoPCP)), EEq, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "tryCounter")]), NoTE, NoQual, NoPCP)))))]); Constr (CDOper (OpCRT (Ident "OwnerPIN", OpName (Ident "check"), [FP (Ident "pin", TScoll (CT (Sequence, STSpec (PathN ([PN (Ident "Integer")]))))); FP (Ident "offset", TSsimple (STSpec (PathN ([PN (Ident "Integer")])))); FP (Ident "length", TSsimple (STSpec (PathN ([PN (Ident "Integer")]))))], RT (TSsimple (STSpec (PathN ([PN (Ident "Boolean")])))))), [CB (Post, OCLExp (EOpImpl (EOpEq (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "tryCounter")]), NoTE, NoQual, NoPCP)), EEq, ELit (LitNum (NumInt (0)))), EOpEq (EImplPropCall (PCall (PathN ([PN (Ident "result")]), NoTE, NoQual, NoPCP)), EEq, ELit (LitBoolFalse))))); CB (Post, OCLExp (EOpImpl (EOpLog (EOpLog (EOpLog (EOpLog (EOpLog (EOpRel (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "tryCounter")]), NoTE, NoQual, NoPCP)), RGT, ELit (LitNum (NumInt (0)))), LAnd, EOpEq (EImplPropCall (PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP)), ENEq, ENull)), LAnd, EOpRel (EImplPropCall (PCall (PathN ([PN (Ident "offset")]), NoTE, NoQual, NoPCP)), RGTE, ELit (LitNum (NumInt (0))))), LAnd, EOpRel (EImplPropCall (PCall (PathN ([PN (Ident "length")]), NoTE, NoQual, NoPCP)), RGTE, ELit (LitNum (NumInt (0))))), LAnd, EOpRel (EOpAdd (EImplPropCall (PCall (PathN ([PN (Ident "offset")]), NoTE, NoQual, NoPCP)), AAdd, EImplPropCall (PCall (PathN ([PN (Ident "length")]), NoTE, NoQual, NoPCP))), RLTE, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP)), PArrow, PCall (PathN ([PN (Ident "size")]), NoTE, NoQual, PCPs (PCPNoDeclNoParam))))), LAnd, EOpEq (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "Util")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "arrayCompare")]), NoTE, NoQual, PCPs (PCPConcrete (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP)), [PCPComma (ELit (LitNum (NumInt (0)))); PCPComma (EImplPropCall (PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP))); PCPComma (EImplPropCall (PCall (PathN ([PN (Ident "offset")]), NoTE, NoQual, NoPCP))); PCPComma (EImplPropCall (PCall (PathN ([PN (Ident "length")]), NoTE, NoQual, NoPCP)))])))), EEq, ELit (LitNum (NumInt (0))))), EOpLog (EOpLog (EOpEq (EImplPropCall (PCall (PathN ([PN (Ident "result")]), NoTE, NoQual, NoPCP)), EEq, ELit (LitBoolTrue)), LAnd, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "isValidated")]), NoTE, NoQual, PCPs (PCPNoDeclNoParam)))), LAnd, EOpEq (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "tryCounter")]), NoTE, NoQual, NoPCP)), EEq, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "maxTries")]), NoTE, NoQual, NoPCP))))))); CB (Post, OCLExp (EOpImpl (EOpLog (EOpRel (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "tryCounter")]), NoTE, NoQual, NoPCP)), RGT, ELit (LitNum (NumInt (0)))), LAnd, EOpUn (UNot, EOpLog (EOpLog (EOpLog (EOpLog (EOpEq (EImplPropCall (PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP)), ENEq, ENull), LAnd, EOpRel (EImplPropCall (PCall (PathN ([PN (Ident "offset")]), NoTE, NoQual, NoPCP)), RGTE, ELit (LitNum (NumInt (0))))), LAnd, EOpRel (EImplPropCall (PCall (PathN ([PN (Ident "length")]), NoTE, NoQual, NoPCP)), RGTE, ELit (LitNum (NumInt (0))))), LAnd, EOpRel (EOpAdd (EImplPropCall (PCall (PathN ([PN (Ident "offset")]), NoTE, NoQual, NoPCP)), AAdd, EImplPropCall (PCall (PathN ([PN (Ident "length")]), NoTE, NoQual, NoPCP))), RLTE, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP)), PArrow, PCall (PathN ([PN (Ident "size")]), NoTE, NoQual, PCPs (PCPNoDeclNoParam))))), LAnd, EOpEq (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "Util")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "arrayCompare")]), NoTE, NoQual, PCPs (PCPConcrete (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP)), [PCPComma (ELit (LitNum (NumInt (0)))); PCPComma (EImplPropCall (PCall (PathN ([PN (Ident "pin")]), NoTE, NoQual, NoPCP))); PCPComma (EImplPropCall (PCall (PathN ([PN (Ident "offset")]), NoTE, NoQual, NoPCP))); PCPComma (EImplPropCall (PCall (PathN ([PN (Ident "length")]), NoTE, NoQual, NoPCP)))])))), EEq, ELit (LitNum (NumInt (0))))))), EOpLog (EOpLog (EOpUn (UNot, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "isValidated")]), NoTE, NoQual, PCPs (PCPNoDeclNoParam)))), LAnd, EOpEq (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "tryCounter")]), NoTE, NoQual, NoPCP)), EEq, EOpAdd (EImplPropCall (PCall (PathN ([PN (Ident "tryCounter")]), AtPre, NoQual, NoPCP)), ASub, ELit (LitNum (NumInt (1)))))), LAnd, EOpLog (EOpLog (EOpLog (EOpUn (UNot, EImplPropCall (PCall (PathN ([PN (Ident "excThrown")]), NoTE, NoQual, PCPs (PCPConcrete (EImplPropCall (PCall (PathN ([PN (Ident "java"); PN (Ident "lang"); PN (Ident "Exception")]), NoTE, NoQual, NoPCP)), []))))), LAnd, EOpEq (EImplPropCall (PCall (PathN ([PN (Ident "result")]), NoTE, NoQual, NoPCP)), EEq, ELit (LitBoolFalse))), LOr, EImplPropCall (PCall (PathN ([PN (Ident "excThrown")]), NoTE, NoQual, PCPs (PCPConcrete (EImplPropCall (PCall (PathN ([PN (Ident "java"); PN (Ident "lang"); PN (Ident "NullPointerException")]), NoTE, NoQual, NoPCP)), []))))), LOr, EImplPropCall (PCall (PathN ([PN (Ident "excThrown")]), NoTE, NoQual, PCPs (PCPConcrete (EImplPropCall (PCall (PathN ([PN (Ident "java"); PN (Ident "lang"); PN (Ident "ArrayIndexOutOfBoundsException")]), NoTE, NoQual, NoPCP)), [])))))))))]); Constr (CDOper (OpC (Ident "OwnerPIN", OpName (Ident "reset"), [])), [CB (Pre, OCLExp (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "isValidated")]), NoTE, NoQual, PCPs (PCPNoDeclNoParam))))); CB (Post, OCLExp (EOpUn (UNot, EImplPropCall (PCall (PathN ([PN (Ident "excThrown")]), NoTE, NoQual, PCPs (PCPConcrete (EImplPropCall (PCall (PathN ([PN (Ident "java"); PN (Ident "lang"); PN (Ident "Exception")]), NoTE, NoQual, NoPCP)), []))))))); CB (Post, OCLExp (EOpUn (UNot, EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "isValidated")]), NoTE, NoQual, PCPs (PCPNoDeclNoParam)))))); CB (Post, OCLExp (EOpEq (EExplPropCall (EImplPropCall (PCall (PathN ([PN (Ident "self")]), NoTE, NoQual, NoPCP)), PDot, PCall (PathN ([PN (Ident "tryCounter")]), NoTE, NoQual, NoPCP)), EEq, EImplPropCall (PCall (PathN ([PN (Ident "tryCounter")]), AtPre, NoQual, NoPCP)))))])]))])

[Linearized tree]

package javacard :: framework context OwnerPIN def : let tryCounter = self . triesLeft -> at (1) inv : self . maxPINSize > 0 inv : self . maxTries > 0 inv : self . tryCounter >= 0 inv : self . tryCounter <= self . maxTries inv : self . pin <> null inv : self . pin -> size () <= self . maxPINSize context OwnerPIN :: OwnerPIN (tryLimit : Integer, maxPINSize : Integer) pre : maxPINSize > 0 pre : tryLimit > 0 post : not excThrown (java :: lang :: Exception) post : self . maxPINSize = maxPINSize post : self . maxTries = tryLimit post : self . tryCounter = tryLimit post : not self . isValidated () context OwnerPIN :: update (pin : Sequence (Integer), offset : Integer, length : Integer) pre : pin <> null pre : offset >= 0 pre : offset + length <= pin -> size () pre : length >= 0 post : not excThrown (java :: lang :: Exception) and Util . arrayCompare (self . pin, 0, pin, offset, length) = 0 or (excThrown (PINException) and length > self . maxPINSize) or (excThrown (TransactionException) and TransactionException . systemInstance . getReason () = TransactionException . BUFFER_FULL) context OwnerPIN :: resetAndUnblock () post : not excThrown (java :: lang :: Exception) post : not self . isValidated () post : self . tryCounter = self . maxTries context OwnerPIN :: isValidated () : Boolean post : not excThrown (java :: lang :: Exception) post : result = true context OwnerPIN :: getTriesRemaining () : Integer post : not excThrown (java :: lang :: Exception) post : result = self . tryCounter context OwnerPIN :: check (pin : Sequence (Integer), offset : Integer, length : Integer) : Boolean post : self . tryCounter = 0 implies result = false post : self . tryCounter > 0 and pin <> null and offset >= 0 and length >= 0 and offset + length <= pin -> size () and Util . arrayCompare (self . pin, 0, pin, offset, length) = 0 implies result = true and self . isValidated () and self . tryCounter = self . maxTries post : self . tryCounter > 0 and not (pin <> null and offset >= 0 and length >= 0 and offset + length <= pin -> size () and Util . arrayCompare (self . pin, 0, pin, offset, length) = 0) implies not self . isValidated () and self . tryCounter = tryCounter @ pre - 1 and (not excThrown (java :: lang :: Exception) and result = false or excThrown (java :: lang :: NullPointerException) or excThrown (java :: lang :: ArrayIndexOutOfBoundsException)) context OwnerPIN :: reset () pre : self . isValidated () post : not excThrown (java :: lang :: Exception) post : not self . isValidated () post : self . tryCounter = tryCounter @ pre endpackage