Cultivating Rigorous Code
Rooting out bugs in AVL trees with property-based testing
Background
Recently, I was tasked with an interesting problem, and I found the way I solved the problem quite interesting and I thought it was worth sharing.
Without going into too much detail of the domain, I would be creating a specialised cache. I needed to be able to order the dataset, and also be able to retrieve relevant data or the closest datapoint quickly. A balanced binary search tree (BST) suited this usecase. After a bit of research, I found that AVL trees (named after inventors Georgy Adelson-Velsky & Evgenii Landis) have slightly better read performance than Red-Black trees due to stricter balancing rules.[1]
However, whilst I knew the general theory behind AVL trees, I had never implemented one myself before - and I knew enough about them to know that they are not simple! This raised the question “How can I be absolutely sure that my AVL tree implementation is correct?” (and related sub-question “How can I prove to my team that my AVL tree is correct?)”
Typically, most programmers write unit tests to give themselves confidence about their code. However with such a tricky/specific data structure, it’s possible that I might miss some test cases; and raises another question “How will I know that I’ve covered all test cases?” - clearly unit tests will not be sufficient for the degree of confidence I want in my code!
After some contemplation, it’s obvious that all of these questions emanate from the same cause - a need of provably thorough testing. After some research I came across a testing technique called property-based testing (PBT).
Theory of Property-Based Testing
Note: I’m not going to go into a lot of detail about the algorithms behind AVL trees here as there are already a large amount of in-depth resources available.
I like to think of PBT as a generalisation of unit testing. That is, if we can say that unit tests validate that when a function is given a single concrete input, we can assert that it gives a specific predetermined output. Then we can say that property-based tests actually test all possible inputs and assert that certain properties always hold true. Compare testing a sample size of 1 versus testing the entire input-space! Can you already begin to see how much more powerful this is?
In order to do this, we need to generalise the behaviour of the function into what PBT calls properties. Simply put, these are things about the code that should always be true, no matter what the inputs to the function are. For my testing, I opted to define two properties for my AVL tree:
- AVL trees are binary-search trees
- i.e. a binary tree where the key of a given node is greater than all the keys in the respective node’s left subtree. Similarly the keys in the right subtree are greater than the current node’s.
- AVL trees are balanced binary trees
- A balanced binary tree is a binary tree that keeps the minimum height possible at all times.
Below is a quick example of an unbalanced versus a balanced binary tree:
Unbalanced Balanced
4 2
/ / \
3 1 3
/ \
2 4
/
1
Note how the balanced tree takes the smallest depth possible.
The Code
With the theory now out of the way, let’s get to coding.
I will include my implementation of the two properties[2] for completeness, though they are not the main focus of the article:
1 const isBinarySearchTree = (tree, min = -Infinity, max = Infinity) => {
2 if (!tree)
3 return true
4
5 const { key, left, right } = tree
6
7 if (!(min < key && key < max))
8 return false
9
10 return isBinarySearchTree(left, min, key) && isBinarySearchTree(right, key, max)
11 }
12
13 const isBalancedBinaryTree = tree => {
14 const checkBalance = node => {
15 if (!node)
16 return [true, 0]
17
18 const { left, right } = node
19
20 const [leftBalanced, leftHeight] = checkBalance(left)
21 const [rightBalanced, rightHeight] = checkBalance(right)
22
23 const balanced = leftBalanced
24 && rightBalanced
25 && Math.abs(leftHeight - rightHeight) <= 1
26 const height = 1 + Math.max(leftHeight, rightHeight)
27
28 return [balanced, height]
29 }
30
31 return checkBalance(tree)[0]
32 }
These properties just need to return either true or false to indicate if the property holds true, or was violated. With these properties defined, we can now write our property-based tests!
I opted to use the JavaScript library fast-check to do my property-based testing. Below are my (property-based) tests for the insertion operation of the AVL tree. (I implemented testing for node removal also, but omitted here for brevity. See links at the end for full source code)
1 import fc from 'fast-check'
2 import { isBinarySearchTree } from './binary-search-tree.test.js'
3 import { search } from './binary-search-tree.js'
4 import { insert, remove } from './avl-tree.js'
5
6 // *snip*: previously-shown property isBalancedBinaryTree()
7
8 describe('AVL tree', () => {
9 describe('insertion', () => {
10 it('constructs valid binary search tree', () => {
11 fc.assert(fc.property(fc.array(fc.integer()),
12 nums => {
13 const tree = nums.reduce(insert, null)
14
15 return isBinarySearchTree(tree)
16 })
17 )
18 })
19
20 it('constructs balanced binary tree', () => {
21 fc.assert(fc.property(fc.array(fc.integer()),
22 nums => {
23 const tree = nums.reduce(insert, null)
24
25 return isBalancedBinaryTree(tree)
26 })
27 )
28 })
29
30 it('adds element to tree', () => {
31 fc.assert(fc.property(fc.array(fc.integer()),
32 nums => {
33 const tree = nums.reduce(insert, null)
34
35 return nums.map(n => search(tree, n))
36 .every(result => !!result || result === 0)
37 })
38 )
39 })
40 })
41
42 describe('removal', () => { /* left as an exercise for the reader... */ })
43 })
The first thing to note is the function fc.assert(fc.property(...)), which as you may guess asserts that the property holds true for all possible inputs.
The next part is that we need to specify what kind of inputs to generate for the tests. In this case, the AVL tree simply holds integer values, so I generated an array of ints to insert into the tree with fc.array(fc.integer()). Notice here how I’m not defining any specific integer values, or even how many values to insert; but rather letting the PBT library generate a random number of random values for me. Under the hood, the library uses an intelligent search algorithm to generate a large number of targeted pseudorandom test cases; trying it’s best to find interesting test cases to fail our test(s).
Next we provide our actual test function, which takes the array of ints I just specified, denoted as nums. We then insert each of these numbers into the tree, and then check if the property under test holds true for the resulting tree.
The astute observers among you may notice that the first two tests actually have the same structure; the only difference is the testing of different properties. You may be asking “But why couldn’t we just write a single test that tests both properties (e.g. return isBinarySearchTree(tree) && isBalancedBinaryTree(tree))?” The answer is that we certainly could, but it’s generally better to keep tests as granular as possible. This way if a test fails, we can quickly identify which property is failing, and thus the root cause of the failure, leading to faster debugging.
The final insertion test simply checks that after inserting the integers into the tree, we can search for each of the inserted values and retrieve them from the tree. I put this in as more of a sanity-check to make sure something strange possibly not covered by the first two properties isn’t happening. For example, adding one to each key before insertion would still pass the BST and balanced binary tree properties, though does not contain the keys we wanted to insert!
Conclusion
So why is this so powerful? This is because now that we have generalised our tests, the PBT library can then generate hundreds of thousands of test cases[3], trying it’s best to find and explore interesting inputs that may invalidate our properties in a targeted search. This is very powerful as I think I would struggle to come up with all units tests required to cover all edge cases of building an AVL tree; whilst our PBT library will happily try to think up strange/interesting trees for us. Also of note is the amount of test-code that would have to otherwise be written for all edge cases if unit-testing! You could say that because the PBT approach is much more succinct, it is a lot less prone to error.
And there you have it, with that small amount of code, I was able to create an extremely powerful and comprehensive set of tests that verify the correctness of my AVL tree implementation. This is the power of property-based testing!
Source
The full source of the test-code from the article can be seen here on my GitHub: https://github.com/Jamie-Rodriguez/data-structs-and-algos/blob/master/avl-tree.test.js. And if you are curious, the implementation of the AVL tree can be seen here https://github.com/Jamie-Rodriguez/data-structs-and-algos/blob/master/avl-tree.js.
Footnotes
- [1]
- A thorough proof of the maximum heights of AVL trees from the University of California, Irvine can be seen at https://ics.uci.edu/~pattis/ICS-23/lectures/notes/AVL.txt
- [2]
- You can have a go at writing these properties yourself with Leetcode 98. Validate Binary Search Tree and Leetcode 110. Balanced Binary Tree
- [3]
- This can be configured to run an even larger number of tests if you so wish.