Commit 28b99bd6 by Michael Hanus

### Support to check equivalence of operations added (combinator <=>)

parent 2f5335b4
 ... ... @@ -12,7 +12,7 @@ and, thus, they are also useful to document the code. The tool can be directly installed by the command > cpm installbin currycheck > cypm install currycheck This installs the executable curry-check in the bin directory of CPM. ... ...
 ... ... @@ -548,6 +548,97 @@ sortSatisfiesSpecification :: [Int] -> Prop sortSatisfiesSpecification x = sort x <~> sort'spec x \end{curry} \subsection{Checking Equivalence of Operations} CurryCheck supports also equivalence checks 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). For instance, the Boolean operations \begin{curry} f1 :: Bool -> Bool f2 :: Bool -> Bool f1 x = not (not x) f2 x = x \end{curry} are equivalent, whereas \begin{curry} g1 :: Bool -> Bool g2 :: Bool -> Bool g1 False = True g2 x = True g1 True = True \end{curry} are not equivalent: \code{g1 failed} has no value but \code{g2 failed} evaluates to \code{True}. To check the equivalence of operations, one can use the property combinator \code{<=>}: \begin{curry} f1_equiv_f2 = f1 <=> f2 g1_equiv_g2 = g1 <=> g2 \end{curry} Each 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. It should be noted that CurryCheck can also check the equivalence of non-terminating operations provided that they are \emph{productive}, i.e., always generate (outermost) constructors after a finite number of steps (otherwise, the test of CurryCheck might not terminate). For instance, CurryCheck reports a counter-example to the equivalence of the following non-terminating operations: \begin{curry} ints1 n = n : ints1 (n+1)$\listline$ 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. 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 but evaluates operations completely. For instance, consider the following definition of permutation sort (the operations \code{perm} and \code{sorted} are defined above): \begin{curry} psort :: Ord a => [a] -> [a] psort xs | sorted ys = ys where ys = perm xs \end{curry} A different definition can be obtained by defining a partial identity on sorted lists: \begin{curry} isort :: Ord a => [a] -> [a] isort xs = idSorted (perm xs) where idSorted [] = [] idSorted [x] = [x] idSorted (x:y:ys) | x<=y = x : idSorted (y:ys) \end{curry} We can check the equivalence of both operations by specializing both operations on some ground type (otherwise, the type checker reports an error due to an unspecified type \code{Ord} context): \begin{curry} psort_equiv_isort = psort <=> (isort :: [Int] -> [Int]) \end{curry} CurryCheck reports a counter example by the 274th test. Since both operations are terminating, we can also check the following property: \begin{curry} psort_equiv_isort'TERMINATE = psort <=> (isort :: [Int] -> [Int]) \end{curry} Now a counter example is found by the 21th test. \subsection{Checking Usage of Specific Operations} In addition to testing dynamic properties of programs, ... ... @@ -567,8 +658,7 @@ Set functions \cite{AntoyHanus09} are used to encapsulate all non-deterministic results of some function in a set structure. Hence, for each top-level function $f$ of arity $n$, the corresponding set function can be expressed in Curry (via operations defined in the module \code{SetFunctions}, see Section~\ref{Library:SetFunctions}) (via operations defined in the library \code{SetFunctions}) by the application \ccode{set$n$ $f$} (this application is used in order to extend the syntax of Curry with a specific notation for set functions). ... ... @@ -580,3 +670,8 @@ Hence, CurryCheck reports such unintended uses of set functions. % LocalWords: CurryCheck %%% Local Variables: %%% mode: latex %%% TeX-master: "main" %%% End:
 -- Testing the equivalence of non-terminating operations: import Nat import Test.Prop -- Two different infinite lists: ints1 :: Int -> [Int] ints1 n = n : ints1 (n+1) ints2 :: Int -> [Int] ints2 n = n : ints2 (n+2) -- Falsified by 47th test: ints1_equiv_ints2 = ints1 <=> ints2
 This directory contains some examples for the use of CurryCheck to check the equivalence of operations. Since most of these are examples to test whether CurryCheck is able to report counter-examples, their test fails intentionally. The module SortISortEquiv contains a successful equivalence test.
 import Test.EasyCheck revrev :: [a] -> [a] revrev xs = reverse (reverse xs) -- Test: is double reverse equivalent to the identity? -- This is not the case if both are applied to the context -- head (... (1:failed)) revrevid'TERMINATE = revrev <=> id
 import Test.Prop -- This is an example which shows the "non-referentiality" of Curry (according -- to [Bacci et al. PPDP'12]), i.e., it shows that two operations, which -- compute the same values, might compute different results in larger -- contexts: data AB = A | B deriving (Eq,Show) data C = C AB deriving (Eq,Show) h A = A g x = C (h x) g' A = C A -- The computed result equivalence of g and g' on ground values -- always holds, i.e., g and g' always compute same values: g_and_g' :: AB -> Prop g_and_g' x = g x <~> g' x -- The contextual equivalence of g and g' does not hold: g_equiv_g' = g <=> g'
 import Test.Prop -- Permutation sort: psort :: Ord a => [a] -> [a] psort xs | sorted ys = ys where ys = perm xs perm [] = [] perm (x:xs) = ndinsert x (perm xs) where ndinsert x ys = x : ys ndinsert x (y:ys) = y : ndinsert x ys sorted [] = True sorted [_] = True sorted (x:y:ys) = x<=y & sorted (y:ys) -- Permutation sort in a different formulation (which is actually not -- equivalent to psort): isort :: Ord a => [a] -> [a] isort xs = idSorted (perm xs) where idSorted [] = [] idSorted [x] = [x] idSorted (x:y:ys) | x<=y = x : idSorted (y:ys) -- The equality of psort and isort on ground values (which always succeeds -- when tested with CurryCheck): --psort_and_isort x = psort x <~> isort x -- Actually, psort and isort are not equivalent, as can be seen by evaluating -- head (isort [2,3,1]). -- Thus, we check the equivalence with CurryCheck (and provide type annotations -- to avoid error message w.r.t. polymorphic types with unspecifed type class -- contexts): -- In PAKCS, the counter example is reported by the 274th test: psort_equiv_isort = psort <=> (isort :: [Int] -> [Int]) -- In PAKCS, the counter example is reported by the 21th test: psort_equiv_isort'TERMINATE = psort <=> (isort :: [Int] -> [Int])
 import Test.Prop -- Permutation sort: psort :: Ord a => [a] -> [a] psort xs | sorted ys = ys where ys = perm xs perm [] = [] perm (x:xs) = ndinsert x (perm xs) where ndinsert x ys = x : ys ndinsert x (y:ys) = y : ndinsert x ys sorted [] = True sorted [_] = True sorted (x:y:ys) = x<=y & sorted (y:ys) -- Insertion sort: The list is sorted by repeated sorted insertion -- of the elements into the already sorted part of the list. insSort :: Ord a => [a] -> [a] insSort [] = [] insSort (x:xs) = insert (insSort xs) where insert [] = [x] insert (y:ys) = if x<=y then x : y : ys else y : insert ys -- Test equivalence of psort and isort (and provide type annotations -- to avoid error message w.r.t. polymorphic types with unspecifed type class -- contexts): psort_equiv_insSort'TERMINATE = psort <=> (insSort :: [Int] -> [Int])
 ... ... @@ -5,9 +5,11 @@ "synopsis": "A tool to support automatic testing of Curry programs", "category": [ "Testing" ], "dependencies": { "base" : ">= 1.0.0, < 2.0.0", : ">= 2.0.0", "flatcurry" : ">= 2.0.0", "rewriting" : ">= 2.0.0" "rewriting" : ">= 2.0.0", "wl-pprint" : ">= 0.0.1" }, "compilerCompatibility": { "pakcs": ">= 2.0.0", ... ... @@ -27,6 +29,9 @@ }, { "src-dir": "examples/withVerification", "modules": [ "ListProp", "SortSpec" ] }, { "src-dir": "examples/equivalent_operations", "modules": [ "SortISortEquiv" ] } ], "documentation": { ... ...
This diff is collapsed.
 ... ... @@ -3,37 +3,49 @@ --- a Curry program. --- --- @author Michael Hanus --- @version October 2016 --- @version December 2017 ------------------------------------------------------------------------ module PropertyUsage ( isProperty, isPropType, isPropIOType ( isProperty, isPropType, isPropIOType, isEquivProperty , propModule, easyCheckModule, easyCheckExecModule ) where import AbstractCurry.Types import AbstractCurry.Select (funcType, resultType, typeOfQualType) import AbstractCurry.Select (funcType, resultType, typeOfQualType, funcRules) ------------------------------------------------------------------------ -- Check whether a function definition is a property, -- i.e., if the result type is Prop or PropIO. --- Check whether a function definition is a property, --- i.e., if the result type is Prop or PropIO. isProperty :: CFuncDecl -> Bool isProperty = isPropertyType . typeOfQualType . funcType where isPropertyType ct = isPropIOType ct || isPropType (resultType ct) -- Is the type expression the type Test.EasyCheck.Prop? --- Is the type expression the type Test.EasyCheck.Prop? isPropType :: CTypeExpr -> Bool isPropType texp = case texp of CTCons (mn,tc) -> tc == "Prop" && isCheckModule mn _ -> False -- Is the type expression the type Test.EasyCheck.PropIO? --- Is the type expression the type Test.EasyCheck.PropIO? isPropIOType :: CTypeExpr -> Bool isPropIOType texp = case texp of CTCons (mn,tc) -> tc == "PropIO" && isCheckModule mn _ -> False --- Check whether a function definition is an equivalence property, i.e., --- has the form test = f1 <=> f2. If yes, returns both operations, --- otherwise Nothing is returned. isEquivProperty :: CFuncDecl -> Maybe (CExpr,CExpr) isEquivProperty fdecl = case funcRules fdecl of [CRule [] (CSimpleRhs (CApply (CApply (CSymbol prop) e1) e2) [])] -> if isEquivSymbol prop then Just (e1,e2) else Nothing _ -> Nothing where isEquivSymbol (qn,mn) = isCheckModule qn && mn=="<=>" -- Is the module name Test.Prop or Test.EasyCheck? isCheckModule :: String -> Bool isCheckModule mn = mn == propModule || mn == easyCheckModule ... ...
 ... ... @@ -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!