Quicksort.curry 1.24 KB
 Michael Hanus committed Mar 30, 2017 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) 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 check should produce an error: quickSortFailure = toError \$ sort [1,2,1]``````