Test.OITestGenerator

This library is based on the following paper:

• Automatic Testing of Operation Invariance, presented at WFLP'14. http://www.iai.uni-bonn.de/~jv/GV14.html

A high-level explanation follows:

(QuickCheck-)tests for data types are often formulated as equations, e.g.

rev_test :: Property
rev_test = property $ \xs ys -> reverse ys ++ reverse xs == reverse (xs ++ ys)

. There are assumptions everyone usually makes about the behaviour of (==), but does not necessarily think about:

1. x == x should always be True (reflexivity).
2. if x == y is True, y == x should also be True (symmetry).
3. if x == y and y == z are True, x == z should also be True (transitivity).
4. if x == y is True, f x == f y should also be True (congruence or operation invariance).

It is unlikely to accidentally write an Eq instance that does not satisfy 1.-3. Operation invariance however is fickle, as it also implies sane behaviour of all functions on the data type.

This framework takes QuickCheck-like equality tests (called axioms) of a data type and functions on the data type (called operations), and uses them to generate the corresponding QuickCheck tests, as well as additional operation invariance tests.

For example, given a queue of integers IntQueue with the following operations.

empty   :: IntQueue                    -- create an empty queue
isEmpty :: IntQueue -> Bool            -- test if a given queue is empty
enqueue :: Int -> IntQueue -> IntQueue -- enqueue an integer to a queue
dequeue :: IntQueue -> IntQueue        -- dequeue the first element of a queue
front   :: IntQueue -> Int             -- get the first element of a queue

A QuickCheck test for this might be

property $ \x q -> not (isEmpty q) ==> dequeue (enqueue x q) == enqueue x (dequeue q)

while this would be formulated as an axiom for use with this package as follows:

q6 x q = not (isEmpty q) ===> dequeue (enqueue x q) =!= enqueue x (dequeue q)

Assuming you wrote six axioms q1-q6, the six corresponding QuickCheck tests can be generated by generate_basic_tests.

{-# LANGUAGE TemplateHaskell #-}
...
queue_basic_tests :: [Property]
queue_basic_tests = $(
    let axs = map axiom ['q1, 'q2, 'q3, 'q4, 'q5, 'q6]
    in generate_basic_tests axs)

The single quotes preceding q1 to q6 quote each following name as a Template Haskell Name. Note that $(...) is a Template Haskell splice and will be evaluated during compile time. Because of this, you may not refer to declarations of the same module except by name (this is called the stage restriction), which is the motivation for the let ... in ... construct.

Additional operation invariance tests can be generated with generate_oi_tests.

may_dequeue :: IntQueue -> Bool
may_dequeue = not . isEmpty

may_front :: IntQueue -> Bool
may_front = not . isEmpty

adt_oi_tests :: [Property]
adt_oi_tests = $(
    let ops = [ op 'empty, op 'enqueue, op 'isEmpty
              , op 'dequeue `withConstraint` 'may_dequeue
              , op 'front `withConstraint` 'may_front
              ]
        axs = map axiom ['q1, 'q2, 'q3, 'q4, 'q5, 'q6 ]
    in generate_oi_tests axs ops)

For every operation f and every axiom lhs =!= rhs, a test f lhs == f rhs will be generated if it is type correct. Note that polymorphic types aren't supported yet, but you can simply rename and specialize them, e.g.

reverse_ints :: [Int] -> [Int]
reverse_ints = reverse

and test the renamed function. Besides type checking, generate_oi_tests takes care of

• passing axiom arguments, e.g. f and ax x = lhs x =!= rhs x will get translated to \x -> f (lhs x) == f (rhs x).
• multiple operation arguments, e.g. for an f :: A -> A -> B -> C and an axiom with result A, both tests f lhs y z == f rhs y z and f x lhs z == f x rhs z will be generated.
• translating constraints of both axioms and operations to ==>. Axiom constraints are specified via ===>, while operation constraints are specified via withConstraint.

Documentation

data AxiomResult a

(===>) :: Bool -> AxiomResult a -> AxiomResult a

Adds a condition to an axiom. If the Bool argument is False, the axiom won't be evaluated. The test will neither count as a failed test, nor as a successful test. It translates to the QuickCheck operator ==>.

Example usage:

q4 :: Int -> IntQueue -> AxiomResult Int
q4 x q = not (isEmpty q) ===> front (enqueue x q) =!= front q

(=!=) :: a -> a -> AxiomResult a

Combine the results of the left- and right-hand sides of an axiom. A simple example is

q1 :: AxiomResult Bool
q1 = isEmpty empty =!= True

while an axiom with variables would be written as a function like this:

q2 :: Int -> IntQueue -> AxiomResult Bool
q2 x q = isEmpty (enqueue x q) =!= False

data Axiom

Instances

HasGens Axiom

axiom :: Name -> Axiom

Axiom constructor. Takes a Name, i.e.

axiom 'q1

or

map axiom ['q1, 'q2, 'q3]

.

type Arg = Int

data Op

An operation. Contains information about the operation's name, which arguments may be tested (all by default), which generators should be used for each argument (arbitrary by default) and possibly a constraint function.

Instances

HasGens Op

op :: Name -> Op

Op constructor.

arg :: Int -> Arg

Arg constructor. Only for readability.

but :: Op -> Arg -> Op

but o i excludes the i-th argument from o when generating tests.

Example:

op 'dequeue `but` arg 1

only :: Op -> Arg -> Op

only o i excludes all but the i-th argument from o when generating tests.

Example:

op 'dequeue `only` arg 1

withConstraint :: Op -> Name -> Op

op withConstraint f adds a constraint function f to op. f must take arguments of the same type as op and return a Bool.

withGens :: HasGens a => a -> [Name] -> a

Use to specify custom generators for the given operation or axiom. The i-th element of the list corresponds to the i-th argument. All generators must be specified. Not using a custom generator for specific arguments can be achieved by passing arbitrary.

generate_oi_tests :: [Axiom] -> [Op] -> ExpQ

Generate all operation invariance tests that type check. For example, given an operation

f :: A -> A -> B -> C

and an axiom

ax :: D -> AxiomResult A
ax x = lhs x =!= rhs x

the following tests are generated:

property $ \y2 y3 -> f (lhs x) y2 y3 == f (rhs x) y2 y3
property $ \y1 y3 -> f y1 (lhs x) y3 == f y1 (rhs x) y3

but not

property $ \y1 y2 -> f y1 y2 (lhs x) == f y1 y2 (rhs x)

because of the types.

All combinations of operations, their respective arguments and axioms are tried.

It returns an expression of type [Property], i.e.

$(generate_oi_tests axs ops) :: [Property]

generate_axiom's_tests :: Axiom -> [Op] -> ExpQ

A convenience function for calling generate_oi_tests with only one axiom.

It returns an expression of type [Property], i.e.

$(generate_axiom's_tests ax ops) :: [Property]

generate_single_test :: Axiom -> Op -> ExpQ

Calls generate_oi_tests with only the given Axiom and Op. It checks if there is exactly one test that can be generated and throws an error otherwise. If multiple applications of the given operation to the given axioms are possible (i.e. it has multiple arguments with a matching type), the allowed arguments have to be restricted using but or only.

It returns an expression of type Property, i.e.

$(generate_single_test ax op) :: Property

generate_basic_tests :: [Axiom] -> ExpQ

Derives one test from each Axiom by translating it to a QuickCheck Property. This is done basically by replacing =!= with == and ===> with ==>.

It returns an expression of type [Property], i.e.

$(generate_basic_tests axs) :: [Property]

show_all_tests :: Maybe (String -> Int -> String -> String) -> [Name] -> [Name] -> ExpQ

show_all_tests Nothing axs ops returns a String typed expression. Print the resulting string to get a piece of code, containing one property for each possible operation invariance test, defined via generate_single_test.

The first argument can replace the default function generating a name for each test, which is

\opn argi ax -> opn ++ show argi ++ "_" ++ ax

. An example output looks like this:

enqueue1_q3 :: Property
enqueue1_q3 = $(generate_single_test (axiom 'q3) (op 'enqueue `only` 1))