SortSpec.curry 1.41 KB
Newer Older
Michael Hanus 's avatar
Michael Hanus committed
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
-- A specification of sorting a list and an implementation based
-- on insertion sort.
-- CurryCheck generates and checks properties which states
-- that the implementation is satisfies the specification
-- and the post-condition.
--
-- To demonstrate the use of statically proven properties,
-- we include a theorem that is used to simplify the postcondition
-- of sort.

import Test.Prop

perm []     = []
perm (x:xs) = ndinsert x (perm xs)
 where
   ndinsert x ys     = x : ys
   ndinsert x (y:ys) = y : ndinsert 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 && sorted ys

-- Specification of sort:
-- A list is a sorted result of an input if it is a permutation and sorted.
sort'spec :: [Int] -> [Int]
29 30
sort'spec xs | sorted ys = ys
 where ys = perm xs
Michael Hanus 's avatar
Michael Hanus committed
31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46

-- An implementation of sort with quicksort:
sort :: [Int] -> [Int]
sort []     = []
sort (x:xs) = insert x (sort xs)

insert :: Int -> [Int] -> [Int]
insert x [] = [x]
insert x (y:ys) = if x<=y then x : y : ys
                          else y : insert x ys

-- A theorem about the length of sorting a list.
-- If this theorem is proved (i.e., if there is a file
-- `proof-sort-preserves-length.*`),
-- it is not checked but used to simplify the postcondition sort'post.
sortPreservesLength xs = length (sort xs) <~> length xs