1from hypothesis import given, strategies as st, control
2import sys
3import random as rd
4import pytest_mutagen as mg
5
6######################################
7#  DEFINITION AND OPERATIONS OF BST  #
8######################################
9
10
11def isLeaf(t):
12    return t.data is None and t.left is None and t.right is None
13
14
15def isNode(t):
16    return t.data is not None and t.left is not None and t.right is not None
17
18
19class BST:
20    def __init__(self, d=None, lt=None, r=None):
21        self.left = lt
22        self.right = r
23        self.data = d
24
25        if (not isLeaf(self)) and (not isNode(self)):
26            sys.exit("Invalid BST")
27
28    def __str__(self):
29        if isLeaf(self):
30            return "Leaf"
31        elif isNode(self):
32            return "Node " + str(self.data) + " (" + str(
33                self.left) + ") (" + str(self.right) + ")"
34        else:
35            sys.exit("Malformed BST : " + str(self.data) + " (" +
36                     str(self.left) + ") (" + str(self.right) + ")")
37
38
39def max(t):
40    if isLeaf(t):
41        return None
42    else:
43        if isLeaf(t.right):
44            return t.data
45        else:
46            return max(t.right)
47
48
49def toList(t):
50    if t is None or isLeaf(t):
51        return []
52    else:
53        return toList(t.left) + [t.data] + toList(t.right)
54
55
56def keys(t):
57    return [x[0] for x in toList(t)]
58
59
60def isBST(t):
61    if t is None:
62        return False
63    if isLeaf(t):
64        return True
65    return (all([x < t.data[0] for x in keys(t.left)])) and \
66        (all([x > t.data[0] for x in keys(t.right)])) and \
67        isBST(t.left) and isBST(t.right)
68
69
70def eq(t1, t2):
71    if isLeaf(t1):
72        return isLeaf(t2)
73    if isLeaf(t2):
74        return False
75    if t1.data != t2.data:
76        return False
77    return eq(t1.left, t2.left) and eq(t1.right, t2.right)
78
79
80def eqWeak(t1, t2):
81    return toList(t1) == toList(t2)
82
83
84def find(x, t):
85    if t is None or isLeaf(t):
86        return None
87
88    k, v = t.data
89    if x == k:
90        return v
91    elif x < k:
92        return find(x, t.left)
93    else:
94        return find(x, t.right)
95
96
97@mg.has_mutant("INSERT_NOUPDATE", file="BST_mutations.py")
98def insert(x, t):
99    if t is None or isLeaf(t):
100        return BST(x, BST(), BST())
101
102    k, v = t.data
103    if x[0] == k:
104        ret = mg.mut("INSERT_NOUPDATE", lambda: BST(x, t.left, t.right),
105                     lambda: t)
106        return ret
107    elif x[0] < k:
108        return BST(t.data, insert(x, t.left), t.right)
109    else:
110        return BST(t.data, t.left, insert(x, t.right))
111
112
113@mg.has_mutant("DELETE_REMAINDER", file="BST_mutations.py")
114def delete(x, t):
115    if t is None or isLeaf(t):
116        return t
117
118    k, v = t.data
119    if x < k:
120        ret = mg.mut("DELETE_REMAINDER",
121                     lambda: BST(t.data, delete(x, t.left), t.right),
122                     lambda: delete(x, t.left))
123        return ret
124    elif x > k:
125        ret = mg.mut("DELETE_REMAINDER",
126                     lambda: BST(t.data, t.left, delete(x, t.right)),
127                     lambda: delete(x, t.right))
128        return ret
129    else:
130        if isLeaf(t.left):
131            return t.right
132        elif isLeaf(t.right):
133            return t.left
134        else:
135            m = max(t.left)
136            return BST(m, delete(m[0], t.left), t.right)
137
138
139def union(t1, t2):
140    lst = toList(t1)
141    if lst == []:
142        return t2
143    else:
144        t = insert(lst[0], t2)
145        for k in range(1, len(lst)):
146            t = insert(lst[k], t)
147        return t
148
149
150def listToBST(l):
151    t = BST()
152    for k in l:
153        t = insert(k, t)
154    return t
155
156
157def genBST():
158    return st.builds(listToBST,
159                     st.lists(st.tuples(st.integers(), st.integers())))
160
161
162###########
163#  TESTS  #
164###########
165
166# Validity properties
167
168
169@given(genBST())
170def test_valid(t):
171    assert isBST(t)
172
173
174@given(st.integers(), st.integers(), genBST())
175def test_insertValid(k, v, t):
176    assert isBST(insert((k, v), t))
177
178
179@given(st.integers(), genBST())
180def test_deleteValid(k, t):
181    assert isBST(delete(k, t))
182
183
184@given(genBST(), genBST())
185def test_unionValid(t1, t2):
186    assert isBST(union(t1, t2))
187
188
189# Postconditions
190
191
192@given(st.integers(), st.integers(), st.integers(), genBST())
193def test_insertPost(k1, v, k2, t):
194    x = find(k2, insert((k1, v), t))
195    if k1 == k2:
196        assert x == v
197    else:
198        assert x == find(k2, t)
199
200
201@given(st.integers(), st.integers(), genBST())
202def test_insertPostSameKey(k, v, t):
203    assert find(k, insert((k, v), t)) == v
204
205
206@given(st.integers(), st.integers(), genBST())
207def test_deletePost(k1, k2, t):
208    x = find(k2, delete(k1, t))
209    if k1 == k2:
210        assert x is None
211    else:
212        assert x == find(k2, t)
213
214
215@given(st.integers(), genBST())
216def test_deletePostSameKey(k, t):
217    assert find(k, delete(k, t)) is None
218
219
220@given(genBST(), genBST(), st.integers())
221def test_unionPost(t1, t2, k):
222    a = find(k, t1)
223    b = find(k, t2)
224    if a is None:
225        assert find(k, union(t1, t2)) == b
226    elif b is None:
227        assert find(k, union(t1, t2)) == a
228    else:
229        assert find(k, union(t1, t2)) == a
230
231
232@given(st.integers(), st.integers(), genBST())
233def test_findPostPresent(k, v, t):
234    assert find(k, insert((k, v), t)) == v
235
236
237@given(st.integers(), genBST())
238def test_findPostAbsent(k, t):
239    assert find(k, delete(k, t)) is None
240
241
242@given(st.integers(), genBST())
243def test_insertDeleteComplete(k, t):
244    f = find(k, t)
245    if f is None:
246        assert eq(t, delete(k, t))
247    else:
248        assert eq(t, insert((k, f), t))
249
250
251# Metamorphic properties
252
253
254@given(st.integers(), st.integers(), st.integers(), st.integers(), genBST())
255def test_insertInsert(k1, v1, k2, v2, t):
256    t2 = insert((k1, v1), insert((k2, v2), t))
257    if k1 != k2:
258        assert eqWeak(t2, insert((k2, v2), insert((k1, v1), t)))
259    else:
260        assert eqWeak(t2, insert((k1, v1), t))
261
262
263@given(st.integers(), st.integers(), st.integers(), st.integers(), genBST())
264def test_insertInsertWeak(k1, v1, k2, v2, t):
265    control.assume(k1 != k2)
266    assert eqWeak(insert((k1, v1), insert((k2, v2), t)),
267                  insert((k2, v2), insert((k1, v1), t)))
268
269
270@given(st.integers(), st.integers(), st.integers(), genBST())
271def test_insertDelete(k1, v1, k2, t):
272    t2 = insert((k1, v1), delete(k2, t))
273    if k1 != k2:
274        assert eqWeak(t2, delete(k2, insert((k1, v1), t)))
275    else:
276        assert eqWeak(t2, insert((k1, v1), t))
277
278
279@given(st.integers(), st.integers(), genBST(), genBST())
280def test_insertUnion(k, v, t1, t2):
281    assert eqWeak(insert((k, v), union(t1, t2)), union(insert((k, v), t1), t2))
282
283
284@given(st.integers(), st.integers(), st.integers(), genBST())
285def test_deleteInsertWeak(k1, k2, v2, t):
286    control.assume(k1 != k2)
287    assert eqWeak(delete(k1, insert((k2, v2), t)),
288                  insert((k2, v2), delete(k1, t)))
289
290
291@given(st.integers(), st.integers(), st.integers(), genBST())
292def test_deleteInsert(k1, k2, v2, t):
293    t2 = delete(k1, insert((k2, v2), t))
294    if k1 == k2:
295        assert eqWeak(t2, delete(k1, t))
296    else:
297        assert eqWeak(t2, insert((k2, v2), delete(k1, t)))
298
299
300@given(st.integers(), st.integers(), genBST())
301def test_deleteDelete(k1, k2, t):
302    assert eqWeak(delete(k1, delete(k2, t)), delete(k2, delete(k1, t)))
303
304
305@given(st.integers(), genBST(), genBST())
306def test_deleteUnion(k, t1, t2):
307    assert eqWeak(delete(k, union(t1, t2)), union(delete(k, t1), delete(k,
308                                                                        t2)))
309
310
311@given(st.integers(), st.integers(), genBST(), genBST())
312def test_unionDeleteInsert(k, v, t1, t2):
313    assert eqWeak(union(delete(k, t1), insert((k, v), t2)),
314                  insert((k, v), union(t1, t2)))
315
316
317@given(genBST())
318def test_unionUnionIdem(t):
319    assert eqWeak(union(t, t), t)
320
321
322@given(genBST(), genBST(), genBST())
323def test_unionUnionAssoc(t1, t2, t3):
324    assert eqWeak(union(t1, union(t2, t3)), union(union(t1, t2), t3))
325
326
327@given(st.integers(), st.integers(), genBST(), genBST())
328def test_findInsert(k1, k2, v2, t):
329    f = find(k1, insert((k2, v2), t))
330    if k1 == k2:
331        assert f == v2
332    else:
333        assert f == find(k1, t)
334
335
336@given(st.integers(), st.integers(), genBST())
337def test_findDelete(k1, k2, t):
338    f = find(k1, delete(k2, t))
339    if k1 == k2:
340        assert f is None
341    else:
342        assert f == find(k1, t)
343
344
345@given(st.integers(), genBST(), genBST())
346def test_findUnion(k, t1, t2):
347    v = find(k, union(t1, t2))
348    assert (v == find(k, t1)) or (v == find(k, t2))
349
350
351# Preservation of equivalence
352
353
354def listToEquivBST(xs):
355    # Removing duplicate keys
356    xs = list(dict(xs).items())
357
358    a = listToBST(xs)
359    rd.shuffle(xs)
360    b = listToBST(xs)
361    return a, b
362
363
364def genEquivBST():
365    return st.builds(listToEquivBST,
366                     st.lists(st.tuples(st.integers(), st.integers())))
367
368
369@given(st.integers(), st.integers(), genEquivBST())
370def test_insertPreservesEquiv(k, v, p):
371    t1, t2 = p
372    assert eqWeak(insert((k, v), t1), insert((k, v), t2))
373
374
375@given(st.integers(), genEquivBST())
376def test_deletePreservesEquiv(k, p):
377    t1, t2 = p
378    assert eqWeak(delete(k, t1), delete(k, t2))
379
380
381@given(genEquivBST(), genEquivBST())
382def test_unionPreservesEquiv(p1, p2):
383    t1, t2 = p1
384    t3, t4 = p2
385    assert eqWeak(union(t1, t3), union(t2, t4))
386
387
388@given(st.integers(), genEquivBST())
389def test_findPreservesEquiv(k, p):
390    t1, t2 = p
391    assert find(k, t1) == find(k, t2)
392
393
394@given(genEquivBST())
395def test_equivs(p):
396    t1, t2 = p
397    assert eqWeak(t1, t2)
398
399
400# Inductive testing
401
402
403@given(st.integers(), st.integers(), genBST(), genBST())
404def test_unionInsert(k, v, t1, t2):
405    assert eqWeak(union(insert((k, v), t1), t2), insert((k, v), union(t1, t2)))
406
407
408def insertions(t):
409    if isLeaf(t):
410        return []
411    return [t.data] + insertions(t.left) + insertions(t.right)
412
413
414@given(genBST())
415def test_insertComplete(t):
416    assert eq(t, listToBST(insertions(t)))
417
418
419@given(st.integers(), genBST())
420def test_insertCompleteForDelete(k, t):
421    t2 = delete(k, t)
422    assert eq(t2, listToBST(insertions(t2)))
423
424
425@given(genBST(), genBST())
426def test_insertCompleteForUnion(t1, t2):
427    t = union(t1, t2)
428    assert eq(t, listToBST(insertions(t)))
429
430
431# Model-based properties
432
433
434def insertSortedList(x, xs):
435    if xs == []:
436        return [x]
437    if x <= xs[0]:
438        return [x] + xs
439    return [xs[0]] + insertSortedList(x, xs[1:])
440
441
442def deleteKey(k, xs):
443    if xs == []:
444        return []
445    x, v = xs[0]
446    if x == k:
447        return deleteKey(k, xs[1:])
448    return [xs[0]] + deleteKey(k, xs[1:])
449
450
451def unionLists(l1, l2):
452    if l1 == []:
453        return l2
454    if l2 == []:
455        return l1
456    if l1[0][0] < l2[0][0]:
457        return [l1[0]] + unionLists(l1[1:], l2)
458    elif l1[0][0] > l2[0][0]:
459        return [l2[0]] + unionLists(l1, l2[1:])
460    else:
461        return [l1[0]] + unionLists(l1[1:], l2[1:])
462
463
464@given(st.integers(), st.integers(), genBST())
465def test_insertModel(k, v, t):
466    assert toList(insert((k, v), t)) == insertSortedList(
467        (k, v), deleteKey(k, toList(t)))
468
469
470@given(st.integers(), genBST())
471def test_deleteModel(k, t):
472    assert toList(delete(k, t)) == deleteKey(k, toList(t))
473
474
475@given(genBST(), genBST())
476def test_unionModel(t1, t2):
477    assert toList(union(t1, t2)) == sorted(unionLists(toList(t1), toList(t2)))
478
479
480@given(st.integers(), genBST())
481def test_findModel(k, t):
482    assert find(k, t) == dict(toList(t)).get(k)
483
484
485###############
486#  MUTATIONS  #
487###############
488
489
490@mg.mutant_of("insert", "INSERT_ERASE")
491def insert_bug1(x, t):
492    return BST(x, BST(), BST())
493
494
495@mg.mutant_of("insert", "INSERT_DUP")
496def insert_bug2(x, t):
497    if t is None or isLeaf(t):
498        return BST(x, BST(), BST())
499
500    k, v = t.data
501    if x[0] < k:
502        return BST(t.data, insert(x, t.left), t.right)
503    else:
504        return BST(t.data, t.left, insert(x, t.right))
505
506
507@mg.mutant_of("delete", "DELETE_REV")
508def delete_bug5(x, t):
509    if t is None or isLeaf(t):
510        return t
511
512    k, v = t.data
513    if x < k:
514        return BST(t.data, t.left, delete(x, t.right))
515    elif x > k:
516        return BST(t.data, delete(x, t.left), t.right)
517    else:
518        if isLeaf(t.left):
519            return t.right
520        elif isLeaf(t.right):
521            return t.left
522        else:
523            m = max(t.left)
524            return BST(m, delete(m[0], t.left), t.right)
525
526
527@mg.mutant_of("union", "UNION_FSTOVERSND")
528def union_bug6(t1, t2):
529    if isLeaf(t1):
530        return t2
531    m = max(t1)
532    return BST(m, delete(m[0], t1), t2)
533
534
535@mg.mutant_of("union", "UNION_ROOT")
536def union_bug7(t1, t2):
537    if isLeaf(t1):
538        return t2
539    if isLeaf(t2):
540        return t1
541    if t1.data < t2.data:
542        m = max(t1)
543        return BST(m, delete(m[0], t1), t2)
544    else:
545        m = max(t2)
546        return BST(m, t1, delete(m[0], t2))
547
548
549@mg.mutant_of("union", "UNION_OTHERPRIORITY")
550def union_bug8(t1, t2):
551    xs = toList(t1)
552    if xs == []:
553        return t2
554    else:
555        t = insert(xs[0], t2)
556        for k in range(0, len(xs)):
557            if find(xs[k], t2) is None:
558                t = insert(xs[k], t)
559        return t