blob: e42a3e3a78464d4d57906785df8dcec3104fee20 (
plain)
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
125
126
127
128
129
130
131
132
133
|
(.using
[library
[lux "*"
["_" test {"+" Test}]
[abstract
[hash {"+" Hash}]
[monad {"+" do}]
[\\specification
["$[0]" equivalence]
["$[0]" hash]
["$[0]" monoid]]]
[data
["[0]" bit ("[1]#[0]" equivalence)]
[collection
["[0]" list]]]
[math
["[0]" random {"+" Random}]
[number
["n" nat]]]]]
[\\library
["[0]" / ("#[0]" equivalence)]])
(def: gen_nat
(Random Nat)
(# random.monad each (n.% 100)
random.nat))
(def: .public test
Test
(<| (_.covering /._)
(_.for [/.Set])
(do [! random.monad]
[size ..gen_nat]
(all _.and
(_.for [/.equivalence]
($equivalence.spec /.equivalence (random.set n.hash size random.nat)))
(_.for [/.hash]
(|> random.nat
(# random.monad each (|>> list (/.of_list n.hash)))
($hash.spec /.hash)))
(_.for [/.monoid]
($monoid.spec /.equivalence (/.monoid n.hash) (random.set n.hash size random.nat)))
(do !
[sizeL ..gen_nat
sizeR ..gen_nat
setL (random.set n.hash sizeL random.nat)
setR (random.set n.hash sizeR random.nat)
non_memberL (random.only (|>> (/.member? setL) not)
random.nat)]
(all _.and
(_.coverage [/.empty]
(/.empty? (/.empty n.hash)))
(do !
[hash (# ! each (function (_ constant)
(is (Hash Nat)
(implementation
(def: equivalence n.equivalence)
(def: (hash _)
constant))))
random.nat)]
(_.coverage [/.member_hash]
(same? hash (/.member_hash (/.empty hash)))))
(_.coverage [/.size]
(n.= sizeL (/.size setL)))
(_.coverage [/.empty?]
(bit#= (/.empty? setL)
(n.= 0 (/.size setL))))
(_.coverage [/.list /.of_list]
(|> setL /.list (/.of_list n.hash) (#= setL)))
(_.coverage [/.member?]
(and (list.every? (/.member? setL) (/.list setL))
(not (/.member? setL non_memberL))))
(_.coverage [/.has]
(let [before_addition!
(not (/.member? setL non_memberL))
after_addition!
(/.member? (/.has non_memberL setL) non_memberL)
size_increase!
(n.= (++ (/.size setL))
(/.size (/.has non_memberL setL)))]
(and before_addition!
after_addition!)))
(_.coverage [/.lacks]
(let [symmetry!
(|> setL
(/.has non_memberL)
(/.lacks non_memberL)
(#= setL))
idempotency!
(|> setL
(/.lacks non_memberL)
(#= setL))]
(and symmetry!
idempotency!)))
(_.coverage [/.union /.sub?]
(let [setLR (/.union setL setR)
sets_are_subs_of_their_unions!
(and (/.sub? setLR setL)
(/.sub? setLR setR))
union_with_empty_set!
(|> setL
(/.union (/.empty n.hash))
(#= setL))]
(and sets_are_subs_of_their_unions!
union_with_empty_set!)))
(_.coverage [/.intersection /.super?]
(let [setLR (/.intersection setL setR)
sets_are_supers_of_their_intersections!
(and (/.super? setLR setL)
(/.super? setLR setR))
intersection_with_empty_set!
(|> setL
(/.intersection (/.empty n.hash))
/.empty?)]
(and sets_are_supers_of_their_intersections!
intersection_with_empty_set!)))
(_.coverage [/.difference]
(let [setL+R (/.union setR setL)
setL_R (/.difference setR setL+R)]
(and (list.every? (/.member? setL+R) (/.list setR))
(not (list.any? (/.member? setL_R) (/.list setR))))))
(_.coverage [/.predicate]
(list.every? (/.predicate setL) (/.list setL)))
))))))
|
