© 1989 by British Computer Society
UMIST OBJ: a Language for Executable Program Specifications
¶1 HP Labs, Hewlett-Packard, Filton Road, Stoke Gifford, Bristol BS12 6QZ, UK, 2 Computation Department, UMIST, PO Box 88, Sackville Street, Manchester M60 1QD, UK
This paper defines the algebraic specification language implemented by the UMIST OBJ system. It also illustrates the use of the language for the definition of abstract, executable specifications of the behaviour of computer programs. The system implements an executable subset of J.A. Goguen's OBJ language, which is based on the algebraic definition of abstract data types. The language permits data type and operations to be defined abstractly, i.e. independently of any particular representation. Moreover, the definitions of an OBJ specification can be treated as an abstract program, by regarding the equations contained in a specification as a set of left-right rewrite rules which may be used to simplify terms. This makes the language useful for formulating and exploring the consequences of abstract designs, and developing relevant parts of the theory of the associated problem domain. The ability to exercise descriptions of the theory of a problem domain is a powerful tool for the programmer. By providing timely feedback on the correctness of design decisions, such use of the language encourages and reinforces the exploration of design possibilities. With these features, UMIST OBJ embodies the foundation of a framework for effective software engineering. It provides an accessible basis for both mechanisable formal notations for program description and semantically motivated support tools.
Received August 1987. revised October 1987.
* HP Labs, Hewlett-Packard, Filton Road, Stoke Gifford, Bristol BS12 6QZ
Computation Department, UMIST, PO Box 88, Sackville Street, Manchester M60 1QD
¶ To whom correspondence should be addressed at: Department of Computer Science, RHBNC, University of London, Egham Hill, Egham, Surrey TW20 0EX, UK.