# EasyCheck

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.

# Properties

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!

# Testing Deterministic Operations

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.

# Testing Nondeterministic Operations

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 (==)`

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

and why is this only possible for deterministic equality?

# Interface Summary

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

# Resources

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