Parse Successful!

[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