diff --git a/docs/manual.tex b/docs/manual.tex index 921179c92c6dd86b5008511e388e8e5fdf195204..0a295e3897bb0857b5745cc0ad818fabf469baf5 100644 --- a/docs/manual.tex +++ b/docs/manual.tex @@ -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) -\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) +\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, diff --git a/examples/SortSpec.curry b/examples/SortSpec.curry index e8460330083b8a962b4225aaac6649ce1e21568a..427efb850096e1bcb488dba98ac78c7d04d1dabe 100644 --- a/examples/SortSpec.curry +++ b/examples/SortSpec.curry @@ -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] diff --git a/examples/equivalent_operations/Fac.curry b/examples/equivalent_operations/Fac.curry new file mode 100644 index 0000000000000000000000000000000000000000..dd0c64b12fe8872c93ee7d4481e92c2962244e5a --- /dev/null +++ b/examples/equivalent_operations/Fac.curry @@ -0,0 +1,20 @@ +--- 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 diff --git a/examples/withVerification/SortSpec.curry b/examples/withVerification/SortSpec.curry index 73910f304f3d3cdf18530608c569e597f3daf4f0..130ddf5f584342917ce63b6a0d64fd1abfaa1b15 100644 --- a/examples/withVerification/SortSpec.curry +++ b/examples/withVerification/SortSpec.curry @@ -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] diff --git a/package.json b/package.json index 59039674896d5c17471491ac3a25a76ada0d662f..31cb3d74aaa14c9a8cbf8b31c8c74d436f611f9f 100644 --- a/package.json +++ b/package.json @@ -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": { diff --git a/src/CC/Options.curry b/src/CC/Options.curry index 50e21bc0c210774c238fa0db2b6aebb7d65530ca..ff2ad2a6547df9a79b7abb3672c3323cf0ede266 100644 --- a/src/CC/Options.curry +++ b/src/CC/Options.curry @@ -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 "") - "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 diff --git a/src/CurryCheck.curry b/src/CurryCheck.curry index 6cc36eddc8fd9d44957a8f899e0a59b5e6e0934e..240c54ce9e5efcf8601d91aa3cda4309973f0fad 100644 --- a/src/CurryCheck.curry +++ b/src/CurryCheck.curry @@ -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) - (applyF (easyCheckModule,"<~>") - [applyE pvalOfFunc [applyF f1 (map CVar xvars)], - applyE pvalOfFunc [applyF f2 (map CVar xvars)]])) + (addPreCond (preConditions tm) [f1,f2] xvars + (applyF (easyCheckModule,"<~>") + [applyE pvalOfFunc [applyF f1 (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]) - (applyF (easyCheckModule,"<~>") - [applyE pvalOfFunc [applyF f1 (map CVar xvars), CVar pvar], - applyE pvalOfFunc [applyF f2 (map CVar xvars), CVar 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]]))) propBody qname texp test = propOrEquivBody (map (\t -> (t,False)) (argTypes texp)) @@ -408,30 +412,29 @@ 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 +-- 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) + expsToEquivTest + (isEquivProperty test) where - makeProperty test = - if isPropIOType (typeOfQualType (funcType test)) - then IOTest tname 0 - else maybe (PropTest tname (typeOfQualType (funcType test)) 0) - expsToEquivTest - (isEquivProperty test) - where - tname = funcName test - - expsToEquivTest exps = case exps of - (CSymbol f1,CSymbol f2) -> - EquivTest tname f1 f2 (defaultingType (funcTypeOf f1)) 0 - (CTyped (CSymbol f1) qtexp, CSymbol f2) -> - EquivTest tname f1 f2 (defaultingType qtexp) 0 - (CSymbol f1, CTyped (CSymbol f2) qtexp) -> - EquivTest tname f1 f2 (defaultingType qtexp) 0 - (CTyped (CSymbol f1) qtexp, CTyped (CSymbol f2) _) -> - EquivTest tname f1 f2 (defaultingType qtexp) 0 - (e1,e2) -> error $ "Illegal equivalence property:\n" ++ - showCExpr e1 ++ " <=> " ++ showCExpr e2 + tname = funcName test + + expsToEquivTest exps = case exps of + (CSymbol f1,CSymbol f2) -> + EquivTest tname f1 f2 (defaultingType (funcTypeOf f1)) 0 + (CTyped (CSymbol f1) qtexp, CSymbol f2) -> + EquivTest tname f1 f2 (defaultingType qtexp) 0 + (CSymbol f1, CTyped (CSymbol f2) qtexp) -> + EquivTest tname f1 f2 (defaultingType qtexp) 0 + (CTyped (CSymbol f1) qtexp, CTyped (CSymbol f2) _) -> + EquivTest tname f1 f2 (defaultingType qtexp) 0 + (e1,e2) -> error $ "Illegal equivalence property:\n" ++ + showCExpr e1 ++ " <=> " ++ showCExpr e2 defaultingType = poly2defaultType opts . typeOfQualType . defaultQualType @@ -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,"<~>") - [applyF qf (map CVar cvars), - applyF (mn,toSpecName fn) (map CVar cvars)])]] + addPreCond prefuns [qf,qfspec] cvars + (applyF (easyCheckModule,"<~>") + [applyF qf (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 + ar = arityOfType texp + 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])