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: April 2017

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


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.

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

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

Properties:

propUndefinedError "<~>" ((<~>))
propUndefinedError "~>" ((~>))
propUndefinedError "<~" ((<~))
propUndefinedError "<~~>" ((<~~>))
propUndefinedError "==>" ((==>))

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.

Properties:

propUndefinedError "is" (is)
propUndefinedError "isAlways" (isAlways)
propUndefinedError "isEventually" (isEventually)
propUndefinedError "uniquely" (uniquely)
propUndefinedError "always" (always)
propUndefinedError "eventually" (eventually)
propUndefinedError "failing" (failing)
propUndefinedError "successful" (successful)
propUndefinedError "deterministic" (deterministic)
propUndefinedError "#" ((#))
propUndefinedError "#<" ((#<))
propUndefinedError "#>" ((#>))
propUndefinedError "for" (for)
propUndefinedError "forAll" (forAll)
propUndefinedError "#" ((<=>))
propUndefinedError "label" (label)
propUndefinedError "classify" (classify)
propUndefinedError "trivial" (trivial)
propUndefinedError "collect" (collect)
propUndefinedError "collectAs" (collectAs)

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.

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

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