Commit 445bbde2 authored by Michael Hanus 's avatar Michael Hanus

Adds options --time and --noiotest

parent d0df9d7a
*~
cdoc/
docs/*.aux
docs/*.pdf
docs/*.toc
docs/*.log
docs/*.out
docs/*.synctex.gz
.curry
.cpm
src/CurryCheckConfig.curry
src/CC/Config.curry
......@@ -80,6 +80,12 @@ S.~Antoy and M.~Hanus.
Aspects of Declarative Languages (PADL 2012)}, pages 33--47. Springer LNCS
7149, 2012.
\bibitem{AntoyHanus18FLOPS}
S.~Antoy and M.~Hanus.
\newblock Equivalence checking of non-deterministic operations.
\newblock In {\em Proc. of the 14th International Symposium on
Functional and Logic Programming (FLOPS 2018)}, to appear in Springer LNCS.
\bibitem{ChristiansenFischer08FLOPS}
J.~Christiansen and S.~Fischer.
\newblock {EasyCheck} - test data for free.
......
......@@ -550,11 +550,12 @@ sortSatisfiesSpecification x = sort x <~> sort'spec x
\subsection{Checking Equivalence of Operations}
CurryCheck supports also equivalence checks for operations.
CurryCheck supports also equivalence tests for operations.
Two operations are considered as \emph{equivalent} if they
can be replaced by each other in any possible context
without changing the computed values (see \cite{AntoyHanus12PADL}
for a precise definition).
without changing the computed values (this is also called
\emph{contextual equivalence} and precisely defined in
\cite{AntoyHanus12PADL} for functional logic programs).
For instance, the Boolean operations
\begin{curry}
f1 :: Bool -> Bool f2 :: Bool -> Bool
......@@ -575,12 +576,16 @@ property combinator \code{<=>}:
f1_equiv_f2 = f1 <=> f2
g1_equiv_g2 = g1 <=> g2
\end{curry}
The left and right argument of this combinator must be a defined operation
or a defined operation with a type annotation in order to specify
the argument types used for checking this property.
CurryCheck transforms such properties into properties
where both operations are compared w.r.t.\ all partial
values and partial results.
The details are described in an upcoming paper.
The details are described in \cite{AntoyHanus18FLOPS}.
It should be noted that CurryCheck can also check
It should be noted that CurryCheck can test
the equivalence of non-terminating operations provided
that they are \emph{productive}, i.e., always generate
(outermost) constructors after a finite number of steps
......@@ -594,13 +599,15 @@ ints2 n = n : ints2 (n+2)
-- This property will be falsified by CurryCheck:
ints1_equiv_ints2 = ints1 <=> ints2
\end{curry}
This is done by guessing depth-bounds and comparing the results
of both operations up to this depth-bound.
This is done by iteratively guessing depth-bounds, computing both operations
up to these depth-bounds, and comparing the computed results.
Since this might be a long process, CurryCheck supports
a faster comparison of operations when it is known
that they are terminating.
If the name of a test contains the suffix \code{'TERMINATE},
then CurryCheck does not iterate over depth-bounds
CurryCheck assumes that the operations to be tested are terminating,
i.e., they always yields a result when applied to ground terms.
In this case, CurryCheck does not iterate over depth-bounds
but evaluates operations completely.
For instance, consider the following definition of
permutation sort (the operations \code{perm} and \code{sorted}
......
......@@ -13,7 +13,7 @@
"pakcs": ">= 1.14.0, < 2.0.0",
"kics2": ">= 0.5.0, < 2.0.0"
},
"configModule": "CurryCheckConfig",
"configModule": "CC.Config",
"executable": {
"name": "curry-check",
"main": "CurryCheck"
......
------------------------------------------------------------------------------
--- Definition and processing of options for CurryCheck
------------------------------------------------------------------------------
module CC.Options where
import Char ( toUpper )
import GetOpt
import IO
import List ( isPrefixOf )
import ReadNumeric ( readNat )
------------------------------------------------------------------------------
-- Representation of command line options.
data Options = Options
{ optHelp :: Bool
, optVerb :: Int
, optKeep :: Bool
, optMaxTest :: Int
, optMaxFail :: Int
, optDefType :: String
, optSource :: Bool
, optIOTest :: Bool
, optProp :: Bool
, optSpec :: Bool
, optDet :: Bool
, optProof :: Bool
, optEquiv :: EquivOption
, optTime :: Bool
, optColor :: Bool
, optMainProg :: String
}
-- Default command line options.
defaultOptions :: Options
defaultOptions = Options
{ optHelp = False
, optVerb = 1
, optKeep = False
, optMaxTest = 0
, optMaxFail = 0
, optDefType = "Ordering"
, optSource = True
, optIOTest = True
, optProp = True
, optSpec = True
, optDet = True
, optProof = True
, optEquiv = Manual
, optTime = False
, optColor = True
, optMainProg = ""
}
--- Options for equivalence tests.
data EquivOption = Safe | Autoselect | Manual
-- Definition of actual command line options.
options :: [OptDescr (Options -> Options)]
options =
[ Option "h?" ["help"] (NoArg (\opts -> opts { optHelp = True }))
"print help and exit"
, Option "q" ["quiet"] (NoArg (\opts -> opts { optVerb = 0 }))
"run quietly (no output, only exit code)"
, Option "v" ["verbosity"]
(OptArg (maybe (checkVerb 3) (safeReadNat checkVerb)) "<n>")
"verbosity level:\n0: quiet (same as `-q')\n1: show test names (default)\n2: show more information about test generation\n3: show test data (same as `-v')\n4: show also some debug information"
, Option "k" ["keep"] (NoArg (\opts -> opts { optKeep = True }))
"keep temporarily generated program files"
, Option "m" ["maxtests"]
(ReqArg (safeReadNat (\n opts -> opts { optMaxTest = n })) "<n>")
"maximal number of tests (default: 100)"
, Option "f" ["maxfails"]
(ReqArg (safeReadNat (\n opts -> opts { optMaxFail = n })) "<n>")
"maximal number of condition failures\n(default: 10000)"
, Option "d" ["deftype"]
(ReqArg checkDefType "<t>")
"type for defaulting polymorphic tests:\nBool | Int | Char | Ordering (default)"
--, Option "e" ["equivalence"]
-- (ReqArg checkEquivOption "<e>")
-- "option for equivalence tests:\nsafe | autoselect | manual (default)"
, Option "t" ["time"] (NoArg (\opts -> opts { optTime = True }))
"show run time for executing each property test"
, Option "" ["nosource"]
(NoArg (\opts -> opts { optSource = False }))
"do not perform source code checks"
, Option "" ["noiotest"]
(NoArg (\opts -> opts { optIOTest = False }))
"do not test I/O properties"
, Option "" ["noprop"]
(NoArg (\opts -> opts { optProp = False }))
"do not perform property tests"
, Option "" ["nospec"]
(NoArg (\opts -> opts { optSpec = False }))
"do not perform specification/postcondition tests"
, Option "" ["nodet"]
(NoArg (\opts -> opts { optDet = False }))
"do not perform determinism tests"
, Option "" ["noproof"]
(NoArg (\opts -> opts { optProof = False }))
"do not consider proofs to simplify properties"
, Option "" ["nocolor"]
(NoArg (\opts -> opts { optColor = False }))
"do not use colors when showing tests"
, Option "" ["mainprog"]
(ReqArg (\s opts -> opts { optMainProg = s }) "<prog>")
"name of generated main program\n(default: TEST<pid>.curry)"
]
where
safeReadNat opttrans s opts =
let numError = error "Illegal number argument (try `-h' for help)" in
maybe numError
(\ (n,rs) -> if null rs then opttrans n opts else numError)
(readNat s)
checkVerb n opts = if n>=0 && n<5
then opts { optVerb = n }
else error "Illegal verbosity level (try `-h' for help)"
checkDefType s opts = if s `elem` ["Bool","Int","Char","Ordering"]
then opts { optDefType = s }
else error "Illegal default type (try `-h' for help)"
checkEquivOption s opts
| ls `isPrefixOf` "SAFE" = opts { optEquiv = Safe }
| ls `isPrefixOf` "AUTOSELECT" = opts { optEquiv = Autoselect }
| ls `isPrefixOf` "MANUAL" = opts { optEquiv = Manual }
| otherwise = error "Illegal equivalence option (try `-h' for help)"
where ls = map toUpper s
--- Further option processing, e.g., setting coloring mode.
processOpts :: Options -> IO Options
processOpts opts = do
isterm <- hIsTerminalDevice stdout
return $ if isterm then opts else opts { optColor = False}
isQuiet :: Options -> Bool
isQuiet opts = optVerb opts == 0
--- Print second argument if verbosity level is not quiet:
putStrIfNormal :: Options -> String -> IO ()
putStrIfNormal opts s = unless (isQuiet opts) (putStr s >> hFlush stdout)
--- Print second argument if verbosity level > 1:
putStrIfDetails :: Options -> String -> IO ()
putStrIfDetails opts s = when (optVerb opts > 1) (putStr s >> hFlush stdout)
--- Print second argument if verbosity level > 3:
putStrLnIfDebug :: Options -> String -> IO ()
putStrLnIfDebug opts s = when (optVerb opts > 3) (putStrLn s >> hFlush stdout)
--- use some coloring (from library AnsiCodes) if color option is on:
withColor :: Options -> (String -> String) -> String -> String
withColor opts coloring = if optColor opts then coloring else id
------------------------------------------------------------------------------
This diff is collapsed.
......@@ -4,10 +4,13 @@
--- Runs a sequence of property tests. Outputs the messages of the failed tests
--- messages and returns exit status 0 if all tests are successful,
--- otherwise status 1.
runPropertyTests :: Bool -> [IO (Maybe String)] -> IO Int
runPropertyTests withcolor props = do
failedmsgs <- sequenceIO props >>= return . Maybe.catMaybes
--- otherwise status 1. If the second argument is `True`, the time
--- needed for checking each property is shown.
runPropertyTests :: Bool -> Bool -> [IO (Maybe String)] -> IO Int
runPropertyTests withcolor withtime props = do
failedmsgs <- sequenceIO (if withtime then map showRunTimeFor props
else props)
>>= return . Maybe.catMaybes
if null failedmsgs
then return 0
else do putStrLn $ (if withcolor then AnsiCodes.red else id) $
......@@ -18,4 +21,13 @@ runPropertyTests withcolor props = do
where
line = take 78 (repeat '=')
--- Prints the run time needed to execute a given IO action.
showRunTimeFor :: IO a -> IO a
showRunTimeFor action = do
t0 <- Profile.getProcessInfos >>= return . maybe 0 id . lookup Profile.RunTime
result <- action
t1 <- Profile.getProcessInfos >>= return . maybe 0 id . lookup Profile.RunTime
putStrLn $ "Run time: " ++ show (t1-t0) ++ " msec."
return result
-------------------------------------------------------------------------
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment