Verification.hs revision a46759a60a40e273585c54c971213d5cd6dc7d00
75f5c2db254c0167a0e396254460de09b775d203trawick{-# LANGUAGE FlexibleContexts #-}
75f5c2db254c0167a0e396254460de09b775d203trawickModule : $Header$
75f5c2db254c0167a0e396254460de09b775d203trawickDescription : Generation of Verification Conditions
75f5c2db254c0167a0e396254460de09b775d203trawickCopyright : (c) Ewaryst Schulz, DFKI Bremen 2011
75f5c2db254c0167a0e396254460de09b775d203trawickLicense : GPLv2 or higher, see LICENSE.txt
75f5c2db254c0167a0e396254460de09b775d203trawickMaintainer : ewaryst.schulz@dfki.de
75f5c2db254c0167a0e396254460de09b775d203trawickStability : experimental
75f5c2db254c0167a0e396254460de09b775d203trawickPortability : non-portable (via imports)
75f5c2db254c0167a0e396254460de09b775d203trawickThis module provides functionality for the generation of verification conditions
75f5c2db254c0167a0e396254460de09b775d203trawickduring program evaluation.
75f5c2db254c0167a0e396254460de09b775d203trawick--import qualified Data.Map as Map
75f5c2db254c0167a0e396254460de09b775d203trawickimport qualified Data.Set as Set
75f5c2db254c0167a0e396254460de09b775d203trawickimport Control.Monad.Trans (MonadIO (..))
75f5c2db254c0167a0e396254460de09b775d203trawickimport Control.Monad.Error (MonadError (..))
75f5c2db254c0167a0e396254460de09b775d203trawick-- ----------------------------------------------------------------------
75f5c2db254c0167a0e396254460de09b775d203trawick-- * Verification Conditions
75f5c2db254c0167a0e396254460de09b775d203trawick-- ----------------------------------------------------------------------
75f5c2db254c0167a0e396254460de09b775d203trawick{- Given an instantiated constant this data structure keeps
75f5c2db254c0167a0e396254460de09b775d203trawick* the value of this constant looked up in the assignment store
75f5c2db254c0167a0e396254460de09b775d203trawick* for function constants its definition (looked up in the assignment store)
75f5c2db254c0167a0e396254460de09b775d203trawick* the for this constant generated verification condition
75f5c2db254c0167a0e396254460de09b775d203trawickdata VCData = VCData
75f5c2db254c0167a0e396254460de09b775d203trawick { vcValue :: EXPRESSION
75f5c2db254c0167a0e396254460de09b775d203trawick , vcDef :: Maybe AssDefinition
75f5c2db254c0167a0e396254460de09b775d203trawick , vcCondition :: EXPRESSION
75f5c2db254c0167a0e396254460de09b775d203trawicktype VCMap = Map.Map InstantiatedConstant VCData
75f5c2db254c0167a0e396254460de09b775d203trawick-- | Extra functionality of 'AssignmentStore's for VC generation
75f5c2db254c0167a0e396254460de09b775d203trawickclass AssignmentStore m => VCGenerator m where
75f5c2db254c0167a0e396254460de09b775d203trawick addVC :: EvalAtom -> EXPRESSION -> m ()
75f5c2db254c0167a0e396254460de09b775d203trawick -- these constants should be already part of the pure assignment store
75f5c2db254c0167a0e396254460de09b775d203trawick getDepGraph :: m (AssignmentDepGraph ())
75f5c2db254c0167a0e396254460de09b775d203trawick updateConstant :: ConstantName -> AssDefinition -> m ()
75f5c2db254c0167a0e396254460de09b775d203trawickgetVCPremises :: (Ord a) => AssignmentDepGraph a -- ^ 'DepGraph' for lookup
75f5c2db254c0167a0e396254460de09b775d203trawick -> EXPRESSION -- ^ generate premise for this term
75f5c2db254c0167a0e396254460de09b775d203trawick -> [EXPRESSION]
75f5c2db254c0167a0e396254460de09b775d203trawickgetVCPremises adg e =
75f5c2db254c0167a0e396254460de09b775d203trawick let scl = Set.map SimpleConstant $ setOfUserDefined e
75f5c2db254c0167a0e396254460de09b775d203trawick f (sc, depGrAnno) = mkVCPrem sc $ annoDef depGrAnno
75f5c2db254c0167a0e396254460de09b775d203trawick in map f $ Set.toList $ upperUntilRefl (const $ const False) adg scl
75f5c2db254c0167a0e396254460de09b775d203trawickmkVCPrem :: ConstantName -> AssDefinition -> EXPRESSION
75f5c2db254c0167a0e396254460de09b775d203trawickmkVCPrem n def
75f5c2db254c0167a0e396254460de09b775d203trawick | null args = toExp ("=", n, e)
75f5c2db254c0167a0e396254460de09b775d203trawick | otherwise = f args
75f5c2db254c0167a0e396254460de09b775d203trawick where e = getDefiniens def
75f5c2db254c0167a0e396254460de09b775d203trawick args = getArguments def
75f5c2db254c0167a0e396254460de09b775d203trawick f (x:l) = g x $ f l
75f5c2db254c0167a0e396254460de09b775d203trawick f _ = toExp ("=", toExp(n, map mkVar args), e)
75f5c2db254c0167a0e396254460de09b775d203trawick g v b = toExp ("all", mkVar v, b)
75f5c2db254c0167a0e396254460de09b775d203trawickmkVC :: ConstantName
75f5c2db254c0167a0e396254460de09b775d203trawick -> AssDefinition
75f5c2db254c0167a0e396254460de09b775d203trawick -> EXPRESSION -- ^ the evaluated term for the constant
75f5c2db254c0167a0e396254460de09b775d203trawick -> [EXPRESSION] -- ^ a list of premises from assignment graph
75f5c2db254c0167a0e396254460de09b775d203trawick -> EXPRESSION
75f5c2db254c0167a0e396254460de09b775d203trawickmkVC _ def evalE prl =
75f5c2db254c0167a0e396254460de09b775d203trawick let prem = foldl f (head prl) $ tail prl
75f5c2db254c0167a0e396254460de09b775d203trawick f a b = toExp ("and", a, b)
a7452f0ad4045af1d42dce45cc25854e7bf3cac4trawick conc = toExp ("=", getDefiniens def, evalE)
75f5c2db254c0167a0e396254460de09b775d203trawick in if null prl then conc else toExp ("impl", prem, conc)
75f5c2db254c0167a0e396254460de09b775d203trawickmkBoolVC :: EXPRESSION -- ^ the Boolean term
75f5c2db254c0167a0e396254460de09b775d203trawick -> Bool -- ^ the evaluated Boolean term
75f5c2db254c0167a0e396254460de09b775d203trawick -> [EXPRESSION] -- ^ a list of premises from assignment graph
75f5c2db254c0167a0e396254460de09b775d203trawick -> EXPRESSION
75f5c2db254c0167a0e396254460de09b775d203trawickmkBoolVC e evalB prl =
75f5c2db254c0167a0e396254460de09b775d203trawick let prem = foldl f (head prl) $ tail prl
75f5c2db254c0167a0e396254460de09b775d203trawick f a b = toExp ("and", a, b)
a7452f0ad4045af1d42dce45cc25854e7bf3cac4trawick conc = if evalB then e else toExp ("not", e)
a7452f0ad4045af1d42dce45cc25854e7bf3cac4trawick in if null prl then conc else toExp ("impl", prem, conc)
75f5c2db254c0167a0e396254460de09b775d203trawickverifyingStepper ::
75f5c2db254c0167a0e396254460de09b775d203trawick (StepDebugger m, VCGenerator m, MonadIO m, MonadError ASError m) =>
75f5c2db254c0167a0e396254460de09b775d203trawick m () -> EvalAtom -> m Bool
75f5c2db254c0167a0e396254460de09b775d203trawickverifyingStepper prog x = do
75f5c2db254c0167a0e396254460de09b775d203trawick -- liftIO $ putStrLn $ "At step " ++ show (prettyEvalAtom x)
75f5c2db254c0167a0e396254460de09b775d203trawick -- liftIO $ putStrLn ""
75f5c2db254c0167a0e396254460de09b775d203trawick b <- evaluateAndVerify prog x
75f5c2db254c0167a0e396254460de09b775d203trawick dm <- getDebugMode
75f5c2db254c0167a0e396254460de09b775d203trawick when dm $ do
75f5c2db254c0167a0e396254460de09b775d203trawick let breakPred s = s == "q" || s == "c" || null s
75f5c2db254c0167a0e396254460de09b775d203trawick s <- readEvalPrintLoop stdin stdout "next>" breakPred
75f5c2db254c0167a0e396254460de09b775d203trawick when (s == "q") $ throwError $ ASError UserError "Quit Debugger"
75f5c2db254c0167a0e396254460de09b775d203trawick when (s == "c") $ setDebugMode False
75f5c2db254c0167a0e396254460de09b775d203trawickevaluateAndVerify :: (VCGenerator m) => m () -> EvalAtom -> m Bool
75f5c2db254c0167a0e396254460de09b775d203trawickevaluateAndVerify _ ea@(AssAtom n def) = do
75f5c2db254c0167a0e396254460de09b775d203trawick adg <- getDepGraph
75f5c2db254c0167a0e396254460de09b775d203trawick let prl = getVCPremises adg $ getDefiniens def
75f5c2db254c0167a0e396254460de09b775d203trawick e <- assign n def
75f5c2db254c0167a0e396254460de09b775d203trawick addVC ea $ mkVC n def e prl
75f5c2db254c0167a0e396254460de09b775d203trawick -- update the depgraph in the assignment store
75f5c2db254c0167a0e396254460de09b775d203trawick updateConstant n $ updateDefinition e def
75f5c2db254c0167a0e396254460de09b775d203trawick return True
75f5c2db254c0167a0e396254460de09b775d203trawickevaluateAndVerify _ ea@(CaseAtom e) = do
75f5c2db254c0167a0e396254460de09b775d203trawick adg <- getDepGraph
75f5c2db254c0167a0e396254460de09b775d203trawick let prl = getVCPremises adg e
75f5c2db254c0167a0e396254460de09b775d203trawick b <- check e
75f5c2db254c0167a0e396254460de09b775d203trawick addVC ea $ mkBoolVC e b prl
75f5c2db254c0167a0e396254460de09b775d203trawickevaluateAndVerify prog ea@(RepeatAtom e) = do
75f5c2db254c0167a0e396254460de09b775d203trawick adg <- getDepGraph
75f5c2db254c0167a0e396254460de09b775d203trawick let prl = getVCPremises adg e
75f5c2db254c0167a0e396254460de09b775d203trawick b <- check e
75f5c2db254c0167a0e396254460de09b775d203trawick addVC ea $ mkBoolVC e b prl