manual.tex 29.4 KB
 Michael Hanus committed Dec 14, 2018 1 \section{CurryCheck: A Tool for Testing Properties of Curry Programs}  Michael Hanus committed Mar 27, 2017 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 committed Dec 14, 2018 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 committed Mar 27, 2017 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 committed Jan 02, 2019 52 \code{Test.EasyCheck}\pindex{Test.EasyCheck} (see package \code{easycheck})  Michael Hanus committed Mar 27, 2017 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 committed Dec 14, 2018 87 > curry-check Rev  Michael Hanus committed Mar 27, 2017 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 committed Dec 14, 2018 110 The command \code{curry-check} has some options to influence  Michael Hanus committed Mar 27, 2017 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 committed Dec 14, 2018 115 Moreover, the return code of \code{curry-check} is \code{0}  Michael Hanus committed Mar 27, 2017 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 committed Dec 14, 2018 236 psort :: [Int] -> [Int]  Michael Hanus committed Mar 27, 2017 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) \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 committed Dec 14, 2018 260 > curry-check ExampleTests  Michael Hanus committed Mar 27, 2017 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 committed Dec 14, 2018 303 > curry-check -v ExampleTests  Michael Hanus committed Mar 27, 2017 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 committed Dec 14, 2018 328 > curry-check -m 200 ExampleTests  Michael Hanus committed Mar 27, 2017 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}  Michael Hanus committed Dec 15, 2017 492 493 \subsection{Checking Equivalence of Operations}  Michael Hanus committed Feb 11, 2018 494 CurryCheck supports also equivalence tests for operations.  Michael Hanus committed Dec 15, 2017 495 496 Two operations are considered as \emph{equivalent} if they can be replaced by each other in any possible context  Michael Hanus committed Feb 11, 2018 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).  Michael Hanus committed Dec 15, 2017 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}  Michael Hanus committed Feb 11, 2018 520 The left and right argument of this combinator must be a defined operation  Michael Hanus committed Dec 15, 2017 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.  Michael Hanus committed Feb 11, 2018 527 The details are described in \cite{AntoyHanus18FLOPS}.  Michael Hanus committed Dec 15, 2017 528   Michael Hanus committed Feb 11, 2018 529 It should be noted that CurryCheck can test  Michael Hanus committed Dec 15, 2017 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}  Michael Hanus committed Feb 11, 2018 543 544 This is done by iteratively guessing depth-bounds, computing both operations up to these depth-bounds, and comparing the computed results.  Michael Hanus committed Dec 15, 2017 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},  Michael Hanus committed Feb 09, 2018 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  Michael Hanus committed Dec 15, 2017 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}  Michael Hanus committed Feb 11, 2018 570 We can test the equivalence of both operations by  Michael Hanus committed Dec 15, 2017 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.  Michael Hanus committed Feb 11, 2018 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.  Michael Hanus committed Feb 11, 2018 631 \end{description}  Michael Hanus committed Feb 09, 2018 632   Michael Hanus committed Dec 15, 2017 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]  Michael Hanus committed Oct 30, 2018 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) \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 committed Nov 21, 2018 701 sortSatisfiesPostCondition x = always (sort'post x (sort x))  702 703 704 705 706 707  sortSatisfiesSpecification :: Prop sortSatisfiesSpecification = sort <=> sort'spec \end{curry}  Michael Hanus committed Nov 01, 2018 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  Michael Hanus committed May 08, 2019 748 If there is a proof file \code{proof-$M$-$f$-IsDeterministic.*},  Michael Hanus committed Nov 01, 2018 749 750 a determinism annotation for operation$M.f$is not tested. \item  Michael Hanus committed May 08, 2019 751 If there is a proof file \code{proof-$M$-$f$-SatisfiesPostCondition.*},  Michael Hanus committed Nov 01, 2018 752 753 a postcondition for operation$M.f$is not tested. \item  Michael Hanus committed May 08, 2019 754 If there is a proof file \code{proof-$M$-$f$-SatisfiesSpecification.*},  Michael Hanus committed Nov 01, 2018 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 committed Mar 27, 2017 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  Michael Hanus committed Dec 15, 2017 792 (via operations defined in the library \code{SetFunctions})  Michael Hanus committed Mar 27, 2017 793 794 795 796 797 798 799 800 801 802 803 by the application \ccode{set$nf$} (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  Michael Hanus committed Dec 15, 2017 804 805 806 807 808  %%% Local Variables: %%% mode: latex %%% TeX-master: "main" %%% End: