UMIST OBJ: a Language for Executable Program Specifications

Open Access
Publisher Website
Google Scholar
Abstract
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.

This publication has 0 references indexed in Scilit: