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: September 2017

Summary of exported operations:

m :: IO ()   
mf :: String -> IO ()   
:: String   
main :: IO ()   
eliminateContracts :: Options -> String -> IO ()   
eliminateContractsInProg :: Options -> AProg TypeExpr -> IO ()   
printWhenStatus :: Options -> String -> IO ()   
printWhenIntermediate :: Options -> String -> IO ()   
printWhenAll :: Options -> String -> IO ()   
printCP :: String -> IO ()   
woPreCondSuffix :: String   
dropWoPreCondSuffix :: (String,String) -> (String,String)   
woPostCondSuffix :: String   
dropWoPostCondSuffix :: (String,String) -> (String,String)   
orgNameOf :: (String,String) -> (String,String)   
Returns the original name (i.e., without possible xxxCondCheck suffix) of a qualified function name.
makeTransInfo :: Options -> [AFuncDecl TypeExpr] -> TransInfo   
makeTransState :: Int -> [(Int,TypeExpr)] -> TransState   
incFreshVarIndex :: TransState -> TransState   
addVarTypes :: [(Int,TypeExpr)] -> TransState -> TransState   
initStats :: Statistics   
showStats :: Statistics -> String   
Shows the statistics in human-readable format.
isOptimized :: Statistics -> Bool   
Was there some optimization of a contract?
addPreCondToStats :: String -> Bool -> Statistics -> Statistics   
Increments the number of preconditions.
addPostCondToStats :: String -> Bool -> Statistics -> Statistics   
Adds an operation to the already processed operations with postconditions.
eliminatePreConditions :: Options -> TransInfo -> AProg TypeExpr -> Statistics -> IO (AProg TypeExpr,Statistics)   
provePreCondition :: Options -> TransInfo -> IORef Statistics -> AFuncDecl TypeExpr -> IO (AFuncDecl TypeExpr)   
optPreConditionInRule :: Options -> TransInfo -> (String,String) -> ARule TypeExpr -> IORef Statistics -> IO (ARule TypeExpr)   
renamePatternVars :: TransState -> ABranchExpr TypeExpr -> (ABranchExpr TypeExpr,TransState)   
eliminatePostConditions :: Options -> TransInfo -> AProg TypeExpr -> Statistics -> IO (AProg TypeExpr,Statistics)   
provePostCondition :: Options -> TransInfo -> AFuncDecl TypeExpr -> [AFuncDecl TypeExpr] -> Statistics -> IO ([AFuncDecl TypeExpr],Statistics)   
findPostConditionChecker :: TransInfo -> AFuncDecl TypeExpr -> Maybe (AFuncDecl TypeExpr,AFuncDecl TypeExpr)   
extractPostConditionProofObligation :: TransInfo -> [Int] -> Int -> ARule TypeExpr -> (BoolExp,TransState)   
preCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (BoolExp,TransState)   
postCondExpOf :: TransInfo -> (String,String) -> [Int] -> TransState -> (BoolExp,TransState)   
applyFunc :: AFuncDecl TypeExpr -> [Int] -> TransState -> (AExpr TypeExpr,TransState)   
pred2bool :: AExpr TypeExpr -> TransState -> (BoolExp,TransState)   
exp2bool :: Bool -> TransInfo -> (Int,AExpr TypeExpr) -> TransState -> (BoolExp,TransState)   
normalizeArgs :: [AExpr TypeExpr] -> TransState -> (([(Int,AExpr TypeExpr)],[AExpr TypeExpr]),TransState)   
unzipBranches :: [ABranchExpr TypeExpr] -> ([APattern TypeExpr],[AExpr TypeExpr])   
updFuncDecl :: AFuncDecl TypeExpr -> [AFuncDecl TypeExpr] -> [AFuncDecl TypeExpr]   
rmFuncDecl :: AFuncDecl TypeExpr -> [AFuncDecl TypeExpr] -> [AFuncDecl TypeExpr]   
addSuffix :: (String,String) -> String -> (String,String)   
checkImplicationWithSMT :: Options -> [(Int,TypeExpr)] -> BoolExp -> BoolExp -> BoolExp -> IO Bool   
axiomatizedOps :: [String]   
type2SMT :: TypeExpr -> String   
typedVars2SMT :: [(Int,TypeExpr)] -> String   
fileInPath :: String -> IO Bool   
Checks whether a file exists in one of the directories on the PATH.

Exported datatypes:

TransInfo

Constructors:

TransState

Constructors:

Statistics

Constructors:

  • Statistics :: [String] -> [String] -> [String] -> [String] -> Statistics

Exported operations:

m :: IO ()   

mf :: String -> IO ()   

main :: IO ()   

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

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

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

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

printCP :: String -> IO ()   

woPreCondSuffix :: String   

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

dropWoPreCondSuffix :: (String,String) -> (String,String)   

woPostCondSuffix :: String   

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

dropWoPostCondSuffix :: (String,String) -> (String,String)   

orgNameOf :: (String,String) -> (String,String)   

Returns the original name (i.e., without possible xxxCondCheck suffix) of a qualified function name.

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

initStats :: Statistics   

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

showStats :: Statistics -> String   

Shows the statistics in human-readable format.

isOptimized :: Statistics -> Bool   

Was there some optimization of a contract?

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

addPreCondToStats :: String -> Bool -> Statistics -> Statistics   

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

addPostCondToStats :: String -> Bool -> Statistics -> Statistics   

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

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

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

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

exp2bool :: Bool -> TransInfo -> (Int,AExpr TypeExpr) -> TransState -> (BoolExp,TransState)   

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

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

addSuffix :: (String,String) -> String -> (String,String)   

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

checkImplicationWithSMT :: Options -> [(Int,TypeExpr)] -> BoolExp -> BoolExp -> BoolExp -> IO Bool   

axiomatizedOps :: [String]   

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

type2SMT :: TypeExpr -> String   

typedVars2SMT :: [(Int,TypeExpr)] -> String   

fileInPath :: String -> IO Bool   

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