sbv-9.1: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Copyright(c) Levent Erkok
LicenseBSD3
Maintainererkokl@gmail.com
Stabilityexperimental
Safe HaskellSafe-Inferred
LanguageHaskell2010

Documentation.SBV.Examples.Misc.Definitions

Description

Demonstrates how we can add actual SMT-definitions for functions that cannot otherwise be defined in SBV. Typically, these are used for recursive definitions.

Synopsis

Documentation

sumToN :: SInteger -> SInteger Source #

Sum of numbers from 0 to the given number. Note that this cannot be defined as a regular Haskell function, as it wouldn't terminate as it recurses on a symbolic argument.

defineSum :: Symbolic () Source #

Add the definition of sum to the SMT solver. Note that SBV performs no checks on your definition, neither that it is well formed, or even has the correct type!

badExample :: IO ThmResult Source #

A simple proof using sumToN. We get a failure, because we haven't given the solver the definition, and thus it goes completely uninterpreted.

We have:

>>> badExample
Falsifiable. Counter-example:
  sumToN :: Integer -> Integer
  sumToN _ = 0

Since sumToN remains uninterpreted, the solver gave us a model that obviously fails the property.

goodExample :: IO ThmResult Source #

Same example, except this time we give the solver the definition of the function, and thus the proof goes through.

We have:

>>> goodExample
Q.E.D.

In this case, the solver has the definition, and proves the predicate as expected.