Test.Speculate

Speculate: discovery of properties by reasoning from test results

Speculate automatically discovers laws about Haskell functions. Those laws involve:

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

_Example:_ the following program prints laws about 0, 1, + 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)
      , background
      , constant "<="  ((<=) :: Int -> Int -> Bool)
      ]
  }

Documentation

speculate :: Args -> IO ()

Calls Speculate. See the example above (at the top of the file). Its only argument is an Args structure.

data Args

Arguments to Speculate

Constructors

Args

Fields

• maxSize :: Int

  maximum size of considered expressions

• maxTests :: Int

  maximum number of test for each law

• constants :: [Expr]

  constants considered when generating expressions

• instances :: [Instances]

  typeclass instance information for Eq, Ord and Listable

• maxSemiSize :: Int

  maximum size of inqualities RHS/LHS

• maxCondSize :: Int

  maximum size of considered condition

• maxVars :: Int

  maximum number of variables allowed in inequalities and conditional equations

• showConstants :: Bool

  repeat constants on output

• showEquations :: Bool

  whether to show equations

• showSemiequations :: Bool

  whether to show inequalties

• showConditions :: Bool

  whether to show conditional equations

• showConstantLaws :: Bool

  whether to show laws with no variables

• autoConstants :: Bool

  automatically include constants taken from tiers of values

• minTests :: Int -> Int

  (intermediary) minimum number of tests for passing postconditions in function of maximum number of tests

• maxConstants :: Maybe Int

  (intermediary) maximum nubmer of constants allowed when considering expressions

• maxDepth :: Maybe Int

  (intermediary) maximum depth of considered expressions

• showCounts :: Bool

  (intermediary) show counts of equations, inequalities and conditional equations

• showTheory :: Bool

  (debug) whether to show raw theory

• showArgs :: Bool

  (debug) show _this_ args before running

• showHelp :: Bool

  (advanced) whether to show the command line help

• evalTimeout :: Maybe Double

  (advanced) timeout when evaluating ground expressions

• force :: Bool

  (advanced) ignore errors

• extra :: [String]

  (advanced) unused, user-defined meaning

• exclude :: [String]

  (advanced) exclude this symbols from signature before running

• onlyTypes :: [String]

  (advanced) only allow those types at top-level equations / semi-equations

• showClassesFor :: [Int]

  (advanced) show equivalence classes of expressions

• showDot :: Bool

  (advanced) whether to show a Graphviz dotfile with an Ord lattice

• quietDot :: Bool

  (advanced) whether to show a Graphviz dotfiel with an Ord lattice (less verbose)

args :: Args

Default arguments to Speculate

The constants list

The following combinators are used to build the constants list from Args.

data Expr

Values of type Expr represent objects or applications between objects. Each object is encapsulated together with its type and string representation. Values encoded in Exprs are always monomorphic.

An Expr can be constructed using:

• val, for values that are Show instances;
• value, for values that are not Show instances, like functions;
• :$, for applications between Exprs.

> val False
False :: Bool

> value "not" not :$ val False
not False :: Bool

An Expr can be evaluated using evaluate, eval or evl.

> evl $ val (1 :: Int) :: Int
1

> evaluate $ val (1 :: Int) :: Maybe Bool
Nothing

> eval 'a' (val 'b')
'b'

Showing a value of type Expr will return a pretty-printed representation of the expression together with its type.

> show (value "not" not :$ val False)
"not False :: Bool"

Expr is like Dynamic but has support for applications and variables (:$, var).

The var underscore convention: Functions that manipulate Exprs usually follow the convention where a value whose String representation starts with '_' represents a variable.

Instances

Eq Expr

O(n). Does not evaluate values when comparing, but rather uses their representation as strings and their types.

This instance works for ill-typed expressions.

Defined in Data.Express.Core

Methods

(==) :: Expr -> Expr -> Bool

(/=) :: Expr -> Expr -> Bool

Ord Expr

Defined in Data.Express.Core

Methods

compare :: Expr -> Expr -> Ordering

(<) :: Expr -> Expr -> Bool

(<=) :: Expr -> Expr -> Bool

(>) :: Expr -> Expr -> Bool

(>=) :: Expr -> Expr -> Bool

max :: Expr -> Expr -> Expr

min :: Expr -> Expr -> Expr

Show Expr

Defined in Data.Express.Core

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

constant :: Typeable a => String -> a -> Expr

showConstant :: (Typeable a, Show a) => a -> Expr

hole :: Typeable a => a -> Expr

O(1). Creates an Expr representing a typed hole of the given argument type.

> hole (undefined :: Int)
_ :: Int

> hole (undefined :: Maybe String)
_ :: Maybe [Char]

A hole is represented as a variable with no name or a value named "_":

hole x = var "" x
hole x = value "_" x

foreground :: Expr

A special Expr value. When provided on the constants list, makes all the following constants foreground constants.

background :: Expr

A special Expr value. When provided on the constants list, makes all the following constants background constants. Background constants can appear in laws about other constants, but not by themselves.

The instances list

The following combinators are used to build the instances list from Args.

type Instances = [Expr]

reifyInstances :: (Typeable a, Listable a, Show a, Eq a, Ord a, Name a) => a -> Instances

reifyEq :: (Typeable a, Eq a) => a -> [Expr]

O(1). Reifies an Eq instance into a list of Exprs. The list will contain == and /= for the given type. (cf. mkEq, mkEquation)

> reifyEq (undefined :: Int)
[ (==) :: Int -> Int -> Bool
, (/=) :: Int -> Int -> Bool ]

> reifyEq (undefined :: Bool)
[ (==) :: Bool -> Bool -> Bool
, (/=) :: Bool -> Bool -> Bool ]

> reifyEq (undefined :: String)
[ (==) :: [Char] -> [Char] -> Bool
, (/=) :: [Char] -> [Char] -> Bool ]

reifyOrd :: (Typeable a, Ord a) => a -> [Expr]

O(1). Reifies an Ord instance into a list of Exprs. The list will contain compare, <= and < for the given type. (cf. mkOrd, mkOrdLessEqual, mkComparisonLE, mkComparisonLT)

> reifyOrd (undefined :: Int)
[ (<=) :: Int -> Int -> Bool
, (<) :: Int -> Int -> Bool ]

> reifyOrd (undefined :: Bool)
[ (<=) :: Bool -> Bool -> Bool
, (<) :: Bool -> Bool -> Bool ]

> reifyOrd (undefined :: [Bool])
[ (<=) :: [Bool] -> [Bool] -> Bool
, (<) :: [Bool] -> [Bool] -> Bool ]

reifyEqOrd :: (Typeable a, Ord a) => a -> [Expr]

O(1). Reifies Eq and Ord instances into a list of Expr.

reifyListable :: (Typeable a, Show a, Listable a) => a -> Instances

mkEq :: Typeable a => (a -> a -> Bool) -> [Expr]

O(1). Builds a reified Eq instance from the given == function. (cf. reifyEq)

> mkEq ((==) :: Int -> Int -> Bool)
[ (==) :: Int -> Int -> Bool
, (/=) :: Int -> Int -> Bool ]

mkOrd :: Typeable a => (a -> a -> Ordering) -> [Expr]

O(1). Builds a reified Ord instance from the given compare function. (cf. reifyOrd, mkOrdLessEqual)

mkOrdLessEqual :: Typeable a => (a -> a -> Bool) -> [Expr]

O(1). Builds a reified Ord instance from the given <= function. (cf. reifyOrd, mkOrd)

mkListable :: (Typeable a, Show a) => [[a]] -> [Expr]

mkNameWith :: Typeable a => String -> a -> [Expr]

O(1). Builds a reified Name instance from the given String and type. (cf. reifyName, mkName)

class Name a where

If we were to come up with a variable name for the given type what name would it be?

An instance for a given type Ty is simply given by:

instance Name Ty where name _ = "x"

Examples:

> name (undefined :: Int)
"x"

> name (undefined :: Bool)
"p"

> name (undefined :: [Int])
"xs"

This is then used to generate an infinite list of variable names:

> names (undefined :: Int)
["x", "y", "z", "x'", "y'", "z'", "x''", "y''", "z''", ...]

> names (undefined :: Bool)
["p", "q", "r", "p'", "q'", "r'", "p''", "q''", "r''", ...]

> names (undefined :: [Int])
["xs", "ys", "zs", "xs'", "ys'", "zs'", "xs''", "ys''", ...]

Minimal complete definition

Nothing

Methods

name :: a -> String

O(1).

Returns a name for a variable of the given argument's type.

> name (undefined :: Int)
"x"

> name (undefined :: [Bool])
"ps"

> name (undefined :: [Maybe Integer])
"mxs"

The default definition is:

name _ = "x"

Instances

Name Bool

name (undefined :: Bool) = "p"
names (undefined :: Bool) = ["p", "q", "r", "p'", "q'", ...]

Defined in Data.Express.Name

Methods

name :: Bool -> String

Name Char

name (undefined :: Char) = "c"
names (undefined :: Char) = ["c", "d", "e", "c'", "d'", ...]

Defined in Data.Express.Name

Methods

name :: Char -> String

Name Double

name (undefined :: Double) = "x"
names (undefined :: Double) = ["x", "y", "z", "x'", ...]

Defined in Data.Express.Name

Methods

name :: Double -> String

Name Float

name (undefined :: Float) = "x"
names (undefined :: Float) = ["x", "y", "z", "x'", ...]

Defined in Data.Express.Name

Methods

name :: Float -> String

Name Int

name (undefined :: Int) = "x"
names (undefined :: Int) = ["x", "y", "z", "x'", "y'", ...]

Defined in Data.Express.Name

Methods

name :: Int -> String

Name Integer

name (undefined :: Integer) = "x"
names (undefined :: Integer) = ["x", "y", "z", "x'", ...]

Defined in Data.Express.Name

Methods

name :: Integer -> String

Name Ordering

name (undefined :: Ordering) = "o"
names (undefined :: Ordering) = ["o", "p", "q", "o'", ...]

Defined in Data.Express.Name

Methods

name :: Ordering -> String

Name Word

Defined in Data.Express.Name

Methods

name :: Word -> String

Name ()

name (undefined :: ()) = "u"
names (undefined :: ()) = ["u", "v", "w", "u'", "v'", ...]

Defined in Data.Express.Name

Methods

name :: () -> String

Name a => Name [a]

names (undefined :: [Int]) = ["xs", "ys", "zs", "xs'", ...]
names (undefined :: [Bool]) = ["ps", "qs", "rs", "ps'", ...]

Defined in Data.Express.Name

Methods

name :: [a] -> String

Name a => Name (Maybe a)

names (undefined :: Maybe Int) = ["mx", "mx1", "mx2", ...]
nemes (undefined :: Maybe Bool) = ["mp", "mp1", "mp2", ...]

Defined in Data.Express.Name

Methods

name :: Maybe a -> String

Name (Ratio a)

name (undefined :: Rational) = "q"
names (undefined :: Rational) = ["q", "r", "s", "q'", ...]

Defined in Data.Express.Name

Methods

name :: Ratio a -> String

Name (a -> b)

names (undefined :: ()->()) = ["f", "g", "h", "f'", ...]
names (undefined :: Int->Int) = ["f", "g", "h", ...]

Defined in Data.Express.Name

Methods

name :: (a -> b) -> String

(Name a, Name b) => Name (Either a b)

names (undefined :: Either Int Int) = ["exy", "exy1", ...]
names (undefined :: Either Int Bool) = ["exp", "exp1", ...]

Defined in Data.Express.Name

Methods

name :: Either a b -> String

(Name a, Name b) => Name (a, b)

names (undefined :: (Int,Int)) = ["xy", "zw", "xy'", ...]
names (undefined :: (Bool,Bool)) = ["pq", "rs", "pq'", ...]

Defined in Data.Express.Name

Methods

name :: (a, b) -> String

(Name a, Name b, Name c) => Name (a, b, c)

names (undefined :: (Int,Int,Int)) = ["xyz","uvw", ...]
names (undefined :: (Int,Bool,Char)) = ["xpc", "xpc1", ...]

Defined in Data.Express.Name

Methods

name :: (a, b, c) -> String

(Name a, Name b, Name c, Name d) => Name (a, b, c, d)

names (undefined :: ((),(),(),())) = ["uuuu", "uuuu1", ...]
names (undefined :: (Int,Int,Int,Int)) = ["xxxx", ...]

Defined in Data.Express.Name

Methods

name :: (a, b, c, d) -> String

(Name a, Name b, Name c, Name d, Name e) => Name (a, b, c, d, e)

Defined in Data.Express.Name

Methods

name :: (a, b, c, d, e) -> String

(Name a, Name b, Name c, Name d, Name e, Name f) => Name (a, b, c, d, e, f)

Defined in Data.Express.Name

Methods

name :: (a, b, c, d, e, f) -> String

(Name a, Name b, Name c, Name d, Name e, Name f, Name g) => Name (a, b, c, d, e, f, g)

Defined in Data.Express.Name

Methods

name :: (a, b, c, d, e, f, g) -> String

(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h) => Name (a, b, c, d, e, f, g, h)

Defined in Data.Express.Name

Methods

name :: (a, b, c, d, e, f, g, h) -> String

(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h, Name i) => Name (a, b, c, d, e, f, g, h, i)

Defined in Data.Express.Name

Methods

name :: (a, b, c, d, e, f, g, h, i) -> String

(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h, Name i, Name j) => Name (a, b, c, d, e, f, g, h, i, j)

Defined in Data.Express.Name

Methods

name :: (a, b, c, d, e, f, g, h, i, j) -> String

(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h, Name i, Name j, Name k) => Name (a, b, c, d, e, f, g, h, i, j, k)

Defined in Data.Express.Name

Methods

name :: (a, b, c, d, e, f, g, h, i, j, k) -> String

(Name a, Name b, Name c, Name d, Name e, Name f, Name g, Name h, Name i, Name j, Name k, Name l) => Name (a, b, c, d, e, f, g, h, i, j, k, l)

Defined in Data.Express.Name

Methods

name :: (a, b, c, d, e, f, g, h, i, j, k, l) -> String

Misc.

report :: Args -> IO ()

getArgs :: Args -> IO Args

module Test.LeanCheck

module Test.LeanCheck.Utils

module Data.Typeable