Cleanroom verification of objects

Verification of Cleanroom objects follows all the usual rules for cleanroom verification, but there is an additional technique.

Any number of invariant conditions may be specified for the state of the object. These conditions are used to ensure that an instance's internal state is consistent.

For example, suppose that for efficient searching your object keeps a list of names, self.nameList, in alphabetical order. You might specify an invariant like:

    Elements of self.nameList are sorted in ascending order.

To verify a class with invariants, you must:

1. Verify that the constructor establishes the invariants.
2. Verify that, assuming the invariant is true on entry, each method leaves the invariant true.

The invariants for an object are often vital in verifying code that uses that object's methods.

For a good discussion of the theory of invariants, refer to Erich Gamma's Design patterns.

For an example of an invariant on a data structure, see skiplist.py, a container class.

Last updated: 2002/09/28 21:55:54
URL: http://www.nmt.edu/~shipman/soft/clean/ooverf.html