Module ContractProver

banner :: String   

contractCheckerModule :: String   

main :: IO ()   

proveContracts :: Options -> String -> IO ()   

proveContractsInProg :: Options -> AProg TypeExpr -> IO ()   

writeTransformedFCY :: Options -> String -> Prog -> IO ()   

writeTransformedTAFCY :: Options -> String -> AProg TypeExpr -> IO ()   

makeTransState :: Int -> [(Int,TypeExpr)] -> TransState   

Further infos:

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

emptyTransState :: TransState   

getFreshVarIndex :: StateT TransState IO Int   

setFreshVarIndex :: Int -> StateT TransState IO ()   

getFreshVar :: StateT TransState IO Int   

getVarTypes :: StateT TransState IO [(Int,TypeExpr)]   

addVarTypes :: [(Int,TypeExpr)] -> StateT TransState IO ()   

getAssertion :: StateT TransState IO Term   

setAssertion :: Term -> StateT TransState IO ()   

addToAssertion :: Term -> StateT TransState IO ()   

addPreConditionCheck :: TypeExpr -> CombType -> (String,String) -> TypeExpr -> [AExpr TypeExpr] -> AExpr TypeExpr   

toNoCheckQName :: (String,String) -> (String,String)   

Transform a qualified name into a name of the corresponding function without precondition checking by adding the suffix "'NOCHECK".

Further infos:

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

fromNoCheckQName :: (String,String) -> (String,String)   

Drops a possible "'NOCHECK" suffix from a qualified name.

addPostConditionCheck :: (String,String) -> ARule TypeExpr -> AExpr TypeExpr   

addPreConditions :: Options -> AProg TypeExpr -> IORef VState -> IO (AProg TypeExpr)   

verifyPreConditions :: Options -> AProg TypeExpr -> IORef VState -> IO (AProg TypeExpr)   

provePreCondition :: Options -> IORef VState -> AFuncDecl TypeExpr -> IO (AFuncDecl TypeExpr)   

optPreConditionInRule :: Options -> VerifyInfo -> (String,String) -> ARule TypeExpr -> IORef VState -> IO (ARule TypeExpr)   

renamePatternVars :: ABranchExpr TypeExpr -> StateT TransState IO (ABranchExpr TypeExpr)   

verifyPostConditions :: Options -> AProg TypeExpr -> IORef VState -> IO (AProg TypeExpr)   

provePostCondition :: Options -> VerifyInfo -> AFuncDecl TypeExpr -> [AFuncDecl TypeExpr] -> IORef VState -> IO [AFuncDecl TypeExpr]   

addPostConditionTo :: (String,String) -> AFuncDecl TypeExpr -> AFuncDecl TypeExpr   

extractPostConditionProofObligation :: VerifyInfo -> [Int] -> Int -> ARule TypeExpr -> StateT TransState IO Term   

preCondExpOf :: VerifyInfo -> (String,String) -> [(Int,TypeExpr)] -> StateT TransState IO Term   

postCondExpOf :: VerifyInfo -> (String,String) -> [(Int,TypeExpr)] -> StateT TransState IO Term   

applyFunc :: AFuncDecl TypeExpr -> [(Int,TypeExpr)] -> StateT TransState IO (AExpr TypeExpr)   

pred2smt :: AExpr TypeExpr -> StateT TransState IO Term   

binding2SMT :: Bool -> VerifyInfo -> (Int,AExpr TypeExpr) -> StateT TransState IO Term   

normalizeArgs :: [AExpr TypeExpr] -> StateT TransState IO ([(Int,AExpr TypeExpr)],[AExpr TypeExpr])   

unzipBranches :: [ABranchExpr TypeExpr] -> ([APattern TypeExpr],[AExpr TypeExpr])   

Further infos:

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

checkImplication :: Options -> IORef VState -> String -> [(Int,TypeExpr)] -> Term -> Term -> Term -> IO (Maybe String)   

checkImplicationWithSMT :: Options -> IORef VState -> String -> [(Int,TypeExpr)] -> Term -> Term -> Term -> IO (Maybe String)   

genSMTTypes :: IORef VState -> [(Int,TypeExpr)] -> [AFuncDecl TypeExpr] -> [Term] -> IO [Command]   

callSMT :: Options -> String -> IO (Maybe String)   

nondetTrans :: [((String,String),Bool)] -> Int -> Term -> (Term,Int)   

nondetTransL :: [((String,String),Bool)] -> Int -> [Term] -> ([Term],Int)   

axiomatizedOps :: [String]   

Further infos:

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

typedVar2SMT :: (Int,TypeExpr) -> Command   

tconsOfTypeExpr :: TypeExpr -> [(String,String)]   

fileInPath :: String -> IO Bool   

Checks whether a file exists in one of the directories on the PATH.

showQNameNoDots :: (String,String) -> String   

showWithLineNums :: String -> String   

Shows a text with line numbers preceded:

ilog :: Int -> Int   

The value of ilog n is the floor of the logarithm in the base 10 of n. Fails if n <= 0. For positive integers, the returned value is 1 less the number of digits in the decimal representation of n.

Example call:

(ilog n)

Parameters:

• n : The argument.

Returns:

the floor of the logarithm in the base 10 of n.