Portability  nonportable (TemplateHaskell) 

Stability  provisional 
Maintainer  haskell@tobias.goedderz.info 
Safe Haskell  None 
This library is based on the following paper:
 Automatic Testing of Operation Invariance, presented at WFLP'14. http://www.iai.unibonn.de/~jv/GV14.html
A highlevel 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:

x == x
should always beTrue
(reflexivity).  if
x == y
isTrue
,y == x
should also beTrue
(symmetry).  if
x == y
andy == z
areTrue
,x == z
should also beTrue
(transitivity).  if
x == y
isTrue
,f x == f y
should also beTrue
(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 QuickChecklike 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
andax 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 resultA
, both testsf lhs y z == f rhs y z
andf 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 viawithConstraint
.
 data AxiomResult a
 (===>) :: Bool > AxiomResult a > AxiomResult a
 (=!=) :: a > a > AxiomResult a
 data Axiom
 axiom :: Name > Axiom
 type Arg = Int
 data Op
 op :: Name > Op
 arg :: Int > Arg
 but :: Op > Arg > Op
 only :: Op > Arg > Op
 withConstraint :: Op > Name > Op
 withGens :: HasGens a => a > [Name] > a
 generate_oi_tests :: [Axiom] > [Op] > ExpQ
 generate_axiom's_tests :: Axiom > [Op] > ExpQ
 generate_single_test :: Axiom > Op > ExpQ
 generate_basic_tests :: [Axiom] > ExpQ
 show_all_tests :: Maybe (String > Int > String > String) > [Name] > [Name] > ExpQ
Documentation
data AxiomResult a Source
(===>) :: Bool > AxiomResult a > AxiomResult aSource
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 aSource
Combine the results of the left and righthand 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
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.
but o i
excludes the i
th argument from o
when generating tests.
Example:
op 'dequeue `but` arg 1
only o i
excludes all but the i
th argument from o
when generating tests.
Example:
op 'dequeue `only` arg 1
withConstraint :: Op > Name > OpSource
op
adds a constraint function withConstraint
ff
to op
. f
must
take arguments of the same type as op
and return a Bool
.
withGens :: HasGens a => a > [Name] > aSource
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] > ExpQSource
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] > ExpQSource
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 > ExpQSource
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] > ExpQSource
show_all_tests :: Maybe (String > Int > String > String) > [Name] > [Name] > ExpQSource
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))