sbvPlugin: Formally prove properties of Haskell programs using SBV/SMT

[ bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers ] [ Propose Tags ] [ Report a vulnerability ]
This version is deprecated.

GHC plugin for proving properties over Haskell functions using SMT solvers, based on the SBV package.

See Data.SBV.Plugin for a quick example, or the modules under Data.SBV.Plugin.Examples for more details.


[Skip to Readme]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

  • No Candidates
Versions [RSS] 0.1, 0.2, 0.3, 0.4, 0.5, 0.6, 0.7, 0.8, 0.9, 0.10, 0.11, 0.12, 9.0.1, 9.2.2, 9.4.4, 9.6.1, 9.8.1, 9.8.2, 9.10.1 (info)
Change log CHANGES.md
Dependencies base (>=4.8 && <5), containers, ghc, ghc-prim, mtl, sbv (>=5.7), template-haskell [details]
License BSD-3-Clause
Author Levent Erkok
Maintainer Levent Erkok (erkokl@gmail.com)
Category Formal methods, Theorem provers, Math, SMT, Symbolic Computation
Home page http://github.com/LeventErkok/sbvPlugin
Bug tracker http://github.com/LeventErkok/sbvPlugin/issues
Source repo head: git clone git://github.com/LeventErkok/sbvPlugin.git
Uploaded by LeventErkok at 2015-12-26T08:55:14Z
Distributions
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 6499 total (49 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs available [build log]
Last success reported on 2015-12-26 [all 1 reports]

Readme for sbvPlugin-0.5

[back to package description]

SBVPlugin: SBV Plugin for GHC

Hackage version Build Status

Example

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

Note the GHC option on the very first line. Either decorate your file with this option, or pass -fplugin=Data.SBV.Plugin as an argument to GHC, either on the command line or via cabal. Same trick also works for GHCi.

When compiled or loaded in to ghci, we get:

$ 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]} #-}

Using SBVPlugin from GHCi

The plugin should work from GHCi with no changes. Note that when run from GHCi, the plugin will behave as if the IgnoreFailure argument is given on all annotations, so that failures do not stop the load process.