EasyCheck is a library for automated, specification-based testing of Curry programs. It is distributed with the Curry implementation KiCS. The ideas behind EasyCheck are described in this paper. This is a tutorial introduction that explains in detail how to use EasyCheck.

In EasyCheck, you define properties for functions that describe their behaviour and EasyCheck automatically checks these properties for a variety of test data. Properties are values of the abstract datatype Prop and can be constructed by the following combinator.

test :: a -> ([a] -> Bool) -> Prop

This combinator takes an arbitrary value as argument and a predicate that is applied to the list of nondeterministic results of this value. The given predicate determines whether the constructed property is satisfied or falsified for the given value.

There are numerous specialized combinators defined in terms of test and we will get to know all of them in the rest of this tutorial. Usually, you will use one of the specialized combinators and not test in order to specify properties. Of course, nobody prevents you from using test directly, if you prefer!

Although Curry is a functional logic language that supports nondeterminism, many Curry operations are deterministic. For example, you may have defined an operation that reverses lists as follows.

reverse :: [a] -> [a]
reverse = foldl (flip (:)) []

Now you doubt whether this is indeed a correct definition of the reverse function and wonder how you could check this. For example, reverse should leave a singleton list untouched, so you recall the above test combinator, import EasyCheck and define a corresponding property.

import EasyCheck

reverse :: [a] -> [a]
reverse = foldl (flip (:)) []

reverseLeavesSingletonUntouched :: a -> Prop
reverseLeavesSingletonUntouched x = test (reverse [x]) valid
 where
  valid results = case results of
                    [[y]] -> x == y
                    _     -> False

This is not exactly a beautiful definition, but it will become nicer soon. First, let's try to check the property with EasyCheck. We need to enable OrBased mode in order to be able to generate test data automatically. We use the operation easyCheck1 because our property takes one argument.

> :set or
> easyCheck1 reverseLeavesSingletonUntouched
CurryRequest.hs:14:39:
  Ambiguous type variable `t0' in the constraint:
    `Curry t0'
      arising from use of `c_easyCheck1' at CurryRequest.hs:14:39-69
  Probable fix: add a type signature that fixes these type variable(s)

This is a kind of weird error message, but KiCS gurus can tell you the reason: EasyCheck does not know what test data to generate because the type of the property is polymorphic. We need to specialize the type, in order to enable EasyCheck to construct test data and decide to use Bool as element type for the lists passed to reverse.

reverseLeavesSingletonUntouched :: Bool -> Prop

Now, EasyCheck succeeds to verify our property.

> easyCheck1 reverseLeavesSingletonUntouched
Passed 2 tests.

As there are only two booleans to check, we did even prove the property! Let's change the element type from Bool to Int in order to see what EasyCheck does with an infinite amount of test data.

reverseLeavesSingletonUntouched :: Int -> Prop

Observe the counter and see how EasyCheck finally reports 1000 successful tests.

> easyCheck1 reverseLeavesSingletonUntouched
Ok, passed 1000 tests.

As reverse does not touch elements, we could already have been confident with the first test. But 1000 looks much more impressive than 2, doesn't it? This is our first successful check but many more will follow and, be warned, you may get addicted to them ;)

Remember that I said you usually won't use test directly? Now, it's time to refurbish our property. EasyCheck provides a combinator to check for equality of deterministic values.

(-=-) :: a -> a -> Prop

If we use it in the definition of reverseLeavesSingletonUntouched, the definition becomes much clearer.

reverseLeavesSingletonUntouched :: Bool -> Prop
reverseLeavesSingletonUntouched x = reverse [x] -=- [x]

In fact, (-=-) is not directly defined in terms of test but in terms of another specialized combinator.

(-=-) :: a -> a -> Prop
x -=- y = (x,y) `is` uncurry (==)

The combinator is is similar to test but demands its first argument to be deterministic.

is :: a -> (a -> Bool) -> Prop
x `is` ok = test x valid
 where
  valid results = case results of
                    [y] -> ok y
                    _   -> False

We can use is to define another property for reverse.

reverseOfNonemptyIsNotNull :: Bool -> [Bool] -> Prop
reverseOfNonemptyIsNotNull x xs = reverse (x:xs) `is` (not . null)

This time, we use easyCheck2 to check our property with now two arguments.

> easyCheck2 reverseOfNonemptyIsNotNull
OK, passed 1000 tests.

Successful again! But to be honest, these properties don't rock - they would even hold for the identity function. Let's come up with a more interesting property. Hmm, … there was something about distribution of reverse over (++), … let's try …

reverseDistributesOverAppend :: [Bool] -> [Bool] -> Prop
reverseDistributesOverAppend xs ys
  = reverse (xs++ys) -=- reverse xs ++ reverse ys

Does this property hold?

> easyCheck2 reverseDistributesOverAppend
Falsified by 8th test.
Arguments:
[True]
[False]
Results:
([False,True],[True,False])

Ouch.. It doesn't. Let's take a closer look. The 8th test falsifies our property. It was called with xs = [True] and ys = [False]. The result of the left side of (-=-) is [False,True], that's ok. The result of the right side of (-=-) is [True,False], that's ok as well. Never blindly trust your properties! We did not expose an error in reverse but in the property used to test it. The correct property should look like this.

reverseAntiDistributesOverAppend :: [Bool] -> [Bool] -> Prop
reverseAntiDistributesOverAppend xs ys
  = reverse (xs++ys) -=- reverse ys ++ reverse xs

Now that we are confident that the property is correct we can go back to check whether our definition of reverse is correct also.

> easyCheck2 reverseAntiDistributesOverAppend
OK, passed 1000 tests.

Passed! foldl (flip (:)) [] does the trick.

Not every Curry operation is deterministic. We have seen the combinators is and (-=-) for testing deterministic operations and will examine their counterparts for testing nondeterministic operations in this part of the tutorial.

In our examples we will check the definition of an operation that inserts an element into a list at an arbitrary position.

insert :: a -> [a] -> [a]
insert x xs     = x : xs
insert x (y:ys) = y : insert x ys

Remember reverseOfNonEmptyIsNotNull? We may want to define a similar property for insert.

insertIsNotNull :: Int -> [Int] -> Prop
insertIsNotNull x xs = insert x xs `is` (not . null)

If we check this property with EasyCheck, we get the following counterexample.

> easyCheck2 insertIsNotNull
Falsified by second test.
Arguments:
0
[1]
Results:
[0,1]
[1,0]

The results are not empty, but there are two of them. The combinator is demands its first argument to be deterministic and fails for nondeterministic values. What do we mean by this property anyway? We need to state whether we want the predicate not . null to hold for all results or only for some result of the call to insert. The following combinators let us express what we mean.

isAlways, isEventually :: a -> (a -> Bool) -> Prop
isAlways     x = test x . all
isEventually x = test x . any

Now we can restate our property as follows.

insertIsNeverNull :: Int -> [Int] -> Prop
insertIsNeverNull x xs = insert x xs `isAlways` (not . null)

Just to be safe, we ask EasyCheck to verify our property.

> easyCheck2 insertIsNeverNull
OK, passed 1000 tests.

What are the counterparts to (-=-)? What different kinds of equality checks are there for nondeterministic operations? EasyCheck provides three of them.

(~>), (<~), (<~>) :: a -> a -> Prop

You may think of them as reduction arrows to feel the difference.

• (~>) demands that its first argument evalautes to every value of its second argument. The set of results of the first argument must be a (not necessarily strict) superset of the set of results of the second argument.
• (<~) is dual to (~>) and demands that the set of results of the first argument is a subset of the set of results of the second argument.
• Finally, (<~>) demands the sets of results of the arguments to be equal.

Note, that (<~>) is not equivalent to (-=-) because the latter demands its arguments to be deterministic.

Now we can specify that insert should yield a list where the given element is inserted as first element.

insertInsertsAsHead :: Int -> [Int] -> Prop
insertInsertsAsHead x xs = insert x xs ~> x:xs

We collect more and more successful tests..

> easyCheck2 insertInsertsAsHead
OK, passed 1000 tests.

Why do we need both (~>) and (<~)? Isn't one just the flipped version of the other? Semantically, yes. Operationally, no. EasyCheck reports failing tests differently for (~>) and (<~). Consider the following - intentionally false - property.

insertIsConsOrFails :: Int -> [Int] -> Prop
insertIsConsOrFails x xs = x:xs ~> insert x xs

It states that x:xs evaluates to all values of insert x xs, i.e., insert is the same as (:) or fails. If we use EasyCheck to check this property, we get the following counterexample.

> easyCheck2 insertIsConsOrFails
Falsified by second test.
Arguments:
0
[1]
Results:
[0,1]

EasyCheck reports the results of the left argument of (~>) but not those of the right argument. If we want to see, why the property fails, we need to restate it using (<~).

insertIsConsOrFails :: Int -> [Int] -> Prop
insertIsConsOrFails x xs = insert x xs <~ x:xs

Now the counterexample is much clearer.

> easyCheck2 insertIsConsOrFails
Falsified by second test.
Arguments:
0
[1]
Results:
[0,1]
[1,0]

The same holds for (<~>). You should always write the expression you want to observe in case of a failing test on the left side of (~>), (<~) or (<~>). If this seems suspicious to you, reconsider the definition of (-=-). Why did we define

x -=- y = (x,y) `is` uncurry (==)

instead of

x -=- y = x `is` (==y)

and why is this only possible for deterministic equality?

This part is meant as quick reference that you can use if you already read the tutorial and only want to see the most important combinators at a glance.

to be completed..

Interested in the search employed by EasyCheck and experiments on test-data distribution? Check out our paper!