PAKCS
Exported names: Imported modules:

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: April 2019

Summary of exported operations:

m :: IO ()   
mf :: String -> IO ()   
:: String   
contractCheckerModule :: String   
main :: IO ()   
proveContracts :: Options -> String -> IO ()   
proveContractsInProg :: Options -> AProg TypeExpr -> IO ()   
writeTransformedProgram :: String -> Prog -> IO ()   
printWhenStatus :: Options -> String -> IO ()   
printWhenIntermediate :: Options -> String -> IO ()   
printWhenAll :: Options -> String -> IO ()   
printCP :: String -> IO ()   
makeTransState :: Int -> [(Int,TypeExpr)] -> TransState   
incFreshVarIndex :: TransState -> TransState   
addVarTypes :: [(Int,TypeExpr)] -> TransState -> TransState   
addPreConditionCheck :: TypeExpr -> CombType -> (String,String) -> TypeExpr -> [AExpr TypeExpr] -> AExpr TypeExpr   
addPostConditionCheck :: (String,String) -> ARule TypeExpr -> AExpr TypeExpr   
verifyPreConditions :: Options -> AProg TypeExpr -> IORef VState -> IO (AProg TypeExpr)   
provePreCondition :: Options -> IORef VState -> AFuncDecl TypeExpr -> IO (AFuncDecl TypeExpr)   
optPreConditionInRule :: Options -> TransInfo -> (String,String) -> ARule TypeExpr -> IORef VState -> IO (ARule TypeExpr)   
renamePatternVars :: TransState -> ABranchExpr TypeExpr -> (ABranchExpr TypeExpr,TransState)   
verifyPostConditions :: Options -> AProg TypeExpr -> IORef VState -> IO (AProg TypeExpr)   
provePostCondition :: Options -> TransInfo -> AFuncDecl TypeExpr -> [AFuncDecl TypeExpr] -> IORef VState -> IO [AFuncDecl TypeExpr]   
addPostCondition :: (String,String) -> [AFuncDecl TypeExpr] -> [AFuncDecl TypeExpr]   
extractPostConditionProofObligation :: TransInfo -> [Int] -> Int -> ARule TypeExpr -> (Term,TransState)   
preCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (Term,TransState)   
postCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (Term,TransState)   
applyFunc :: AFuncDecl TypeExpr -> [Int] -> TransState -> (AExpr TypeExpr,TransState)   
pred2smt :: AExpr TypeExpr -> TransState -> (Term,TransState)   
exp2smt :: Bool -> TransInfo -> (Int,AExpr TypeExpr) -> TransState -> (Term,TransState)   
normalizeArgs :: [AExpr TypeExpr] -> TransState -> (([(Int,AExpr TypeExpr)],[AExpr TypeExpr]),TransState)   
unzipBranches :: [ABranchExpr TypeExpr] -> ([APattern TypeExpr],[AExpr TypeExpr])   
checkImplication :: Options -> IORef VState -> [(Int,TypeExpr)] -> Term -> Term -> Term -> IO (Maybe String)   
checkImplicationWithSMT :: Options -> IORef VState -> [(Int,TypeExpr)] -> Term -> Term -> Term -> IO (Maybe String)   
axiomatizedOps :: [String]   
typedVar2SMT :: (Int,TypeExpr) -> Command   
fileInPath :: String -> IO Bool   
Checks whether a file exists in one of the directories on the PATH.
showQNameNoDots :: (String,String) -> String   

Exported datatypes:

TransState

Constructors:

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

    Fields:

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

Exported operations:

m :: IO ()   

mf :: String -> IO ()   

contractCheckerModule :: String   

main :: IO ()   

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

writeTransformedProgram :: String -> Prog -> IO ()   

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

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

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

printCP :: String -> IO ()   

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

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

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

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

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

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

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

addPostCondition :: (String,String) -> [AFuncDecl TypeExpr] -> [AFuncDecl TypeExpr]   

preCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (Term,TransState)   

postCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (Term,TransState)   

exp2smt :: Bool -> TransInfo -> (Int,AExpr TypeExpr) -> TransState -> (Term,TransState)   

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

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

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

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

axiomatizedOps :: [String]   

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

typedVar2SMT :: (Int,TypeExpr) -> Command   

fileInPath :: String -> IO Bool   

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

showQNameNoDots :: (String,String) -> String