Application of Model Based Testing to a Binary Search Tree - Part II

Okay, today I want to wrap up on the model based testing of the binary search tree implementation I did last time. Remember how we uncovered a problem that the model did not cover all of the code? Drawing from our experience from the Application of Code Coverage to Model Based Testing post we understand that our model does not reflect closely the actual implementation, and we have a risk in terms of a test hole.

Understanding the problem

Before we jump in to adding additional tests, let’s try and understand what the problem really is. Remember I hinted that it has to do with our choice of container in the model. So let’s try to understand this some more by building some trees from the model:

Notice that even though these three trees are very different constructs, the internal set representation of the model reads (0, 1, 2) for all cases.

Application of Model Based Testing to a Binary Search Tree - Part I

I wanted to post some real modeling examples for a change, where I show how to use model based testing to explore test case combinatorics. The obvious choice is of course the more than sufficiently modeled calculator. So I decided not to choose a calculator, but something a bit different. I thought to myself, why not a simple Binary Search Tree? Hmm, but does it have any potential?

BSTs are really nice in that you can write invariants for them: 

For all nodes n in T: value(left(n)) < value(n) < value(right(n))

However, in a normal functional testing paradigm this is not entirely sufficient to validate the tree. The problem is that any given sub-tree of the BST will pass the integrity check – thus if I were to introduce a bug that removed the whole sub-tree when deleting a node from the tree, the resulting tree is still a valid BST but it’s not the expected! Normally we would need to check the node count and also that the expected values are to be found in the tree, however in a model based testing paradigm this is no longer required as we will see later on.