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

Copyright | (c) Brian Schroeder
License | BSD3
Maintainer | erkokl@gmail.com
Stability | experimental
Safe Haskell | None
Language | Haskell2010

Documentation.SBV.Examples.Transformers.SymbolicEval

Contents

- Allocation of symbolic variables, so we can extract a model later.
- Symbolic term evaluation
- Property evaluation
- Checking whether a program satisfies a property
- Some examples

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

- newtype Alloc a = Alloc {
  - runAlloc :: SymbolicT (ExceptT String IO) a
  }
- data Env = Env {
  - envX :: SBV Integer
  - envY :: SBV Integer
  - result :: Maybe SVal
  }
- alloc :: String -> Alloc (SBV Integer)
- allocEnv :: Alloc Env
- data Term :: * -> * where
  - 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 = Eval {
  - unEval :: ReaderT Env (Except String) a
  }
- unsafeCastSBV :: SBV a -> SBV b
- eval :: Term r -> Eval (SBV r)
- runEval :: Env -> Term a -> Except String (SBV a)
- newtype Program a = Program (Term a)
- newtype Result = Result SVal
- mkResult :: SBV a -> Result
- runProgramEval :: Env -> Program a -> Except String Result
- newtype Property = Property (Term Bool)
- runPropertyEval :: Result -> Env -> Property -> Except String (SBV Bool)
- data CheckResult
  - = Proved
  - | Counterexample Integer Integer
- generalize :: Monad m => Identity a -> m a
- newtype Q a = Q {
  - runQ :: QueryT (ExceptT String IO) a
  }
- mkQuery :: Env -> Q CheckResult
- check :: Program a -> Property -> IO (Either String CheckResult)
- ex1 :: IO (Either String CheckResult)
- ex2 :: IO (Either String CheckResult)
- ex3 :: IO (Either String CheckResult)

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

newtype Alloc a Source #

Monad for allocating free variables.

Constructors

Alloc |

Fields

- runAlloc :: SymbolicT (ExceptT String IO) a

#### 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 Methods symbolicEnv :: Alloc State Source #
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

- envX :: SBV Integer
- envY :: SBV Integer
- result :: Maybe SVal

#### 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

- unEval :: ReaderT Env (Except String) a

#### 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 `check`ing 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

- runQ :: QueryT (ExceptT String IO) a

#### 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 Methods queryState :: Q State Source #
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"