-------------------------------------------------------------------- -- | -- Module : Test.SmallCheck.Property -- Copyright : (c) Colin Runciman et al. -- License : BSD3 -- Maintainer: Roman Cheplyaka <roma@ro-che.info> -- -- Properties and tools to construct them. -------------------------------------------------------------------- module Test.SmallCheck.Property ( -- * Basic definitions TestCase(..), TestResult(..), resultIsOk, Property, Depth, Testable(..), property, mkProperty, -- * Constructing tests (==>), exists, existsDeeperBy, exists1, exists1DeeperBy, -- ** 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. forAll, forAllElem, thereExists, thereExistsElem, thereExists1, thereExists1Elem ) where import Test.SmallCheck.Series data TestResult = Pass | Fail | Inappropriate -- ^ 'Inappropriate' means that the precondition of '==>' -- was not satisfied data TestCase = TestCase { result :: TestResult, arguments :: [String] } -- | Wrapper type for 'Testable's newtype Property = Property (Depth -> [TestCase]) -- | Wrap a 'Testable' into a 'Property' property :: Testable a => a -> Property property = Property . test -- | 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. mkProperty :: (Depth -> [TestCase]) -> Property mkProperty = Property -- | Anything of a 'Testable' type can be regarded as a \"test\" class Testable a where test :: a -> Depth -> [TestCase] instance Testable Bool where test b _ = [TestCase (boolToResult b) []] instance (Serial a, Show a, Testable b) => Testable (a->b) where test f = f' where Property f' = forAll series f instance Testable Property where test (Property f) d = f d forAll :: (Show a, Testable b) => Series a -> (a->b) -> Property forAll xs f = Property $ \d -> [ r{arguments = show x : arguments r} | x <- xs d, r <- test (f x) d ] forAllElem :: (Show a, Testable b) => [a] -> (a->b) -> Property forAllElem xs = forAll (const xs) existence :: (Show a, Testable b) => Bool -> Series a -> (a->b) -> Property existence u xs f = Property existenceDepth where existenceDepth d = [ TestCase (boolToResult valid) arguments ] where witnesses = [ show x | x <- xs d, all (resultIsOk . result) (test (f x) d) ] valid = enough witnesses enough = if u then unique else (not . null) arguments = if valid then [] else if null witnesses then ["non-existence"] else "non-uniqueness" : take 2 witnesses unique :: [a] -> Bool unique [_] = True unique _ = False -- | Return 'False' iff the result is 'Fail' resultIsOk :: TestResult -> Bool resultIsOk r = case r of Fail -> False Pass -> True Inappropriate -> True boolToResult :: Bool -> TestResult boolToResult b = if b then Pass else Fail thereExists :: (Show a, Testable b) => Series a -> (a->b) -> Property thereExists = existence False thereExists1 :: (Show a, Testable b) => Series a -> (a->b) -> Property thereExists1 = existence True thereExistsElem :: (Show a, Testable b) => [a] -> (a->b) -> Property thereExistsElem xs = thereExists (const xs) thereExists1Elem :: (Show a, Testable b) => [a] -> (a->b) -> Property thereExists1Elem xs = thereExists1 (const xs) -- | @'exists' p@ holds iff it is possible to find an argument @a@ (within the -- depth constraints!) satisfying the predicate @p@ exists :: (Show a, Serial a, Testable b) => (a->b) -> Property exists = thereExists series -- | Like 'exists', but additionally require the uniqueness of the -- argument satisfying the predicate exists1 :: (Show a, Serial a, Testable b) => (a->b) -> Property exists1 = thereExists1 series -- | 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 @'Depth' -> 'Depth'@ function: -- -- >prop_append2 :: [Bool] -> [Bool] -> Property -- >prop_append2 xs ys = existsDeeperBy (*2) $ \zs -> zs == xs++ys existsDeeperBy :: (Show a, Serial a, Testable b) => (Depth->Depth) -> (a->b) -> Property existsDeeperBy f = thereExists (series . f) -- | Like 'existsDeeperBy', but additionally require the uniqueness of the -- argument satisfying the predicate exists1DeeperBy :: (Show a, Serial a, Testable b) => (Depth->Depth) -> (a->b) -> Property exists1DeeperBy f = thereExists1 (series . f) infixr 0 ==> -- | 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. (==>) :: Testable a => Bool -> a -> Property True ==> x = Property (test x) False ==> x = Property (const [nothing]) where nothing = TestCase { result = Inappropriate, arguments = [] }