speculate: discovery of properties about Haskell functions

[ bsd3, library, testing ] [ Propose Tags ]

Speculate automatically discovers laws about Haskell functions. Give Speculate a bunch of Haskell functions and it will discover laws like:

equations, such as id x == x ;
inequalities, such as 0 <= x * x ;
conditional equations, such as x <= 0 ==> x + abs x == 0 .

[Skip to Readme]

Versions [faq]	0.2.0, 0.2.1, 0.2.2, 0.2.3, 0.2.4, 0.2.5, 0.2.6, 0.2.7, 0.2.8, 0.2.9, 0.2.10, 0.3.0, 0.3.1, 0.3.2, 0.3.3, 0.3.4, 0.3.5, 0.4.0, 0.4.1, 0.4.2
Dependencies	base (==4.*), cmdargs, containers, express (>=0.1.3), leancheck (>=0.9.3) [details]
License	BSD-3-Clause
Author	Rudy Matela, Colin Runciman
Maintainer	Rudy Matela <rudy@matela.com.br>
Category	Testing
Home page	https://github.com/rudymatela/speculate#readme
Source repo	head: git clone https://github.com/rudymatela/speculate this: git clone https://github.com/rudymatela/speculate(tag v0.4.2)
Uploaded	by rudymatela at 2020-04-05T16:26:09Z
Distributions	LTSHaskell:0.3.5, NixOS:0.4.2, Stackage:0.3.5
Downloads	9833 total (28 in the last 30 days)
Rating	2.0 (votes: 1) [estimated by Bayesian average]
Your Rating	λ λ λ
Status	Docs available [build log] Last success reported on 2020-04-05 [all 1 reports]

Downloads

speculate-0.4.2.tar.gz [browse] (Cabal source package)
Package description (as included in the package)

Maintainer's Corner

For package maintainers and hackage trustees

edit package information

Readme for speculate-0.4.2

[back to package description]

Speculate

Speculate logo

Speculate automatically discovers laws about Haskell functions. Give Speculate a bunch of Haskell functions and it will discover laws like:

equations, such as id x == x;
inequalities, such as 0 <= x * x;
conditional equations, such as x <= 0 ==> x + abs x == 0.

Speculate is similar to, and inspired by, QuickSpec.

Installing Speculate

To install the latest Speculate version from Hackage, just:

$ cabal update
$ cabal install speculate

Pre-requisites are cmdargs, express and leancheck. They should be automatically resolved and installed by Cabal.

Using Speculate

Speculate is used as a library: import it, then call the function speculate with relevant arguments. The following program Speculates about the functions (+) and abs:

import Test.Speculate

main :: IO ()
main = speculate args
  { constants =
      [ showConstant (0::Int)
      , showConstant (1::Int)
      , constant "+"   ((+)  :: Int -> Int -> Int)
      , constant "abs" (abs  :: Int -> Int)
      ]
  }

when run, it prints the following:

_ :: Int  (holes: Int)
0 :: Int
1 :: Int
(+) :: Int -> Int -> Int
abs :: Int -> Int

    abs (abs x) == abs x
          x + 0 == x
          x + y == y + x
    (x + y) + z == x + (y + z)
abs (x + abs x) == x + abs x
  abs x + abs x == abs (x + x)
abs (1 + abs x) == 1 + abs x

x <= abs x
0 <= abs x
x <= x + 1

Now, if we add <= and < as background constants on args

  , constants =
      [ showConstant (0::Int)
      , showConstant (1::Int)
      , constant "+"   ((+)  :: Int -> Int -> Int)
      , constant "abs" (abs  :: Int -> Int)
      , background
      , constant "<="  ((<=) :: Int -> Int -> Bool)
      , constant "<"   ((<)  :: Int -> Int -> Bool)
      ]

then run again, we get the following as well:

    y <= x ==> abs (x + abs y) == x + abs y
    x <= 0 ==>       x + abs x == 0
abs x <= y ==>     abs (x + y) == x + y
abs y <= x ==>     abs (x + y) == x + y

For more examples, see the eg folder.

Similarities and Differences to QuickSpec

Speculate is inspired by QuickSpec. Like QuickSpec, Speculate uses testing to speculate equational laws about given Haskell functions. There are some differences:

Speculate tests enumeratively using LeanCheck, QuickSpec tests randomly using QuickCheck;
Speculate is able to report inequalities directly;
QuickSpec allows polymorphism, Speculate does not;
For most examples, Speculate runs slower than QuickSpec 2 but faster than QuickSpec 1.