Formal specification as a design tool

ABSTRACT

The formulation and analysis of a design specification is almost always of more utility than the verification of the consistency of a program with its specification. Good specification tools can assist in this process, but have generally not been proposed and evaluated in this light. In this paper we outline a specification language combining algebraic axioms and predicate transformers, present part of a non-trivial example (the specification of a high-level interface to a display), and finally discuss the analysis of this specification.

REFERENCES

• 1: Edsger Wybe Dijkstra, A Discipline of Programming, Prentice Hall PTR, Upper Saddle River, NJ, 1997
• 2: {Goguen 78} J. A. Goguen, J. W. Thatcher, and E. G. Wagner, "An Initial Algebra Approach to the Specification, Correctness, and Implementation of Abstract Data Types," Current Trends in Programming Methodology Volume IV (ed. Raymond T. Yeh), Prentice-Hall, 1978.
• 3: John Guttag, Abstract data types and the development of data structures, Communications of the ACM, v.20 n.6, p.396-404, June 1977 [doi>10.1145/359605.359618]
• 4: {Guttag 78} J. V. Guttag and J. J. Horning, "The Algebraic Specification of Abstract Data Types," Acta Informatica10, 1, pp. 27-52, 1978.
• 5: {Guttag 79} J. V. Guttag, "Notes on Type Abstraction," Proc. Specifications of Reliable Software Conference, IEEE Cat. No. 79 CHI401-9C, pp. 36-46, April 1979.
• 6: {Liskov 77} B. H. Liskov and S. N. Zilles, "An Introduction to Formal Specifications of Data Abstractions," Current Trends in Programming Methodology, Volume I, (ed. Raymond Yeh), Prentice-Hall, 1977.