1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
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
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
|
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
|
