verifiable-expressions-0.6.1: An intermediate language for Hoare logic style verification.
Safe HaskellNone
LanguageHaskell2010

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

The verification monad

data Verifier v a Source #

Instances

Instances details
MonadReader SMTConfig (Verifier v) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Language.Verification.Core

Methods

liftIO :: IO a -> Verifier v a #

MonadError (VerifierError v) (Verifier v) Source # 
Instance details

Defined in Language.Verification.Core

Methods

throwError :: VerifierError v -> Verifier v a #

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

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

The query monad

data Query v a Source #

Instances

Instances details
Monad (Query v) Source # 
Instance details

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) Source # 
Instance details

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) Source # 
Instance details

Defined in Language.Verification.Core

Methods

fail :: String -> Query v a #

Applicative (Query v) Source # 
Instance details

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) Source # 
Instance details

Defined in Language.Verification.Core

Methods

liftIO :: IO a -> Query v a #

Verifiable variables

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

Associated Types

type VarKey v Source #

type VarSym v :: * -> * Source #

type VarEnv v :: * 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 #

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 #

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

SBV re-exports

data SMTConfig #

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

Instances details
Show SMTConfig

We show the name of the solver for the config. Arguably this is misleading, but better than nothing.

Instance details

Defined in Data.SBV.Core.Symbolic

NFData SMTConfig 
Instance details

Defined in Data.SBV.Core.Symbolic

Methods

rnf :: SMTConfig -> () #

MonadReader SMTConfig (Verifier v) Source # 
Instance details

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 #

The default solver used by SBV. This is currently set to z3.