Parse Succesful!

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

[Linearized Tree]
package javacard :: framework context OwnerPIN def : let tryCounter = self . triesLeft -> at (1) inv : self . maxPINSize > 0inv : self . maxTries > 0inv : self . tryCounter >= 0inv : self . tryCounter <= self . maxTries inv : self . pin <> null inv : self . pin -> size () <= self . maxPINSize context OwnerPIN :: OwnerPIN (tryLimit : Integer, maxPINSize : Integer) pre : maxPINSize > 0pre : tryLimit > 0post : 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 >= 0pre : offset + length <= pin -> size () pre : length >= 0post : not excThrown (java :: lang :: Exception) and Util . arrayCompare (self . pin, 0, pin, offset, length) = 0or (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 = 0implies result = false post : self . tryCounter > 0and pin <> null and offset >= 0and length >= 0and offset + length <= pin -> size () and Util . arrayCompare (self . pin, 0, pin, offset, length) = 0implies result = true and self . isValidated () and self . tryCounter = self . maxTries post : self . tryCounter > 0and not (pin <> null and offset >= 0and length >= 0and offset + length <= pin -> size () and Util . arrayCompare (self . pin, 0, pin, offset, length) = 0) implies not self . isValidated () and self . tryCounter = tryCounter @ pre - 1and (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