CurryInfo: contract-prover-4.0.0 / ContractProver.main

definition: 
main :: IO ()
main = do
  args <- getArgs
  (opts,progs) <- processOptions banner args
  let optname = optName opts
  if not (null optname)
    then putStrLn $ "Precondition for '" ++ optname ++ "':\n" ++
                    encodeContractName (optname ++ "'pre") ++ "\n" ++
                    "Postcondition for '" ++ optname ++ "':\n" ++
                    encodeContractName (optname ++ "'post")
    else do
      when (optVerb opts > 0) $ putStrLn banner
      z3exists <- fileInPath "z3"
      unless (z3exists || not (optVerify opts)) $ putStrLn $ unlines $
        [ "WARNING: CONTRACT VERIFICATION SKIPPED:"
        , "The SMT solver Z3 is required for the verifier"
        , "but the program 'z3' is not found in the PATH!"]
      let opts' = if z3exists then opts else opts { optVerify = False }
      mapM_ (proveContracts opts') progs
demand: 
no demanded arguments
deterministic: 
deterministic operation
failfree: 
<FAILING>
indeterministic: 
referentially transparent operation
infix: 
no fixity defined
iotype: 
{() |-> _}
name: 
main
precedence: 
no precedence defined
result-values: 
_
signature: 
Prelude.IO ()
solution-complete: 
operation might suspend on free variables
terminating: 
possibly non-terminating
totally-defined: 
possibly non-reducible on same data term