sbv-8.6: 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

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 

Fields

Instances

Instances details
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

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 

Fields

Instances

Instances details
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.

Constructors

Var :: String -> Term r 
Lit :: Integer -> Term Integer 
Plus :: Term Integer -> Term Integer -> Term Integer 
LessThan :: Term Integer -> Term Integer -> Term Bool 
GreaterThan :: Term Integer -> Term Integer -> Term Bool 
Equals :: Term Integer -> Term Integer -> Term Bool 
Not :: Term Bool -> Term Bool 
Or :: Term Bool -> Term Bool -> Term Bool 
And :: Term Bool -> Term Bool -> Term Bool 
Implies :: Term Bool -> Term Bool -> Term Bool 

newtype Eval a Source #

Monad for performing symbolic evaluation.

Constructors

Eval 

Fields

Instances

Instances details
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

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

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

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

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

data CheckResult Source #

The result of checking the combination of a Program and a Property.

Constructors

Proved 
Counterexample Integer Integer 

Instances

Instances details
Eq CheckResult Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

(==) :: CheckResult -> CheckResult -> Bool

(/=) :: CheckResult -> CheckResult -> Bool

Show CheckResult Source # 
Instance details

Defined in Documentation.SBV.Examples.Transformers.SymbolicEval

Methods

showsPrec :: Int -> CheckResult -> ShowS

show :: CheckResult -> String

showList :: [CheckResult] -> ShowS

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

Instances details
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

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"