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
|
{-# OPTIONS_CYMAKE -F --pgmF=currypp #-}
{-# OPTIONS_CYMAKE -Wnone #-}
-- Example for using integrated code, default rules, and contracts in one
-- module
import Format
import Test.Prop
showInt i = ``format "%+.3d",i''
-- Bubble sort formulation with default rule as deterministic operation:
sort :: [a] ->DET [a]
sort (xs++[x,y]++ys) | x>y = sort (xs++[y,x]++ys)
sort'default xs = xs
-- Precondition: we don't like to sort empty lists...
sort'pre xs = length xs > 0
-- Postcondition: input and output lists should have the same length
sort'post xs ys = length xs == length ys
sort7 = sort (map showInt [7,1,6,3,5,4,2]) -=- map (\d -> "+00"++show d) [1..7]
sortEmpty = toError (sort [])
|
