|
definition:
|
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
|