manual.tex 29.4 KB
Newer Older
Michael Hanus 's avatar
Michael Hanus committed
1
\section{CurryCheck: A Tool for Testing Properties of Curry Programs}
Michael Hanus 's avatar
Michael Hanus committed
2 3 4 5 6 7 8 9 10 11 12 13 14 15 16
\label{sec-currycheck}

CurryCheck\index{CurryCheck}\index{testing programs}\index{program!testing}
is a tool that supports the automation of
testing Curry programs.
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.
CurryCheck is based on EasyCheck \cite{ChristiansenFischer08FLOPS}.
Actually, the properties to be tested are written
by combinators proposed for EasyCheck, which are actually
influenced by QuickCheck \cite{ClaessenHughes00}
but extended to the demands of functional logic programming.

Michael Hanus 's avatar
Michael Hanus committed
17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32
\subsection{Installation}

The current implementation of CurryCheck is a package
managed by the Curry Package Manager CPM.
Thus, to install the newest version of CurryCheck, use the following commands:
%
\begin{curry}
> cypm update
> cypm install currycheck
\end{curry}
%
This downloads the newest package, compiles it, and places
the executable \code{curry-check} into the directory \code{\$HOME/.cpm/bin}.
Hence it is recommended to add this directory to your path
in order to execute CurryCheck as described below.

Michael Hanus 's avatar
Michael Hanus committed
33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51
\subsection{Testing Properties}

To start with a concrete example, consider the following naive definition of
reversing a list:
\begin{curry}
rev :: [a] -> [a]
rev []     = []
rev (x:xs) = rev xs ++ [x]
\end{curry}
To get some confidence in the code, we add some unit tests,
i.e., test with concrete test data:
\begin{curry}
revNull = rev []      -=- []
rev123  = rev [1,2,3] -=- [3,2,1]
\end{curry}
The operator \ccode{-=-} specifies a test where both sides must
have a single identical value. Since this operator (as many more, see below)
are defined in the library \code{Test.Prop}\pindex{Test.Prop},\footnote{%
The library \code{Test.Prop} is a clone of the library
Michael Hanus 's avatar
Michael Hanus committed
52
\code{Test.EasyCheck}\pindex{Test.EasyCheck} (see package \code{easycheck})
Michael Hanus 's avatar
Michael Hanus committed
53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86
which defines only the interface but not the actual test implementations.
Thus, the library \code{Test.Prop} has less import dependencies.
When CurryCheck generates programs to execute the tests,
it automatically replaces references to \code{Test.Prop}
by references to \code{Test.EasyCheck} in the generated programs.}
we also have to import this library.
Apart from unit tests, which are often tedious to write,
we can also write a property, i.e., a test parameterized over
some arguments. For instance, an interesting property of reversing a list
is the fact that reversing a list two times provides the input list:
\begin{curry}
revRevIsId xs = rev (rev xs) -=- xs
\end{curry}
Note that each property is defined as a Curry operation
where the arguments are the parameters of the property.
Altogether, our program is as follows:
\begin{curry}
module Rev(rev) where

import Test.Prop

rev :: [a] -> [a]
rev []     = []
rev (x:xs) = rev xs ++ [x]

revNull = rev []      -=- []
rev123  = rev [1,2,3] -=- [3,2,1]

revRevIsId xs = rev (rev xs) -=- xs
\end{curry}
Now we can run all tests by invoking the CurryCheck tool.
If our program is stored in the file \code{Rev.curry},
we can execute the tests as follows:
\begin{curry}
Michael Hanus 's avatar
Michael Hanus committed
87
> curry-check Rev
Michael Hanus 's avatar
Michael Hanus committed
88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109
...
Executing all tests...
revNull (module Rev, line 7):
 Passed 1 test.
rev123 (module Rev, line 8):
 Passed 1 test.
revRevIsId_ON_BASETYPE (module Rev, line 10):
 OK, passed 100 tests.
\end{curry}
Since the operation \code{rev} is polymorphic,
the property \code{revRevIsId} is also polymorphic in its argument.
In order to select concrete values to test this property,
CurryCheck replaces such polymorphic tests by defaulting the type
variable to prelude type \code{Ordering}
(the actual default type can also be set by a command-line flag).
If we want to test this property on integers numbers,
we can explicitly provide a type signature,
where \code{Prop} denotes the type of a test:
\begin{curry}
revRevIsId :: [Int] -> Prop
revRevIsId xs = rev (rev xs) -=- xs
\end{curry}
Michael Hanus 's avatar
Michael Hanus committed
110
The command \code{curry-check} has some options to influence
Michael Hanus 's avatar
Michael Hanus committed
111 112 113 114
the output, like \ccode{-q} for a quiet execution
(only errors and failed tests are reported) or
\ccode{-v} for a verbose execution where all generated test cases
are shown.
Michael Hanus 's avatar
Michael Hanus committed
115
Moreover, the return code of \code{curry-check} is \code{0}
Michael Hanus 's avatar
Michael Hanus committed
116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235
in case of successful tests, otherwise, it is \code{1}.
Hence, CurryCheck can be easily integrated in tool chains
for automatic testing.

In order to support the inclusion of properties in the source code,
the operations defined the properties do not have to be exported,
as show in the module \code{Rev} above.
Hence, one can add properties to any library and export only
library-relevant operations. To test these properties,
CurryCheck creates a copy of the library where all operations
are public, i.e., CurryCheck requires write permission on the
directory where the source code is stored.

The library \code{Test.Prop} defines many combinators
to construct properties. In particular, there are a couple of
combinators for dealing with non-deterministic operations
(note that this list is incomplete):
\begin{itemize}
\item
The combinator \ccode{<\char126>} is satisfied if the set of values
of both sides are equal.
\item
The property \code{$x$ \char126> $y$} is satisfied if $x$
evaluates to every value of $y$.
Thus, the set of values of $y$ must be a subset of the set of values of $x$.
\item
The property \code{$x$ <\char126 $y$} is satisfied if $y$
evaluates to every value of $x$, i.e.,
the set of values of $x$ must be a subset of the set of values of $y$.
\item
The combinator \ccode{<\char126\char126>} is satisfied
if the multi-set of values of both sides are equal.
Hence, this operator can be used to compare the number
of computed solutions of two expressions.
\item
The property \code{always $x$} is satisfied if all values of $x$ are true.
\item
The property \code{eventually $x$} is satisfied if some value
of $x$ is true.
\item
The property \code{failing $x$} is satisfied if $x$ has no value,
i.e., its evaluation fails.
\item
The property \code{$x$ \# $n$} is satisfied if $x$ has $n$
different values.
\end{itemize}
%
For instance, consider the insertion of an element at an arbitrary
position in a list:
\begin{curry}
insert :: a -> [a] -> [a]
insert x xs     = x : xs
insert x (y:ys) = y : insert x ys
\end{curry}
The following property states that the element is inserted
(at least) at the beginning or the end of the list:
\begin{curry}
insertAsFirstOrLast :: Int -> [Int] -> Prop
insertAsFirstOrLast x xs = insert x xs ~> (x:xs ? xs++[x])
\end{curry}
%
A well-known application of \code{insert} is to use it to define
a permutation of a list:
\begin{curry}
perm :: [a] -> [a]
perm []     = []
perm (x:xs) = insert x (perm xs)
\end{curry}
We can check whether the length of a permuted lists is unchanged:
\begin{curry}
permLength :: [Int] -> Prop
permLength xs = length (perm xs) <~> length xs
\end{curry}
Note that the use of \ccode{<\char126>} is relevant since
we compare non-deterministic values. Actually, the left argument
evaluates to many (identical) values.

One might also want to check whether \code{perm} computes the
correct number of solutions. Since we know that a list of length $n$
has $n!$ permutations, we write the following property:
\begin{curry}
permCount :: [Int] -> Prop
permCount xs = perm xs # fac (length xs)
\end{curry}
where \code{fac} is the factorial function.
However, this test will be falsified with the argument \code{[1,1]}.
Actually, this list has only one permuted value since the two
possible permutations are identical and the combinator \ccode{\#}
counts the number of \emph{different} values.
The property would be correct if all elements in the input list \code{xs}
are different.
This can be expressed by a conditional property:
the property \code{$b$ ==> $p$} is satisfied if $p$
is satisfied for all values where $b$ evaluates to \code{True}.
Therefore, if we define a predicate \code{allDifferent} by
\begin{curry}
allDifferent []     = True
allDifferent (x:xs) = x `notElem` xs && allDifferent xs
\end{curry}
then we can reformulate our property as follows:
\begin{curry}
permCount xs = allDifferent xs ==> perm xs # fac (length xs)
\end{curry}
%
Now consider a predicate to check whether a list is sorted:
\begin{curry}
sorted :: [Int] -> Bool
sorted []       = True
sorted [_]      = True
sorted (x:y:zs) = x<=y && sorted (y:zs)
\end{curry}
This predicate is useful to test whether there are also sorted permutations:
\begin{curry}
permIsEventuallySorted :: [Int] -> Prop
permIsEventuallySorted xs = eventually $\code{\$}$ sorted (perm xs)
\end{curry}
%
The previous operations can be exploited to provide
a high-level specification of sorting a list:
\begin{curry}
Michael Hanus 's avatar
Michael Hanus committed
236
psort :: [Int] -> [Int]
Michael Hanus 's avatar
Michael Hanus committed
237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259
psort xs | sorted ys = ys
 where ys = perm xs
\end{curry}
Again, we can write some properties:
\begin{curry}
psortIsAlwaysSorted xs = always $\code{\$}$ sorted (psort xs)$\listline$
psortKeepsLength xs = length (psort xs) <~> length xs
\end{curry}
Of course, the sort specification via permutations is not useful
in practice. However, it can be used as an oracle to test
more efficient sorting algorithms like quicksort:
\begin{curry}
qsort :: [Int] -> [Int] 
qsort []     = []
qsort (x:l)  = qsort (filter (<x) l) ++ x : qsort (filter (>x) l)
\end{curry}
The following property specifies the correctness of quicksort:
\begin{curry}
qsortIsSorting xs = qsort xs <~> psort xs
\end{curry}
Actually, if we test this property, we obtain a failure:
%
\begin{curry}
Michael Hanus 's avatar
Michael Hanus committed
260
> curry-check ExampleTests
Michael Hanus 's avatar
Michael Hanus committed
261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302
...
qsortIsSorting (module ExampleTests, line 53) failed
Falsified by third test.
Arguments:
[1,1]
Results:
[1]
\end{curry}
%
The result shows that, for the given argument \code{[1,1]},
an element has been dropped in the result.
Hence, we correct our implementation, e.g., by replacing
\code{(>x)} with \code{(>=x)}, and obtain a successful test execution.

For I/O operations, it is difficult to execute them with random data.
Hence, CurryCheck only supports specific I/O unit tests:
\begin{itemize}
\item \code{$a$ `returns` $x$} is satisfied if the I/O action $a$
returns the value $x$.
\item \code{$a$ `sameReturns` $b$} is satisfied if the I/O actions
$a$ and $b$ return identical values.
\end{itemize}
%
Since CurryCheck executes the tests written in a source program
in their textual order, one can write several I/O tests that are
executed in a well-defined order.


\subsection{Generating Test Data}

CurryCheck test properties by enumerating test data and
checking a given property with these values.
Since these values are generated in a systematic way,
one can even prove a property if the number of test cases
is finite. For instance, consider the following property
from Boolean logic:
\begin{curry}
neg_or b1 b2 = not (b1 || b2) -=- not b1 && not b2
\end{curry}
This property is validated by checking it with all possible values:
%
\begin{curry}
Michael Hanus 's avatar
Michael Hanus committed
303
> curry-check -v ExampleTests
Michael Hanus 's avatar
Michael Hanus committed
304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327
...
0:
False
False
1:
False
True
2:
True
False
3:
True
True
neg_or (module ExampleTests, line 67):
 Passed 4 tests.
\end{curry}
%
However, if the test data is infinite, like lists of integers,
CurryCheck stops checking after a given limit for all tests.
As a default, the limit is 100 tests but it can be changed
by the command-line flag \ccode{-m}. For instance, to test
each property with 200 tests, CurryCheck can be invoked by
%
\begin{curry}
Michael Hanus 's avatar
Michael Hanus committed
328
> curry-check -m 200 ExampleTests
Michael Hanus 's avatar
Michael Hanus committed
329 330 331 332 333 334 335 336 337 338 339 340 341 342 343 344 345 346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396 397 398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 437 438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491
\end{curry}
%
For a given type, CurryCheck automatically enumerates all values
of this type (except for function types).
In KiCS2, this is done by exploiting the functional logic features
of Curry, i.e., by simply collecting all values of a free variable.
For instance, the library \code{Test.EasyCheck}\pindex{Test.EasyCheck}
defines an operation
\begin{curry}
valuesOf :: a -> [a]
\end{curry}
which computes the list of all values of the given argument
according to a fixed strategy (in the current implementation:
randomized level diagonalization \cite{ChristiansenFischer08FLOPS}).
For instance, we can get 20 values for a list of integers by
%
\begin{curry}
Test.EasyCheck> take 20 (valuesOf (_::[Int]))
[[],[-1],[-3],[0],[1],[-1,0],[-2],[0,0],[3],[-1,1],[-3,0],[0,1],[2],
[-1,-1],[-5],[0,-1],[5],[-1,2],[-9],[0,2]]
\end{curry}
%
Since the features of PAKCS for search space exploration are more limited,
PAKCS uses in CurryCheck explicit generators for search tree structures
which are defined in the module \code{SearchTreeGenerators}.
For instance, the operations
%
\begin{curry}
genInt :: SearchTree Int$\listline$
genList :: SearchTree a -> SearchTree [a]
\end{curry}
generates (infinite) trees of integer and lists values.
To extract all values in a search tree, the library \code{Test.EasyCheck}
also defines an operation
\begin{curry}
valuesOfSearchTree :: SearchTree a -> [a]
\end{curry}
so that we obtain 20 values for a list of integers in PAKCS by
%
\begin{curry}
...> take 20 (valuesOfSearchTree (genList genInt))
[[],[1],[1,1],[1,-1],[2],[6],[3],[5],[0],[0,1],[0,0],[-1],[-1,0],[-2],
[-3],[1,5],[1,0],[2,-1],[4],[3,-1]]
\end{curry}
%
Apart from the different implementations,
CurryCheck can test properties on predefined types, as already shown,
as well as on user-defined types.
For instance, we can define our own Peano representation of
natural numbers with an addition operation and two properties as follows:
%
\begin{curry}
data Nat = Z | S Nat$\listline$
add :: Nat -> Nat -> Nat
add Z     n = n
add (S m) n = S(add m n)$\listline$
addIsCommutative x y = add x y -=- add y x$\listline$
addIsAssociative x y z = add (add x y) z -=- add x (add y z)
\end{curry}
%
Properties can also be defined for polymorphic types.
For instance, we can define general polymorphic trees,
operations to compute the leaves of a tree and mirroring a tree
as follows:
\begin{curry}
data Tree a = Leaf a | Node [Tree a]$\listline$
leaves (Leaf x) = [x]
leaves (Node ts) = concatMap leaves ts$\listline$
mirror (Leaf x) = Leaf x
mirror (Node ts) = Node (reverse (map mirror ts))
\end{curry}
Then we can state and check two properties on mirroring:
\begin{curry}
doubleMirror t = mirror (mirror t) -=- t$\listline$
leavesOfMirrorAreReversed t = leaves t -=- reverse (leaves (mirror t))
\end{curry}
%
In some cases, it might be desirable to define own test data
since the generated structures are not appropriate for testing
(e.g., balanced trees to check algorithms that require work
on balanced trees).
Of course, one could drop undesired values by an explicit condition.
For instance, consider the following operation that adds all numbers
from 0 to a given limit:
%
\begin{curry}
sumUp n = if n==0 then 0 else n + sumUp (n-1)
\end{curry}
%
Since there is also a simple formula to compute this sum,
we can check it:
%
\begin{curry}
sumUpIsCorrect n = n>=0 ==> sumUp n -=- n * (n+1) `div` 2
\end{curry}
Note that the condition is important since \code{sumUp}
diverges on negative numbers.
CurryCheck tests this property by enumerating integers,
i.e., also many negative numbers which are dropped for the tests.
In order to generate only valid test data, we define
our own generator for a search tree containing only valid data:
%
\begin{curry}
genInt = genCons0 0 ||| genCons1 (+1) genInt
\end{curry}
%
The combinator \code{genCons0} constructs a search tree
containing only this value, whereas \code{genCons1}
constructs from a given search tree a new tree where the function
given in the first argument is applied to all values.
Similarly, there are also combinators \code{genCons2},
\code{genCons3} etc.\ for more than one argument.
The combinator \ccode{|||} combines two search trees.

If the Curry program containing properties defines a generator
operation with the name \code{gen$\tau$},
then CurryCheck uses this generator to test properties
with argument type $\tau$.
Hence, if we put the definition of \code{genInt}
in the Curry program where \code{sumUpIsCorrect} is defined,
the values to check this property are only non-negative integers.
Since these integers are slowly increasing, i.e., the search tree
is actually degenerated to a list, we can also use
the following definition to obtain a more balanced search tree:
%
\begin{curry}
genInt = genCons0 0 ||| genCons1 (\n -> 2*(n+1)) genInt
                    ||| genCons1 (\n -> 2*n+1)   genInt
\end{curry}
The library \code{SearchTree} defines the structure of search trees
as well as operations on search trees, like limiting the depth
of a search tree (\code{limitSearchTree}) or showing a search tree
(\code{showSearchTree}). For instance, to structure
of the generated search tree up to some depth
can be visualized as follows:
\begin{curry}
...SearchTree> putStr (showSearchTree (limitSearchTree 6 genInt))
\end{curry}
%
If we want to use our own generator only for specific properties,
we can do so by introducing a new data type and defining a generator
for this data type.
For instance, to test only the operation \code{sumUpIsCorrect} with non-negative
integers, we do not define a generator \code{genInt} as above,
but define a wrapper type for non-negative integers and
a generator for this type:
%
\begin{curry}
data NonNeg = NonNeg { nonNeg :: Int }$\listline$
genNonNeg = genCons1 NonNeg genNN
 where
   genNN = genCons0 0 ||| genCons1 (\n -> 2*(n+1)) genNN
                      ||| genCons1 (\n -> 2*n+1)   genNN
\end{curry}
Now we can either redefine \code{sumUpIsCorrect} on this type
\begin{curry}
sumUpIsCorrectOnNonNeg (NonNeg n) = sumUp n -=- n * (n+1) `div` 2
\end{curry}
or we simply reuse the old definition by
\begin{curry}
sumUpIsCorrectOnNonNeg = sumUpIsCorrect . nonNeg
\end{curry}

492 493
\subsection{Checking Equivalence of Operations}

494
CurryCheck supports also equivalence tests for operations.
495 496
Two operations are considered as \emph{equivalent} if they
can be replaced by each other in any possible context
497 498 499
without changing the computed values (this is also called
\emph{contextual equivalence} and precisely defined in
\cite{AntoyHanus12PADL} for functional logic programs).
500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519
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}
520
The left and right argument of this combinator must be a defined operation
521 522 523 524 525 526
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.
527
The details are described in \cite{AntoyHanus18FLOPS}.
528

529
It should be noted that CurryCheck can test
530 531 532 533 534 535 536 537 538 539 540 541 542
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}
543 544
This is done by iteratively guessing depth-bounds, computing both operations
up to these depth-bounds, and comparing the computed results.
545 546 547 548
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},
549 550 551
CurryCheck assumes that the operations to be tested are terminating,
i.e., they always yields a result when applied to ground terms.
In this case, CurryCheck does not iterate over depth-bounds
552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569
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}
570
We can test the equivalence of both operations by
571 572 573 574 575 576 577 578 579 580 581 582 583 584
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.

585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616
Instead of annotating the property name to use more efficient equivalence
tests for terminating operations, one can also ask CurryCheck
to analyze the operations in order to safely approximate
termination or productivity properties.
For this purpose, one can call CurryCheck with the option
\ccode{--equivalence=$equiv$} or \ccode{-e$equiv$}.
The parameter $equiv$ determines the mode for equivalence checking
which must have one of the following values (or a prefix of them):
%
\begin{description}
\item[\code{manual}:]
This is the default mode. In this mode, all equivalence tests
are executed with first technique described above, unless
the name of the test has the suffix \code{'TERMINATE}.
\item[\code{autoselect}:]
This mode automatically selects the improved transformation
for terminating operations by a program analysis, i.e.,
if it can be proved that both operations are terminating, then
the equivalence test for terminating operations is used.
It is also used when the name of the test has the suffix \code{'TERMINATE}.
\item[\code{safe}:]
This mode analyzes the productivity behavior of operations.
If it can be proved that both operations are terminating
or the test name has the suffix \code{'TERMINATE}, then
the more efficient equivalence test for terminating operations is used.
If it can be proved that both operations are productive
or the test name has the suffix \code{'PRODUCTIVE}, then
the first general test technique is used.
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).
617 618 619 620 621 622 623 624 625 626 627 628 629 630
\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.
631
\end{description}
632

633

634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679
\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]
680
sort'spec xs | sorted ys = ys  where ys = perm xs
681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700

-- 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
Michael Hanus 's avatar
Michael Hanus committed
701
sortSatisfiesPostCondition x = always (sort'post x (sort x))
702 703 704 705 706 707

sortSatisfiesSpecification :: Prop
sortSatisfiesSpecification = sort <=> sort'spec
\end{curry}


708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747
\subsection{Combining Testing and Verification}

Usually, CurryCheck tests all user-defined properties as well as
postconditions or specifications,
as described in Section~\ref{sec:currycheck:contracts}.
If a programmer uses some other tool to verify such properties,
it is not necessary to check such properties with test data.
In order to advice CurryCheck to do so,
it is sufficient to store the proofs in specific files.
Since the proof might be constructed by some tool
unknown to CurryCheck or even manually,
CurryCheck does not check the proof file but trusts the programmer
and uses a naming convention for files containing proofs.
If there is a property \code{p} in a module \code{M}
for which a proof in file \code{proof-M-p.*}
(the name is case independent), then
CurryCheck assumes that this file contains
a valid proof for this property.
For instance, the following property states that
sorting a list does not change its length:
%
\begin{curry}
sortlength xs = length (sort xs) <~> length xs
\end{curry}
%
If this property is contained in module \code{Sort} and
there is a file \code{proof-Sort-sortlength.txt}
containing a proof for this property,
CurryCheck considers this property as valid and does not check it.
Moreover, it uses this information to simplify other properties to be tested.
For instance, consider the property \code{sortSatisfiesPostCondition}
of Section~\ref{sec:currycheck:contracts}.
This can be simplified to
\code{always$\;$True} so that it does not need to be tested.

One can also provide proofs for generated properties,
e.g., determinism, postconditions, specifications,
so that they are not tested:
\begin{itemize}
\item
748
If there is a proof file \code{proof-$M$-$f$-IsDeterministic.*},
749 750
a determinism annotation for operation $M.f$ is not tested.
\item
751
If there is a proof file \code{proof-$M$-$f$-SatisfiesPostCondition.*},
752 753
a postcondition for operation $M.f$ is not tested.
\item
754
If there is a proof file \code{proof-$M$-$f$-SatisfiesSpecification.*},
755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772
a specification for operation $M.f$ is not tested.
\end{itemize}
Note that the file suffix and all non-alpha-numberic characters
in the name of the proof file are ignored.
Furthermore, the name is case independent
This should provide enough flexibility when other verification tools
require specific naming conventions.
For instance, a proof for the property \code{Sort.sortlengh}
could be stored in the following files in order to be considered
by CurryCheck:
\begin{curry}
proof-Sort-sortlength.tex
PROOF_Sort_sortlength.agda
Proof-Sort_sortlength.smt
ProofSortSortlength.smt
\end{curry}


Michael Hanus 's avatar
Michael Hanus committed
773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791
\subsection{Checking Usage of Specific Operations}

In addition to testing dynamic properties of programs,
CurryCheck also examines the source code of the given
program for unintended uses of specific operations
(these checks can be omitted via the option \ccode{--nosource}).
Currently, the following source code checks are performed:

\begin{itemize}
\item
The prelude operation \ccode{=:<=} is used to implement
functional patterns \cite{AntoyHanus05LOPSTR}. It should not be
used in source programs to avoid unintended uses.
Hence, CurryCheck reports such unintended uses.
\item
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
792
(via operations defined in the library \code{SetFunctions})
Michael Hanus 's avatar
Michael Hanus committed
793 794 795 796 797 798 799 800 801 802 803
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).
However, it is not intended to apply the operator \ccode{set$n$}
to lambda abstractions, locally defined operations
or operations with an arity different from $n$.
Hence, CurryCheck reports such unintended uses of set functions.
\end{itemize}


% LocalWords: CurryCheck
804 805 806 807 808

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "main"
%%% End: