Commit d0df9d7a authored by Michael Hanus 's avatar Michael Hanus

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

parent 9a9fcb48
......@@ -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,90 @@ 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}
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 :: [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 :: [a] -> [a]
isort xs = idSorted (perm xs)
where idSorted [] = []
idSorted [x] = [x]
idSorted (x:y:ys) | x<=y = x : idSorted (y:ys)
\end{curry}
When checking the equivalence of both operations by
\begin{curry}
psort_equiv_isort = psort <=> isort
\end{curry}
CurryCheck reports a counter example by the 89th test.
Since both operations are terminating, we can also check
the following property:
\begin{curry}
psort_equiv_isort'TERMINATE = psort <=> isort
\end{curry}
Now a counter example is found by the 11th test.
\subsection{Checking Usage of Specific Operations}
In addition to testing dynamic properties of programs,
......@@ -567,8 +651,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 +663,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 n = n : ints1 (n+1)
ints2 n = n : ints2 (n+2)
-- Falsified by 47th test:
ints1_equiv_ints2 = ints1 <=> ints2
This directory contains some example for the use
of CurryCheck to check the equivalence of operations.
Since these are examples to test whether CurryCheck
is able to report counter-examples, their test fails
intentionally.
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
data C = C AB
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 :: [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 :: [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:
-- In PAKCS, the counter example is reported by the 89th test:
psort_equiv_isort = psort <=> isort
-- In PAKCS, the counter example is reported by the 11th test:
psort_equiv_isort'TERMINATE = psort <=> isort
{
"name": "currycheck",
"version": "1.0.1",
"version": "1.1.0",
"author": "Michael Hanus <mh@informatik.uni-kiel.de>",
"synopsis": "A tool to support automatic testing of Curry programs",
"category": [ "Testing" ],
......
This diff is collapsed.
......@@ -3,37 +3,49 @@
--- a Curry program.
---
--- @author Michael Hanus
--- @version Augsut 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)
import AbstractCurry.Select (funcType, resultType, 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 . 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 (QName,QName)
isEquivProperty fdecl =
case funcRules fdecl of
[CRule []
(CSimpleRhs (CApply (CApply (CSymbol prop) (CSymbol f1)) (CSymbol f2)) [])] -> if isEquivSymbol prop then Just (f1,f2) 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
......
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