sbv-2.7: sbv.cabal
Name: sbv
Version: 2.7
Category: Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT
Synopsis: SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
Description: Express properties about Haskell programs and automatically prove them using SMT
(Satisfiability Modulo Theories) solvers. Automatically generate C programs from
Haskell functions. The SBV library adds support for symbolic bit vectors and other
symbolic types, allowing formal models of Haskell programs to be created.
.
> $ ghci -XScopedTypeVariables
> Prelude> :m Data.SBV
> Prelude Data.SBV> prove $ \(x::SWord8) -> x `shiftL` 2 .== 4*x
> Q.E.D.
> Prelude Data.SBV> prove $ forAll ["x"] $ \(x::SWord8) -> x `shiftL` 2 .== x
> Falsifiable. Counter-example:
> x = 128 :: SWord8
.
The SBV library uses Microsoft's Z3 SMT solver (<http://research.microsoft.com/en-us/um/redmond/projects/z3/>) as the default underlying solver. It is also possible to use SRI's Yices SMT solver with SBV as well (<http://yices.csl.sri.com/download-yices2.shtml>), although the Z3 binding is much more richer.
.
SBV introduces the following types and concepts:
.
* 'SBool': Symbolic Booleans (bits)
.
* 'SWord8', 'SWord16', 'SWord32', 'SWord64': Symbolic Words (unsigned)
.
* 'SInt8', 'SInt16', 'SInt32', 'SInt64': Symbolic Ints (signed)
.
* 'SInteger': Symbolic unbounded integers (signed)
.
* 'SReal': Symbolic algebraic reals (signed)
.
* 'SArray', 'SFunArray': Flat arrays of symbolic values
.
* 'STree': Full binary trees of symbolic values (for fast symbolic access)
.
* Symbolic polynomials over GF(2^n), and polynomial arithmetic
.
* Uninterpreted constants and functions over symbolic values, with user defined axioms.
.
* Uninterpreted sorts, and proofs over such sorts, potentially with axioms.
.
Functions built out of these types can be:
.
* proven correct via an external SMT solver (the 'prove' function)
.
* checked for satisfiability (the 'sat', and 'allSat' functions)
.
* used in synthesis (the 'sat' function with existential variables)
.
* optimized with respect to cost functions (the 'optimize', 'maximize',
and 'minimize' functions)
.
* quick-checked
.
* used in concrete test case generation (the 'genTest' function), rendered as
values in various languages, including Haskell and C.
.
Predicates can have both existential and universal variables. Use of
alternating quantifiers provides considerable expressive power.
Furthermore, existential variables allow synthesis via model generation.
.
The SBV library can also compile Haskell functions that manipulate symbolic
values directly to C, rendering them as straight-line C programs.
.
In addition to the library, the installation will create the
executable @SBVUnitTests@. You should run it once the installation is complete,
to make sure the unit tests are run and all is well.
.
SBV is hosted at GitHub: <http://github.com/LeventErkok/sbv>. Comments,
bug reports, and patches are always welcome.
.
The following people reported bugs, provided comments/feedback, or contributed to the
development of SBV in various ways: Ian Blumenfeld, Ian Calvert, Iavor Diatchki, John
Erickson, Tom Hawkins, Lee Pike, Austin Seipp, Don Stewart, Josef Svenningsson, and
Nis Wegmann.
.
Release notes can be seen at: <http://github.com/LeventErkok/sbv/blob/master/RELEASENOTES>.
Copyright: Levent Erkok, 2010-2012
License: BSD3
License-file: LICENSE
Stability: Experimental
Author: Levent Erkok
Homepage: http://github.com/LeventErkok/sbv
Bug-reports: http://github.com/LeventErkok/sbv/issues
Maintainer: Levent Erkok (erkokl@gmail.com)
Build-Type: Simple
Cabal-Version: >= 1.14
Data-Files: SBVUnitTest/GoldFiles/*.gold
Extra-Source-Files: INSTALL, README, COPYRIGHT, RELEASENOTES
source-repository head
type: git
location: git://github.com/LeventErkok/sbv.git
Library
default-language: Haskell2010
ghc-options : -Wall
other-extensions: BangPatterns
-- Currently commented out since Cabal doesn't yet recognize DefaultSignatures extension yet. Uncomment when it does.
-- The current list can be seen at: https://github.com/haskell/cabal/blob/master/Cabal/Language/Haskell/Extension.hs
-- DefaultSignatures
DeriveDataTypeable
FlexibleContexts
FlexibleInstances
FunctionalDependencies
GeneralizedNewtypeDeriving
MultiParamTypeClasses
OverlappingInstances
ParallelListComp
PatternGuards
Rank2Types
RankNTypes
ScopedTypeVariables
TupleSections
TypeOperators
TypeSynonymInstances
Build-Depends : base >= 4 && < 5
, array, containers, deepseq, directory, filepath, old-time
, pretty, process, mtl, QuickCheck, random, syb
Exposed-modules : Data.SBV
, Data.SBV.Internals
, Data.SBV.Examples.BitPrecise.BitTricks
, Data.SBV.Examples.BitPrecise.Legato
, Data.SBV.Examples.BitPrecise.MergeSort
, Data.SBV.Examples.BitPrecise.PrefixSum
, Data.SBV.Examples.CodeGeneration.AddSub
, Data.SBV.Examples.CodeGeneration.CRC_USB5
, Data.SBV.Examples.CodeGeneration.Fibonacci
, Data.SBV.Examples.CodeGeneration.GCD
, Data.SBV.Examples.CodeGeneration.PopulationCount
, Data.SBV.Examples.CodeGeneration.Uninterpreted
, Data.SBV.Examples.Crypto.AES
, Data.SBV.Examples.Crypto.RC4
, Data.SBV.Examples.Existentials.CRCPolynomial
, Data.SBV.Examples.Existentials.Diophantine
, Data.SBV.Examples.Polynomials.Polynomials
, Data.SBV.Examples.Puzzles.Coins
, Data.SBV.Examples.Puzzles.Counts
, Data.SBV.Examples.Puzzles.DogCatMouse
, Data.SBV.Examples.Puzzles.Euler185
, Data.SBV.Examples.Puzzles.MagicSquare
, Data.SBV.Examples.Puzzles.NQueens
, Data.SBV.Examples.Puzzles.Sudoku
, Data.SBV.Examples.Puzzles.U2Bridge
, Data.SBV.Examples.Uninterpreted.AUF
, Data.SBV.Examples.Uninterpreted.Deduce
, Data.SBV.Examples.Uninterpreted.Function
, Data.SBV.Examples.Uninterpreted.Sort
Other-modules : Data.SBV.BitVectors.AlgReals
, Data.SBV.BitVectors.Data
, Data.SBV.BitVectors.Model
, Data.SBV.BitVectors.PrettyNum
, Data.SBV.BitVectors.SignCast
, Data.SBV.BitVectors.Splittable
, Data.SBV.BitVectors.STree
, Data.SBV.Compilers.C
, Data.SBV.Compilers.CodeGen
, Data.SBV.SMT.SMT
, Data.SBV.SMT.SMTLib
, Data.SBV.SMT.SMTLib1
, Data.SBV.SMT.SMTLib2
, Data.SBV.Provers.Prover
, Data.SBV.Provers.SExpr
, Data.SBV.Provers.Yices
, Data.SBV.Provers.Z3
, Data.SBV.Tools.ExpectedValue
, Data.SBV.Tools.GenTest
, Data.SBV.Tools.Optimize
, Data.SBV.Tools.Polynomial
, Data.SBV.Utils.Boolean
, Data.SBV.Utils.TDiff
, Data.SBV.Utils.Lib
Executable SBVUnitTests
default-language: Haskell2010
ghc-options : -Wall
other-extensions: Rank2Types
RankNTypes
ScopedTypeVariables
TupleSections
Build-depends : base >= 4 && < 5
, HUnit, directory, filepath, process, sbv
Hs-Source-Dirs : SBVUnitTest
main-is : SBVUnitTest.hs
Other-modules : SBVUnitTestBuildTime
, SBVTest
, SBVTestCollection
, Examples.Arrays.Memory
, Examples.Basics.BasicTests
, Examples.Basics.Higher
, Examples.Basics.Index
, Examples.Basics.ProofTests
, Examples.Basics.QRem
, Examples.CRC.CCITT
, Examples.CRC.CCITT_Unidir
, Examples.CRC.GenPoly
, Examples.CRC.Parity
, Examples.CRC.USB5
, Examples.Puzzles.PowerSet
, Examples.Puzzles.Temperature
, Examples.Uninterpreted.Uninterpreted
, TestSuite.Arrays.Memory
, TestSuite.Basics.ArithNoSolver
, TestSuite.Basics.ArithSolver
, TestSuite.Basics.BasicTests
, TestSuite.Basics.Higher
, TestSuite.Basics.Index
, TestSuite.Basics.ProofTests
, TestSuite.Basics.QRem
, TestSuite.BitPrecise.BitTricks
, TestSuite.BitPrecise.Legato
, TestSuite.BitPrecise.MergeSort
, TestSuite.BitPrecise.PrefixSum
, TestSuite.CodeGeneration.AddSub
, TestSuite.CodeGeneration.CgTests
, TestSuite.CodeGeneration.CRC_USB5
, TestSuite.CodeGeneration.Fibonacci
, TestSuite.CodeGeneration.GCD
, TestSuite.CodeGeneration.PopulationCount
, TestSuite.CodeGeneration.Uninterpreted
, TestSuite.Crypto.AES
, TestSuite.Crypto.RC4
, TestSuite.Existentials.CRCPolynomial
, TestSuite.CRC.CCITT
, TestSuite.CRC.CCITT_Unidir
, TestSuite.CRC.GenPoly
, TestSuite.CRC.Parity
, TestSuite.CRC.USB5
, TestSuite.Puzzles.Coins
, TestSuite.Polynomials.Polynomials
, TestSuite.Puzzles.Counts
, TestSuite.Puzzles.DogCatMouse
, TestSuite.Puzzles.Euler185
, TestSuite.Puzzles.MagicSquare
, TestSuite.Puzzles.NQueens
, TestSuite.Puzzles.PowerSet
, TestSuite.Puzzles.Sudoku
, TestSuite.Puzzles.U2Bridge
, TestSuite.Puzzles.Temperature
, TestSuite.Uninterpreted.AUF
, TestSuite.Uninterpreted.Function
, TestSuite.Uninterpreted.Uninterpreted
Test-Suite SBVBasicTests
type : exitcode-stdio-1.0
default-language: Haskell2010
ghc-options : -Wall
Build-depends : base >= 4 && < 5
, HUnit, directory, filepath, sbv
Hs-Source-Dirs : SBVUnitTest
main-is : SBVBasicTests.hs
Other-modules : SBVBasicTests
, SBVTestCollection