Skip to content

GitLab

Commit 1b7709e3 authored by Michael Hanus 's avatar Michael Hanus
Browse files

Test.EasyCheck removed (Test.Prop is sufficient)

parent ceb3fffd
Hide whitespace changes
Inline Side-by-side
src/Test/Contract.curry deleted 100644 → 0
View file @ ceb3fffd
------------------------------------------------------------------------
--- This library defines some auxiliaries to check contracts
--- based on specifications or pre- and postconditions provided
--- in a Curry module.
--- The interface might probably change with the further
--- development of the contract implementation.
---
--- @author Michael Hanus
--- @version May 2016
--- @category general
------------------------------------------------------------------------
module Test.Contract
( withContract1, withContract2
, withContract1ND, withContract2ND
, withPreContract1, withPreContract2
, withPostContract0, withPostContract1, withPostContract2
, withPostContract0ND, withPostContract1ND, withPostContract2ND
) where
import SetFunctions
import Unsafe(trace)
---------------------------------------------------------------------------
-- Report the result of checking the pre/postconditions.
-- The first argument is a tag (the name of the operation).
-- The second argument is unified with () (used by enforceable constraints).
-- The third argument is a Boolean result that must not be False for
-- a satisfied condition.
-- The fourth argument is a string describing the context (arguments,result).
checkPre :: String -> Bool -> String -> Bool
checkPre fname result arg = case result of
True -> True
False -> traceLines
["Precondition of "++fname++" violated for:",arg]
(error "Execution aborted due to contract violation!")
checkPreND :: String -> Values Bool -> String -> Bool
checkPreND fname result arg = case False `valueOf` result of
True -> traceLines
["Precondition of "++fname++" violated for:",arg]
(error "Execution aborted due to contract violation!")
False -> True
checkPost :: String -> Bool -> String -> Bool
checkPost fname result arg = case result of
True -> True
False -> traceLines
["Postcondition of "++fname++" violated "++
"for:", arg]
(error "Execution aborted due to contract violation!")
checkPostND :: String -> Values Bool -> String -> Bool
checkPostND fname result arg = case False `valueOf` result of
True -> traceLines
["Postcondition of "++fname++" violated "++
"for:", arg]
(error "Execution aborted due to contract violation!")
False -> True
-- print some lines of output on stderr with flushing after each line
traceLines :: [String] -> a -> a
traceLines ls x = trace (unlines ls) x
-- show operation used to show argument or result terms to the user:
-- Currently, we use Prelude.show but this has the risk that it suspends
-- or loops.
showATerm :: Show a => a -> String
showATerm = show -- or Unsafe.showAnyTerm --
---------------------------------------------------------------------------
-- Combinators for checking of contracts having pre- and postconditions
withContract1 :: (Show a, Show b) => String
-> (a -> Bool) -> (a -> b -> Bool) -> (b -> b)
-> (a -> b) -> a -> b
withContract1 fname precond postcond postobserve fun arg
| checkPre fname (precond arg) (showATerm arg)
&> checkPost fname (postcond arg result)
(unwords [showATerm arg, "->", showATerm (postobserve result)])
= result
where result = fun arg
withContract1ND :: (Show a, Show b) => String
-> (a -> Values Bool) -> (a -> b -> Values Bool) -> (b -> b)
-> (a -> b) -> a -> b
withContract1ND fname precond postcond postobserve fun arg
| checkPreND fname (precond arg) (showATerm arg)
&> checkPostND fname (postcond arg result)
(unwords [showATerm arg, "->", showATerm (postobserve result)])
= result
where result = fun arg
withContract2 :: (Show a, Show b, Show c) => String
-> (a -> b -> Bool) -> (a -> b -> c -> Bool)
-> (c -> c) -> (a -> b -> c) -> a -> b -> c
withContract2 fname precond postcond postobserve fun arg1 arg2
| checkPre fname (precond arg1 arg2)
(unwords [showATerm arg1,showATerm arg2])
&> checkPost fname (postcond arg1 arg2 result)
(unwords [showATerm arg1, showATerm arg2, "->",
showATerm (postobserve result)])
= result
where result = fun arg1 arg2
withContract2ND :: (Show a, Show b, Show c) => String
-> (a -> b -> Values Bool) -> (a -> b -> c -> Values Bool)
-> (c -> c) -> (a -> b -> c) -> a -> b -> c
withContract2ND fname precond postcond postobserve fun arg1 arg2
| checkPreND fname (precond arg1 arg2)
(unwords [showATerm arg1,showATerm arg2])
&> checkPostND fname (postcond arg1 arg2 result)
(unwords [showATerm arg1, showATerm arg2, "->",
showATerm (postobserve result)])
= result
where result = fun arg1 arg2
---------------------------------------------------------------------------
-- Combinators for checking contracts without postconditions:
withPreContract1 :: Show a => String -> (a -> Bool) -> (a -> b) -> a -> b
withPreContract1 fname precond fun arg
| checkPre fname (precond arg) (showATerm arg)
= fun arg
withPreContract2 :: (Show a, Show b) => String -> (a -> b -> Bool)
-> (a -> b -> c) -> a -> b -> c
withPreContract2 fname precond fun arg1 arg2
| checkPre fname (precond arg1 arg2)
(unwords [showATerm arg1,showATerm arg2])
= fun arg1 arg2
---------------------------------------------------------------------------
-- Combinators for checking contracts without preconditions:
-- Add postcondition contract to 0-ary operation:
withPostContract0 :: Show a => String -> (a -> Bool) -> (a -> a) -> a -> a
withPostContract0 fname postcond postobserve val
| checkPost fname (postcond val) (unwords [showATerm (postobserve val)])
= val
-- Add postcondition contract to 0-ary operation:
withPostContract0ND :: Show a => String -> (a -> Values Bool) -> (a -> a) -> a -> a
withPostContract0ND fname postcond postobserve val
| checkPostND fname (postcond val) (unwords [showATerm (postobserve val)])
= val
withPostContract1 :: (Show a, Show b) => String -> (a -> b -> Bool) -> (b -> b)
-> (a -> b) -> a -> b
withPostContract1 fname postcond postobserve fun arg
| checkPost fname (postcond arg result)
(unwords [showATerm arg, "->", showATerm (postobserve result)])
= result
where result = fun arg
withPostContract1ND :: (Show a, Show b) => String
-> (a -> b -> Values Bool) -> (b -> b)
-> (a -> b) -> a -> b
withPostContract1ND fname postcond postobserve fun arg
| checkPostND fname (postcond arg result)
(unwords [showATerm arg, "->", showATerm (postobserve result)])
= result
where result = fun arg
withPostContract2 :: (Show a, Show b, Show c) =>
String -> (a -> b -> c -> Bool) -> (c -> c)
-> (a -> b -> c) -> a -> b -> c
withPostContract2 fname postcond postobserve fun arg1 arg2
| checkPost fname (postcond arg1 arg2 result)
(unwords [showATerm arg1, showATerm arg2, "->",
showATerm (postobserve result)])
= result
where result = fun arg1 arg2
withPostContract2ND :: (Show a, Show b, Show c) =>
String -> (a -> b -> c -> Values Bool) -> (c -> c)
-> (a -> b -> c) -> a -> b -> c
withPostContract2ND fname postcond postobserve fun arg1 arg2
| checkPostND fname (postcond arg1 arg2 result)
(unwords [showATerm arg1, showATerm arg2, "->",
showATerm (postobserve result)])
= result
where result = fun arg1 arg2
---------------------------------------------------------------------------
src/Test/EasyCheck.curry deleted 100644 → 0
View file @ ceb3fffd
-------------------------------------------------------------------------
--- 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 June 2016
--- @category general
-------------------------------------------------------------------------
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 Findall (getAllValues)
import List ( (\\), delete, diagonal, nub )
import SearchTree ( SearchTree, someSearchTree )
import SearchTreeTraversal
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 (Bool -> String -> IO (Maybe String))
--- 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` done)
--- 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" ++ showError 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)
-------------------------------------------------------------------------
--- Abstract type to represent a single test for a property to be checked.
--- A test consists of the result computed for this test,
--- the arguments used for this test, and the labels possibly assigned
--- to this test by annotating properties.
data Test = Test Result [String] [String]
--- Data type to represent the result of checking a property.
data Result = Undef | Ok | Falsified [String] | Ambigious [Bool] [String]
--- Abstract type to represent properties to be checked.
--- Basically, it contains all tests to be executed to check the property.
data Prop = Prop [Test]
--- 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 :: (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 $##)
-------------------------------------------------------------------------
src/Test/EasyCheckExec.curry deleted 100644 → 0
View file @ ceb3fffd
-------------------------------------------------------------------------
--- 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).
--- This module implements the operations to actually execute
--- the tests.
---
--- @author Sebastian Fischer (with extensions by Michael Hanus)
--- @version June 2016
--- @category general
-------------------------------------------------------------------------
module Test.EasyCheckExec (
-- configurations
Config(..), verboseConfig, quietConfig, easyConfig, setMaxTest, setMaxFail,
-- test functions
checkWithValues0, checkWithValues1, checkWithValues2,
checkWithValues3, checkWithValues4, checkWithValues5,
check0, check1, check2, check3, check4, check5,
easyCheck0, easyCheck1, easyCheck2, easyCheck3, easyCheck4, easyCheck5,
verboseCheck0, verboseCheck1, verboseCheck2, verboseCheck3, verboseCheck4,
verboseCheck5,
--easyCheck', easyCheck1', easyCheck2', easyCheck3', easyCheck4', easyCheck5',
-- operations used by the CurryCheck tool
checkPropWithMsg, checkPropIOWithMsg
) where
import AllSolutions ( getAllValues )
import Distribution ( curryCompiler )
import IO ( hFlush, stdout )
import List ( group, intersperse, nub )
import Sort ( leqList, leqString, sortBy )
import Test.EasyCheck
-------------------------------------------------------------------------
--- The configuration of property testing.
--- The configuration contains
--- * the maximum number of tests,
--- * the maximum number of condition failures before giving up,
--- * an operation that shows the number and arguments of each test,
--- * a status whether it should work quietly.
data Config = Config
{ maxTest :: Int
, maxFail :: Int
, every :: Int -> [String] -> String
, isQuiet :: Bool
}
--- Sets the maximum number of tests in a test configuration.
setMaxTest :: Int -> Config -> Config
setMaxTest n config = config { maxTest = n }
--- Sets the maximum number of condition failures in a test configuration.
setMaxFail :: Int -> Config -> Config
setMaxFail n config = config { maxFail = n }
--- The default configuration for EasyCheck shows and deletes the number
--- for each test.
easyConfig :: Config
easyConfig =
Config { maxTest = 100
, maxFail = 10000
, every = (\n _ -> let s = ' ':show (n+1) in s ++ [ chr 8 | _ <- s ])
, isQuiet = False
}
--- A verbose configuration which shows the arguments of every test.
verboseConfig :: Config
verboseConfig = easyConfig { every = (\n xs -> show n ++ ":\n" ++ unlines xs) }
--- A quiet configuration which shows nothing but failed tests.
quietConfig :: Config
quietConfig = easyConfig { isQuiet = True, every = (\_ _ -> "") }
-------------------------------------------------------------------------
-- Test Functions
-- Note that this does not work with PAKCS! However, if CurryCheck is used,
-- this operation is not replaced by explicit generator operations.
suc :: Show b => (a -> Prop) -> (b -> a) -> Prop
suc n = forAllValues n (valuesOf unknown)
--- Checks a unit test with a given configuration (first argument)
--- and a name for the test (second argument).
--- Returns a flag whether the test was successful.
check0 :: Config -> String -> Prop -> IO Bool
check0 = check
--- The property `forValues xs p` is satisfied if all values of `xs`
--- satisfy property `p x`.
forValues :: Show a => [a] -> (a -> Prop) -> Prop
forValues xs p = forAllValues id xs p
--- Checks a unit test with a given configuration (first argument)
--- and a name for the test (second argument).
--- Returns a flag whether the test was successful.
checkWithValues0 :: Config -> String -> Prop -> IO Bool
checkWithValues0 = check
--- Checks a property parameterized over a single argument
--- with a given configuration (first argument),
--- a name for the test (second argument),
--- and all values given in the third argument.
--- Returns a flag whether the test was successful.
checkWithValues1 :: Show a => Config -> String -> [a] -> (a -> Prop) -> IO Bool
checkWithValues1 config msg xs p = check config msg (forValues xs p)
--- Checks a property parameterized over two arguments
--- with a given configuration (first argument)