1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331 332 333 334 335 336 337 338 339 340 |
------------------------------------------------------------------------- --- 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) . length . nub) --- The property `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 $##) ------------------------------------------------------------------------- |