------------------------------------------------------------------------- --- EasyCheck is a library for automated, property-based testing of --- Curry programs. The ideas behind EasyCheck are described in --- [this paper](http://www-ps.informatik.uni-kiel.de/~sebf/pub/flops08.html). --- The CurryCheck tool automatically executes tests 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](http://www.informatik.uni-kiel.de/~mh/papers/LOPSTR16.html). --- --- Note that this module defines the interface of EasyCheck to --- define properties. The operations to actually execute the tests --- are contained in the accompanying library `Test.EasyCheckExec`. --- --- @author Sebastian Fischer (with extensions by Michael Hanus) --- @version November 2020 ------------------------------------------------------------------------- module Test.EasyCheck ( -- test specification: PropIO, returns, sameReturns, toError, toIOError, Test, Prop, (==>), for, forAll, test, is, isAlways, isEventually, uniquely, always, eventually, failing, successful, deterministic, (-=-), (<~>), (~>), (<~), (<~~>), (#), (#<), (#>), (<=>), solutionOf, -- test annotations label, trivial, classify, collect, collectAs, -- enumerating values valuesOfSearchTree, valuesOf, -- for EasyCheckExec Result(..), result, args, updArgs, stamp, testsOf, ioTestOf, forAllValues ) where import Control.Monad ( unless ) import Data.List ( (\\), delete, diagonal, nub ) import Control.Findall ( getAllValues ) import Control.SearchTree ( SearchTree, someSearchTree ) import Control.SearchTree.Traversal import Test.Prop.Types infix 1 `is`, `isAlways`, `isEventually` infix 1 -=-, <~>, ~>, <~, <~~>, `trivial`, #, #<, #>, <=> infix 1 `returns`, `sameReturns` infixr 0 ==> ------------------------------------------------------------------------- -- Properties involving I/O actions: --- The property `returns a x` is satisfied if the execution of the --- I/O action `a` returns the value `x`. returns :: (Eq a, Show a) => IO a -> a -> PropIO returns act r = PropIO (testIO act (return r)) --- The property `sameReturns a1 a2` is satisfied if the execution of the --- I/O actions `a1` and `a2` return identical values. sameReturns :: (Eq a, Show a) => IO a -> IO a -> PropIO sameReturns a1 a2 = PropIO (testIO a1 a2) --- The property `toError a` is satisfied if the evaluation of the argument --- to normal form yields an exception. toError :: a -> PropIO toError x = toIOError (getAllValues x >>= \rs -> (id $!! rs) `seq` return ()) --- The property `toIOError a` is satisfied if the execution of the --- I/O action `a` causes an exception. toIOError :: IO a -> PropIO toIOError act = PropIO (hasIOError act) --- Extracts the tests of an I/O property (used by the test runner). ioTestOf :: PropIO -> (Bool -> String -> IO (Maybe String)) ioTestOf (PropIO t) = t -- Test an IO property, i.e., compare the results of two IO actions. testIO :: (Eq a, Show a) => IO a -> IO a -> Bool -> String -> IO (Maybe String) testIO act1 act2 quiet msg = catch (do r1 <- act1 r2 <- act2 if r1 == r2 then unless quiet (putStr (msg++": OK\n")) >> return Nothing else do putStrLn $ msg ++ ": FAILED!\nResults: " ++ show (r1,r2) return (Just msg) ) (\err -> do putStrLn $ msg ++ ": EXECUTION FAILURE:\n" ++ show err return (Just msg) ) -- Test whether an IO action produces an error. hasIOError :: IO a -> Bool -> String -> IO (Maybe String) hasIOError act quiet msg = catch (act >> return (Just msg)) (\_ -> unless quiet (putStr (msg++": OK\n")) >> return Nothing) ------------------------------------------------------------------------- -- Some auxiliaries: --- Extracts the tests of a property (used by the test runner). testsOf :: Prop -> [Test] testsOf (Prop ts) = ts --- An empty test. notest :: Test notest = Test Undef [] [] --- Extracts the result of a test. result :: Test -> Result result (Test r _ _) = r --- Set the result of a test. setResult :: Result -> Test -> Test setResult res (Test _ s a) = Test res a s --- Extracts the arguments of a test. args :: Test -> [String] args (Test _ a _) = a --- Extracts the labels of a test. stamp :: Test -> [String] stamp (Test _ _ s) = s --- Updates the arguments of a test. updArgs :: ([String] -> [String]) -> Test -> Test updArgs upd (Test r a s) = Test r (upd a) s --- Updates the labels of a test. updStamp :: ([String] -> [String]) -> Test -> Test updStamp upd (Test r a s) = Test r a (upd s) -- Test Specification --- Constructs a property to be tested from an arbitrary expression --- (first argument) and a predicate that is applied to the list of --- non-deterministic values. The given predicate determines whether --- the constructed property is satisfied or falsified for the given --- expression. test :: Show a => a -> ([a] -> Bool) -> Prop test x f = Prop [setResult res notest] where xs = valuesOf x res = case valuesOf (f xs) of [True] -> Ok [False] -> Falsified (map show xs) bs -> Ambigious bs (map show xs) --- The property `x -=- y` is satisfied if `x` and `y` have deterministic --- values that are equal. (-=-) :: (Eq a, Show a) => a -> a -> Prop x -=- y = (x,y) `is` uncurry (==) --- 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 x <~> y = test x (isSameSet (valuesOf y)) --- 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`. (~>) :: (Eq a, Show a) => a -> a -> Prop x ~> y = test x (isSubsetOf (valuesOf y)) --- 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`. (<~) :: (Eq a, Show a) => a -> a -> Prop x <~ y = test x (`isSubsetOf` (valuesOf y)) --- The property `x <~~> y` is satisfied if the multisets of the values of --- `x` and `y` are equal. (<~~>) :: (Eq a, Show a) => a -> a -> Prop x <~~> y = test x (isSameMSet (valuesOf y)) isSameSet :: Eq a => [a] -> [a] -> Bool isSameSet xs ys = xs' `subset` ys' && ys' `subset` xs' where xs' = nub xs ys' = nub ys isSubsetOf :: Eq a => [a] -> [a] -> Bool xs `isSubsetOf` ys = nub xs `subset` ys subset :: Eq a => [a] -> [a] -> Bool xs `subset` ys = null (xs\\ys) -- compare to lists if they represent the same multi-set isSameMSet :: Eq a => [a] -> [a] -> Bool isSameMSet [] ys = ys == [] isSameMSet (x:xs) ys | x `elem` ys = isSameMSet xs (delete x ys) | otherwise = False --- A conditional property is tested if the condition evaluates to `True`. (==>) :: Bool -> Prop -> Prop cond ==> p = if True `elem` valuesOf cond then p else Prop [notest] --- `solutionOf p` returns (non-deterministically) a solution --- of predicate `p`. This operation is useful to test solutions --- of predicates. solutionOf :: Data a => (a -> Bool) -> a solutionOf pred = pred x &> x where x free --- The property `is x p` is satisfied if `x` has a deterministic value --- which satisfies `p`. is :: Show a => a -> (a -> Bool) -> Prop is x f = test x (\xs -> case xs of [y] -> f y _ -> False) --- The property `isAlways x p` is satisfied if all values of `x` satisfy `p`. isAlways :: Show a => a -> (a -> Bool) -> Prop isAlways x = test x . all --- The property `isEventually x p` is satisfied if some value of `x` --- satisfies `p`. isEventually :: Show a => a -> (a -> Bool) -> Prop isEventually x = test x . any --- The property `uniquely x` is satisfied if `x` has a deterministic value --- which is true. uniquely :: Bool -> Prop uniquely = (`is` id) --- The property `always x` is satisfied if all values of `x` are true. always :: Bool -> Prop always = (`isAlways` id) --- The property `eventually x` is satisfied if some value of `x` is true. eventually :: Bool -> Prop eventually = (`isEventually` id) --- The property `failing x` is satisfied if `x` has no value. failing :: Show a => a -> Prop failing x = test x null --- The property `successful x` is satisfied if `x` has at least one value. successful :: Show a => a -> Prop successful x = test x (not . null) --- The property `deterministic x` is satisfied if `x` has exactly one value. deterministic :: Show a => a -> Prop deterministic x = x `is` const True --- The property `x # n` is satisfied if `x` has `n` values. (#) :: (Eq a, Show a) => a -> Int -> Prop x # n = test x ((n==) . length . nub) --- The property `x #< n` is satisfied if `x` has less than `n` values. (#<) :: (Eq a, Show a) => a -> Int -> Prop x #< n = test x (( n` is satisfied if `x` has more than `n` values. (#>) :: (Eq a, Show a) => a -> Int -> Prop x #> n = test x ((>n) . length . nub) --- The property `for x p` is satisfied if all values `y` of `x` --- satisfy property `p y`. for :: Show a => a -> (a -> Prop) -> Prop for x p = forAll (valuesOf x) p --- The property `forAll xs p` is satisfied if all values `x` of the list `xs` --- satisfy property `p x`. forAll :: Show a => [a] -> (a -> Prop) -> Prop forAll xs p = forAllValues id xs p --- Only for internal use by the test runner. forAllValues :: Show a => (b -> Prop) -> [a] -> (a -> b) -> Prop forAllValues c vals f = Prop $ diagonal [[ updArgs (show y:) t | let Prop ts = c (f y), t <- ts ] | y <- vals ] --- 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. (<=>) :: a -> a -> Prop _ <=> _ = error $ "Test.Prop.<=> not executable. Use CurryCheck to test this property!" ------------------------------------------------------------------------- -- Test Annotations --- Assign a label to a property. --- All labeled tests are counted and shown at the end. label :: String -> Prop -> Prop label l (Prop ts) = Prop (map (updStamp (l:)) ts) --- 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 --- classify :: Bool -> String -> Prop -> Prop classify True name = label name classify False _ = id --- Assign the label "trivial" to a property if the first argument is `True`. --- All labeled tests are counted and shown at the end. trivial :: Bool -> Prop -> Prop trivial = (`classify` "trivial") --- Assign a label showing the given argument to a property. --- All labeled tests are counted and shown at the end. collect :: Show a => a -> Prop -> Prop collect = label . show --- Assign a label showing a given name and the given argument to a property. --- All labeled tests are counted and shown at the end. collectAs :: Show a => String -> a -> Prop -> Prop collectAs name = label . ((name++": ")++) . show ------------------------------------------------------------------------- -- Value generation --- Extracts values of a search tree according to a given strategy --- (here: randomized diagonalization of levels with flattening). valuesOfSearchTree :: SearchTree a -> [a] valuesOfSearchTree -- = depthDiag -- = rndDepthDiag 0 -- = levelDiag -- = rndLevelDiag 0 = rndLevelDiagFlat 5 0 -- = allValuesB --- Computes the list of all values of the given argument --- according to a given strategy (here: --- randomized diagonalization of levels with flattening). valuesOf :: a -> [a] valuesOf = valuesOfSearchTree . someSearchTree . (id $##) -------------------------------------------------------------------------