Module VerifierState

Summary of exported operations:

initVState
                  :: VState

showStats
                  :: VState -> String

Shows the statistics in human-readable format.

isVerified
                  :: VState -> Bool

Are all non-failing properties verified?

addFailedFuncToStats
                  :: String -> String -> VState -> VState

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

incNumAllInStats
                  :: VState -> VState

Increments the number of all tested functions.

incNumNFCInStats
                  :: VState -> VState

Increments the number of operations with nonfail conditions.

incPatTestInStats
                  :: VState -> VState

Increments the number of missing pattern tests.

incFailTestInStats
                  :: VState -> VState

Increments the number of test of posibble failure calls.

addProgToState
                  :: AProg TypeExpr -> VState -> VState

Adds a new typed FlatCurry program to the state.

tdeclOf
                  :: VState -> (String,String) -> Maybe TypeDecl

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

Exported datatypes:

VState

Constructors:

VState :: [(String,String)] -> Int -> Int -> Int -> Int -> [AProg TypeExpr] -> VState
Fields:
- failedFuncs :: [(String,String)]
- numAllFuncs :: Int
- numNFCFuncs :: Int
- numPatTests :: Int
- numFailTests :: Int
- currTAProgs :: [AProg TypeExpr]

Exported operations:

initVState :: VState

Further infos:

solution complete, i.e., able to compute all solutions

showStats :: VState -> String

Shows the statistics in human-readable format.

isVerified :: VState -> Bool

Are all non-failing properties verified?

Further infos:

solution complete, i.e., able to compute all solutions

addFailedFuncToStats :: String -> String -> VState -> VState

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

Further infos:

solution complete, i.e., able to compute all solutions

incNumAllInStats :: VState -> VState

Increments the number of all tested functions.

incNumNFCInStats :: VState -> VState

Increments the number of operations with nonfail conditions.

incPatTestInStats :: VState -> VState

Increments the number of missing pattern tests.

incFailTestInStats :: VState -> VState

Increments the number of test of posibble failure calls.

addProgToState :: AProg TypeExpr -> VState -> VState

Adds a new typed FlatCurry program to the state.

Further infos:

solution complete, i.e., able to compute all solutions

tdeclOf :: VState -> (String,String) -> Maybe TypeDecl

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