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 2021

Summary of exported operations:

returns :: (Eq a, Show a) => IO a -> a -> PropIO  Deterministic 
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  Deterministic 
The property sameReturns a1 a2 is satisfied if the execution of the I/O actions a1 and a2 return identical values.
toError :: a -> PropIO  Deterministic 
The property toError a is satisfied if the evaluation of the argument to normal form yields an exception.
toIOError :: IO a -> PropIO  Deterministic 
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)  Deterministic 
Extracts the tests of an I/O property (used by the test runner).
testsOf :: Prop -> [Test]  Deterministic 
Extracts the tests of a property (used by the test runner).
result :: Test -> Result  Deterministic 
Extracts the result of a test.
args :: Test -> [String]  Deterministic 
Extracts the arguments of a test.
stamp :: Test -> [String]  Deterministic 
Extracts the labels of a test.
updArgs :: ([String] -> [String]) -> Test -> Test  Deterministic 
Updates the arguments of a test.
test :: Show a => a -> ([a] -> Bool) -> Prop  Deterministic 
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  Deterministic 
The property x -=- y is satisfied if x and y have deterministic values that are equal.
(<~>) :: (Eq a, Show a) => a -> a -> Prop  Deterministic 
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  Deterministic 
The property x ~> y is satisfied if x evaluates to every value of y.
(<~) :: (Eq a, Show a) => a -> a -> Prop  Deterministic 
The property x <~ y is satisfied if y evaluates to every value of x.
(<~~>) :: (Eq a, Show a) => a -> a -> Prop  Deterministic 
The property x <~~> y is satisfied if the multisets of the values of x and y are equal.
(==>) :: Bool -> Prop -> Prop  Deterministic 
A conditional property is tested if the condition evaluates to True.
solutionOf :: Data a => (a -> Bool) -> a  Non-deterministic 
solutionOf p returns (non-deterministically) a solution of predicate p.
is :: Show a => a -> (a -> Bool) -> Prop  Deterministic 
The property is x p is satisfied if x has a deterministic value which satisfies p.
isAlways :: Show a => a -> (a -> Bool) -> Prop  Deterministic 
The property isAlways x p is satisfied if all values of x satisfy p.
isEventually :: Show a => a -> (a -> Bool) -> Prop  Deterministic 
The property isEventually x p is satisfied if some value of x satisfies p.
uniquely :: Bool -> Prop  Deterministic 
The property uniquely x is satisfied if x has a deterministic value which is true.
always :: Bool -> Prop  Deterministic 
The property always x is satisfied if all values of x are true.
eventually :: Bool -> Prop  Deterministic 
The property eventually x is satisfied if some value of x is true.
failing :: Show a => a -> Prop  Deterministic 
The property failing x is satisfied if x has no value.
successful :: Show a => a -> Prop  Deterministic 
The property successful x is satisfied if x has at least one value.
deterministic :: Show a => a -> Prop  Deterministic 
The property deterministic x is satisfied if x has exactly one value.
(#) :: (Eq a, Show a) => a -> Int -> Prop  Deterministic 
The property x # n is satisfied if x has n values.
(#<) :: (Eq a, Show a) => a -> Int -> Prop  Deterministic 
The property x #< n is satisfied if x has less than n values.
(#>) :: (Eq a, Show a) => a -> Int -> Prop  Deterministic 
The property x #> n is satisfied if x has more than n values.
for :: Show a => a -> (a -> Prop) -> Prop  Deterministic 
The property for x p is satisfied if all values y of x satisfy property p y.
forAll :: Show a => [a] -> (a -> Prop) -> Prop  Deterministic 
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  Deterministic 
Only for internal use by the test runner.
(<=>) :: a -> a -> Prop  Deterministic 
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  Deterministic 
Assign a label to a property.
classify :: Bool -> String -> Prop -> Prop  Deterministic 
Assign a label to a property if the first argument is True.
trivial :: Bool -> Prop -> Prop  Deterministic 
Assign the label "trivial" to a property if the first argument is True.
collect :: Show a => a -> Prop -> Prop  Deterministic 
Assign a label showing the given argument to a property.
collectAs :: Show a => String -> a -> Prop -> Prop  Deterministic 
Assign a label showing a given name and the given argument to a property.
valuesOfSearchTree :: SearchTree a -> [a]  Deterministic 
Extracts values of a search tree according to a given strategy (here: randomized diagonalization of levels with flattening).
valuesOf :: a -> [a]  Deterministic 
Computes the list of all values of the given argument according to a given strategy (here: randomized diagonalization of levels with flattening).

Exported operations:

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

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  Deterministic 

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  Deterministic 

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

toIOError :: IO a -> PropIO  Deterministic 

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

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

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  Deterministic 

Extracts the result of a test.

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

args :: Test -> [String]  Deterministic 

Extracts the arguments of a test.

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

stamp :: Test -> [String]  Deterministic 

Extracts the labels of a test.

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

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

Updates the arguments of a test.

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

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  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

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

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

solutionOf :: Data a => (a -> Bool) -> a  Non-deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

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  Deterministic 

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

always :: Bool -> Prop  Deterministic 

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

eventually :: Bool -> Prop  Deterministic 

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

failing :: Show a => a -> Prop  Deterministic 

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

successful :: Show a => a -> Prop  Deterministic 

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

deterministic :: Show a => a -> Prop  Deterministic 

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

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

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  Deterministic 

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  Deterministic 

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  Deterministic 

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

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

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  Deterministic 

Only for internal use by the test runner.

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

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  Deterministic 

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

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

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  Deterministic 

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  Deterministic 

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  Deterministic 

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

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

valuesOf :: a -> [a]  Deterministic 

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