Module ContractProver

A tool to prove pre- or postconditions via an SMT solver (Z3) and to remove the statically proven conditions from a program.

Author: Michael Hanus

Version: October 2024

Summary of exported operations:

:: String  Deterministic 
getContractCheckerModulePath :: IO String  Deterministic 
main :: IO ()  Non-deterministic 
proveContracts :: Options -> String -> IO ()  Non-deterministic 
proveContractsInProg :: Options -> AProg TypeExpr -> IO ()  Non-deterministic 
writeTransformedFCY :: Options -> String -> Prog -> IO ()  Non-deterministic 
writeTransformedTAFCY :: Options -> String -> AProg TypeExpr -> IO ()  Non-deterministic 
makeTransState :: Int -> [(Int,TypeExpr)] -> TransState  Deterministic 
emptyTransState :: TransState  Deterministic 
getFreshVarIndex :: StateT TransState IO Int  Deterministic 
setFreshVarIndex :: Int -> StateT TransState IO ()  Deterministic 
getFreshVar :: StateT TransState IO Int  Deterministic 
getVarTypes :: StateT TransState IO [(Int,TypeExpr)]  Deterministic 
addVarTypes :: [(Int,TypeExpr)] -> StateT TransState IO ()  Deterministic 
getAssertion :: StateT TransState IO Term  Deterministic 
setAssertion :: Term -> StateT TransState IO ()  Deterministic 
addToAssertion :: Term -> StateT TransState IO ()  Deterministic 
addPreConditionCheck :: TypeExpr -> CombType -> (String,String) -> TypeExpr -> [AExpr TypeExpr] -> AExpr TypeExpr  Deterministic 
toNoCheckQName :: (String,String) -> (String,String)  Deterministic 
Transform a qualified name into a name of the corresponding function without precondition checking by adding the suffix "'NOCHECK".
fromNoCheckQName :: (String,String) -> (String,String)  Deterministic 
Drops a possible "'NOCHECK" suffix from a qualified name.
addPostConditionCheck :: (String,String) -> ARule TypeExpr -> AExpr TypeExpr  Deterministic 
showDictOf :: TypeExpr -> Maybe (AExpr TypeExpr)  Deterministic 
showDictTypeOf :: TypeExpr -> TypeExpr  Deterministic 
addPreConditions :: Options -> AProg TypeExpr -> IORef VState -> IO (AProg TypeExpr)  Deterministic 
verifyPreConditions :: Options -> AProg TypeExpr -> IORef VState -> IO (AProg TypeExpr)  Non-deterministic 
provePreCondition :: Options -> IORef VState -> AFuncDecl TypeExpr -> IO (AFuncDecl TypeExpr)  Non-deterministic 
optPreConditionInRule :: Options -> VerifyInfo -> (String,String) -> ARule TypeExpr -> IORef VState -> IO (ARule TypeExpr)  Non-deterministic 
renamePatternVars :: ABranchExpr TypeExpr -> StateT TransState IO (ABranchExpr TypeExpr)  Deterministic 
verifyPostConditions :: Options -> AProg TypeExpr -> IORef VState -> IO (AProg TypeExpr)  Non-deterministic 
provePostCondition :: Options -> VerifyInfo -> AFuncDecl TypeExpr -> [AFuncDecl TypeExpr] -> IORef VState -> IO [AFuncDecl TypeExpr]  Non-deterministic 
addPostConditionTo :: (String,String) -> AFuncDecl TypeExpr -> AFuncDecl TypeExpr  Deterministic 
extractPostConditionProofObligation :: VerifyInfo -> [Int] -> Int -> ARule TypeExpr -> StateT TransState IO Term  Deterministic 
preCondExpOf :: VerifyInfo -> (String,String) -> [(Int,TypeExpr)] -> StateT TransState IO Term  Deterministic 
postCondExpOf :: VerifyInfo -> (String,String) -> [(Int,TypeExpr)] -> StateT TransState IO Term  Deterministic 
applyFunc :: AFuncDecl TypeExpr -> [(Int,TypeExpr)] -> StateT TransState IO (AExpr TypeExpr)  Deterministic 
pred2smt :: AExpr TypeExpr -> StateT TransState IO Term  Deterministic 
binding2SMT :: Bool -> VerifyInfo -> (Int,AExpr TypeExpr) -> StateT TransState IO Term  Deterministic 
normalizeArgs :: [AExpr TypeExpr] -> StateT TransState IO ([(Int,AExpr TypeExpr)],[AExpr TypeExpr])  Deterministic 
unzipBranches :: [ABranchExpr TypeExpr] -> ([APattern TypeExpr],[AExpr TypeExpr])  Deterministic 
checkImplication :: Options -> IORef VState -> String -> [(Int,TypeExpr)] -> Term -> Term -> Term -> IO (Maybe String)  Non-deterministic 
checkImplicationWithSMT :: Options -> IORef VState -> String -> [(Int,TypeExpr)] -> Term -> Term -> Term -> IO (Maybe String)  Non-deterministic 
genSMTTypes :: IORef VState -> [(Int,TypeExpr)] -> [AFuncDecl TypeExpr] -> [Term] -> IO [Command]  Deterministic 
callSMT :: Options -> String -> IO (Maybe String)  Deterministic 
nondetTrans :: [((String,String),Bool)] -> Int -> Term -> (Term,Int)  Deterministic 
nondetTransL :: [((String,String),Bool)] -> Int -> [Term] -> ([Term],Int)  Deterministic 
axiomatizedOps :: [String]  Deterministic 
typedVar2SMT :: (Int,TypeExpr) -> Command  Deterministic 
tconsOfTypeExpr :: TypeExpr -> [(String,String)]  Deterministic 
getIncludePath :: String -> IO String  Deterministic 
Returns the path of a file provided as an argument in the include directory of the package or, if this does not exists, in the local include directory.
fileInPath :: String -> IO Bool  Deterministic 
Checks whether a file exists in one of the directories on the PATH.
showQNameNoDots :: (String,String) -> String  Deterministic 
showWithLineNums :: String -> String  Deterministic 
Shows a text with line numbers preceded:
ilog :: Int -> Int  Deterministic 
The value of ilog n is the floor of the logarithm in the base 10 of n.

Exported datatypes:


TransState

Constructors:

  • TransState :: Term -> Int -> [(Int,TypeExpr)] -> TransState

    Fields:

    • cAssertion :: Term
    • freshVar :: Int
    • varTypes :: [(Int,TypeExpr)]

TransStateM

Type synonym: TransStateM a = StateT TransState IO a


Exported operations:

getContractCheckerModulePath :: IO String  Deterministic 

main :: IO ()  Non-deterministic 

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

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

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

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

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

setFreshVarIndex :: Int -> StateT TransState IO ()  Deterministic 

getFreshVar :: StateT TransState IO Int  Deterministic 

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

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

setAssertion :: Term -> StateT TransState IO ()  Deterministic 

addToAssertion :: Term -> StateT TransState IO ()  Deterministic 

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

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

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

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

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

showDictOf :: TypeExpr -> Maybe (AExpr TypeExpr)  Deterministic 

showDictTypeOf :: TypeExpr -> TypeExpr  Deterministic 

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

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

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

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

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

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

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

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

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

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

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

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

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

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

axiomatizedOps :: [String]  Deterministic 

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

typedVar2SMT :: (Int,TypeExpr) -> Command  Deterministic 

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

getIncludePath :: String -> IO String  Deterministic 

Returns the path of a file provided as an argument in the include directory of the package or, if this does not exists, in the local include directory. If both does not exist, a warning is issued.

fileInPath :: String -> IO Bool  Deterministic 

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

showQNameNoDots :: (String,String) -> String  Deterministic 

showWithLineNums :: String -> String  Deterministic 

Shows a text with line numbers preceded:

ilog :: Int -> Int  Deterministic 

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.
Further infos:
  • partially defined