Next / Previous / Contents / Shipman's homepage

9. Additional principles for object-oriented programming

To verify the correctness of a Python class, we use invariants.

An invariant is a condition that must be true if an instance is to be considered in a valid state. Typically you will declare invariants on attributes of the instance.

For example, let's suppose you are implementing a binary tree data structure. Suppose further that your program needs to know how many nodes are in the tree, and you want to write the class's .__len__() special method to return that count.

It is quite simple to write a recursive algorithm that counts the nodes, but such an approach might be time-consuming for a tree with millions of nodes.

If the performance of the .__len__() method is impacting the whole system's performance, one way to optimize it is to maintain a count of the nodes as a private attribute of the class. The constructor sets this count to zero; a method that adds a node to the tree adds one to the count; and a method that deletes a node from the tree subtracts one from the count.

However, for correct functioning, we must be sure that anything that adds or removes nodes also increases or decreases the node count so that the current count is also accurate. So we declare that the count attribute has an invariant: its value is always equal to the number of nodes in the tree.

Here, then, are the rules for class invariants.

  1. The constructor must establish the invariant. In our example case, the .__init__() method sets the node count to zero.

  2. For every method in the class, you must prove that, assuming the invariant is true on entry to the method, it is also true for every path through the method.

    In our example, if there is only one method that adds a node, and only one method that removes a node, you need only prove that the add method increments the node count and the remove method decrements the node count. It is not necessary to prove this for any method that does not change either the count attribute or the number of nodes in the tree.