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

• 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

• 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

An encoded Haskell functional-application expression for use by Speculate.

Instances

Eq Expr

Methods

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

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

Ord Expr

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

Methods

showsPrec :: Int -> Expr -> ShowS

show :: Expr -> String

showList :: [Expr] -> ShowS

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

Encode a constant Haskell expression for use by Speculate. It takes a string representation of a value and a value, returning an Expr. Examples:

constant "0" 0
constant "'a'" 'a'
constant "True" True
constant "id" (id :: Int -> Int)
constant "(+)" ((+) :: Int -> Int -> Int)
constant "sort" (sort :: [Bool] -> [Bool])

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

A shorthand for constant to be used on values that are Show instances. Examples:

showConstant 0     =  constant "0" 0
showConstant 'a'   =  constant "'a'" 'a' 
showConstant True  =  constant "True" True

hole :: (Listable a, Typeable a) => a -> Expr

(intended for advanced users)

hole (undefined :: Ty) returns a hole of type Ty

By convention, a Hole is a variable named with the empty string.

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 = [Instance]

Type information needed to Speculate expressions.

ins :: (Typeable a, Listable a, Show a, Eq a, Ord a) => String -> a -> Instances

eq :: (Typeable a, Eq a) => a -> Instances

ord :: (Typeable a, Ord a) => a -> Instances

eqWith :: (Typeable a, Eq a) => (a -> a -> Bool) -> Instances

ordWith :: (Typeable a, Ord a) => (a -> a -> Bool) -> Instances

names :: Instances -> TypeRep -> [String]

Misc.

report :: Args -> IO ()

getArgs :: Args -> IO Args

module Test.LeanCheck

module Test.LeanCheck.Utils

module Data.Typeable