Object Oriented Specification and Refinement

Abstract

The increasing demand for high integrity and safety critical systems is giving the development of formal methods for software production a high priority. A large number of different approaches to specifying, developing and implementing systems have been devised, however, despite this widespread (but mainly academic) research, formal methods are still very rarely used in industrial practice. This failure can be attributed to a number of causes, among them the inability of the techniques to scale easily to industrial sized problems.

This paper proposes an approach to specification that helps alleviate the problems of scalability by providing a strong separation between parts of a specification, allowing their independent refinement, and hence allowing refinements of the total specification to be produced relatively cheaply. The separation is provided by producing specifications as a set of objects, each of which is described by two specifications, an algebraic export specification and a model oriented body specification. The export describes the object to those who will use it, while the body specification will form the basis of subsequent refinement and implementation.

This approach to specification provides a framework within which to specify and develop software. We describe relationships within this framework for which we must be able to derive and discharge relevant proof obligations in order to verify the specifications. In particular we describe the refinement relation between the object’s export and body specifications, the substitution relation implied when we use one object within another, and the composition relation which allows us to correctly combine a set of objects to form a complete system.