In the following, we consider a problem involving binary search trees. We attempt to solve the problem two ways, first iteratively, then recursively, and prove correctness for each.

Whereas proving correctness for loops, or iteration, is done using a loop invariant, for recursion, we prove correctness using induction, or in our case of structural recursion, structural induction.

# Problem:

For a value num, and a binary search tree, find the largest number smaller than num, if such exists, otherwise return -1.

For the sake of brevity, we will refer to this value as the predecessor, or simply, pred.

# Iterative solution and proof:

A solution using loops might look like this:

result = -1
while curr:
if curr.val < num:
result = max(result, curr.val)
curr = curr.right
else:
curr = curr.left
return result

Invariant property:

We have either result = pred, or the value pred exists somewhere in the tree rooted at curr.

Initialization:

If the original tree has any values less than num, then the value pred exists in this tree, otherwise, pred = -1, the initial value of result.

Maintenance:

Case 1: curr.val < num

Then for any node in the subtree at curr.left, we have node.val ≤ curr.val.

Then our desired value is either in result, curr.val, or the subtree at curr.right, and property still holds after setting result = max(result, curr.val), and curr = curr.right.

Case 2: curr.val ≥ num

Then for any node in the subtree at curr.right, we have node.val ≥ num.

Then our desired value is either in result or the subtree at curr.left, and property still holds after setting curr = curr.left.

Termination:

When the loop terminates, there are no values in the subtree at curr, thus result = pred.

# Recursive solution and proof

A recursive solution might look like this.

findValue :: Node -> Int
findValue node
| null node         = -1
| value node <  num = max (value node) (findValue (right node))
| value node >= num = findValue (left node)

Claim:

For any node, if the subtree at node contains any value less than num, findValue will return the largest such, otherwise it returns -1.

Base Case:

If node is null, then there are no values in the subtree at node, and findValue correctly returns -1.

Inductive step:

We consider for a non-null node, with value v = value node.

Case 1: v < num

For any value u in subtree at left node we have u ≤ v.

Then, if there were any values w in the subtree at node such that v < w < num, they will be in the subtree at right node.

By inductive hypothesis, findValue will return the appropriate value when applied to right node. Taking the max as defined above, completes the inductive step for the first case.

Case 2: v ≥ num

Then for any value w in the subtree at right node we have w ≥ num.

If there are any values u in the subtree at node such that u < num, they will be in the subtree at left node.

Inductive hypothesis ensures findValue returns correct value for left node.