Module Test.Prop

This module defines the interface of properties that can be checked with the CurryCheck tool, an automatic property-based test tool based on the EasyCheck library. The ideas behind EasyCheck are described in this paper. CurryCheck automatically tests properties 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.

Basically, this module is a stub clone of the EasyCheck library which contains only the interface of the operations used to specify properties. Hence, this library does not import any other library. This supports the definition of properties in any other module (execept for the prelude).

Author: Sebastian Fischer (with extensions by Michael Hanus)

Version: January 2019

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

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

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

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