Test.QuickSpec

The main QuickSpec module.

Look at the introduction (https://github.com/nick8325/quickspec/blob/master/README.asciidoc), read the examples (http://github.com/nick8325/quickspec/tree/master/examples), or read the paper (http://www.cse.chalmers.se/~nicsma/quickspec.pdf) before venturing in here.

Running QuickSpec

quickSpec :: Signature a => a -> IO ()

Run QuickSpec on a signature.

sampleTerms :: Signature a => a -> IO ()

Generate random terms from a signature. Useful when QuickSpec is generating too many terms and you want to know what they look like.

The Signature class

data Sig

A signature.

Instances

Show Sig

Typeable Sig

Monoid Sig

Signature Sig

class Signature a where

The class of things that can be used as a signature.

Methods

signature :: a -> Sig

Instances

Signature Sig

Signature a => Signature [a]

Adding functions to a signature

You can add f to the signature by using "f" `funN` f, where N is the arity of the function. For example,

 "&&" `fun2` (&&)

will add the binary function (&&) to the signature.

If f is polymorphic, you must explicitly give it a monomorphic type. This module exports types A, B and C for that purpose.

For example:

 "++" `fun2` ((++) :: [A] -> [A] -> [A])

The result type of the function must be a member of Ord. If it isn't, use the blindN family of functions (below) instead. If you want to get equations over a type that isn't in Ord, you must use the observerN family of functions (below) to define an observation function for that type.

con :: (Ord a, Typeable a) => String -> a -> Sig

A constant. The same as fun0.

fun0 :: (Ord a, Typeable a) => String -> a -> Sig

A constant. The same as con.

fun1 :: (Typeable a, Typeable b, Ord b) => String -> (a -> b) -> Sig

A unary function.

fun2 :: (Typeable a, Typeable b, Typeable c, Ord c) => String -> (a -> b -> c) -> Sig

A binary function.

fun3 :: (Typeable a, Typeable b, Typeable c, Typeable d, Ord d) => String -> (a -> b -> c -> d) -> Sig

A ternary function.

fun4 :: (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Ord e) => String -> (a -> b -> c -> d -> e) -> Sig

A function of four arguments.

fun5 :: (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable f, Ord f) => String -> (a -> b -> c -> d -> e -> f) -> Sig

A function of five arguments.

Adding functions whose results are not in Ord

These functions work the same as funN (above), but don't use Ord to compare the results of the functions. Instead you can use the observerN family of functions (below) to define an observation function.

blind0 :: forall a. Typeable a => String -> a -> Sig

A constant.

blind1 :: forall a b. (Typeable a, Typeable b) => String -> (a -> b) -> Sig

A unary function.

blind2 :: forall a b c. (Typeable a, Typeable b, Typeable c) => String -> (a -> b -> c) -> Sig

A binary function.

blind3 :: forall a b c d. (Typeable a, Typeable b, Typeable c, Typeable d) => String -> (a -> b -> c -> d) -> Sig

A ternary function.

blind4 :: forall a b c d e. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e) => String -> (a -> b -> c -> d -> e) -> Sig

A function of arity 4.

blind5 :: forall a b c d e f. (Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Typeable f) => String -> (a -> b -> c -> d -> e -> f) -> Sig

A function of arity 5.

Adding variables to a signature

vars :: forall a. (Arbitrary a, Typeable a) => [String] -> a -> Sig

Declare a set of variables of a particular type.

For example, vars ["x","y","z"] (undefined :: Int) defines three variables, x, y and z, of type Int.

gvars :: forall a. Typeable a => [String] -> Gen a -> Sig

Similar to vars, but takes a generator as a parameter.

gvars xs (arbitrary :: Gen a) is the same as vars xs (undefined :: a).

Observational equality

Use this to define comparison operators for types that have no Ord instance.

For example, suppose we have a type Regex of regular expressions, and a matching function match :: String -> Regex -> Bool. We want our equations to talk about semantic equality of regular expressions, but we probably won't have an Ord instance that does that. Instead, we can use blindN to add the regular expression operators to the signature, and then write

 observer2 match

(the 2 is because match has arity two). Then, when QuickSpec wants to compare two Regexes, r1 and r2, it will generate a random String xs, and compare match xs r1 with match xs r2.

Thus you can use observerN to get laws about things that can't be directly compared for equality but can be tested.

observer1 :: (Typeable a, Typeable b, Ord b) => (a -> b) -> Sig

An observation function of arity 1.

observer2 :: (Arbitrary a, Typeable a, Typeable b, Typeable c, Ord c) => (a -> b -> c) -> Sig

An observation function of arity 2.

observer3 :: (Arbitrary a, Arbitrary b, Typeable a, Typeable b, Typeable c, Typeable d, Ord d) => (a -> b -> c -> d) -> Sig

An observation function of arity 3.

observer4 :: (Arbitrary a, Arbitrary b, Arbitrary c, Typeable a, Typeable b, Typeable c, Typeable d, Typeable e, Ord e) => (a -> b -> c -> d -> e) -> Sig

An observation function of arity 4.

Modifying a signature

background :: Signature a => a -> Sig

Mark all the functions in a signature as background functions.

QuickSpec will only print a law if it contains at least one non-background function.

The functions in e.g. prelude are declared as background functions.

withDepth :: Int -> Sig

If withDepth n is in your signature, QuickSpec will consider terms of up to depth n (the default is 3).

withSize :: Int -> Sig

If withSize n is in your signature, QuickSpec will consider terms of up to size n (the default is 100).

withTests :: Int -> Sig

If withTests n is in your signature, QuickSpec will run at least n tests (the default is 500).

withQuickCheckSize :: Int -> Sig

If withQuickCheckSize n is in your signature, QuickSpec will generate test data of up to size n (the default is 20).

without :: Signature a => a -> [String] -> Sig

sig `without` xs will remove the functions in xs from the signature sig. Useful when you want to use prelude but exclude some functions. Example: prelude (undefined :: A) `without` ["head", "tail"].

The standard QuickSpec prelude, to include in your own signatures

data A

Just a type. You can instantiate your polymorphic functions at this type to include them in a signature.

Instances

Eq A

Ord A

Show A

Typeable A

Arbitrary A

CoArbitrary A

Partial A

data B

Instances

Eq B

Ord B

Show B

Typeable B

Arbitrary B

CoArbitrary B

Partial B

data C

Instances

Eq C

Ord C

Show C

Typeable C

Arbitrary C

CoArbitrary C

Partial C

data Two

A type with two elements. Use this instead of A if testing doesn't work well because the domain of A is too large.

Instances

Eq Two

Ord Two

Show Two

Typeable Two

Arbitrary Two

CoArbitrary Two

prelude :: (Typeable a, Ord a, Arbitrary a) => a -> Sig

The QuickSpec prelude. Contains boolean, arithmetic and list functions, and some variables. Instantiate it as e.g. prelude (undefined :: A). For more precise control over what gets included, see bools, arith, lists, funs and without.

bools :: Sig

A signature containing boolean functions: (||), (&&), not, True, False.

arith :: forall a. (Typeable a, Ord a, Num a, Arbitrary a) => a -> Sig

A signature containing arithmetic operations: 0, 1, (+), (*). Instantiate it with e.g. arith (undefined :: Int).

lists :: forall a. (Typeable a, Ord a, Arbitrary a) => a -> Sig

A signature containing list operations: [], (:), head, tail, (++). Instantiate it with e.g. lists (undefined :: A).

funs :: forall a. (Typeable a, Ord a, Arbitrary a, CoArbitrary a) => a -> Sig

A signature containing higher-order functions: (.), id, and some function variables. Useful for testing map.