Using assertions about traces to write abstract specifications for software modules

A specification for a software module is a statement of the requirements that the final programs must meet. In this paper we concentrate on that portion of the specification that describes the interface between the module being specified and other programs (or persons) that will interact with that module. Because of the complexity of software products, it is advantageous to be able to evaluate the design of this interface without reference to any possible implementations. The first sections of this paper present an approach to the writing of black box specifications, that takes advantage of Guttag's work on abstract specification [9]. Then we illustrate it on a number of small examples, and discuss checking the completeness of a specification. Finally we describe a case history of a module design. Although the module is a simple one, the early specifications (written using an earlier notation) contained design flaws that were not detected in spite of the involvement of several persons in a series of discussions about the module. These errors are easily recognized using the method introduced in this paper.