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
|
{-# OPTIONS_CYMAKE -F --pgmF=currypp --optF=contracts #-}
{-# OPTIONS_CYMAKE -Wnone #-}
import Test.Prop
-- A specification of sorting a list and an implementation based
-- on the quicksort algorithm
perm [] = []
perm (x:xs) = insert (perm xs)
where insert ys = x:ys
insert (y:ys) = y : insert ys
sorted [] = True
sorted [_] = True
sorted (x:y:ys) = x<=y && sorted (y:ys)
-- Trivial precondition, just for testing
sort'pre xs = length xs >= 0
-- 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 x | y =:= perm x & sorted y = y where y free
-- A buggy implementation of quicksort:
sort :: [Int] -> [Int]
sort [] = []
sort (x:xs) = sort (filter (<x) xs) ++ [x] ++ sort (filter (>x) xs)
input = [26,18,5,4,16,8,22,17]
-- Buggy implementation ok for different elements:
quickSortCorrect xs = allDifferent xs ==> always (sorted (sort xs))
where
allDifferent [] = True
allDifferent (x:xs) = x `notElem` xs && allDifferent xs
-- In this example, the contract checks should produce an error:
quickSortFailure = toError $ sort [1,2,1]
|
