sbv-8.2: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.

Copyright(c) Brian Schroeder
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellNone
LanguageHaskell2010

Documentation.SBV.Examples.Transformers.SymbolicEval

Contents

Description

A demonstration of the use of the SymbolicT and QueryT transformers in the setting of symbolic program evaluation.

In this example, we perform symbolic evaluation across three steps:

  1. allocate free variables, so we can extract a model after evaluation
  2. perform symbolic evaluation of a program and an associated property
  3. querying the solver for whether it's possible to find a set of program inputs that falsify the property. if there is, we extract a model.

To simplify the example, our programs always have exactly two integer inputs named x and y.

Synopsis

Allocation of symbolic variables, so we can extract a model later.

newtype Alloc a Source #

Monad for allocating free variables.

Constructors

Alloc 
Instances
Monad Alloc Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

(>>=) :: Alloc a -> (a -> Alloc b) -> Alloc b #

(>>) :: Alloc a -> Alloc b -> Alloc b #

return :: a -> Alloc a #

fail :: String -> Alloc a #

Functor Alloc Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

fmap :: (a -> b) -> Alloc a -> Alloc b #

(<$) :: a -> Alloc b -> Alloc a #

Applicative Alloc Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

pure :: a -> Alloc a #

(<*>) :: Alloc (a -> b) -> Alloc a -> Alloc b #

liftA2 :: (a -> b -> c) -> Alloc a -> Alloc b -> Alloc c #

(*>) :: Alloc a -> Alloc b -> Alloc b #

(<*) :: Alloc a -> Alloc b -> Alloc a #

MonadIO Alloc Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

liftIO :: IO a -> Alloc a #

MonadSymbolic Alloc Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

MonadError String Alloc Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

throwError :: String -> Alloc a #

catchError :: Alloc a -> (String -> Alloc a) -> Alloc a #

data Env Source #

Environment holding allocated variables.

Constructors

Env 
Instances
Eq Env Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

(==) :: Env -> Env -> Bool #

(/=) :: Env -> Env -> Bool #

Show Env Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

showsPrec :: Int -> Env -> ShowS #

show :: Env -> String #

showList :: [Env] -> ShowS #

MonadReader Env Eval Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

ask :: Eval Env #

local :: (Env -> Env) -> Eval a -> Eval a #

reader :: (Env -> a) -> Eval a #

alloc :: String -> Alloc (SBV Integer) Source #

Allocate an integer variable with the provided name.

allocEnv :: Alloc Env Source #

Allocate an Env holding all input variables for the program.

Symbolic term evaluation

data Term :: * -> * where Source #

The term language we use to express programs and properties.

newtype Eval a Source #

Monad for performing symbolic evaluation.

Constructors

Eval 

Fields

Instances
Monad Eval Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

(>>=) :: Eval a -> (a -> Eval b) -> Eval b #

(>>) :: Eval a -> Eval b -> Eval b #

return :: a -> Eval a #

fail :: String -> Eval a #

Functor Eval Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

fmap :: (a -> b) -> Eval a -> Eval b #

(<$) :: a -> Eval b -> Eval a #

Applicative Eval Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

pure :: a -> Eval a #

(<*>) :: Eval (a -> b) -> Eval a -> Eval b #

liftA2 :: (a -> b -> c) -> Eval a -> Eval b -> Eval c #

(*>) :: Eval a -> Eval b -> Eval b #

(<*) :: Eval a -> Eval b -> Eval a #

MonadReader Env Eval Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

ask :: Eval Env #

local :: (Env -> Env) -> Eval a -> Eval a #

reader :: (Env -> a) -> Eval a #

MonadError String Eval Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

throwError :: String -> Eval a #

catchError :: Eval a -> (String -> Eval a) -> Eval a #

unsafeCastSBV :: SBV a -> SBV b Source #

Unsafe cast for symbolic values. In production code, we would check types instead.

eval :: Term r -> Eval (SBV r) Source #

Symbolic evaluation function for Term.

runEval :: Env -> Term a -> Except String (SBV a) Source #

Runs symbolic evaluation, sending a Term to a symbolic value (or failing). Used for symbolic evaluation of programs and properties.

newtype Program a Source #

A program that can reference two input variables, x and y.

Constructors

Program (Term a) 

newtype Result Source #

A symbolic value representing the result of running a program -- its output.

Constructors

Result SVal 

mkResult :: SBV a -> Result Source #

Makes a Result from a symbolic value.

runProgramEval :: Env -> Program a -> Except String Result Source #

Performs symbolic evaluation of a Program.

Property evaluation

newtype Property Source #

A property describes a quality of a Program. It is a Term yields a boolean value.

Constructors

Property (Term Bool) 

runPropertyEval :: Result -> Env -> Property -> Except String (SBV Bool) Source #

Performs symbolic evaluation of a 'Property.

Checking whether a program satisfies a property

generalize :: Monad m => Identity a -> m a Source #

Sends an Identity computation to an arbitrary monadic computation.

newtype Q a Source #

Monad for querying a solver.

Constructors

Q 

Fields

Instances
Monad Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

(>>=) :: Q a -> (a -> Q b) -> Q b #

(>>) :: Q a -> Q b -> Q b #

return :: a -> Q a #

fail :: String -> Q a #

Functor Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

fmap :: (a -> b) -> Q a -> Q b #

(<$) :: a -> Q b -> Q a #

Applicative Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

pure :: a -> Q a #

(<*>) :: Q (a -> b) -> Q a -> Q b #

liftA2 :: (a -> b -> c) -> Q a -> Q b -> Q c #

(*>) :: Q a -> Q b -> Q b #

(<*) :: Q a -> Q b -> Q a #

MonadIO Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

liftIO :: IO a -> Q a #

MonadQuery Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

MonadError String Q Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

throwError :: String -> Q a #

catchError :: Q a -> (String -> Q a) -> Q a #

mkQuery :: Env -> Q CheckResult Source #

Creates a computation that queries a solver and yields a CheckResult.

check :: Program a -> Property -> IO (Either String CheckResult) Source #

Checks a Property of a Program (or fails).

Some examples

ex1 :: IO (Either String CheckResult) Source #

Check that x+y+1 generates a counter-example for the property that the result is less than 10 when x+y is at least 9. We have:

>>> ex1
Right (Counterexample 0 9)

ex2 :: IO (Either String CheckResult) Source #

Check that the program x+y correctly produces a result greater than 1 when both x and y are at least 1. We have:

>>> ex2
Right Proved

ex3 :: IO (Either String CheckResult) Source #

Check that we catch the cases properly through the monad stack when there is a syntax error, like an undefined variable. We have:

>>> ex3
Left "unknown variable"