Commit d2019fd7 authored by Michael Hanus 's avatar Michael Hanus

Specifications are checked as equivalent to implementations, ground equivalence testing added

parent 570544cb
......@@ -473,81 +473,6 @@ or we simply reuse the old definition by
sumUpIsCorrectOnNonNeg = sumUpIsCorrect . nonNeg
\end{curry}
\subsection{Checking Contracts and Specifications}
\label{sec:currycheck:contracts}
The expressive power of Curry supports
writing high-level specifications
as well as efficient implementations for a given problem
in the same programming language,
as discussed in \cite{AntoyHanus12PADL}.
If a specification or contract is provided for some function,
then CurryCheck automatically generates properties
to test this specification or contract.
Following the notation proposed in \cite{AntoyHanus12PADL},
a \emph{specification}\index{specification}
for an operation $f$ is an operation \code{$f$'spec}
of the same type as $f$.
A \emph{contract}\index{constract} consists
of a pre- and a postcondition, where the precondition could be omitted.
A \emph{precondition}\index{precondition} for an operation $f$
of type $\tau \to \tau'$ is an operation
\begin{curry}
$f$'pre :: $\tau$ ->$~$Bool
\end{curry}
whereas
a \emph{postcondition}\index{postcondition} for $f$
is an operation
\begin{curry}
$f$'post :: $\tau$ ->$~\tau'$ ->$~$Bool
\end{curry}
which relates input and output values
(the generalization to operations with more than one argument
is straightforward).
As a concrete example, consider again the problem of sorting a list.
We can write a postcondition and a specification for
a sort operation \code{sort} and an implementation via quicksort
as follows (where \code{sorted} and \code{perm}
are defined as above):
\begin{curry}
-- Postcondition: input and output lists should have the same length
sort'post xs ys = length xs == length ys
-- Specification:
-- A correct result is a permutation of the input which is sorted.
sort'spec :: [Int] -> [Int]
sort'spec xs | ys == perm xs && sorted ys = ys where ys free
-- An implementation of sort with quicksort:
sort :: [Int] -> [Int]
sort [] = []
sort (x:xs) = sort (filter (<x) xs) ++ [x] ++ sort (filter (>=x) xs)
\end{curry}
%
If we process this program with CurryCheck,
properties to check the specification and postcondition
are automatically generated. For instance,
a specification is satisfied if it yields the same values as
the implementation, and a postcondition is satisfied
if each value computed for some input satisfies the postcondition
relation between input and output. For our example, CurryCheck generates
the following properties (if there are also
preconditions for some operation, these preconditions are used
to restrict the test cases via the condition operater \ccode{==>}):
\begin{curry}
sortSatisfiesPostCondition :: [Int] -> Prop
sortSatisfiesPostCondition x =
let r = sort x
in (r == r) ==> always (sort'post x r)
sortSatisfiesSpecification :: [Int] -> Prop
sortSatisfiesSpecification x = sort x <~> sort'spec x
\end{curry}
\subsection{Checking Equivalence of Operations}
CurryCheck supports also equivalence tests for operations.
......@@ -673,9 +598,99 @@ Otherwise, the equivalence property is \emph{not} tested.
Thus, this mode is useful if one wants to ensure that all
equivalence tests always terminate (provided that the additional
user annotations are correct).
\item[\code{ground}:]
In this mode, only ground equivalence is tested, i.e.,
each equivalence property
\begin{curry}
g1_equiv_g2 = g1 <=> g2
\end{curry}
is transformed into a property which states that both
operations must deliver the same values on same input values, i.e.,
\begin{curry}
g1_equiv_g2 x1 ... xn = g1 x1 ... xn <~> g2 x1 ... xn
\end{curry}
Note this property is more restrictive than contextual equivalence.
For instance, the non-equivalence of \code{g1} and \code{g2}
as shown above cannot be detected by testing ground equivalence only.
\end{description}
\subsection{Checking Contracts and Specifications}
\label{sec:currycheck:contracts}
The expressive power of Curry supports
writing high-level specifications
as well as efficient implementations for a given problem
in the same programming language,
as discussed in \cite{AntoyHanus12PADL}.
If a specification or contract is provided for some function,
then CurryCheck automatically generates properties
to test this specification or contract.
Following the notation proposed in \cite{AntoyHanus12PADL},
a \emph{specification}\index{specification}
for an operation $f$ is an operation \code{$f$'spec}
of the same type as $f$.
A \emph{contract}\index{constract} consists
of a pre- and a postcondition, where the precondition could be omitted.
A \emph{precondition}\index{precondition} for an operation $f$
of type $\tau \to \tau'$ is an operation
\begin{curry}
$f$'pre :: $\tau$ ->$~$Bool
\end{curry}
whereas
a \emph{postcondition}\index{postcondition} for $f$
is an operation
\begin{curry}
$f$'post :: $\tau$ ->$~\tau'$ ->$~$Bool
\end{curry}
which relates input and output values
(the generalization to operations with more than one argument
is straightforward).
As a concrete example, consider again the problem of sorting a list.
We can write a postcondition and a specification for
a sort operation \code{sort} and an implementation via quicksort
as follows (where \code{sorted} and \code{perm}
are defined as above):
\begin{curry}
-- Postcondition: input and output lists should have the same length
sort'post xs ys = length xs == length ys
-- Specification:
-- A correct result is a permutation of the input which is sorted.
sort'spec :: [Int] -> [Int]
sort'spec xs | ys == perm xs && sorted ys = ys where ys free
-- An implementation of sort with quicksort:
sort :: [Int] -> [Int]
sort [] = []
sort (x:xs) = sort (filter (<x) xs) ++ [x] ++ sort (filter (>=x) xs)
\end{curry}
%
If we process this program with CurryCheck,
properties to check the specification and postcondition
are automatically generated. For instance,
a specification is satisfied if it is equivalent to its
implementation, and a postcondition is satisfied
if each value computed for some input satisfies the postcondition
relation between input and output. For our example, CurryCheck generates
the following properties (if there are also
preconditions for some operation, these preconditions are used
to restrict the test cases via the condition operater \ccode{==>}):
\begin{curry}
sortSatisfiesPostCondition :: [Int] -> Prop
sortSatisfiesPostCondition x =
let r = sort x
in (r == r) ==> always (sort'post x r)
sortSatisfiesSpecification :: Prop
sortSatisfiesSpecification = sort <=> sort'spec
\end{curry}
\subsection{Checking Usage of Specific Operations}
In addition to testing dynamic properties of programs,
......
......@@ -20,7 +20,8 @@ sort'post xs ys = length xs == length ys
-- Specification of sort:
-- A list is a sorted result of an input if it is a permutation and sorted.
sort'spec :: [Int] -> [Int]
sort'spec xs | ys == perm xs && sorted ys = ys where ys free
sort'spec xs | sorted ys = ys
where ys = perm xs
-- An implementation of sort with quicksort:
sort :: [Int] -> [Int]
......
--- Example stating the equivalence of an iterative implementation
--- of the factorial function and its recursive specification.
import Test.Prop
-- Recursive definition of factorial.
-- Requires precondition to avoid infinite loops.
fac'spec :: Int -> Int
fac'spec n = if n==0 then 1 else n * fac (n-1)
fac'spec'pre :: Int -> Bool
fac'spec'pre n = n >= 0
-- An iterative implementation of the factorial function.
-- Note that this implementation delivers 1 for negative numbers.
fac :: Int -> Int
fac n = fac' 1 1
where
fac' m p = if m>n then p else fac' (m+1) (m*p)
\ No newline at end of file
......@@ -26,7 +26,8 @@ sort'post xs ys = length xs == length ys && sorted ys
-- Specification of sort:
-- A list is a sorted result of an input if it is a permutation and sorted.
sort'spec :: [Int] -> [Int]
sort'spec xs | ys == perm xs && sorted ys = ys where ys free
sort'spec xs | sorted ys = ys
where ys = perm xs
-- An implementation of sort with quicksort:
sort :: [Int] -> [Int]
......
......@@ -26,14 +26,18 @@
{ "src-dir": "examples",
"options": "-m70",
"modules": [ "DefaultRulesTest", "DetOperations", "ExampleTests",
"ExamplesFromManual", "FloatTest", "ListSpecifications",
"ExamplesFromManual", "FloatTest",
"Nats", "SEBF", "Sum", "SortSpec", "Tree" ]
},
{ "src-dir": "examples",
"options": "-m70 -e ground",
"modules": [ "ListSpecifications" ]
},
{ "src-dir": "examples/withVerification",
"modules": [ "ListProp", "SortSpec" ]
},
{ "src-dir": "examples/equivalent_operations",
"modules": [ "SortISortEquiv" ]
"modules": [ "Fac", "SortISortEquiv" ]
}
],
"documentation": {
......
......@@ -53,7 +53,7 @@ defaultOptions = Options
}
--- Options for equivalence tests.
data EquivOption = Safe | Autoselect | Manual
data EquivOption = Safe | Autoselect | Manual | Ground
deriving Eq
-- Definition of actual command line options.
......@@ -79,7 +79,7 @@ options =
"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 for equivalence tests:\nsafe | autoselect | manual (default) | ground"
, Option "t" ["time"] (NoArg (\opts -> opts { optTime = True }))
"show run time for executing each property test"
, Option "" ["nosource"]
......@@ -126,6 +126,7 @@ options =
| ls `isPrefixOf` "SAFE" = opts { optEquiv = Safe }
| ls `isPrefixOf` "AUTOSELECT" = opts { optEquiv = Autoselect }
| ls `isPrefixOf` "MANUAL" = opts { optEquiv = Manual }
| ls `isPrefixOf` "GROUND" = opts { optEquiv = Ground }
| otherwise = error "Illegal equivalence option (try `-h' for help)"
where ls = map toUpper s
......
......@@ -14,7 +14,7 @@
--- (together with possible preconditions).
---
--- @author Michael Hanus, Jan-Patrick Baye
--- @version August 2018
--- @version October 2018
-------------------------------------------------------------------------
import AnsiCodes
......@@ -56,7 +56,7 @@ ccBanner :: String
ccBanner = unlines [bannerLine,bannerText,bannerLine]
where
bannerText = "CurryCheck: a tool for testing Curry programs (Version " ++
packageVersion ++ " of 24/08/2018)"
packageVersion ++ " of 08/10/2018)"
bannerLine = take (length bannerText) (repeat '-')
-- Help text
......@@ -149,18 +149,20 @@ genTestName test =
-- * test operations
-- * name of generators defined in this module (i.e., starting with "gen"
-- and of appropriate result type)
-- * the names of functions with preconditions defined in the test module
data TestModule = TestModule
{ orgModuleName :: String
, testModuleName :: String
, staticErrors :: [String]
, propTests :: [Test]
, generators :: [QName]
, preConditions :: [QName]
}
-- A test module with only static errors.
staticErrorTestMod :: String -> [String] -> TestModule
staticErrorTestMod modname staterrs =
TestModule modname modname staterrs [] []
TestModule modname modname staterrs [] [] []
-- Is this a test module that should be tested?
testThisModule :: TestModule -> Bool
......@@ -250,9 +252,10 @@ genTestFuncs opts terminating productivity mainmod tm =
pvalOfFunc = ctype2pvalOf mainmod "pvalOf" (resultType texp)
in propOrEquivBody (map (\t -> (t,True)) (argTypes texp)) test
(cLambda (map CPVar xvars)
(addPreCond (preConditions tm) [f1,f2] xvars
(applyF (easyCheckModule,"<~>")
[applyE pvalOfFunc [applyF f1 (map CVar xvars)],
applyE pvalOfFunc [applyF f2 (map CVar xvars)]]))
applyE pvalOfFunc [applyF f2 (map CVar xvars)]])))
-- Operation equivalence test for arbitrary operations:
equivBodyAny f1 f2 texp test =
......@@ -264,9 +267,10 @@ genTestFuncs opts terminating productivity mainmod tm =
[(ctype2BotType mainmod (resultType texp), False)])
test
(CLambda (map CPVar xvars ++ [CPVar pvar])
(addPreCond (preConditions tm) [f1,f2] xvars
(applyF (easyCheckModule,"<~>")
[applyE pvalOfFunc [applyF f1 (map CVar xvars), CVar pvar],
applyE pvalOfFunc [applyF f2 (map CVar xvars), CVar pvar]]))
applyE pvalOfFunc [applyF f2 (map CVar xvars), CVar pvar]])))
propBody qname texp test =
propOrEquivBody (map (\t -> (t,False)) (argTypes texp))
......@@ -408,11 +412,10 @@ makeAllPublic (CurryProg modname imports dfltdecl clsdecls instdecls
makePublic (CmtFunc cmt name arity _ typeExpr rules) =
CmtFunc cmt name arity Public typeExpr rules
-- classify the tests as either PropTest or IOTest
classifyTests :: Options -> CurryProg -> [CFuncDecl] -> [Test]
classifyTests opts prog = map makeProperty
where
makeProperty test =
-- Classify the test represented by a function declaration
-- as either PropTest or IOTest.
classifyTest :: Options -> CurryProg -> CFuncDecl -> Test
classifyTest opts prog test =
if isPropIOType (typeOfQualType (funcType test))
then IOTest tname 0
else maybe (PropTest tname (typeOfQualType (funcType test)) 0)
......@@ -441,10 +444,12 @@ classifyTests opts prog = map makeProperty
-- Extracts all tests from a given Curry module and transforms
-- all polymorphic tests into tests on a base type.
-- The result contains a triple consisting of all actual tests,
-- all ignored tests, and the public version of the original module.
-- The result contains a tuple consisting of all actual tests,
-- all ignored tests, the name of all operations with defined preconditions
-- (needed to generate meaningful equivalence tests),
-- and the public version of the original module.
transformTests :: Options -> String -> CurryProg
-> IO ([CFuncDecl],[CFuncDecl],CurryProg)
-> IO ([CFuncDecl],[CFuncDecl],[QName],CurryProg)
transformTests opts srcdir
prog@(CurryProg mname imps dfltdecl clsdecls instdecls
typeDecls functions opDecls) = do
......@@ -459,7 +464,8 @@ transformTests opts srcdir
-- generate post condition tests:
postCondTests = concatMap (genPostCondTest preCondOps postCondOps) funcs
-- generate specification tests:
specOpTests = concatMap (genSpecTest preCondOps specOps) funcs
specOpTests = concatMap (genSpecTest opts preCondOps specOps) funcs
grSpecOpTests = if optEquiv opts == Ground then specOpTests else []
(realtests,ignoredtests) = partition fst $
if not (optProp opts)
......@@ -468,9 +474,11 @@ transformTests opts srcdir
-- ignore already proved properties:
filter (\fd -> funcName fd `notElem` map funcName theofuncs)
usertests ++
(if optSpec opts then postCondTests ++ specOpTests else [])
return (map snd realtests,
(if optSpec opts then grSpecOpTests ++ postCondTests else [])
return (map snd realtests ++
(if optSpec opts && optEquiv opts /= Ground then specOpTests else []),
map snd ignoredtests,
preCondOps,
CurryProg mname
(nub (easyCheckModule:imps))
dfltdecl clsdecls instdecls
......@@ -478,8 +486,28 @@ transformTests opts srcdir
(simpfuncs ++ map snd (realtests ++ ignoredtests))
opDecls)
where
(usertests, funcs) = partition isProperty functions
(rawusertests, funcs) = partition isProperty functions
usertests = if optEquiv opts == Ground
then map equivProp2Ground rawusertests
else rawusertests
-- transform an equivalence property (f1 <=> f2) into a property
-- testing ground equivalence, i.e., f1 x1...xn <~> f2 x1...xn
equivProp2Ground fdecl =
maybe fdecl
(\ _ -> case classifyTest opts prog fdecl of
EquivTest _ f1 f2 texp _ ->
let ar = arityOfType texp
cvars = map (\i -> (i,"x"++show i)) [1 .. ar]
in stFunc (funcName fdecl) ar Public (propResultType texp)
[simpleRule (map CPVar cvars)
(applyF (easyCheckModule,"<~>")
[applyF f1 (map CVar cvars),
applyF f2 (map CVar cvars)])]
_ -> error "transformTests: internal error"
)
(isEquivProperty fdecl)
-- Extracts all determinism tests from a given Curry module and
-- transforms deterministic operations back into non-deterministic operations
......@@ -540,18 +568,14 @@ propResultType te = case te of
-- fSatisfiesPostCondition x1...xn y = always (f'post x1...xn (f x1...xn))
genPostCondTest :: [QName] -> [QName] -> CFuncDecl -> [CFuncDecl]
genPostCondTest prefuns postops (CmtFunc _ qf ar vis texp rules) =
genSpecTest prefuns postops (CFunc qf ar vis texp rules)
genPostCondTest prefuns postops (CFunc qf ar vis texp rules)
genPostCondTest prefuns postops
(CFunc qf@(mn,fn) _ _ (CQualType clscon texp) _) =
if qf `notElem` postops then [] else
[CFunc (mn, fn ++ postCondSuffix) ar Public
(CQualType clscon (propResultType texp))
[simpleRule (map CPVar cvars) $
if qf `elem` prefuns
then applyF (easyCheckModule,"==>")
[applyF (mn,toPreCondName fn) (map CVar cvars), postprop]
else postprop
]]
addPreCond prefuns [qf] cvars postprop ]]
where
ar = arityOfType texp
cvars = map (\i -> (i,"x"++show i)) [1 .. ar]
......@@ -562,29 +586,57 @@ genPostCondTest prefuns postops
-- Transforms a function declaration into a specification test if
-- there is a specification for this function (i.e., an operation named
-- f'spec). The specification test is of the form
-- f'spec). The generated specification test has the form
-- fSatisfiesSpecification = f <=> f'spec
genSpecTest :: Options -> [QName] -> [QName] -> CFuncDecl -> [CFuncDecl]
genSpecTest opts prefuns specops (CmtFunc _ qf ar vis texp rules) =
genSpecTest opts prefuns specops (CFunc qf ar vis texp rules)
genSpecTest opts prefuns specops
(CFunc qf@(mn,fn) _ _ (CQualType clscon texp) _)
| qf `notElem` specops
= []
| optEquiv opts == Ground
= [genSpecGroundEquivTest prefuns qf clscon texp]
| otherwise
= [CFunc (mn, fn ++ satSpecSuffix) 0 Public
(emptyClassType (propResultType unitType))
[simpleRule [] (applyF (easyCheckModule,"<=>")
[constF qf, constF (mn,toSpecName fn)])]]
-- Transforms a function declaration into a ground equivalence test
-- against the specification (i.e., an operation named `f'spec` exists).
-- The generated specification test is of the form
-- fSatisfiesSpecification x1...xn =
-- f'pre x1...xn ==> (f x1...xn <~> f'spec x1...xn)
genSpecTest :: [QName] -> [QName] -> CFuncDecl -> [CFuncDecl]
genSpecTest prefuns specops (CmtFunc _ qf ar vis texp rules) =
genSpecTest prefuns specops (CFunc qf ar vis texp rules)
genSpecTest prefuns specops
(CFunc qf@(mn,fn) _ _ (CQualType clscon texp) _) =
if qf `notElem` specops then [] else
[CFunc (mn, fn ++ satSpecSuffix) ar Public
genSpecGroundEquivTest :: [QName] -> QName -> CContext -> CTypeExpr -> CFuncDecl
genSpecGroundEquivTest prefuns qf@(mn,fn) clscon texp =
CFunc (mn, fn ++ satSpecSuffix) ar Public
(CQualType (addShowContext clscon) (propResultType texp))
[simpleRule (map CPVar cvars) $
addPreCond (applyF (easyCheckModule,"<~>")
addPreCond prefuns [qf,qfspec] cvars
(applyF (easyCheckModule,"<~>")
[applyF qf (map CVar cvars),
applyF (mn,toSpecName fn) (map CVar cvars)])]]
applyF (mn,toSpecName fn) (map CVar cvars)])]
where
cvars = map (\i -> (i,"x"++show i)) [1 .. ar]
ar = arityOfType texp
addPreCond exp = if qf `elem` prefuns
then applyF (easyCheckModule,"==>")
[applyF (mn,toPreCondName fn) (map CVar cvars), exp]
else exp
cvars = map (\i -> (i,"x"++show i)) [1 .. ar]
qfspec = (mn, toSpecName fn)
-- Adds the preconditions of operations (second argument), if they are
-- present in the list of functions with preconditions in the first argument,
-- on the given variables to the property expression `propexp`.
addPreCond :: [QName] -> [QName] -> [CVarIName] -> CExpr -> CExpr
addPreCond prefuns fs pvars propexp =
let preconds = concatMap precondCall fs
in if null preconds
then propexp
else applyF (easyCheckModule,"==>")
[foldr1 (\x y -> applyF (pre "&&") [x,y]) preconds, propexp]
where
precondCall qn@(mn,fn) =
if qn `elem` prefuns
then [applyF (mn, toPreCondName fn) (map CVar pvars)]
else []
-- Revert the transformation for deterministic operations performed
-- by currypp, i.e., replace rule "f x = selectValue (set f_ORGNDFUN x)"
......@@ -619,10 +671,7 @@ genDetProp prefuns (CFunc (mn,fn) ar _ (CQualType clscon texp) _) =
CFunc (mn, forg ++ isDetSuffix) ar Public
(CQualType (addShowContext clscon) (propResultType texp))
[simpleRule (map CPVar cvars) $
if (mn,forg) `elem` prefuns
then applyF (easyCheckModule,"==>")
[applyF (mn,toPreCondName forg) (map CVar cvars), rnumcall]
else rnumcall ]
addPreCond prefuns [(mn,forg)] cvars rnumcall ]
where
forg = take (length fn - 9) fn
cvars = map (\i -> (i,"x"++show i)) [1 .. ar]
......@@ -784,7 +833,7 @@ analyseCurryProg opts modname orgprog = do
let words = map firstWord (lines progtxt)
staticerrs = missingCPP ++ map (showOpError words) staticoperrs
putStrIfDetails opts "Generating property tests...\n"
(rawTests,ignoredTests,pubmod) <-
(rawTests,ignoredTests,preCondOps,pubmod) <-
transformTests opts srcdir . renameCurryModule (modname++"_PUBLIC")
. makeAllPublic $ prog
let (rawDetTests,ignoredDetTests,pubdetmod) =
......@@ -803,14 +852,16 @@ analyseCurryProg opts modname orgprog = do
(progName pubmod)
staticerrs
(addLinesNumbers words
(classifyTests opts pubmod rawTests))
(map (classifyTest opts pubmod) rawTests))
(generatorsOfProg pubmod)
preCondOps
dettm = TestModule modname
(progName pubdetmod)
[]
(addLinesNumbers words
(classifyTests opts pubdetmod rawDetTests))
(map (classifyTest opts pubdetmod) rawDetTests))
(generatorsOfProg pubmod)
[]
when (testThisModule tm) $ writeCurryProgram opts topdir pubmod ""
when (testThisModule dettm) $ writeCurryProgram opts topdir pubdetmod ""
return (if testThisModule dettm then [tm,dettm] else [tm])
......
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