SortSpec.curry 904 Bytes
Newer Older
 Michael Hanus committed Mar 27, 2017 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 ``````-- 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] `````` 23 24 ``````sort'spec xs | sorted ys = ys where ys = perm xs `````` Michael Hanus committed Mar 27, 2017 25 26 27 28 29 `````` -- An implementation of sort with quicksort: sort :: [Int] -> [Int] sort [] = [] sort (x:xs) = sort (filter (=x) xs)``````