Documentation

Run QuickSpec. See the documentation at the top of this file.

Run QuickSpec, returning the list of discovered properties.

Add some properties to the background theory.

A signature.

A class of things that can be used as a QuickSpec signature.

Declare a constant with a given name and value. If the constant you want to use is polymorphic, you can use the types A, B, C, D, E to monomorphise it, for example:

constant "reverse" (reverse :: [A] -> [A])

QuickSpec will then understand that the constant is really polymorphic.

Add a custom constant.

Type class constraints as first class citizens

Lift a constrained type to a ==> type which QuickSpec can work with

Add an instance of a type class to the signature

Declare a predicate with a given name and value. The predicate should be a function which returns Bool. It will appear in equations just like any other constant, but will also be allowed to appear as a condition.

For example:

sig = [
  con "delete" (delete :: Int -> [Int] -> [Int]),
  con "insert" (insert :: Int -> [Int] -> [Int]),
  predicate "member" (member :: Int -> [Int] -> Bool) ]

Declare a predicate with a given name and value. The predicate should be a function which returns Bool. It will appear in equations just like any other constant, but will also be allowed to appear as a condition. The third argument is a generator for values satisfying the predicate.

Declare a new monomorphic type. The type must implement Ord and Arbitrary.

Like monoType, but designed to be used with TypeApplications directly.

For example, you can add Foo to your signature via:

mono @Foo

Declare a new monomorphic type using observational equivalence. The type must implement Observe and Arbitrary.

Like monoTypeObserve, but designed to be used with TypeApplications directly.

For example, you can add Foo to your signature via:

monoObserve @Foo

Declare a new monomorphic type using observational equivalence, saying how you want variables of that type to be named.

Like monoTypeObserveWithVars, but designed to be used with TypeApplications directly.

For example, you can add Foo to your signature via:

monoObserveVars @Foo ["foo"]

Declare a new monomorphic type, saying how you want variables of that type to be named.

Like monoTypeWithVars designed to be used with TypeApplications directly.

For example, you can add Foo to your signature via:

monoVars @Foo ["foo"]

Customize how variables of a particular type are named.

Constrain how variables of a particular type may occur in a term. The default value is UpTo 4.

Declare a typeclass instance. QuickSpec needs to have an Ord and | Declare a typeclass instance. QuickSpec needs to have an Ord and Arbitrary instance for each type you want it to test.

For example, if you are testing Map k v, you will need to add the following two declarations to your signature:

inst (Sub Dict :: (Ord A, Ord B) :- Ord (Map A B))
inst (Sub Dict :: (Arbitrary A, Arbitrary B) :- Arbitrary (Map A B))

Declare an arbitrary value to be used by instance resolution.

Declare some functions as being background functions. These are functions which are not interesting on their own, but which may appear in interesting laws with non-background functions. Declaring background functions may improve the laws you get out.

Here is an example, which tests ++ and length, giving 0 and + as background functions:

main = quickSpec [
  con "++" ((++) :: [A] -> [A] -> [A]),
  con "length" (length :: [A] -> Int),

  background [
    con "0" (0 :: Int),
    con "+" ((+) :: Int -> Int -> Int) ] ]

Remove a function or predicate from the signature. Useful in combination with prelude and friends.

Run QuickCheck on a series of signatures. Tests the functions in the first signature, then adds the functions in the second signature, then adds the functions in the third signature, and so on.

This can be useful when you have a core API you want to test first, and a larger API you want to test later. The laws for the core API will be printed separately from the laws for the larger API.

Here is an example which first tests 0 and + and then adds ++ and length:

main = quickSpec (series [sig1, sig2])
  where
    sig1 = [
      con "0" (0 :: Int),
      con "+" ((+) :: Int -> Int -> Int) ]
    sig2 = [
      con "++" ((++) :: [A] -> [A] -> [A]),
      con "length" (length :: [A] -> Int) ]

Set the maximum size of terms to explore (default: 7).

Set how many times to test each discovered law (default: 1000).

Set the maximum value for QuickCheck's size parameter when generating test data (default: 20).

Set which type polymorphic terms are tested at.

Set how QuickSpec should display its discovered equations (default: ForHumans).

If you'd instead like to turn QuickSpec's output into QuickCheck tests, set this to ForQuickCheck.

Set how hard QuickSpec tries to filter out redundant equations (default: no limit).

If you experience long pauses when running QuickSpec, try setting this number to 2 or 3.

Set the maximum term size QuickSpec will reason about when it filters out redundant equations (default: same as maximum term size).

If you get laws you believe are redundant, try increasing this number to 1 or 2 more than the maximum term size.

Set the random number seed used for test case generation. Useful if you want repeatable results.

Automatically infer types to add to the universe from available type class instances

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

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

A signature containing list operations: [], (:), (++).

A signature containing higher-order functions: (.) and id. Useful for testing map and similar.

The QuickSpec prelude. Contains boolean, arithmetic and list functions, and function composition. For more precise control over what gets included, see bools, arith, lists, funs and without.