Mercurial > 12ws.info2

comparison exercises/src/SetPairList.hs @ 26:ce9610f08925

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Merge
author Markus Kaiser <markus.kaiser@in.tum.de>
date Wed, 09 Jan 2013 19:45:47 +0100
parents 34fea195e238 ea3fba2381bc
children
comparison
equal deleted inserted replaced
24:34fea195e238 26:ce9610f08925
1 -- ? 1 module SetPairList(Set, empty, insert, isin, size, union, delete) where
2 2
3 -- Abstraction function 3 -- Abstraction function
4 {- 4 {-
5 alpha (S x) = undefined 5 alpha :: Set a -> {a}
6 alpha (S []) = {}
7 alpha (S ((a, b):xs)) = {a..b} union (alpha xs)
6 8
7 To show: (10 things) 9 To show: (10 things)
10 alpha empty = {}
11 invar s ==> alpha (insert x s) = {x} union alpha s
12 invar s ==> alpha (delete x s) = alpha s \ {x}
13 invar s ==> isin x s = x \in alpha s
14 invar s ==> size s = |alpha s|
15 invar s1, invar s2 ==> alpha (union s1 s2) = (alpha s1) union (alpha s2)
16
17 invar empty
18 invar s ==> invar (insert x s)
19 invar s ==> invar(delete x s)
20 invar s1, invar s2 ==> invar (union s1 s2)
8 -} 21 -}
9 22
10 -- Interface 23 -- Interface
11 newtype Set a = S (...) 24 newtype Set a = S (PairList a)
12 25
13 invar :: Integral a => Set a -> Bool 26 invar :: Integral a => Set a -> Bool
14 invar (S s) = undefined 27 invar (S s) = invarPL s
15 28
16 empty :: Set a 29 empty :: Set a
17 empty = undefined 30 empty = S emptyPL
18 31
19 insert :: Integral a => a -> Set a -> Set a 32 insert :: Integral a => a -> Set a -> Set a
20 insert n (S s) = undefined 33 insert n (S s) = S (insertPL n s)
21 34
22 isin :: Integral a => a -> Set a -> Bool 35 isin :: Integral a => a -> Set a -> Bool
23 isin n (S s) = undefined 36 isin n (S s) = isinPL n s
24 37
25 size :: Integral a => Set a -> Integer 38 size :: Integral a => Set a -> Integer
26 size (S s) = undefined 39 size (S s) = sizePL s
27 40
28 union :: Integral a => Set a -> Set a -> Set a 41 union :: Integral a => Set a -> Set a -> Set a
29 union (S s1) (S s2) = undefined 42 union (S s1) (S s2) = S (unionPL s1 s2)
30 43
31 delete :: Integral a => a -> Set a -> Set a 44 delete :: Integral a => a -> Set a -> Set a
32 delete n (S s) = undefined 45 delete n (S s) = S (deletePL n s)
33 46
34 -- Implementation 47 -- Implementation
35 type PairList a = [(a, a)] 48 type PairList a = [(a, a)]
36 49
37 invarPL :: Integral a => PairList a -> Bool 50 invarPL :: Integral a => PairList a -> Bool