It is shown how design time testing can be used in conjunction with formal specification. Emphasis is placed on the benefits of using an executable specification language OBJ, of having a design controlled by requirements specification, and of adherence to the regularity and uniformity hypotheses in dynamic validation. It is shown that such an approach offers positive benefits by providing early design validation and a controlled, disciplined design process.>

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.

Abstract This paper assesses Concurrent Pascal against its design aims. The language is shown to be suitable for writing reliable non‐trivial concurrent applications programs and operating systems. The major weakness of the language is its inability to provide an environment for other Concurrent Pascal programs. A new language construct, group, is proposed to remedy this difficulty.