OBJ

OBJ is a family of languages created by Joseph Goguen. In OBJ a program is a set of equations and running it means rewriting terms with those equations until they reach a normal form. Goguen designed it in 1976 for writing and testing algebraic specifications of abstract data types. Over the next quarter-century it was reimplemented as OBJ0, OBJT, OBJ1, OBJ2 and OBJ3. The best-known member is OBJ3, released in 1988.

OBJ is a specification language you can execute. The same text is a mathematical theory with a precise meaning and also a program you can run, test and prove things with. That idea, plus a module system built from theories, views and module expressions, became the basis of what Goguen called parameterized programming. Later systems including Maude, CafeOBJ and CASL inherited it.

History & Origins

Abstract data types and Clear (mid-1970s)

In the mid-1970s Goguen worked with James Thatcher, Eric Wagner and Jesse Wright on the algebraic theory of abstract data types. This is the “initial algebra” approach, where a data type is defined by its operations and the equations between them. In the same years Goguen and Rod Burstall were designing Clear, a language for putting specifications together out of smaller, parameterized pieces. Their paper “Putting theories together to make specifications” appeared at IJCAI in 1977.

The OBJ3 manual’s own history of the language starts here: “OBJ was designed in 1976 by Goguen, using ’error algebras’ to extend algebraic abstract data type theory with error handling and partial functions.” The first design also took parameterized modules from Clear, “thus giving birth to parameterized programming.” The design was written up in Goguen’s paper “Abstract errors for abstract data types”, given at the first IFIP Working Conference on Formal Description of Programming Concepts in 1977.

First implementations at UCLA (1977-1979)

According to the manual, “the first implementations of OBJ were done from 1977 to 1979 at UCLA by Joseph Tardo and Joseph Goguen.” There were two:

• OBJ0 was based on unsorted equational logic. Goguen described it in “Some design principles and theory for OBJ-0”, in Springer’s Lecture Notes in Computer Science volume 75 (1979).
• OBJT used error algebras and an “image” construct for parameterization. Tardo wrote it up in his 1981 UCLA PhD thesis.

The paper that introduced OBJ to a wider audience was Goguen and Tardo’s “An Introduction to OBJ: A Language for Writing and Testing Software Specifications”, in the IEEE volume Specification of Reliable Software (1979). It was reprinted in 1985 in Gehani and McGettrick’s anthology Software Specification Techniques.

OBJ1 and OBJ2 at SRI (1982-1985)

The work moved to SRI International’s Computer Science Laboratory in Menlo Park. There David Plaisted built OBJ1 during 1982-83 on top of OBJT, based on design work with Goguen and José Meseguer. OBJ1 added:

• rewriting modulo associativity and/or commutativity
• hash-coded memo functions
• theories with loose semantics, alongside objects with initial semantics
• new interactive features

OBJ2 was built during 1984-85 at SRI by Kokichi Futatsugi and Jean-Pierre Jouannaud, using parts of OBJ1, with Meseguer and Goguen also working on the design. The big change was replacing error algebras with order-sorted algebra. In order-sorted algebra, sorts (types) form a hierarchy, so Nat can be a subsort of Int. That gives errors, partial functions, overloading and multiple inheritance a cleaner footing. The manual notes that error algebras “sometimes fail to have initial models”, while the order-sorted approach “seems entirely satisfactory to us.” OBJ2 also had Clear-style parameterized modules, theories and views, “although not in full generality”. It was presented as “Principles of OBJ2” at the 12th ACM Symposium on Principles of Programming Languages (POPL) in 1985.

Other groups built their own implementations. The manual lists UMIST-OBJ (UMIST) and Abstract Pascal (University of Manchester), both in Pascal, and MC-OBJ (University of Milan) in C. All three implement OBJ1. There was also a Franz Lisp OBJ2 from Washington State University.

OBJ3 (1988 onward)

On 14 July 1988 Goguen, Meseguer and Timothy Winkler announced on the types and fp mailing lists that “Release 1.0 of OBJ3 is now available!” OBJ3 was written in Kyoto Common Lisp and had been compiled on Sun-3 workstations. SRI sent it out on tape for a licence fee of $150. The OBJ3 syntax is close to OBJ2’s. But it was a new implementation, based on a simpler approach to order-sorted rewriting, and its parameterized programming was much more complete. The manual calls it “the first language to fully implement parameterized programming.”

Winkler announced Release 2.0 on 6 April 1992. It added language extensions, matching modulo associativity, commutativity and identity, and “a facility for controlled rewriting” to support equational theorem proving. It also had a faster implementation: by Winkler’s own account, with no benchmark given, rewriting was “often twice as fast as in the original implementation”. Winkler and Goguen continued the work at Oxford’s Programming Research Group, and version 2.04 added small bug fixes made at Oxford.

Design Philosophy

The OBJ3 manual sums up the design in one sentence. OBJ languages are “logical languages, in the sense that their programs are sets of sentences in some logical system, and their operational semantics is given by deduction in that logical system.” The 1988 announcement split this into three parts. Statements are sentences in a logic (order-sorted equational logic). A program’s denotational meaning is the initial model of those sentences. Running it is efficient deduction in that logic.

Some practical consequences:

1. Computation is proof. In the manual’s words, “the reductions really are proofs, because the programs really are logical theories and computation really is deduction.” OBJ3 can therefore be used directly as a theorem prover for equational logic.
2. Higher-order power without higher-order logic. Parameterized modules give much of the structuring power of higher-order functions while the logic stays first-order. Goguen argued this at length in “Higher-Order Functions Considered Unnecessary for Higher-Order Programming” (1990).
3. Specification and prototype are the same text. A specification can be run straight away, so it can be tested against examples before anyone writes an implementation.

Key Features

The 1988 announcement and the manual list these features of OBJ3:

A taste of OBJ3

This parameterized list is taken from the OBJ3 manual. TRIV is the trivial theory: it requires only a sort Elt. So LIST can be instantiated with any module:

th TRIV is sort Elt . endth

obj LIST[X :: TRIV] is
  sorts List NeList .
  subsorts Elt < NeList < List .
  op nil : -> List .
  op __ : List List -> List [assoc id: nil prec 9] .
  op __ : NeList List -> NeList [assoc prec 9] .
  op head_ : NeList -> Elt .
  op tail_ : NeList -> List .
  op empty?_ : List -> Bool .
  var X : Elt .
  var L : List .
  eq head(X L) = X .
  eq tail(X L) = L .
  eq empty? L = L == nil .
endo

The list constructor is just juxtaposition (__), declared associative with nil as its identity. OBJ3 matches patterns modulo those laws, so head(X L) matches any non-empty list no matter how it is bracketed.

Proofs as programs

The 1988 release announcement included “a cute little proof in OBJ3” of the case p = 3 of Fermat’s little theorem, m³ ≡ m (mod 3). It does induction by hand: the induction hypothesis is added as an equation, and then the step is reduced:

obj NAT is sort Nat .
  op 0 : -> Nat .
  op s_ : Nat -> Nat [prec 1] .
  ops (_+_)(_*_) : Nat Nat -> Nat [assoc comm] .
  vars L M N : Nat .
  eq M + 0 = M .
  eq M + s N = s(M + N) .
  eq M * 0 = 0 .
  eq M * s N = (M * N)+ M .
  eq L * (M + N) = (L * M)+(L * N) .
  eq M + M + M = 0 .
endo
---> base case, m = 0
reduce 0 * 0 * 0 == 0 .
---> induction variable and hypothesis
obj VARS is extending NAT .
  op m : -> Nat .
  eq m * m * m = m .
endo
---> induction step
reduce (s m)*(s m)*(s m) == s m .

Evolution

OBJ was also extended in many directions, often under new names:

• Eqlog: logic (relational) programming
• FOOPS: object-oriented programming
• OOZE: object-oriented specification
• TOOR: requirements tracing
• LOTOS-style specification of communication protocols

By the time the manual was revised in 1999, newer languages were being built on OBJ:

• CafeOBJ, under Kokichi Futatsugi at the Japan Advanced Institute of Science and Technology, adds hidden algebra for behavioural specification and rewriting logic.
• Maude, under José Meseguer at SRI, extends OBJ with rewriting logic.
• CASL, from the European CoFI consortium, is “loosely based on OBJ ideas”.

Goguen’s own group at UCSD later built BOBJ (Behavioural OBJ).

Current Relevance

OBJ3 itself is a historical system. The last release from Goguen’s group was 2.09, in September 2003 according to Joseph Kiniry’s ChangeLog. It updated the code for GCL 2.5.3 and CMU Common Lisp 18e, and it shipped with Lutz Hamel’s TRIM compiler, which was integrated from 2.08 on. Goguen died in July 2006. Since then, enthusiasts have published the source on GitHub with patches so it builds under current Lisps. One repository, created in 2019, updates OBJ3 and TRIM (as “2.10”) to build under GCL 2.6.12, and another, from 2025, targets SBCL. These are community efforts, not official releases.

The ideas are very much alive in OBJ’s descendants. Maude in particular is still in active use for rewriting-logic specification and verification. OBJ’s equational, sort-hierarchical way of writing specifications also survives in CafeOBJ and in CASL.

Why It Matters

• Executable algebraic specification. OBJ showed that algebraic specifications of abstract data types could be run. Goguen’s OBJ family page says that “the first implementation of initial algebra semantics via term rewriting appeared in the earliest versions of OBJ, from the mid 1970s”.
• Parameterized programming. Theories as interfaces, views as bindings and module expressions as a way to build systems became a lasting model of generic modules. Goguen’s OBJ family page goes further and says the module systems of Ada, ML, C++ and LOTOS “have all been influenced by the OBJ module system”. That is the creator’s own assessment. LOTOS’s use of initial algebra semantics, which Goguen credits to OBJ, is easier to trace.
• Order-sorted algebra in practice. OBJ2 and OBJ3 put order-sorted algebra into a working language. It gave a formal account of subtypes, overloading and exceptions that later algebraic specification languages adopted.
• A theorem prover you can program. Through the textbooks Algebraic Semantics of Imperative Programs (Goguen and Malcolm, MIT Press, 1997) and Software Engineering with OBJ (Goguen and Malcolm, eds., Kluwer, 2000), a generation of students learned program semantics by running their proofs as OBJ3 reductions.