The OBJ Family

Contents
Introduction
"OBJ" refers to the language family, while "OBJ2," "OBJ3", "CafeOBJ," "BOBJ," etc. refer to particular members of the family. The OBJ languages are broad spectrum algebraic programming and specification languages, based on order sorted equational logic, possibly enriched with other logics (such as rewriting logic, hidden equational logic, or first order logic), and providing the powerful module system of parameterized programming (see the paragraph after next).

All the OBJ languages are rigorously based upon a logical system; more precisely, they 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. All recent OBJ languages use some version of order sorted algebra, which provides a rigorous basis for user definable sub-types, exception handling, multiple inheritance, overloading, multiple representations, coercions, and more. They also support user definable mixfix syntax, user definable execution strategies, rewriting modulo standard equational theories (A,C,I, and their combinations), and memoization.

All recent OBJ languages provide parameterized programming, with parameterized modules, module instantiation, views, module expressions, etc., to support very flexible program structuring and reuse; see An Implementation-Oriented Semantics for Module Composition, by Joseph Goguen and Will Tracz for much more information about parameterized programming and software reuse, including a description of a module composition system for Ada called Lileanna.

The module systems of Ada, ML, C++ and Lotos have all been influenced by the OBJ module system; Lotos also uses the initial algebra semantics that was pioneered by OBJ. The OBJ module system ideas are a further development of ideas pioneered in the Clear language, which was joint work of Joseph Goguen and Rod Burstall in the 1970s. The first implementation of initial algebra semantics via term rewriting appeared in the earliest versions of OBJ, from the mid 1970s.

OBJ3
OBJ3 is based on order sorted equational logic, and has been successfully used for research and teaching in software design and specification, rapid prototyping, theorem proving, user interface design, and hardware verification, among other things. It was the first language to fully implement parameterized programming. Details on OBJ3 may be found in the official OBJ3 manual, Introducing OBJ; see the bibliography below for the detailed citation (there are also pdf and gzip compressed postscript versions available). An OBJ3 Survival Guide was written to help beginners get started. See also the standard prelude, which is the code that generates the OBJ3 builtin modules (it is also listed in Introducing OBJ).

OBJ3 in Education

OBJ3 is used in the UCSD core graduate course on programming languages, CSE 230. OBJ3 is also used in courses on the semantics of imperative programs taught at several universities, including the University of Illinois at Urbana-Champaign and Oxford, where the original version of this course can still be found (maybe). The textbook, Algebraic Semantics of Imperative Programs, by Joseph Goguen and Grant Malcolm, MIT Press, 1997, is used in these courses. A number of comments on this book may be found in the course notes for CSE 230.

A detailed discussion of how we used OBJ in teaching appears in An Executable Course in the Algebraic Semantics of Imperative Programs, by Joseph Goguen and Grant Malcolm, in Teaching and Learning Formal Methods, edited by Michael Hinchey and C. Nevill Dean, Academic Press, 1996, pages 161-179.

Oxford University also used OBJ3 in teaching a course on Theorem Proving; the course textbook, Theorem Proving and Algebra, by Joseph Goguen is in preparation and will be published by MIT Press; Chapters 1, 8 and the references are available over the web. Chapter 1 is the introduction and Chapter 8 is an elegant algebraic treatment of first order logic, proof planning and induction.
 

Selected OBJ3 Bibliography

Information on many automated reasoning systems, including OBJ3, is available in a standard format from a site Stanford University administered by Carolyn Talcott.

Some OBJ3 Examples
Obtaining OBJ3

Source code, and compiled code for Sun workstations, for OBJ3 version 2.04 can be obtained by ftp from ftp://www.cs.ucsd.edu/pub/fac/goguen. It is no longer necessary to obtain a license from SRI International. It is necessary to use some version of Common Lisp if you compile the code yourself, and there may be difficulties for platforms other than Sun; see the README file at the ftp site mentioned above. WARNING: This ftp website now requires host authentication, so you probably cannot use it from a laptop over a wireless network.

There is a new release (from June 2000) of OBJ3, version 2.06; it is a cleaned-up version OBJ3 version 2.04 (from 1992), engineered by Joseph Kiniry and Sula Ma, and built and supported by Joseph Kiniry; it runs under GCL 2.2.2, and has modern open source documentation.

BOBJ

BOBJ is UCSD's implementation of next generation technology for algebraic specification and verification. It extends OBJ3 with support for behavioral specification and verification, and in particular, it provides circular coinductive rewriting with case analysis for conditional equations over behavioral theories, as well as behavioral and ordinary rewriting over order sorted theories, modulo attributes that can be any combination of associative, commutative and identity. BOBJ also supports concurrent connection of behavioral theories, cobasis declaration, default cobasis generation, operations with multiple hidden arguments, non-congruent operations, higher order parameterized programming (with modules parameterized by modules, and instianted with morphisms), sort constraints, and membership equational logic. In addition, BOBJ, like OBJ3, supports ordinary rewriting for order sorted equational logic (modulo attributes), as well as first order parameterized programming. BOBJ is written in pure Java and so should run on any machine.

The BOBJ homepage gives a less brief orientation to BOBJ, with links to pages containing many examples, and to papers containing theory; the website assumes some familiarity with OBJ3 and hidden algebra. You can also get the (more or less) most recent version of BOBJ from the BOBJ ftp site. WARNING: This ftp website now requires host authentication, so you probably cannot use it from a laptop over a wireless network.

CafeOBJ is a new generation algebraic specification language developed in Japan under the direction of Prof. Kokichi Futatsugi of the Language Design Lab at the Japan Advanced Inst of Science and Technology (JAIST); Prof. Futatsugi was one of the original developers of OBJ2. CafeOBJ preserves the distinctive useful features of OBJ3, including mix-fix syntax, subtyping by ordered sorts, modules with parameterized programming, and adds new features for hidden algebra, rewriting logic, and their combinations with order sorted algebra. This multi-paradigm approach has an elegant mathematical semantics based on multiple institutions, due to Razvan Diaconescu, as illustrated in the "CafeOBJ cube" below. Some theorem proving capabilities are also supported, including behavioral rewriting and attribute coinduction. The most comprehensive treatment of the language and system currently available can be found in:

CafeOBJ Report: The Language, Proof Techniques, and Methodologies for Object-Oriented Algebraic Specification, by Rãzvan Diaconescu and Kokichi Futatsugi, Volume 6 of AMAST series in Computing, World Scientific, 1998.

More information about CafeOBJ is available from the CafeOBJ homepage at JAIST, for which there is a mirror site in Romania; a CafeOBJ interpreter is available via these sites. In addition, CafeOBJ has a compiled mode, based on an abstract rewriting machine, with the same efficiency as modern functional programming systems. The CafeOBJ project is also building an environment intended to make formal methods available for ordinary software engineers. Some steps taken at UCSD towards this ambitious goal are outlined in Semiotics, Proof Webs and Distributed Cooperative Proving by Joseph Goguen and Akira Mori, as part of the Kumo Project. See also the short Press Release on UCSD work on the CafeOBJ project.

Maude
Maude incorporates most features of OBJ3, sometimes with small syntactic changes, and adds an implementation of rewriting logic, using a new and more powerful rewriting engine, and using the membership equational logic generalization of order sorted equational logic. The Computer Science Lab at SRI International has a Maude homepage; see also the SRI CSL rewriting logic homepage.

Some Systems Built Using OBJ
Systems built using OBJ3 include those listed below. OBJ3 is convenient for this kind of development because of its capability for "user defined builtins" provided in Lisp code, and BOBJ is convenient because it is written in pure Java.
Kumo and the Tatami Project
BOBJ is used in the Tatami project, which is developing the Kumo proof assistant and proof website generator. More information about this project is given by the following:

CASL and CoFI
A group called "CoFI", consisting (largely) of European theoretical computer scientists has designed and built a "common" algebraic specification language, called "CASL". Major participants include: Bernd Krieg-Bruckner, who designed the Ada module system (much influenced by OBJ), Peter Mosses, Don Sanella, Till Mossakowsky, Maura Cerioli, Michel Bidoit, and Andre Tarlecki. Although it is not clear that they would like CASL to be called a descendent of OBJ, it certainly does have significant similarities to OBJ3. The latest design documents can be found at:
www.cofi.info/CASL.html
To systems index page
Maintained by Joseph Goguen
Last modified: Fri Dec 30 12:11:33 PST 2005