Commit 051e19fc authored by Michael Hanus 's avatar Michael Hanus
Browse files

Add comments, examples, and extend check for default rules usage

parent 24e4e7ef
# CurryCheck - A Property Testing Tool for Curry
CurryCheck - A Property Testing Tool for Curry
==============================================
This package contains the tool `curry-check` that supports
the automation of testing Curry programs.
......@@ -6,9 +7,27 @@ The tests to be executed can be unit tests as well as
property tests parameterized over some arguments.
The tests can be part of any Curry source program
and, thus, they are also useful to document the code.
## Installing the tool
The basic ideas of CurryCheck are described in a
[LOPSTR 2016 paper](http://dx.doi.org/10.1007/978-3-319-63139-4_13).
In addition to the functionality of other property-based tools,
like [QuickCheck](https://en.wikipedia.org/wiki/QuickCheck),
CurryCheck tests also
[specifications and contracts in Curry programs](http://dx.doi.org/10.1007/978-3-642-27694-1_4),
[determinism properties of operations](http://dx.doi.org/10.1007/978-3-319-51676-9_1),
[equivalence of operations](http://dx.doi.org/10.1007/978-3-319-90686-7_10),
and performs some source code analysis to check the correct usage
of some Curry features, like
[set functions](http://doi.acm.org/10.1145/1599410.1599420),
[default rules](http://doi.org/10.1017/S1471068416000168),
or primitives to implement
[functional patterns](https://doi.org/10.1007/11680093_2).
Thus, it is recommended to use CurryCheck regularly
when developing Curry programs.
Installing CurryCheck
---------------------
The tool can be directly installed by the command
......@@ -17,10 +36,27 @@ The tool can be directly installed by the command
This installs the executable `curry-check` in the bin directory of CPM.
## Using the tool
Using CurryCheck
----------------
If the bin directory of CPM (default: `~/.cpm/bin`) is in your path,
execute the tool with the module containing the properties, e.g.,
> curry-check Nats
Examples
--------
The directory `examples` of this package contains
various example programs to demonstrate the functionality
of CurryCheck. It also contains the following subdirectories
with specific examples:
* `equivalent_operations`: Examples to check the semantic equivalence
of operations as described in the
[FLOPS 2018 paper](http://dx.doi.org/10.1007/978-3-319-90686-7_10).
* `withVerification`: Examples to demonstrate the combination of
testing and verification.
* `illegal_programs`: Some programs showing unindented uses of
Curry features that are detected by CurryCheck.
---------------------------------------------------------------------------
-- Here are some examples for problems to be detected by CurryCheck
---------------------------------------------------------------------------
-- Examples for unintended uses of contracts:
-- Here there is no implementation of the operation `some`:
some'pre _ = True
some'post _ _ = True
some'spec x = x
-- The specification has a different type than the implementation:
k'spec x = x
k x _ = x
inc :: Int -> Int
inc n = n + 1
-- Illegal contract types:
inc'pre x = x
inc'post x y = x+y
---------------------------------------------------------------------------
---------------------------------------------------------------------------
-- Here are some examples for problems to be detected by CurryCheck
---------------------------------------------------------------------------
-- Examples for unintended uses of default rules.
-- Note that a default rule for an operation `f` must have the name
-- `f'default` where `f` is a top-level operation.
-- A default rule without an implementation is not allowed.
some'default _ = True
-- It is not allowed to have more than one default rule.
and :: Bool -> Bool -> Bool
and True True = True
and'default True _ = False
and'default False _ = False
-- Default rules cannot be added to locally defined operations.
land :: Bool -> Bool -> Bool
land x y = g y
where
g True = x
g'default _ = False
---------------------------------------------------------------------------
---------------------------------------------------------------------------
-- Here are some examples for problems to be detected by CurryCheck
---------------------------------------------------------------------------
-- Examples for intended and unintended uses of `Prelude.DET` type synonym.
-- Note that `DET` should only be used to mark the result type of a
-- top-level operation.
-- Ok (but superfluous):
detok :: Bool -> Bool ->DET Bool
detok x _ = x
-- Not allowed: DET must occur in the result type
deterr1 :: DET Bool -> Bool
deterr1 x = x
-- Not allowed: DET must occur outermost in the result type
deterr2 :: Bool -> [DET Bool]
deterr2 x = [x]
-- Not allowed: DET can only be used for top-level operations
deterr3 :: Bool -> Bool
deterr3 x = f x
where
f :: Bool -> DET Bool
f x = x
---------------------------------------------------------------------------
---------------------------------------------------------------------------
-- Here are some examples for problems detected by CurryCheck
---------------------------------------------------------------------------
---------------------------------------------------------------------------
-- The direct use primitives to implement functional patterns is
-- not allowed since their intended use is not ensured.
testNonStrictUniv x | 3 =:<= x = True -- not allowed!
---------------------------------------------------------------------------
---------------------------------------------------------------------------
-- Here are some examples for problems to be detected by CurryCheck
-- Here are some examples for problems detected by CurryCheck
---------------------------------------------------------------------------
import Control.SetFunctions
---------------------------------------------------------------------------
-- Detection of unintended uses of set functions and functional pattern unif.
test1 x | 3 =:<= x = True -- not allowed!
-- Detection of unintended uses of set functions.
-- Note that `setN` must be applied to an `N`-ary top-level operation
-- but not to locally defined operations, lambda abstractions, etc.
test2 = set2 (++) [] [42] -- ok
......@@ -23,42 +22,3 @@ test6 x = set1 f x -- not allowed since f is not a top-level function
test7 xs = set1 (++) xs -- not allowed since (++) has arity 2
---------------------------------------------------------------------------
-- Examples for intended and unintended uses of Prelude.DET type synonym:
-- Ok (but superfluous):
detok :: Bool -> Bool ->DET Bool
detok x _ = x
deterr1 :: DET Bool -> Bool
deterr1 x = x
deterr2 :: Bool -> [DET Bool]
deterr2 x = [x]
deterr3 :: Bool -> Bool
deterr3 x = f x
where
f :: Bool -> DET Bool
f x = x
---------------------------------------------------------------------------
-- Examples for unintended uses of contracts:
some'pre _ = True
some'post _ _ = True
some'spec x = x
k'spec x = x
k x _ = x
inc :: Int -> Int
inc n = n + 1
-- Illegal contract types:
inc'pre x = x
inc'post x y = x+y
---------------------------------------------------------------------------
......@@ -42,9 +42,11 @@ To get some confidence in its general correctness, we test it:
Since everything looks fine, we try to prove it with Agda.
For this purpose, we translate the property and all involved
functions into an Agda program:
functions into an Agda program with the tool `curry-verify`
(see Curry package
[verify](https://www-ps.informatik.uni-kiel.de/~cpm/pkgs/verify.html)):
> curry2verify ListProp
> curry-verify ListProp
...
Agda module 'TO-PROVE-appendAddLengths.agda' written.
...
......
......@@ -66,7 +66,7 @@ ccBanner :: String
ccBanner = unlines [bannerLine,bannerText,bannerLine]
where
bannerText = "CurryCheck: a tool for testing Curry programs (Version " ++
packageVersion ++ " of 06/07/2021)"
packageVersion ++ " of 15/07/2021)"
bannerLine = take (length bannerText) (repeat '-')
-- Help text
......
......@@ -23,24 +23,50 @@ containsDefaultRules = not . null . filter isDefaultFunc . functions
--- for incorrect uses.
checkDefaultRules :: CurryProg -> [(QName,String)]
checkDefaultRules prog =
let (defruledecls,fdecls) = partition isDefaultFunc (functions prog)
in concatMap (checkDefaultRule fdecls) defruledecls
let allfunctions = functions prog
(defruledecls,fdecls) = partition isDefaultFunc allfunctions
in concatMap (checkDefaultRule fdecls) defruledecls ++
concatMap checkLocalDefaultRule allfunctions
checkDefaultRule :: [CFuncDecl] -> CFuncDecl -> [(QName,String)]
checkDefaultRule funcs (CmtFunc _ qf ar vis texp rules) =
checkDefaultRule funcs (CFunc qf ar vis texp rules)
checkDefaultRule funcs (CFunc defqn@(mn,deffn) ar _ _ rules)
| null rules
= [(defqn,"Default rule without right-hand side!")]
| length rules > 1
= [(defqn,"More than one default rule for function!")]
= [(defqn,"More than one default rule for function '" ++ orgfn ++ "'!")]
| otherwise
= maybe [(defqn,"Default rule given but no such function defined!")]
= maybe [(defqn,"Default rule given but function '" ++ orgfn ++ "' not defined!")]
(\fd -> if funcArity fd == ar
then []
else [(defqn,"Default rule has wrong arity!")])
(find (\fd -> funcName fd == qn) funcs)
where qn = (mn, fromDefaultName deffn)
checkDefaultRule funcs (CmtFunc _ qf ar vis texp rules) =
checkDefaultRule funcs (CFunc qf ar vis texp rules)
then []
else [(defqn,"Default rule has wrong arity!")])
(find (\fd -> funcName fd == orgqn) funcs)
where
orgfn = fromDefaultName deffn
orgqn = (mn, orgfn)
checkLocalDefaultRule :: CFuncDecl -> [(QName,String)]
checkLocalDefaultRule (CmtFunc _ qf ar vis texp rules) =
checkLocalDefaultRule (CFunc qf ar vis texp rules)
checkLocalDefaultRule (CFunc defqn@(mn,deffn) ar _ _ rules) =
checkLocalRules (concatMap allLocalDecls rules)
where
checkLocalRules ldecls =
map (\ (_,fn) -> (defqn, "Local default rule '" ++ fn ++ "' is not allowed!"))
(filter (isDefaultName . snd) (concatMap funcNamesOfLDecl ldecls))
--- Get all local declarations of a rule.
allLocalDecls :: CRule -> [CLocalDecl]
allLocalDecls (CRule _ rhs) = localsInRHS rhs
where
localsInRHS (CSimpleRhs _ ldecls) = concatMap localsInLDecls ldecls
localsInRHS (CGuardedRhs _ ldecls) = concatMap localsInLDecls ldecls
localsInLDecls ldecl = ldecl : case ldecl of
CLocalFunc fd -> concatMap allLocalDecls (funcRules fd)
CLocalPat _ e -> localsInRHS e
CLocalVars _ -> []
--- Is this function a declaration of a default rule?
isDefaultFunc :: CFuncDecl -> Bool
......
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