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
.__len__() special method to return that
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.
The constructor must establish the invariant. In our
example case, the
.__init__() method sets the
node count to zero.
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.