Module Test.EasyCheck

EasyCheck is a library for automated, property-based testing of Curry programs. The ideas behind EasyCheck are described in this paper. The CurryCheck tool automatically executes tests defined with this library. CurryCheck supports the definition of unit tests (also for I/O operations) and property tests parameterized over some arguments. CurryCheck is described in more detail in this paper.

Note that this module defines the interface of EasyCheck to define properties. The operations to actually execute the tests are contained in the accompanying library Test.EasyCheckExec.

Author: Sebastian Fischer (with extensions by Michael Hanus)

Version: June 2016

Summary of exported operations:

returns :: (Eq a, Show a) => IO a -> a -> PropIO   
The property returns a x is satisfied if the execution of the I/O action a returns the value x.
sameReturns :: (Eq a, Show a) => IO a -> IO a -> PropIO   
The property sameReturns a1 a2 is satisfied if the execution of the I/O actions a1 and a2 return identical values.
toError :: a -> PropIO   
The property toError a is satisfied if the evaluation of the argument to normal form yields an exception.
toIOError :: IO a -> PropIO   
The property toIOError a is satisfied if the execution of the I/O action a causes an exception.
ioTestOf :: PropIO -> Bool -> String -> IO (Maybe String)   
Extracts the tests of an I/O property (used by the test runner).
testsOf :: Prop -> [Test]   
Extracts the tests of a property (used by the test runner).
result :: Test -> Result   
Extracts the result of a test.
args :: Test -> [String]   
Extracts the arguments of a test.
stamp :: Test -> [String]   
Extracts the labels of a test.
updArgs :: ([String] -> [String]) -> Test -> Test   
Updates the arguments of a test.
test :: Show a => a -> ([a] -> Bool) -> Prop   
Constructs a property to be tested from an arbitrary expression (first argument) and a predicate that is applied to the list of non-deterministic values.
(-=-) :: (Eq a, Show a) => a -> a -> Prop   
The property x -=- y is satisfied if x and y have deterministic values that are equal.
(<~>) :: (Eq a, Show a) => a -> a -> Prop   
The property x <~> y is satisfied if the sets of the values of x and y are equal.
(~>) :: (Eq a, Show a) => a -> a -> Prop   
The property x ~> y is satisfied if x evaluates to every value of y.
(<~) :: (Eq a, Show a) => a -> a -> Prop   
The property x <~ y is satisfied if y evaluates to every value of x.
(<~~>) :: (Eq a, Show a) => a -> a -> Prop   
The property x <~~> y is satisfied if the multisets of the values of x and y are equal.
(==>) :: Bool -> Prop -> Prop   
A conditional property is tested if the condition evaluates to True.
solutionOf :: (a -> Bool) -> a   
solutionOf p returns (non-deterministically) a solution of predicate p.
is :: Show a => a -> (a -> Bool) -> Prop   
The property is x p is satisfied if x has a deterministic value which satisfies p.
isAlways :: Show a => a -> (a -> Bool) -> Prop   
The property isAlways x p is satisfied if all values of x satisfy p.
isEventually :: Show a => a -> (a -> Bool) -> Prop   
The property isEventually x p is satisfied if some value of x satisfies p.
uniquely :: Bool -> Prop   
The property uniquely x is satisfied if x has a deterministic value which is true.
always :: Bool -> Prop   
The property always x is satisfied if all values of x are true.
eventually :: Bool -> Prop   
The property eventually x is satisfied if some value of x is true.
failing :: Show a => a -> Prop   
The property failing x is satisfied if x has no value.
successful :: Show a => a -> Prop   
The property successful x is satisfied if x has at least one value.
deterministic :: Show a => a -> Prop   
The property deterministic x is satisfied if x has exactly one value.
(#) :: (Eq a, Show a) => a -> Int -> Prop   
The property x # n is satisfied if x has n values.
(#<) :: (Eq a, Show a) => a -> Int -> Prop   
The property x #< n is satisfied if x has less than n values.
(#>) :: (Eq a, Show a) => a -> Int -> Prop   
The property x #> n is satisfied if x has more than n values.
for :: Show a => a -> (a -> Prop) -> Prop   
The property for x p is satisfied if all values y of x satisfy property p y.
forAll :: Show a => [a] -> (a -> Prop) -> Prop   
The property forAll xs p is satisfied if all values x of the list xs satisfy property p x.
forAllValues :: Show a => (b -> Prop) -> [a] -> (a -> b) -> Prop   
Only for internal use by the test runner.
(<=>) :: a -> a -> Prop   
The property f <=> g is satisfied if f and g are equivalent operations, i.e., they can be replaced in any context without changing the computed results.
label :: String -> Prop -> Prop   
Assign a label to a property.
classify :: Bool -> String -> Prop -> Prop   
Assign a label to a property if the first argument is True.
trivial :: Bool -> Prop -> Prop   
Assign the label "trivial" to a property if the first argument is True.
collect :: Show a => a -> Prop -> Prop   
Assign a label showing the given argument to a property.
collectAs :: Show a => String -> a -> Prop -> Prop   
Assign a label showing a given name and the given argument to a property.
valuesOfSearchTree :: SearchTree a -> [a]   
Extracts values of a search tree according to a given strategy (here: randomized diagonalization of levels with flattening).
valuesOf :: a -> [a]   
Computes the list of all values of the given argument according to a given strategy (here: randomized diagonalization of levels with flattening).

Exported datatypes:


PropIO

Abstract type to represent properties involving IO actions.

Constructors:


Test

Abstract type to represent a single test for a property to be checked. A test consists of the result computed for this test, the arguments used for this test, and the labels possibly assigned to this test by annotating properties.

Constructors:


Result

Data type to represent the result of checking a property.

Constructors:

  • Undef :: Result
  • Ok :: Result
  • Falsified :: [String] -> Result
  • Ambigious :: [Bool] -> [String] -> Result

Prop

Abstract type to represent properties to be checked. Basically, it contains all tests to be executed to check the property.

Constructors:


Exported operations:

returns :: (Eq a, Show a) => IO a -> a -> PropIO   

The property returns a x is satisfied if the execution of the I/O action a returns the value x.

Further infos:
  • defined as non-associative infix operator with precedence 1

sameReturns :: (Eq a, Show a) => IO a -> IO a -> PropIO   

The property sameReturns a1 a2 is satisfied if the execution of the I/O actions a1 and a2 return identical values.

Further infos:
  • defined as non-associative infix operator with precedence 1

toError :: a -> PropIO   

The property toError a is satisfied if the evaluation of the argument to normal form yields an exception.

toIOError :: IO a -> PropIO   

The property toIOError a is satisfied if the execution of the I/O action a causes an exception.

ioTestOf :: PropIO -> Bool -> String -> IO (Maybe String)   

Extracts the tests of an I/O property (used by the test runner).

Further infos:
  • solution complete, i.e., able to compute all solutions

testsOf :: Prop -> [Test]   

Extracts the tests of a property (used by the test runner).

Further infos:
  • solution complete, i.e., able to compute all solutions

result :: Test -> Result   

Extracts the result of a test.

Further infos:
  • solution complete, i.e., able to compute all solutions

args :: Test -> [String]   

Extracts the arguments of a test.

Further infos:
  • solution complete, i.e., able to compute all solutions

stamp :: Test -> [String]   

Extracts the labels of a test.

Further infos:
  • solution complete, i.e., able to compute all solutions

updArgs :: ([String] -> [String]) -> Test -> Test   

Updates the arguments of a test.

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

Constructs a property to be tested from an arbitrary expression (first argument) and a predicate that is applied to the list of non-deterministic values. The given predicate determines whether the constructed property is satisfied or falsified for the given expression.

(-=-) :: (Eq a, Show a) => a -> a -> Prop   

The property x -=- y is satisfied if x and y have deterministic values that are equal.

Further infos:
  • defined as non-associative infix operator with precedence 1

(<~>) :: (Eq a, Show a) => a -> a -> Prop   

The property x <~> y is satisfied if the sets of the values of x and y are equal.

Further infos:
  • defined as non-associative infix operator with precedence 1

(~>) :: (Eq a, Show a) => a -> a -> Prop   

The property x ~> y is satisfied if x evaluates to every value of y. Thus, the set of values of y must be a subset of the set of values of x.

Further infos:
  • defined as non-associative infix operator with precedence 1

(<~) :: (Eq a, Show a) => a -> a -> Prop   

The property x <~ y is satisfied if y evaluates to every value of x. Thus, the set of values of x must be a subset of the set of values of y.

Further infos:
  • defined as non-associative infix operator with precedence 1

(<~~>) :: (Eq a, Show a) => a -> a -> Prop   

The property x <~~> y is satisfied if the multisets of the values of x and y are equal.

Further infos:
  • defined as non-associative infix operator with precedence 1

(==>) :: Bool -> Prop -> Prop   

A conditional property is tested if the condition evaluates to True.

Further infos:
  • defined as right-associative infix operator with precedence 0

solutionOf :: (a -> Bool) -> a   

solutionOf p returns (non-deterministically) a solution of predicate p. This operation is useful to test solutions of predicates.

is :: Show a => a -> (a -> Bool) -> Prop   

The property is x p is satisfied if x has a deterministic value which satisfies p.

Further infos:
  • defined as non-associative infix operator with precedence 1

isAlways :: Show a => a -> (a -> Bool) -> Prop   

The property isAlways x p is satisfied if all values of x satisfy p.

Further infos:
  • defined as non-associative infix operator with precedence 1

isEventually :: Show a => a -> (a -> Bool) -> Prop   

The property isEventually x p is satisfied if some value of x satisfies p.

Further infos:
  • defined as non-associative infix operator with precedence 1

uniquely :: Bool -> Prop   

The property uniquely x is satisfied if x has a deterministic value which is true.

always :: Bool -> Prop   

The property always x is satisfied if all values of x are true.

eventually :: Bool -> Prop   

The property eventually x is satisfied if some value of x is true.

failing :: Show a => a -> Prop   

The property failing x is satisfied if x has no value.

successful :: Show a => a -> Prop   

The property successful x is satisfied if x has at least one value.

deterministic :: Show a => a -> Prop   

The property deterministic x is satisfied if x has exactly one value.

(#) :: (Eq a, Show a) => a -> Int -> Prop   

The property x # n is satisfied if x has n values.

Further infos:
  • defined as non-associative infix operator with precedence 1

(#<) :: (Eq a, Show a) => a -> Int -> Prop   

The property x #< n is satisfied if x has less than n values.

Further infos:
  • defined as non-associative infix operator with precedence 1

(#>) :: (Eq a, Show a) => a -> Int -> Prop   

The property x #> n is satisfied if x has more than n values.

Further infos:
  • defined as non-associative infix operator with precedence 1

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

The property for x p is satisfied if all values y of x satisfy property p y.

forAll :: Show a => [a] -> (a -> Prop) -> Prop   

The property forAll xs p is satisfied if all values x of the list xs satisfy property p x.

forAllValues :: Show a => (b -> Prop) -> [a] -> (a -> b) -> Prop   

Only for internal use by the test runner.

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

The property f <=> g is satisfied if f and g are equivalent operations, i.e., they can be replaced in any context without changing the computed results.

Further infos:
  • defined as non-associative infix operator with precedence 1

label :: String -> Prop -> Prop   

Assign a label to a property. All labeled tests are counted and shown at the end.

classify :: Bool -> String -> Prop -> Prop   

Assign a label to a property if the first argument is True. All labeled tests are counted and shown at the end. Hence, this combinator can be used to classify tests:

multIsComm x y = classify (x<0 || y<0) "Negative" $ x*y -=- y*x

trivial :: Bool -> Prop -> Prop   

Assign the label "trivial" to a property if the first argument is True. All labeled tests are counted and shown at the end.

Further infos:
  • defined as non-associative infix operator with precedence 1

collect :: Show a => a -> Prop -> Prop   

Assign a label showing the given argument to a property. All labeled tests are counted and shown at the end.

collectAs :: Show a => String -> a -> Prop -> Prop   

Assign a label showing a given name and the given argument to a property. All labeled tests are counted and shown at the end.

valuesOfSearchTree :: SearchTree a -> [a]   

Extracts values of a search tree according to a given strategy (here: randomized diagonalization of levels with flattening).

valuesOf :: a -> [a]   

Computes the list of all values of the given argument according to a given strategy (here: randomized diagonalization of levels with flattening).