Maintainer  Roman Cheplyaka <roma@roche.info> 

Properties and tools to construct them.
 data TestCase = TestCase {
 result :: TestResult
 arguments :: [String]
 data TestResult
 = Pass
  Fail
  Inappropriate
 resultIsOk :: TestResult > Bool
 data Property
 type Depth = Int
 class Testable a where
 property :: Testable a => a > Property
 mkProperty :: (Depth > [TestCase]) > Property
 (==>) :: Testable a => Bool > a > Property
 exists :: (Show a, Serial a, Testable b) => (a > b) > Property
 existsDeeperBy :: (Show a, Serial a, Testable b) => (Depth > Depth) > (a > b) > Property
 exists1 :: (Show a, Serial a, Testable b) => (a > b) > Property
 exists1DeeperBy :: (Show a, Serial a, Testable b) => (Depth > Depth) > (a > b) > Property
 forAll :: (Show a, Testable b) => Series a > (a > b) > Property
 forAllElem :: (Show a, Testable b) => [a] > (a > b) > Property
 thereExists :: (Show a, Testable b) => Series a > (a > b) > Property
 thereExistsElem :: (Show a, Testable b) => [a] > (a > b) > Property
 thereExists1 :: (Show a, Testable b) => Series a > (a > b) > Property
 thereExists1Elem :: (Show a, Testable b) => [a] > (a > b) > Property
Basic definitions
data TestResult Source
Pass  
Fail  
Inappropriate 

resultIsOk :: TestResult > BoolSource
Maximum depth of generated test values
For data values, it is the depth of nested constructor applications.
For functional values, it is both the depth of nested case analysis and the depth of results.
Anything of a Testable
type can be regarded as a "test"
mkProperty :: (Depth > [TestCase]) > PropertySource
A lowerlevel way to create properties. Use property
if possible.
The argument is a function that produces the list of results given the depth of testing.
Constructing tests
(==>) :: Testable a => Bool > a > PropertySource
The ==>
operator can be used to express a
restricting condition under which a property should hold. For example,
testing a propositionallogic module (see examples/logical), we might
define:
prop_tautEval :: Proposition > Environment > Property prop_tautEval p e = tautology p ==> eval p e
But here is an alternative definition:
prop_tautEval :: Proposition > Property prop_taut p = tautology p ==> \e > eval p e
The first definition generates p and e for each test, whereas the second only generates e if the tautology p holds.
The second definition is far better as the testspace is reduced from PE to T'+TE where P, T, T' and E are the numbers of propositions, tautologies, nontautologies and environments.
exists :: (Show a, Serial a, Testable b) => (a > b) > PropertySource
holds iff it is possible to find an argument exists
pa
(within the
depth constraints!) satisfying the predicate p
existsDeeperBy :: (Show a, Serial a, Testable b) => (Depth > Depth) > (a > b) > PropertySource
The default testing of existentials is bounded by the same depth as their context. This rule has important consequences. Just as a universal property may be satisfied when the depth bound is shallow but fail when it is deeper, so the reverse may be true for an existential property. So when testing properties involving existentials it may be appropriate to try deeper testing after a shallow failure. However, sometimes the default samedepthbound interpretation of existential properties can make testing of a valid property fail at all depths. Here is a contrived but illustrative example:
prop_append1 :: [Bool] > [Bool] > Property prop_append1 xs ys = exists $ \zs > zs == xs++ys
existsDeeperBy
transforms the depth bound by a given
function:
Depth
> Depth
prop_append2 :: [Bool] > [Bool] > Property prop_append2 xs ys = existsDeeperBy (*2) $ \zs > zs == xs++ys
exists1 :: (Show a, Serial a, Testable b) => (a > b) > PropertySource
Like exists
, but additionally require the uniqueness of the
argument satisfying the predicate
exists1DeeperBy :: (Show a, Serial a, Testable b) => (Depth > Depth) > (a > b) > PropertySource
Like existsDeeperBy
, but additionally require the uniqueness of the
argument satisfying the predicate
Series and listbased constructors
Combinators below can be used to explicitly specify the domain of
quantification (as Series
or lists).
Hopefully, their meaning is evident from their names and types.
forAllElem :: (Show a, Testable b) => [a] > (a > b) > PropertySource
thereExistsElem :: (Show a, Testable b) => [a] > (a > b) > PropertySource
thereExists1Elem :: (Show a, Testable b) => [a] > (a > b) > PropertySource