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 |
------------------------------------------------------------------------- --- This module defines the interface of properties that can be checked --- with the CurryCheck tool, an automatic property-based test tool --- based on the EasyCheck library. --- The ideas behind EasyCheck are described in --- [this paper](http://www-ps.informatik.uni-kiel.de/~sebf/pub/flops08.html). --- CurryCheck automatically tests properties 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). --- --- Basically, this module is a stub clone of the EasyCheck library --- which contains only the interface of the operations used to specify --- properties. Hence, this library does not import any other library. --- This supports the definition of properties in any other module --- (execept for the prelude). --- --- @author Sebastian Fischer (with extensions by Michael Hanus) --- @version April 2017 --- @category general ------------------------------------------------------------------------- module Test.Prop ( -- test specification: PropIO, returns, sameReturns, toError, toIOError, Prop, (==>), for, forAll, is, isAlways, isEventually, uniquely, always, eventually, failing, successful, deterministic, (-=-), (<~>), (~>), (<~), (<~~>), (#), (#<), (#>), (<=>), solutionOf, -- test annotations label, trivial, classify, collect, collectAs, -- enumerating values valuesOf ) where infix 1 `is`, `isAlways`, `isEventually` infix 1 -=-, <~>, ~>, <~, <~~>, `trivial`, #, #<, #>, <=> infix 1 `returns`, `sameReturns` infixr 0 ==> ------------------------------------------------------------------------- --- Abstract type to represent properties involving IO actions. data PropIO = PropIO --- The property `returns a x` is satisfied if the execution of the --- I/O action `a` returns the value `x`. returns :: IO a -> a -> PropIO returns _ _ = propUndefinedError "returns" --- The property `sameReturns a1 a2` is satisfied if the execution of the --- I/O actions `a1` and `a2` return identical values. sameReturns :: IO a -> IO a -> PropIO sameReturns _ _ = propUndefinedError "sameReturns" --- The property `toError a` is satisfied if the evaluation of the argument --- to normal form yields an exception. toError :: a -> PropIO toError _ = propUndefinedError "toError" --- The property `toIOError a` is satisfied if the execution of the --- I/O action `a` causes an exception. toIOError :: IO a -> PropIO toIOError _ = propUndefinedError "toIOError" ------------------------------------------------------------------------- --- Abstract type to represent properties to be checked. --- Basically, it contains all tests to be executed to check the property. data Prop = Prop --- The property `x -=- y` is satisfied if `x` and `y` have deterministic --- values that are equal. (-=-) :: a -> a -> Prop _ -=- _ = propUndefinedError "-=-" --- The property `x <~> y` is satisfied if the sets of the values of --- `x` and `y` are equal. (<~>) :: a -> a -> Prop _ <~> _ = propUndefinedError "<~>" --- 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`. (~>) :: a -> a -> Prop _ ~> _ = propUndefinedError "~>" --- 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`. (<~) :: a -> a -> Prop _ <~ _ = propUndefinedError "<~" --- The property `x <~~> y` is satisfied if the multisets of the values of --- `x` and `y` are equal. (<~~>) :: a -> a -> Prop _ <~~> _ = propUndefinedError "<~~>" --- A conditional property is tested if the condition evaluates to `True`. (==>) :: Bool -> Prop -> Prop _ ==> _ = propUndefinedError "==>" --- `solutionOf p` returns (non-deterministically) a solution --- of predicate `p`. This operation is useful to test solutions --- of predicates. solutionOf :: (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 :: a -> (a -> Bool) -> Prop is _ _ = propUndefinedError "is" --- The property `isAlways x p` is satisfied if all values of `x` satisfy `p`. isAlways :: a -> (a -> Bool) -> Prop isAlways _ = propUndefinedError "isAlways" --- The property `isEventually x p` is satisfied if some value of `x` --- satisfies `p`. isEventually :: a -> (a -> Bool) -> Prop isEventually _ = propUndefinedError "isEventually" --- The property `uniquely x` is satisfied if `x` has a deterministic value --- which is true. uniquely :: Bool -> Prop uniquely _ = propUndefinedError "uniquely" --- The property `always x` is satisfied if all values of `x` are true. always :: Bool -> Prop always _ = propUndefinedError "always" --- The property `eventually x` is satisfied if some value of `x` is true. eventually :: Bool -> Prop eventually _ = propUndefinedError "eventually" --- The property `failing x` is satisfied if `x` has no value. failing :: _ -> Prop failing _ = propUndefinedError "failing" --- The property `successful x` is satisfied if `x` has at least one value. successful :: _ -> Prop successful _ = propUndefinedError "successful" --- The property `deterministic x` is satisfied if `x` has exactly one value. deterministic :: _ -> Prop deterministic _ = propUndefinedError "deterministic" --- The property `x # n` is satisfied if `x` has `n` values. (#) :: _ -> Int -> Prop _ # _ = propUndefinedError "#" --- The property `x #< n` is satisfied if `x` has less than `n` values. (#<) :: _ -> Int -> Prop _ #< _ = propUndefinedError "#<" --- The property `x #> n` is satisfied if `x` has more than `n` values. (#>) :: _ -> Int -> Prop _ #> _ = propUndefinedError "#>" --- The property `for x p` is satisfied if all values `y` of `x` --- satisfy property `p y`. for :: a -> (a -> Prop) -> Prop for _ _ = propUndefinedError "for" --- The property `forAll xs p` is satisfied if all values `x` of the list `xs` --- satisfy property `p x`. forAll :: [a] -> (a -> Prop) -> Prop forAll _ _ = propUndefinedError "forAll" --- 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 _ <=> _ = propUndefinedError "#" ------------------------------------------------------------------------- -- Test Annotations --- Assign a label to a property. --- All labeled tests are counted and shown at the end. label :: String -> Prop -> Prop label _ _ = propUndefinedError "label" --- 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 _ _ _ = propUndefinedError "classify" --- 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 _ _ = propUndefinedError "trivial" --- Assign a label showing the given argument to a property. --- All labeled tests are counted and shown at the end. collect :: a -> Prop -> Prop collect _ _ = propUndefinedError "collect" --- 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 :: String -> a -> Prop -> Prop collectAs _ _ _ = propUndefinedError "collectAs" ------------------------------------------------------------------------- -- Value generation --- 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 = error "Test.Prop.valuesOf undefined. Use Test.EasyCheck to actually run it!" propUndefinedError :: String -> _ propUndefinedError op = error $ "Test.Prop." ++ op ++ " undefined. Use Test.EasyCheck to actually run it!" ------------------------------------------------------------------------- |