UMIST OBJ: a language for executable program specifications

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 types 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.