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 > 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