quickspec-0.9.2: Equational laws for free

Safe HaskellNone

Test.QuickSpec

Contents

Description

The main QuickSpec module.

This will not make sense if you haven't seen some examples! Look at http://github.com/nick8325/quickspec/tree/master/examples, or read the paper at http://www.cse.chalmers.se/~nicsma/quickspec.pdf.

Synopsis

Running QuickSpec

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

Run QuickSpec on a signature.

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

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 Source

A signature.

class Signature a whereSource

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

Methods

signature :: a -> SigSource

Instances

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 -> SigSource

A constant. The same as fun0.

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

A constant. The same as con.

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

A unary function.

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

A binary function.

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

A ternary function.

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

A function of four 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 -> SigSource

A constant.

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

A unary function.

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

A binary function.

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

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) -> SigSource

A function of arity 4.

Adding variables to a signature

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

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 -> SigSource

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) -> SigSource

An observation function of arity 1.

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

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) -> SigSource

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) -> SigSource

An observation function of arity 4.

Modifying a signature

background :: Signature a => a -> SigSource

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 -> SigSource

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

withSize :: Int -> SigSource

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

withTests :: Int -> SigSource

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

withQuickCheckSize :: Int -> SigSource

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] -> SigSource

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 Source

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

data Two Source

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

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

The QuickSpec prelude. Contains boolean, arithmetic and list functions, and some variables. Instantiate it as e.g. prelude (undefined :: A).

bools :: SigSource

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

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

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 -> SigSource

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 -> SigSource

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