Module VerifierState

Summary of exported operations:

initVerifyInfo :: Options -> VerifyInfo  Deterministic 
addFunsToVerifyInfo' :: [AFuncDecl TypeExpr] -> VerifyInfo -> VerifyInfo  Deterministic 
isContractOp :: (String,String) -> Bool  Deterministic 
Is an operation name the name of a contract or similar?
isProperty :: AFuncDecl TypeExpr -> Bool  Deterministic 
Is a function declaration a property?
initVState :: Options -> VState  Deterministic 
modifyOptions :: (Options -> Options) -> StateT VState IO ()  Deterministic 
getOption :: (Options -> a) -> StateT VState IO a  Deterministic 
evalOption :: (Options -> a) -> (a -> Bool) -> StateT VState IO () -> StateT VState IO ()  Deterministic 
whenOption :: (Options -> Bool) -> StateT VState IO () -> StateT VState IO ()  Deterministic 
printWhenStatus :: String -> StateT VState IO ()  Deterministic 
printWhenIntermediate :: String -> StateT VState IO ()  Deterministic 
printWhenAll :: String -> StateT VState IO ()  Deterministic 
printCP :: String -> StateT VState IO ()  Deterministic 
showFailfreeStats :: VState -> String  Deterministic 
Shows the statistics for the failfree verification in human-readable format.
showContractStats :: VState -> String  Deterministic 
Shows the statistics for the contract checking in human-readable format.
showStats :: StateT VState IO ()  Deterministic 
Shows the statistics in human-readable format.
isVerifiedFailfree :: VState -> Bool  Deterministic 
Are all non-failing properties verified?
isVerifiedContracts :: VState -> Bool  Deterministic 
Are all contracts verified?
addFunsToVerifyInfo :: [AFuncDecl TypeExpr] -> StateT VState IO ()  Deterministic 
addFailedFuncToStats :: String -> String -> StateT VState IO ()  Deterministic 
Adds a possibly failing call in a functions and the called function.
incNumAllInStats :: StateT VState IO ()  Deterministic 
Increments the number of all tested functions.
incNumNFCInStats :: StateT VState IO ()  Deterministic 
Increments the number of operations with nonfail conditions.
incPatTestInStats :: StateT VState IO ()  Deterministic 
Increments the number of missing pattern tests.
incFailTestInStats :: StateT VState IO ()  Deterministic 
Increments the number of test of possible failure calls.
addPreCondToStats :: String -> Bool -> StateT VState IO ()  Deterministic 
Increments the number of preconditions.
addPostCondToStats :: String -> Bool -> StateT VState IO ()  Deterministic 
Adds an operation to the already processed operations with postconditions.
addProgsToState :: [AProg TypeExpr] -> StateT VState IO ()  Deterministic 
Adds a new typed FlatCurry program to the state.
tdeclOf :: (String,String) -> StateT VState IO (Maybe TypeDecl)  Deterministic 
Selects the type declaration of a type constructor from the state.

Exported datatypes:


VerifyInfo

Constructors:


VState

Constructors:

  • VState :: VerifyInfo -> [(String,String)] -> Int -> Int -> Int -> Int -> [String] -> [String] -> [String] -> [String] -> [TAProg] -> VState

    Fields:

    • trInfo :: VerifyInfo
    • failedFuncs :: [(String,String)]
    • numAllFuncs :: Int
    • numNFCFuncs :: Int
    • numPatTests :: Int
    • numFailTests :: Int
    • uPreCond :: [String]
    • vPreCond :: [String]
    • uPostCond :: [String]
    • vPostCond :: [String]
    • currTAProgs :: [TAProg]

VStateM

Type synonym: VStateM a = StateT VState IO a


Exported operations:

initVerifyInfo :: Options -> VerifyInfo  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

isContractOp :: (String,String) -> Bool  Deterministic 

Is an operation name the name of a contract or similar?

isProperty :: AFuncDecl TypeExpr -> Bool  Deterministic 

Is a function declaration a property?

initVState :: Options -> VState  Deterministic 

Further infos:
  • solution complete, i.e., able to compute all solutions

modifyOptions :: (Options -> Options) -> StateT VState IO ()  Deterministic 

getOption :: (Options -> a) -> StateT VState IO a  Deterministic 

evalOption :: (Options -> a) -> (a -> Bool) -> StateT VState IO () -> StateT VState IO ()  Deterministic 

whenOption :: (Options -> Bool) -> StateT VState IO () -> StateT VState IO ()  Deterministic 

printWhenStatus :: String -> StateT VState IO ()  Deterministic 

printWhenIntermediate :: String -> StateT VState IO ()  Deterministic 

printWhenAll :: String -> StateT VState IO ()  Deterministic 

printCP :: String -> StateT VState IO ()  Deterministic 

showFailfreeStats :: VState -> String  Deterministic 

Shows the statistics for the failfree verification in human-readable format.

showContractStats :: VState -> String  Deterministic 

Shows the statistics for the contract checking in human-readable format.

showStats :: StateT VState IO ()  Deterministic 

Shows the statistics in human-readable format.

isVerifiedFailfree :: VState -> Bool  Deterministic 

Are all non-failing properties verified?

Further infos:
  • solution complete, i.e., able to compute all solutions

isVerifiedContracts :: VState -> Bool  Deterministic 

Are all contracts verified?

Further infos:
  • solution complete, i.e., able to compute all solutions

addFailedFuncToStats :: String -> String -> StateT VState IO ()  Deterministic 

Adds a possibly failing call in a functions and the called function.

incNumAllInStats :: StateT VState IO ()  Deterministic 

Increments the number of all tested functions.

incNumNFCInStats :: StateT VState IO ()  Deterministic 

Increments the number of operations with nonfail conditions.

incPatTestInStats :: StateT VState IO ()  Deterministic 

Increments the number of missing pattern tests.

incFailTestInStats :: StateT VState IO ()  Deterministic 

Increments the number of test of possible failure calls.

addPreCondToStats :: String -> Bool -> StateT VState IO ()  Deterministic 

Increments the number of preconditions. If the first argument is true, a precondition has been verified.

addPostCondToStats :: String -> Bool -> StateT VState IO ()  Deterministic 

Adds an operation to the already processed operations with postconditions. If the second argument is true, the postcondition of this operation has been verified.

addProgsToState :: [AProg TypeExpr] -> StateT VState IO ()  Deterministic 

Adds a new typed FlatCurry program to the state.

tdeclOf :: (String,String) -> StateT VState IO (Maybe TypeDecl)  Deterministic 

Selects the type declaration of a type constructor from the state.