Copyright | (c) Levent Erkok |
---|---|
License | BSD3 |
Maintainer | erkokl@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
(The sbvPlugin is hosted at http://github.com/LeventErkok/sbvPlugin. Comments, bug reports, and patches are always welcome.)
SBVPlugin: A GHC Plugin for SBV, SMT Based Verification
SBV is a library for express properties about Haskell programs and automatically proving them using SMT solvers. The SBVPlugin allows simple annotations on Haskell functions to prove them directly during GHC compilation time.
Consider the following simple program:
{-# OPTIONS_GHC -fplugin=Data.SBV.Plugin #-} module Test where import Data.SBV.Plugin {-# ANN test theorem #-} test :: Integer -> Integer -> Bool test x y = x + y >= x - y
We have:
$ ghc -c Test.hs [SBV] Test.hs:9:1-4 Proving "test", using Z3. [Z3] Falsifiable. Counter-example: x = 0 :: Integer y = -1 :: Integer [SBV] Failed. (Use option 'IgnoreFailure' to continue.)
Note that the compilation will be aborted, since the theorem doesn't hold. As shown in the hint, GHC can be instructed to continue in that case, using an annotation of the form:
{-# ANN test theorem {options = [IgnoreFailure]} #-}
The plugin should work from GHCi with no changes. Note that when run from GHCi, the plugin will behave as if the IgnoreFailure option is given on all annotations, so that failures do not stop the load process.
- plugin :: Plugin
- newtype SBVAnnotation = SBV {}
- sbv :: SBVAnnotation
- theorem :: SBVAnnotation
- data SBVOption
Entry point
Annotations
newtype SBVAnnotation Source
The actual annotation.
A property annotation, using default options.
theorem :: SBVAnnotation Source
Synonym for sbv really, just looks cooler
Plugin options
Plugin options. Note that we allow picking multiple solvers, which
will all be run in parallel. If you want to run all available solvers,
use the option AnySolver
. The default is to error-out on failure, using
the default-SMT solver picked by SBV, which is currently Z3.
IgnoreFailure | Continue even if proof fails |
Skip String | Skip the proof. Can be handy for properties that we currently do not want to focus on. |
Verbose | Produce verbose output, good for debugging |
Safety | Check for safety |
QuickCheck | Perform quickCheck |
Uninterpret | Uninterpret this binding for proof purposes |
Names [String] | Use these names for the arguments; need not be exhaustive |
Z3 | Use Z3 |
Yices | Use Yices |
Boolector | Use Boolector |
CVC4 | Use CVC4 |
MathSAT | Use MathSAT |
ABC | Use ABC |
AnySolver | Use all installed solvers |