On object-oriented design and verification

We present a theory of object-orientation on the basis of the refinement calculus. This theory allows for specifying the behaviour of objects and provides a calculus for the proof of relationships between classes such as refinement. Given two similar, but not identical classes, we present an algorithm to construct a common superclass which is refined by both classes, and an algorithm to construct a common subclass which refines both classes. As an example, we present an account manager to illustrate design and verification. The overall approach aims at giving a simple theoretical basis for incremental object-oriented software construction. We demonstrate how formal specification and verification can be integrated into the development process, and thus can be put into practical use.