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