Commit aeef0777 authored by Michael Hanus 's avatar Michael Hanus

CurryCheck sources packaged

parents
*~
.curry
.cpm
src/CurryCheckConfig.curry
# currycheck - A Property Testing Tool for Curry
This package contains the tool `curry-check` 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.
## Installing the tool
The tool can be directly installed by the command
> cpm installbin currycheck
This installs the executable `curry-check` in the bin directory of CPM.
## Using the tool
If the bin directory of CPM (default: `~/.cpm/bin`) is in your path,
execute the tool with the module containing the properties, e.g.,
> curry-check Nats
This directory contains some documention for the CurryCheck tool:
manual.tex:
A short description to be included in the main manual of the Curry system.
This diff is collapsed.
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=defaultrules #-}
{-# OPTIONS_CYMAKE -Wnone #-}
import Test.Prop
-- We test whether our definition of zip with default rules is
-- equivalent to the standard one:
-- zip2 with default rule:
zip2 :: [a] -> [b] -> [(a,b)]
zip2 (x:xs) (y:ys) = (x,y) : zip2 xs ys
zip2'default _ _ = []
zip2_is_zip xs ys = zip2 xs ys -=- Prelude.zip xs ys
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=defaultrules #-}
--- Examples for specifying deterministic operations via
--- the DET annotation in the type.
--- CurryCheck generates and check properties which states
--- that the original operations are indeed deterministic.
-- Computes the last element of a list.
last :: [a] ->DET a
last (_ ++ [x]) = x
last'pre = not . null
-- Definition of bubble sort with default rule as a deterministic operaion.
sort :: [Int] ->DET [Int]
sort (xs++[x,y]++ys) | x>y = sort (xs++[y,x]++ys)
sort'default xs = xs
-- In order to write a test, we have to import the module Test.Prop:
import Test.Prop
-- We import the System module for performing some I/O tests on operations
-- in this module:
import System
--------------------------------------------------------------------------
-- Deterministic tests:
-- We can write simple equational tests where both sides
-- evaluate to a single value:
rev_123 = reverse [1,2,3] -=- [3,2,1]
not_True = not True -=- False
not_False = not False -=- True
-- However, we can also use EasyCheck to guess input values to check
-- parameterized properties:
not_not_is_id b = not (not b) -=- b
-- In the former test, EasyCheck makes an exhaustive test by enumerating
-- all possible Boolean values. For types, with infinitely many values,
-- this is not possible. Anyway, EasyCheck can also enumerate many values,
-- e.g., to check the commutativity property of the addition on integers:
plusComm :: Int -> Int -> Prop
plusComm x y = x + y -=- y + x
-- We can even write a polymorphic test:
rev_rev_is_id :: [a] -> Prop
rev_rev_is_id xs = reverse (reverse xs) -=- xs
-- A polymorphic test will be automatically transformed into the same
-- test specialized to values of type Ordering.
-- Nevertheless, we can still define our own specialization:
rev_rev_is_id_int :: [Int] -> Prop
rev_rev_is_id_int = rev_rev_is_id
-- Sometimes it is necessary to add a condition to the generated
-- test inputs. This can be done by the operator `==>`:
tail_length xs =
not (null xs) ==> length (tail xs) -=- length xs - 1
--------------------------------------------------------------------------
-- Of course, in Curry we also have to test Non-deterministic operations
-- like `coin`:
coin = 0 ? 1
-- We can test whether `coin` evaluates at least to some value:
coin_yields_0 = coin ~> 0
coin_yields_1 = coin ~> 1
-- If we want to check for all results of an operation, we can also
-- check the set of all results for equality:
coin_yields_0_1 = coin <~> (0?1)
-- In this way, we can check whether Curry really implements call-time choice:
double x = x+x
double_coin_yields_0_2 = double coin <~> (0?2)
-- Note that the operator `<~>` compares the set of all results of both sides.
-- Thus, duplicated elements do not count:
coin_plus_coin = coin+coin <~> (0?1?2)
-- However, if we are interested in the detailed operational semantics,
-- we could also compare the multi-sets of the values with the operator `<~~>`:
coin_plus_coin_multi = coin+coin <~~> (0?1?1?2)
-- As a more advanced example, we want to test whether the operation
-- `last` defined with a functional pattern always yields a single result.
-- This can be done by checking whether each call of `last` with
-- a non-empty list yields a single result:
last :: [a] -> a
last (_ ++ [x]) = x
last_has_single_results xs = not (null xs) ==> last xs # 1
--------------------------------------------------------------------------
-- I/O tests:
-- We can also check properties of I/O actions. In this case,
-- these I/O actions must be deterministic (otherwise, currycheck reports
-- failure) and we can specify which value we expect from the I/O action.
-- As an example, we check the setting of environment variables.
-- For this purpose, we use the following environment variable:
evar = "abc123"
-- First, we check whether setting this variable works:
set_environ = (setEnviron evar "SET" >> getEnviron evar) `returns` "SET"
-- Now we check whether unsetting works:
unset_environ = (unsetEnviron evar >> getEnviron evar) `returns` ""
-- We can also compare the results of two actions with `sameReturns`:
sameIO = return (6*7) `sameReturns` return 42
--------------------------------------------------------------------------
import Test.Prop
import SearchTreeGenerators
rev :: [a] -> [a]
rev [] = []
rev (x:xs) = rev xs ++ [x]
-- Unit tests:
revNull = rev [] -=- []
rev123 = rev [1,2,3] -=- [3,2,1]
-- Property: reversing two times is the identity:
revRevIsId xs = rev (rev xs) -=- xs
-- Non-deterministic list insertion:
insert :: a -> [a] -> [a]
insert x xs = x : xs
insert x (y:ys) = y : insert x ys
insertAsFirstOrLast :: Int -> [Int] -> Prop
insertAsFirstOrLast x xs = insert x xs ~> (x:xs ? xs++[x])
-- A permutation of a list:
perm :: [a] -> [a]
perm [] = []
perm (x:xs) = insert x (perm xs)
permLength :: [Int] -> Prop
permLength xs = length (perm xs) <~> length xs
permCount :: [Int] -> Prop
permCount xs = allDifferent xs ==> perm xs # fac (length xs)
where
fac n = foldr (*) 1 [1..n]
allDifferent [] = True
allDifferent (x:xs) = x `notElem` xs && allDifferent xs
-- Is a list sorted?
sorted :: [Int] -> Bool
sorted [] = True
sorted [_] = True
sorted (x:y:zs) = x<=y && sorted (y:zs)
permIsEventuallySorted :: [Int] -> Prop
permIsEventuallySorted xs = eventually $ sorted (perm xs)
-- Permutation sort:
psort :: [Int] -> [Int]
psort xs | sorted ys = ys
where ys = perm xs
psortIsAlwaysSorted xs = always $ sorted (psort xs)
psortKeepsLength xs = length (psort xs) <~> length xs
-- Quicksort:
qsort :: [Int] -> [Int]
qsort [] = []
qsort (x:l) = qsort (filter (<x) l) ++ x : qsort (filter (>=x) l)
qsortIsSorting xs = qsort xs <~> psort xs
--------------------------------------------------------------------------
-- Generating test data:
neg_or b1 b2 = not (b1 || b2) -=- not b1 && not b2
-- Natural numbers defined by s-terms (Z=zero, S=successor):
data Nat = Z | S Nat
-- addition on natural numbers:
add :: Nat -> Nat -> Nat
add Z n = n
add (S m) n = S(add m n)
-- Property: the addition operator is commutative
addIsCommutative x y = add x y -=- add y x
-- Property: the addition operator is associative
addIsAssociative x y z = add (add x y) z -=- add x (add y z)
-- A general tree type:
data Tree a = Leaf a | Node [Tree a]
-- The leaves of a tree:
leaves (Leaf x) = [x]
leaves (Node ts) = concatMap leaves ts
-- Mirror a tree:
mirror (Leaf x) = Leaf x
mirror (Node ts) = Node (reverse (map mirror ts))
-- Property: double mirroring is the identity
doubleMirror t = mirror (mirror t) -=- t
-- Property: the leaves of a mirrored are in reverse order
leavesOfMirrorAreReversed t = leaves t -=- reverse (leaves (mirror t))
-- Sum up all numbers:
sumUp n = if n==0 then 0 else n + sumUp (n-1)
sumUpIsCorrect n = n>=0 ==> sumUp n -=- n * (n+1) `div` 2
-- To test sumUpIsCorrect explicitly on non-ngeative integers,
-- we define a new data type to wrap integers:
data NonNeg = NonNeg { nonNeg :: Int }
-- We define our own generator for producing only non-negative integers:
genNonNeg = genCons1 NonNeg genNN
where
genNN = genCons0 0 ||| genCons1 (\n -> 2*(n+1)) genNN
||| genCons1 (\n -> 2*n+1) genNN
-- Now we write our own test:
sumUpIsCorrectOnNonNeg = sumUpIsCorrect . nonNeg
-- Some tests on floats.
import Float
import Test.Prop
-- Property: the addition operator is commutative
addIsCommutative :: Float -> Float -> Prop
addIsCommutative x y = x +. y -=- y +. x
-- Property: the addition operator is almost associative due to rounding errors
addIsAssociative :: Float -> Float -> Float -> Prop
addIsAssociative x y z = always (almostEqual ((x +. y) +. z) (x +. (y +. z)))
almostEqual :: Float -> Float -> Bool
almostEqual x y = absf (x -. y) < 0.00001
where
absf x = if x < 0 then 0.0 -. x else x
--- This module contains some specifications of operations from the List
--- module.
--- Since the preprocessor also depends on the list module,
--- we cannot write these specifications directly into the list module.
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=defaultrules #-}
import qualified List
import Test.Prop
nub :: [a] -> [a]
nub = List.nub
nub'spec :: [a] ->DET [a]
nub'spec (xs++[e]++ys++[e]++zs) = nub'spec (xs++[e]++ys++zs)
nub'spec'default xs = xs
isPrefixOf :: [a] -> [a] -> Bool
isPrefixOf = List.isPrefixOf
isPrefixOf'spec :: [a] -> [a] ->DET Bool
isPrefixOf'spec xs (xs ++ _) = True
isPrefixOf'spec'default _ _ = False
isSuffixOf :: [a] -> [a] -> Bool
isSuffixOf = List.isSuffixOf
isSuffixOf'spec :: [a] -> [a] ->DET Bool
isSuffixOf'spec xs (_ ++ xs) = True
isSuffixOf'spec'default _ _ = False
isInfixOf :: [a] -> [a] -> Bool
isInfixOf = List.isInfixOf
isInfixOf'spec :: [a] -> [a] ->DET Bool
isInfixOf'spec xs (_ ++ xs ++ _) = True
isInfixOf'spec'default _ _ = False
-- Some examples for the use of CurryCheck with user-defined data
import Test.Prop
-- Natural numbers defined by s-terms (Z=zero, S=successor):
data Nat = Z | S Nat
-- addition on natural numbers:
add :: Nat -> Nat -> Nat
add Z n = n
add (S m) n = S(add m n)
-- subtraction is defined by reversing the addition:
sub x y | add y z == x = z where z free
-- less-or-equal predicate on natural numbers:
leq Z _ = True
leq (S _) Z = False
leq (S x) (S y) = leq x y
-- Property: the addition operator is commutative
add_commutative x y = add x y -=- add y x
-- Property: the addition operator is associative
add_associative x y z = add (add x y) z -=- add x (add y z)
-- Properties: subtracting a value which was added yields the same value
sub_addl x y = sub (add x y) x -=- y
sub_addr x y = sub (add x y) y -=- x
-- Property: adding a number yields always a greater-or-equal number
leq_add x y = always $ leq x (add x y)
module Proof-last-is-deterministic where
-- Show that last is a deterministic operation.
-- The property to show is:
--
-- l == l1 ++ [x1] and l == l2 ++ [x2] implies x1 == x2
--
-- Here we show the simplified property
--
-- l1 ++ [x1] == l2 ++ [x2] implies x1 == x2
--
-- The initial property can be derived from this one by by symmetry
-- and transitivity of Boolean equality.
open import bool
open import bool-thms
open import bool-thms2
open import list
open import nat
open import eq
-- Auxiliary statements: an empty list cannot be equal to a list with
-- an element at the end:
nonemptylast : ∀ (l : 𝕃 ℕ)(x : ℕ) → =𝕃 _=ℕ_ [] (l ++ [ x ]) ≡ ff
nonemptylast [] x = refl
nonemptylast (z :: l) x = refl
nonemptylastr : ∀ (l : 𝕃 ℕ)(x : ℕ) → =𝕃 _=ℕ_ (l ++ [ x ]) [] ≡ ff
nonemptylastr [] x = refl
nonemptylastr (z :: l) x = refl
-- Main property formulated as Boolean implication:
lasteqp : ∀ (l1 l2 : 𝕃 ℕ)(x1 x2 : ℕ)
→ (=𝕃 _=ℕ_ (l1 ++ [ x1 ]) (l2 ++ [ x2 ])) imp (x1 =ℕ x2) ≡ tt
lasteqp [] [] x1 x2 rewrite &&-tt (x1 =ℕ x2) | imp-same (x1 =ℕ x2) = refl
lasteqp [] (x :: l2) x1 x2
rewrite nonemptylast l2 x2 | &&-ff (x1 =ℕ x) = refl
lasteqp (x :: l1) [] x1 x2
rewrite nonemptylastr l1 x1 | &&-ff (x =ℕ x2) = refl
lasteqp (z1 :: l1) (z2 :: l2) x1 x2 with (z1 =ℕ z2)
lasteqp (z1 :: l1) (z2 :: l2) x1 x2 | tt
rewrite lasteqp l1 l2 x1 x2 = refl
lasteqp (z1 :: l1) (z2 :: l2) x1 x2 | ff = refl
-- Main property formulated as propositional implication:
lasteq : ∀ (l1 l2 : 𝕃 ℕ)(x1 x2 : ℕ)
→ =𝕃 _=ℕ_ (l1 ++ [ x1 ]) (l2 ++ [ x2 ]) ≡ tt
→ x1 =ℕ x2 ≡ tt
lasteq l1 l2 x1 x2 p = imp-mp (lasteqp l1 l2 x1 x2) p
--------------------------------------------------------------------------
-- Some tests from Sebastian's tutorial on EasyCheck.
-- In order to write a test, we have to import the module Test.Prop:
import Test.Prop
--------------------------------------------------------------------------
-- Deterministic tests:
appendIsAssociative xs ys zs = (xs ++ ys) ++ zs -=- xs ++ (ys ++ zs)
reverseLeavesSingletonUntouched x = reverse [x] -=- [x]
reverseOfNonemptyIsNotNull x xs = reverse (x:xs) `is` (not . null)
reverseAntiDistributesOverAppend xs ys
= reverse (xs++ys) -=- reverse ys ++ reverse xs
-- Testing non-deterministic operations:
insert :: a -> [a] -> [a]
insert x xs = x : xs
insert x (y:ys) = y : insert x ys
insertIsNeverNull :: Int -> [Int] -> Prop
insertIsNeverNull x xs = insert x xs `isAlways` (not . null)
insertInsertsAsHead :: Int -> [Int] -> Prop
insertInsertsAsHead x xs = insert x xs ~> x:xs
--------------------------------------------------------------------------
-- A specification of sorting a list and an implementation based
-- on the quicksort algorithm.
-- CurryCheck generates and checks properties which states
-- that the implementation is satisfies the specification
-- and the post-condition.
perm [] = []
perm (x:xs) = insert x (perm xs)
where
insert x ys = x : ys
insert x (y:ys) = y : insert x ys
sorted [] = True
sorted [_] = True
sorted (x:y:ys) | x<=y && sorted (y:ys) = True
-- Postcondition: input and output lists should have the same length
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
-- An implementation of sort with quicksort:
sort :: [Int] -> [Int]
sort [] = []
sort (x:xs) = sort (filter (<x) xs) ++ [x] ++ sort (filter (>=x) xs)
-- Add numbers and define a specific generator for non-negative integers
import SearchTreeGenerators
import Test.Prop
sumUp n = if n==0 then 0 else n + sumUp (n-1)
sumUpIsCorrect n = n>=0 ==> sumUp n -=- n * (n+1) `div` 2
sumUpIsCorrectL n = label "MH" $ n>=0 ==> sumUp n -=- n * (n+1) `div` 2
sumUpIsCorrectC n = classify (n>9) "NODIGIT" $ n>=0 ==> sumUp n -=- n * (n+1) `div` 2
sumUpIsCorrectC2 n = classify (n>20) ">20" $ classify (n>9) "NODIGIT" $ n>=0 ==> sumUp n -=- n * (n+1) `div` 2
--genInt = genCons0 0 ||| genCons1 (\n -> 2*(n+1)) genInt
-- ||| genCons1 (\n -> 2*n+1) genInt
multIsCommutative x y = classify (x<0 || y<0) "Negative" $ x*y -=- y*x
--addIsCommutative x y = collectAs "ARG" (x,y) $ x*y -=- y*x
-- Some examples for the use of CurryCheck with user-defined data
import Test.Prop
-- A general tree type:
data Tree a = Leaf a | Node [Tree a]
leaves (Leaf x) = [x]
leaves (Node ts) = concatMap leaves ts
mirror (Leaf x) = Leaf x
mirror (Node ts) = Node (reverse (map mirror ts))
-- Property: double mirroring is the identity
mirror_mirror t = mirror (mirror t) -=- t
-- Property: the leaves of a mirrored are in reverse order
leaves_mirror t = leaves t -=- reverse (leaves (mirror t))
---------------------------------------------------------------------------
-- Here are some examples for problems to be detected by CurryCheck
---------------------------------------------------------------------------
import SetFunctions
---------------------------------------------------------------------------
-- Detection of unintended uses of set functions and functional pattern unif.
test1 x | 3 =:<= x = True -- not allowed!
test2 = set2 (++) [] [42] -- ok
test3 = set0 ([]++[42]) -- illegal!
test4 = set0 failed -- ok
test5 = set1 (\x->x) (1?2) -- unintended!
test6 x = set1 f x -- not allowed since f is not a top-level function
where f y = y
test7 xs = set1 (++) xs -- not allowed since (++) has arity 2
---------------------------------------------------------------------------
-- Examples for intended and unintended uses of Prelude.DET type synonym:
-- Ok (but superfluous):
detok :: Bool -> Bool ->DET Bool
detok x _ = x
deterr1 :: DET Bool -> Bool
deterr1 x = x
deterr2 :: Bool -> [DET Bool]
deterr2 x = [x]
deterr3 :: Bool -> Bool
deterr3 x = f x
where
f :: Bool -> DET Bool
f x = x
---------------------------------------------------------------------------
-- Examples for unintended uses of contracts:
some'pre _ = True
some'post _ _ = True
some'spec x = x
k'spec x = x
k x _ = x
inc :: Int -> Int
inc n = n + 1
-- Illegal contract types:
inc'pre x = x
inc'post x y = x+y
---------------------------------------------------------------------------
--- This module contains some contracts for list operations.
import Test.Prop
-- The well-known list concatenation. We give it another name,
-- otherwise we cannot specify contracts for it.
append :: [a] -> [a] -> [a]
append xs ys = xs ++ ys
-- Postcondition: append add length of input lists.
append'post xs ys zs = length xs + length ys == length zs
-- We formulate the postcondition as a property:
appendAddLengths xs ys = length xs + length ys -=- length (append xs ys)
-- Agda program using the Iowa Agda library
open import bool
module PROOF-appendAddLengths
(Choice : Set)
(choose : Choice → 𝔹)
(lchoice : Choice → Choice)
(rchoice : Choice → Choice)
where
open import eq
open import nat
open import list
open import maybe
---------------------------------------------------------------------------
-- Translated Curry operations:
++ : {a : Set} → 𝕃 a → 𝕃 a → 𝕃 a
++ [] x = x
++ (y :: z) u = y :: (++ z u)
append : {a : Set} → 𝕃 a → 𝕃 a → 𝕃 a
append x y = ++ x y
---------------------------------------------------------------------------
appendAddLengths : {a : Set} → (x : 𝕃 a) → (y : 𝕃 a)
→ ((length x) + (length y)) ≡ (length (append x y))
appendAddLengths [] y = refl
appendAddLengths (x :: xs) y rewrite appendAddLengths xs y = refl
---------------------------------------------------------------------------
-- Agda program using the Iowa Agda library
open import bool