CurryInfo: contract-prover-4.0.0 / ContractProver.provePostCondition

 
provePostCondition :: Options -> VerifyInfo -> TAFuncDecl -> [TAFuncDecl]
                   -> IORef VState -> IO [TAFuncDecl]
provePostCondition opts ti postfun allfuns vstref = do
  maybe (do putStrLn $ "Postcondition: " ++ pcname ++ "\n" ++
                       "Operation of this postcondition not found!"
            return allfuns)
        --(\checkfun -> provePC checkfun) --TODO: simplify definition
        (\checkfun -> evalStateT (provePC (simpFuncDecl checkfun))
                                 emptyTransState)
        (find (\fd -> toPostCondName (snd (funcName fd)) ==
                      decodeContractName pcname)
              allfuns)
 where
  pcname = snd (funcName postfun)

  provePC checkfun = do
    let (postmn,postfn) = funcName postfun
        mainfunc        = snd (funcName checkfun)
        orgqn           = (postmn, reverse (drop 5 (reverse postfn)))
    -- lift $ putStrLn $ "Check postcondition of operation " ++ mainfunc
    let farity = funcArity checkfun
        ftype  = funcType checkfun
        targsr = zip [1..] (argTypes ftype ++ [resultType ftype])
    bodyformula     <- extractPostConditionProofObligation ti
                         [1 .. farity] (farity+1) (funcRule checkfun)
    precondformula  <- preCondExpOf ti orgqn (init targsr)
    postcondformula <- applyFunc postfun targsr >>= pred2smt
    let title = "verify postcondition of '" ++ mainfunc ++ "'..."
    lift $ printWhenIntermediate opts $ "Trying to " ++ title
    vartypes <- getVarTypes
    pcproof <- lift $
      checkImplication opts vstref ("SMT script to " ++ title) vartypes
                       (tConj [precondformula, bodyformula])
                       tTrue postcondformula
    lift $ modifyIORef vstref (addPostCondToStats mainfunc (isJust pcproof))
    maybe
      (do lift $ (printWhenStatus opts $ mainfunc ++ ": POSTCOND CHECK ADDED")
          return (map (addPostConditionTo (funcName postfun)) allfuns) )
      (\proof -> do
         unless (optNoProof opts) $ lift $
           writeFile ("PROOF_" ++ showQNameNoDots orgqn ++ "_" ++
                      "SatisfiesPostCondition.smt") proof
         lift $ printWhenStatus opts $ mainfunc ++ ": POSTCONDITION VERIFIED"
         return allfuns )
      pcproof

 no demanded arguments

 deterministic operation

 <FAILING>

 referentially transparent operation

 no fixity defined

 {(_,_,_,_,_) |-> _}

 provePostCondition

 no precedence defined

 _

 ToolOptions.Options -> VerifierState.VerifyInfo
-> FlatCurry.Annotated.Types.AFuncDecl FlatCurry.Types.TypeExpr
-> [FlatCurry.Annotated.Types.AFuncDecl FlatCurry.Types.TypeExpr]
-> Data.IORef.IORef VerifierState.VState
-> Prelude.IO [FlatCurry.Annotated.Types.AFuncDecl FlatCurry.Types.TypeExpr]

 operation might suspend on free variables

 possibly non-terminating

 possibly non-reducible on same data term