blob: e4b71e513aca069e9a687e1a09429703e82d3fed (
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
|
(.using
[library
[lux (.full)
["_" test (.only Test)]
[abstract
[monad (.only do)]
["[0]" predicate]
[\\specification
["$[0]" equivalence]]]
[math
["[0]" random (.only Random)]
[number
["n" nat]]]]]
[\\library
["[0]" / (.only Bits)]])
(def: (size min max)
(-> Nat Nat (Random Nat))
(|> random.nat
(# random.monad each (|>> (n.% (++ max)) (n.max min)))))
(def: .public random
(Random Bits)
(do [! random.monad]
[size (# ! each (n.% 1,000) random.nat)]
(case size
0 (in /.empty)
_ (do [! random.monad]
[idx (|> random.nat (# ! each (n.% size)))]
(in (/.one idx /.empty))))))
(def: .public test
Test
(<| (_.covering /._)
(_.for [/.Bits])
(all _.and
(_.for [/.equivalence]
($equivalence.spec /.equivalence ..random))
(do random.monad
[sample ..random]
(_.coverage [/.empty? /.size]
(if (/.empty? sample)
(n.= 0 (/.size sample))
(n.> 0 (/.size sample)))))
(_.coverage [/.empty]
(/.empty? /.empty))
(do [! random.monad]
[size (# ! each (|>> (n.% 1,000) ++) random.nat)
idx (# ! each (n.% size) random.nat)
sample ..random]
(all _.and
(_.coverage [/.bit /.one]
(and (|> /.empty (/.bit idx) not)
(|> /.empty (/.one idx) (/.bit idx))))
(_.coverage [/.zero]
(|> /.empty (/.one idx) (/.zero idx) (/.bit idx) not))
(_.coverage [/.flipped]
(and (|> /.empty (/.flipped idx) (/.bit idx))
(|> /.empty (/.flipped idx) (/.flipped idx) (/.bit idx) not)))
(_.coverage [/.Chunk /.capacity /.chunk_size]
(and (n.= 0 (/.capacity /.empty))
(|> /.empty (/.one idx) /.capacity
(n.- idx)
(predicate.or (n.>= 0)
(n.< /.chunk_size)))
(let [grown (/.flipped idx /.empty)]
(and (n.> 0 (/.capacity grown))
(same? /.empty (/.flipped idx grown))))))
(_.coverage [/.intersects?]
(and (not (/.intersects? /.empty
/.empty))
(/.intersects? (/.one idx /.empty)
(/.one idx /.empty))
(not (/.intersects? (/.one (++ idx) /.empty)
(/.one idx /.empty)))
(not (/.intersects? sample (/.not sample)))))
(_.coverage [/.not]
(and (same? /.empty (/.not /.empty))
(or (same? /.empty sample)
(and (not (# /.equivalence = sample (/.not sample)))
(# /.equivalence = sample (/.not (/.not sample)))))))
(_.coverage [/.xor]
(and (same? /.empty (/.xor sample sample))
(n.= (/.size (/.xor sample (/.not sample)))
(/.capacity sample))))
(_.coverage [/.or]
(and (# /.equivalence = sample (/.or sample sample))
(n.= (/.size (/.or sample (/.not sample)))
(/.capacity sample))))
(_.coverage [/.and]
(and (# /.equivalence = sample (/.and sample sample))
(same? /.empty (/.and sample (/.not sample)))))
)))))
|
