Language.Verification

Strongly-typed utilities to aid in automatic verification (e.g. of programs) using an SMT solver.

This is mainly just a wrapper around Data.SBV that allows for inspection and manipulation of symbolic values, especially variable substitution.

The verification monad

data Verifier v a

Instances

MonadReader SMTConfig (Verifier v)

Defined in Language.Verification.Core

Methods

ask :: Verifier v SMTConfig

local :: (SMTConfig -> SMTConfig) -> Verifier v a -> Verifier v a

reader :: (SMTConfig -> a) -> Verifier v a

Monad (Verifier v)

Defined in Language.Verification.Core

Methods

(>>=) :: Verifier v a -> (a -> Verifier v b) -> Verifier v b

(>>) :: Verifier v a -> Verifier v b -> Verifier v b

return :: a -> Verifier v a

Functor (Verifier v)

Defined in Language.Verification.Core

Methods

fmap :: (a -> b) -> Verifier v a -> Verifier v b

(<$) :: a -> Verifier v b -> Verifier v a

Applicative (Verifier v)

Defined in Language.Verification.Core

Methods

pure :: a -> Verifier v a

(<*>) :: Verifier v (a -> b) -> Verifier v a -> Verifier v b

liftA2 :: (a -> b -> c) -> Verifier v a -> Verifier v b -> Verifier v c

(*>) :: Verifier v a -> Verifier v b -> Verifier v b

(<*) :: Verifier v a -> Verifier v b -> Verifier v a

MonadIO (Verifier v)

Defined in Language.Verification.Core

Methods

liftIO :: IO a -> Verifier v a

MonadError (VerifierError v) (Verifier v)

Defined in Language.Verification.Core

Methods

throwError :: VerifierError v -> Verifier v a

catchError :: Verifier v a -> (VerifierError v -> Verifier v a) -> Verifier v a

runVerifier :: VerifiableVar v => Verifier v a -> IO (Either (VerifierError v) a)

runVerifierWith :: VerifiableVar v => SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a)

data VerifierError v

Constructors

VEMismatchedSymbolType (VarKey v)

The same variable was used for two different symbol types

VESbvException String String

When running a query, SBV threw an exception

Instances

Show (VarKey v) => Show (VerifierError v)

Defined in Language.Verification.Core

Methods

showsPrec :: Int -> VerifierError v -> ShowS

show :: VerifierError v -> String

showList :: [VerifierError v] -> ShowS

(Typeable v, l ~ VarKey v, Show l, Typeable l) => Exception (VerifierError v)

Defined in Language.Verification.Core

Methods

toException :: VerifierError v -> SomeException

fromException :: SomeException -> Maybe (VerifierError v)

displayException :: VerifierError v -> String

MonadError (VerifierError v) (Verifier v)

Defined in Language.Verification.Core

Methods

throwError :: VerifierError v -> Verifier v a

catchError :: Verifier v a -> (VerifierError v -> Verifier v a) -> Verifier v a

The query monad

data Query v a

Instances

Monad (Query v)

Defined in Language.Verification.Core

Methods

(>>=) :: Query v a -> (a -> Query v b) -> Query v b

(>>) :: Query v a -> Query v b -> Query v b

return :: a -> Query v a

Functor (Query v)

Defined in Language.Verification.Core

Methods

fmap :: (a -> b) -> Query v a -> Query v b

(<$) :: a -> Query v b -> Query v a

MonadFail (Query v)

Defined in Language.Verification.Core

Methods

fail :: String -> Query v a

Applicative (Query v)

Defined in Language.Verification.Core

Methods

pure :: a -> Query v a

(<*>) :: Query v (a -> b) -> Query v a -> Query v b

liftA2 :: (a -> b -> c) -> Query v a -> Query v b -> Query v c

(*>) :: Query v a -> Query v b -> Query v b

(<*) :: Query v a -> Query v b -> Query v a

MonadIO (Query v)

Defined in Language.Verification.Core

Methods

liftIO :: IO a -> Query v a

query :: VerifiableVar v => Query v SBool -> VarEnv v -> Verifier v Bool

Verifiable variables

class (Typeable v, Ord (VarKey v), Show (VarKey v), Typeable (VarKey v)) => VerifiableVar v where

Associated Types

type VarKey v

type VarSym v :: * -> *

type VarEnv v :: *

Methods

symForVar :: v a -> VarEnv v -> Symbolic (VarSym v a)

varKey :: v a -> VarKey v

eqVarTypes :: v a -> v b -> Maybe (a :~: b)

castVarSym :: v a -> VarSym v b -> Maybe (VarSym v a)

Instances

VerifiableVar (WhileVar String)

Defined in Language.While.Syntax

Associated Types

type VarKey (WhileVar String)

type VarSym (WhileVar String) :: Type -> Type

type VarEnv (WhileVar String)

Methods

symForVar :: WhileVar String a -> VarEnv (WhileVar String) -> Symbolic (VarSym (WhileVar String) a)

varKey :: WhileVar String a -> VarKey (WhileVar String)

eqVarTypes :: WhileVar String a -> WhileVar String b -> Maybe (a :~: b)

castVarSym :: WhileVar String a -> VarSym (WhileVar String) b -> Maybe (VarSym (WhileVar String) a)

Verifier actions

evalProp :: (HMonad expr, HTraversable expr, VerifiableVar v, Exception (VerifierError v), HFoldableAt k expr, HFoldableAt k LogicOp, Monad m) => (forall a. Query v a -> m a) -> (forall a. VarSym v a -> m (k a)) -> Prop (expr v) b -> m (k b)

evalProp' :: (HMonad expr, HTraversable expr, VerifiableVar v, Exception (VerifierError v), HFoldableAt (Compose m k) expr, HFoldableAt (Compose m k) LogicOp, Monad m) => (forall a. Query v a -> m a) -> (forall a. VarSym v a -> m (k a)) -> Prop (expr v) b -> m (k b)

evalPropSimple :: (HMonad expr, HTraversable expr, VerifiableVar v, Exception (VerifierError v), HFoldableAt SBV expr, VarSym v ~ SBV) => Prop (expr v) b -> Query v (SBV b)

Miscellaneous combinators

subVar :: (HPointed expr, VerifiableVar v, Eq (VarKey v)) => expr v a -> v a -> v b -> expr v b

If the two variables match in both type and name, return the given expression. Otherwise, return an expression just containing this variable.

This is substitution into an expression, where the old expression is just a variable.

Expressions

module Language.Expression

SBV re-exports

data SMTConfig

Constructors

SMTConfig

Fields

• verbose :: Bool
• timing :: Timing
• printBase :: Int
• printRealPrec :: Int
• crackNum :: Bool
• satCmd :: String
• allSatMaxModelCount :: Maybe Int
• allSatPrintAlong :: Bool
• satTrackUFs :: Bool
• isNonModelVar :: String -> Bool
• validateModel :: Bool
• optimizeValidateConstraints :: Bool
• transcript :: Maybe FilePath
• smtLibVersion :: SMTLibVersion
• dsatPrecision :: Maybe Double
• solver :: SMTSolver
• extraArgs :: [String]
• allowQuantifiedQueries :: Bool
• roundingMode :: RoundingMode
• solverSetOptions :: [SMTOption]
• ignoreExitCode :: Bool
• redirectVerbose :: Maybe FilePath

Instances

Show SMTConfig

Defined in Data.SBV.Core.Symbolic

Methods

showsPrec :: Int -> SMTConfig -> ShowS

show :: SMTConfig -> String

showList :: [SMTConfig] -> ShowS

NFData SMTConfig

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SMTConfig -> ()

MonadReader SMTConfig (Verifier v)

Defined in Language.Verification.Core

Methods

ask :: Verifier v SMTConfig

local :: (SMTConfig -> SMTConfig) -> Verifier v a -> Verifier v a

reader :: (SMTConfig -> a) -> Verifier v a

defaultSMTCfg :: SMTConfig