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 --optF=-e #-}
-- Implementation of quicksort with partition
-- Use option "-e" for contract wrapper (see part'post below).
perm [] = []
perm (x:xs) = ndinsert (perm xs)
where ndinsert [] = [x]
ndinsert (y:ys) = (x:y:ys) ? (y:ndinsert ys)
sorted [] = success
sorted [_] = success
sorted (x:y:ys) = (x<=y)=:=True & sorted (y:ys)
-- User contract:
sort'pre _ = True
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
-- Implementation of sort with quicksort and partition:
sort :: [Int] -> [Int]
sort [] = []
sort (x:xs) = let (low,high) = part x xs in sort low ++ x : sort high
-- Contract for partition: since we put no restriction on the order
-- of the partioned elements, the result can be any permutation
-- (i.e., this is not a precise but a weak specification).
-- Consequence: the postcondition is nondeterministic if the input list
-- contains multiple values. Thus, it should be checked with option "-e".
part'pre _ _ = True
part'post x xs (u,v) | (u++v) =:= perm xs = all (<x) u && all (>=x) v
part :: Int -> [Int] -> ([Int],[Int])
part _ [] = ([],[])
part x (y:ys) = if y<x then (y:u,v) else (u,y:v)
where (u,v) = part x ys
input = [26,18,5,4,16,8,22,17]
main = sort input
|
