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
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
|
module StdSetTest
/* Test module StdSet
Voor werken met Gast:
(*) gebruik Environment 'Gast'
(*) zet Project Options op 'Basic Values Only' en '8M' Maximum Heap Size.
*/
import gast
import GenLexOrd
import StdSet
Start = testn 2000
(\n` n2` m -> let n = cast [A,B,C] n`
n2 = cast [A,B,C] n2`
in
membership m n /\
conversion_invariant n /\
length_property n /\
subset_property n n2 /\
strictsubset_property n n2 /\
empty_properties m n /\
disjoint_properties n n2 /\
product_properties n n2 /\
intersect_properties n n2 /\
setminus_properties n n2 /\
union_properties n n2 /\
powset_properties n /\
True
)
:: Enum = A | B | C
derive bimap []
derive ggen Enum
derive genShow Enum
derive gEq Enum
derive gLexOrd Enum
instance == Enum where (==) x y = gEq{|*|} x y
instance < Enum where (<) x y = gEq{|*|} (gLexOrd{|*|} x y) LT
// clean should have something like this!
cast :: a a -> a
cast _ x = x
membership :: Enum [Enum] -> Property
membership x xs
= name "membership"
( memberOfSet x s <==> isMember x xs )
where s = toSet xs
conversion_invariant :: [Enum] -> Property
conversion_invariant xs
= name "conversion_invariant"
( toSet (fromSet xs`) == xs` )
where xs` = toSet xs
length_property :: [Enum] -> Property
length_property xs
= name "length_property"
( nrOfElements s == length (removeDup xs) )
where s = toSet xs
subset_property :: [Enum] [Enum] -> Property
subset_property xs ys
= name "subset_property"
( (isSubset u v) <==> all (flip isMember ys) xs)
where (u,v) = (toSet xs, toSet ys)
strictsubset_property :: [Enum] [Enum] -> Property
strictsubset_property xs ys
= name "strictsubset_property"
( (isStrictSubset u v) <==> (all (flip isMember ys) xs && not (all (flip isMember xs) ys)) )
where (u,v) = (toSet xs, toSet ys)
// everything you alwys wanted to know about the empty set...
// ... but were afraid to ask
empty_properties :: Enum [Enum] -> Property
empty_properties x xs
= name "empty_properties"
( isEmptySet (cast dummy zero) /\ isEmptySet (toSet (cast [A] [])) /\
((nrOfElements s == 0) <==> isEmptySet s) /\
((zero == s) <==> isEmptySet s) )
where s = toSet xs
dummy :: Set Enum
dummy = undef
product_properties :: [Enum] [Enum] -> Property
product_properties xs ys
= name "product_properties"
( product u v == toSet [(x,y) \\ x<-xs, y<-ys ] )
where (u,v) = (toSet xs, toSet ys)
powset_properties :: [Enum] -> Property
powset_properties xs
= name "powset_properties"
( powerSet s == toSet (map toSet (subs xs)) )
where s = toSet xs
subs [] = [[]]
subs [x:xs] = subs xs ++ [ [x:xs`] \\ xs` <- subs xs ]
union_properties :: [Enum] [Enum] -> Property
union_properties xs ys
= name "union_properties"
( union u v == toSet (xs++ys) )
where (u,v) = (toSet xs, toSet ys)
intersect_properties :: [Enum] [Enum] -> Property
intersect_properties xs ys
= name "intersect_properties"
( intersection u v == toSet [ x \\ x<-xs | isMember x ys ] )
where (u,v) = (toSet xs, toSet ys)
setminus_properties :: [Enum] [Enum] -> Property
setminus_properties xs ys
= name "setminus_properties"
( without u v == toSet [ x \\ x<-xs | not (isMember x ys) ])
where (u,v) = (toSet xs, toSet ys)
disjoint_properties :: [Enum] [Enum] -> Property
disjoint_properties xs ys
= name "disjoint_properties"
( isDisjoint u v <==> (nrOfElements u + nrOfElements v == nrOfElements (union u v)) )
where (u,v) = (toSet xs, toSet ys)
|
