| Safe Haskell | None |
|---|---|
| Language | Haskell2010 |
Language.Verification
Description
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.
Synopsis
- data 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
- data Query v a
- query :: VerifiableVar v => Query v SBool -> VarEnv v -> Verifier v Bool
- class (Typeable v, Ord (VarKey v), Show (VarKey v), Typeable (VarKey v)) => VerifiableVar v where
- 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)
- subVar :: (HPointed expr, VerifiableVar v, Eq (VarKey v)) => expr v a -> v a -> v b -> expr v b
- module Language.Expression
- data SMTConfig = SMTConfig {
- verbose :: Bool
- timing :: Timing
- printBase :: Int
- printRealPrec :: Int
- satCmd :: String
- allSatMaxModelCount :: Maybe Int
- allSatPrintAlong :: Bool
- satTrackUFs :: Bool
- isNonModelVar :: Text -> 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
- defaultSMTCfg :: SMTConfig
The verification monad
Instances
| MonadReader SMTConfig (Verifier v) Source # | |
| Monad (Verifier v) Source # | |
| Functor (Verifier v) Source # | |
| Applicative (Verifier v) Source # | |
Defined in Language.Verification.Core | |
| MonadIO (Verifier v) Source # | |
Defined in Language.Verification.Core | |
| MonadError (VerifierError v) (Verifier v) Source # | |
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) Source #
runVerifierWith :: VerifiableVar v => SMTConfig -> Verifier v a -> IO (Either (VerifierError v) a) Source #
data VerifierError v Source #
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) Source # | |
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) Source # | |
Defined in Language.Verification.Core Methods toException :: VerifierError v -> SomeException # fromException :: SomeException -> Maybe (VerifierError v) # displayException :: VerifierError v -> String # | |
| MonadError (VerifierError v) (Verifier v) Source # | |
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
Verifiable variables
class (Typeable v, Ord (VarKey v), Show (VarKey v), Typeable (VarKey v)) => VerifiableVar v where Source #
Methods
symForVar :: v a -> VarEnv v -> Symbolic (VarSym v a) Source #
varKey :: v a -> VarKey v Source #
eqVarTypes :: v a -> v b -> Maybe (a :~: b) Source #
castVarSym :: v a -> VarSym v b -> Maybe (VarSym v a) Source #
Instances
| VerifiableVar (WhileVar String) Source # | |
Defined in Language.While.Syntax Associated Types type VarKey (WhileVar String) Source # Methods symForVar :: WhileVar String a -> VarEnv (WhileVar String) -> Symbolic (VarSym (WhileVar String) a) Source # varKey :: WhileVar String a -> VarKey (WhileVar String) Source # eqVarTypes :: WhileVar String a -> WhileVar String b -> Maybe (a :~: b) Source # castVarSym :: WhileVar String a -> VarSym (WhileVar String) b -> Maybe (VarSym (WhileVar String) a) Source # | |
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) Source #
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) Source #
evalPropSimple :: (HMonad expr, HTraversable expr, VerifiableVar v, Exception (VerifierError v), HFoldableAt SBV expr, VarSym v ~ SBV) => Prop (expr v) b -> Query v (SBV b) Source #
Miscellaneous combinators
subVar :: (HPointed expr, VerifiableVar v, Eq (VarKey v)) => expr v a -> v a -> v b -> expr v b Source #
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
Solver configuration. See also z3, yices, cvc4, boolector, mathSAT, etc.
which are instantiations of this type for those solvers, with reasonable defaults. In particular, custom configuration can be
created by varying those values. (Such as z3{verbose=True}.)
Most fields are self explanatory. The notion of precision for printing algebraic reals stems from the fact that such values does
not necessarily have finite decimal representations, and hence we have to stop printing at some depth. It is important to
emphasize that such values always have infinite precision internally. The issue is merely with how we print such an infinite
precision value on the screen. The field printRealPrec controls the printing precision, by specifying the number of digits after
the decimal point. The default value is 16, but it can be set to any positive integer.
When printing, SBV will add the suffix ... at the and of a real-value, if the given bound is not sufficient to represent the real-value
exactly. Otherwise, the number will be written out in standard decimal notation. Note that SBV will always print the whole value if it
is precise (i.e., if it fits in a finite number of digits), regardless of the precision limit. The limit only applies if the representation
of the real value is not finite, i.e., if it is not rational.
The printBase field can be used to print numbers in base 2, 10, or 16. If base 2 or 16 is used, then floating-point values will
be printed in their internal memory-layout format as well, which can come in handy for bit-precise analysis.
Constructors
| SMTConfig | |
Fields
| |
Instances
| Show SMTConfig | We show the name of the solver for the config. Arguably this is misleading, but better than nothing. |
| NFData SMTConfig | |
Defined in Data.SBV.Core.Symbolic | |
| MonadReader SMTConfig (Verifier v) Source # | |
The default solver used by SBV. This is currently set to z3.