blob: 117617468f023a87687daf3067b3f012979cb117 (
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
|
(.module:
[library
[lux "*"
["_" test {"+" [Test]}]
[abstract
[monad {"+" [do]}]
[\\specification
["$[0]" equivalence]
["$[0]" functor {"+" [Injection]}]]]
[data
["[0]" bit ("[1]\[0]" equivalence)]
[collection
["[0]" set]
["[0]" list ("[1]\[0]" monoid)]]]
[math
["[0]" random]
[number
["n" nat]]]]]
[\\library
["[0]" /]])
(def: injection
(Injection /.Queue)
(|>> list /.of_list))
(def: .public test
Test
(<| (_.covering /._)
(_.for [/.Queue])
(do [! random.monad]
[size (\ ! each (n.% 100) random.nat)
members (random.set n.hash size random.nat)
non_member (random.only (|>> (set.member? members) not)
random.nat)
.let [members (set.list members)
sample (/.of_list members)]]
($_ _.and
(_.for [/.equivalence]
($equivalence.spec (/.equivalence n.equivalence) (random.queue size random.nat)))
(_.for [/.functor]
($functor.spec ..injection /.equivalence /.functor))
(_.cover [/.of_list /.list]
(|> members /.of_list /.list
(\ (list.equivalence n.equivalence) = members)))
(_.cover [/.size]
(n.= size (/.size sample)))
(_.cover [/.empty?]
(bit\= (n.= 0 size) (/.empty? sample)))
(_.cover [/.empty]
(let [empty_is_empty!
(/.empty? /.empty)
all_empty_queues_look_the_same!
(bit\= (/.empty? sample)
(\ (/.equivalence n.equivalence) =
sample
/.empty))]
(and empty_is_empty!
all_empty_queues_look_the_same!)))
(_.cover [/.front]
(case [members (/.front sample)]
[(#.Item head tail) (#.Some first)]
(n.= head first)
[#.End #.None]
true
_
false))
(_.cover [/.member?]
(let [every_member_is_identified!
(list.every? (/.member? n.equivalence sample)
(/.list sample))
non_member_is_not_identified!
(not (/.member? n.equivalence sample non_member))]
(and every_member_is_identified!
non_member_is_not_identified!)))
(_.cover [/.end]
(let [pushed (/.end non_member sample)
size_increases!
(n.= (++ (/.size sample)) (/.size pushed))
new_member_is_identified!
(/.member? n.equivalence pushed non_member)
has_expected_order!
(\ (list.equivalence n.equivalence) =
(list\composite (/.list sample) (list non_member))
(/.list pushed))]
(and size_increases!
new_member_is_identified!
has_expected_order!)))
(_.cover [/.next]
(case members
(#.Item target expected)
(let [popped (/.next sample)
size_decreases!
(n.= (-- (/.size sample))
(/.size popped))
popped_member_is_not_identified!
(not (/.member? n.equivalence popped target))
has_expected_order!
(\ (list.equivalence n.equivalence) =
expected
(/.list popped))]
(and size_decreases!
popped_member_is_not_identified!
has_expected_order!))
#.End
(and (/.empty? sample)
(/.empty? (/.next sample)))))
))))
|
