qc-oi-testgenerator- Compile time generation of operation invariance tests for QuickCheck

Safe HaskellNone




(===>) :: 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 QuickChecks ==> 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 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 Source


axiom :: Name -> AxiomSource

Axiom constructor. Takes a Name, i.e.

 axiom 'q1


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


type Arg = IntSource

data Op Source

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.


op :: Name -> OpSource

Op constructor.

arg :: Int -> ArgSource

Arg constructor. Only for readability.

but :: Op -> Arg -> OpSource

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


 op 'dequeue `but` arg 1

only :: Op -> Arg -> OpSource

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


 op 'dequeue `only` arg 1

withConstraint :: Op -> Name -> OpSource

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] -> 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 typecheck. 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

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