Introducing OBJ

Abstract

This is an introduction to the philosophy and use of OBJ, emphasizing its oper-ational semantics, with aspects of its history and its logical semantics. Release 2 of OBJ3 is described in detail, with many examples. OBJ is a wide spectrum first-order functional language that is rigorously based on (order sorted) equational logic and parameterized programming, supporting a declarative style that facilitates verification and allows OBJ to be used as a theorem prover. Order sorted algebra provides a notion of subsort that rigorously supports multiple inheritance, exception handling and overloading. Parameterized programming gives powerful support for design, verification, reuse, and maintenance, using two kinds of module: objects to encapsulate executable code, and in particular to define abstract data types by initial algebra semantics; and (loose) theories to specify both syntactic and semantic properties of modules. Each kind of module can be parameterized, where actual parameters may be modules. For parameter instantiation, a view binds the formal entities in an interface theory to actual entities in a module, and also asserts that the target module satisfies the semantic conditions of the interface theory. Module expressions allow complex combinations of already defined modules, including sums, instantiations, and transformations; moreover, evaluating a module expression actually constructs the described software (sub)system from the given components. Default views can greatly reduce the effort of instantiating modules, by allowing obvious correspondences to be left out. We argue that first-order parameterized programming includes much of the power of higher-order programming, in a form that is often more convenient. Although OBJ executable code normally consists of equations that are interpreted as rewrite rules, OBJ3 objects can also encapsulate Lisp code, e.g., to provide efficient built-in data types, or to augment the system with new capabilities; we describe the syntax of this facility, and provide some examples. In addition, OBJ provides rewriting modulo associative, commutative and/or identity equations, as well as user-definable evaluation strategies that allow lazy, eager, and mixed evaluation strategies on an operator-by-operator basis; memoization is also available on an operator-by-operator basis. In addition, OBJ3 supports the application of equations one at a time, either forwards or backwards; this is needed for equational theorem proving. Finally, OBJ provides user-definable mixfix syntax, which supports the notational conventions of particular application domains.