A proof is much harder in the OOP world because of side effects, unrestricted inheritance, and null
being a member of every type. Most proofs rely on an induction principle to show that you've covered every possibility, and all 3 of those things make that harder to prove.
Let's say we're implementing binary trees that contain integer values (for the sake of keeping the syntax simpler, I won't bring generic programming into this, though it wouldn't change anything.) In Standard ML, I would define that like this:
datatype tree = Empty | Node of (tree * int * tree)
This introduces a new type called tree
whose values can come in exactly two varieties (or classes, not to be confused with the OOP concept of a class) - an Empty
value which carries no information, and Node
values which carry a 3-tuple whose first and last elements are tree
s and whose middle element is an int
. The closest approximation to this declaration in OOP would look like this:
public class Tree {
private Tree() {} // Prevent external subclassing
public static final class Empty extends Tree {}
public static final class Node extends Tree {
public final Tree leftChild;
public final int value;
public final Tree rightChild;
public Node(Tree leftChild, int value, Tree rightChild) {
this.leftChild = leftChild;
this.value = value;
this.rightChild = rightChild;
}
}
}
With the caveat that variables of type Tree can never be null
.
Now let's write a function to calculate the height (or depth) of the tree, and assume we have access to a max
function that returns the larger of two numbers:
fun height(Empty) =
0
| height(Node (leftChild, value, rightChild)) =
1 + max( height(leftChild), height(rightChild) )
We've defined the height
function by cases - there's one definition for Empty
trees and one definition for Node
trees. The compiler knows how many classes of trees exist and would issue a warning if you didn't define both cases. The expression Node (leftChild, value, rightChild)
in the function signature binds the values of the 3-tuple to the variables leftChild
, value
, and rightChild
respectively so we can refer to them in the function definition. It's akin to having declared local variables like this in an OOP language:
Tree leftChild = tuple.getFirst();
int value = tuple.getSecond();
Tree rightChild = tuple.getThird();
How can we prove we've implemented height
correctly? We can use structural induction, which consists of:
1. Prove that height
is correct in the base case(s) of our tree
type (Empty
)
2. Assuming that recursive calls to height
are correct, prove that height
is correct for the non-base case(s) (when the tree is actually a Node
).
For step 1, we can see that the function always returns 0 when the argument is an Empty
tree. This is correct by definition of the height of a tree.
For step 2, the function returns 1 + max( height(leftChild), height(rightChild) )
. Assuming that the recursive calls truly do return the height of the children, we can see that this is also correct.
And that completes the proof. Steps 1 and 2 combined exhaust all the possibilities. Note, however, that we have no mutation, no nulls, and there are exactly two varieties of trees. Take away those three conditions and the proof quickly becomes more complicated, if not impractical.
EDIT: Since this answer has risen to the top, I'd like to add a less trivial example of a proof and cover structural induction a bit more thoroughly. Above we proved that if height
returns, its return value is correct. We haven't proved it always returns a value, though. We can use structural induction to prove this, too (or any other property.) Again, during step 2, we're allowed to assume the property holds of the recursive calls as long as the recursive calls all operate on a direct child of the tree.
A function can fail to return a value in two situations: if it throws an exception, and if it loops forever. First let's prove that if no exceptions are thrown, the function terminates:
Prove that (if no exceptions are thrown) the function terminates for the base cases (Empty
). Since we unconditionally return 0, it terminates.
Prove that the function terminates in the non-base cases (Node
). There's three function calls here: +
, max
, and height
. We know that +
and max
terminate because they're part of the language's standard library and they're defined that way. As mentioned earlier, we're allowed to assume the property we're trying to prove is true on recursive calls as long as they operate on immediate subtrees, so calls to height
terminate too.
That concludes the proof. Note that you wouldn't be able to prove termination with a unit test. Now all that's left is to show that height
doesn't throw exceptions.
- Prove that
height
doesn't throw exceptions on the base case (Empty
). Returning 0 can't throw an exception, so we're done.
- Prove that
height
doesn't throw exception on the non-base case (Node
). Assume once again that we know +
and max
don't throw exceptions. And structural induction allows us to assume the recursive calls won't throw either (because the operate on the tree's immediate children.) But wait! This function is recursive, but not tail recursive. We could blow the stack! Our attempted proof has uncovered a bug. We can fix it by changing height
to be tail recursive.
I hope this shows proofs don't have to be scary or complicated. In fact, whenever you write code, you've informally constructed a proof in your head (otherwise, you wouldn't be convinced you just implemented the function.) By avoiding null, unnecessary mutation, and unrestricted inheritance you can prove your intuition is correct fairly easily. These restrictions are not as harsh as you might think:
null
is a language flaw and doing away with it is unconditionally good.
- Mutation is sometimes unavoidable and necessary, but it's needed a lot less often than you'd think - especially when you have persistent data structures.
- As for having a finite number of classes (in the functional sense)/subclasses (in the OOP sense) vs an unlimited number of them, that's a subject too big for a single answer. Suffice to say there's a design trade off there - provability of correctness vs flexibility of extension.
null
).