Maintainer | Roman Cheplyaka <roma@ro-che.info> |
---|---|
Safe Haskell | Safe-Inferred |
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 lower-level 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 propositional-logic 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 test-space is reduced from PE to T'+TE where P, T, T' and E are the numbers of propositions, tautologies, non-tautologies 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 same-depth-bound 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 list-based 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