- Introduction
- OBJ3
- BOBJ
- CafeOBJ
- Maude
- Systems Built Using OBJ3
- Kumo and the Tatami Project
- CASL and CoFI

"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 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,

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.

- Perhaps the best general introduction to OBJ is
**Algebraic Semantics of Imperative Programs**(see left), by Joseph Goguen and Grant Malcolm, MIT Press, 1997; ISBN 0-262-07172-X. - A detailed treatment of the use of OBJ in education is given 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. - The official OBJ3 manual, with much tutorial material and many examples,
as revised and extended August 1999, is
*Introducing OBJ*by Joseph Goguen, Timothy Winkler, José Meseguer, Kokichi Futatsugi and Jean-Pierre Jouannaud, which appears in**Software Engineering with OBJ: algebraic specification in action**, edited with Grant Malcolm, Kluwer, 2000, ISBN 0-7923-7757-5. This book also includes several case studies on the use of OBJ; its Introduction with a table of contents, and the paper*More Higher Order Programming with OBJ3*, are also available online. Also, pdf and gzip compressed postscript versions of the manual are available. - The OBJ3 Survival Guide gives basic hints to help new users get over the hump in the learning curve.

- Syntax and semantics of a simple programming language
- Term unification
- Proof of a property of maps on lists
- The lambda calculus
- OBJ is used in the Kumo proof assistant and website generator system.
- Lutz Hamel built an optimizing compiler TRIM
for OBJ and proved it correct using hidden algebra; see
*Towards a Provably Correct Compiler for OBJ3*by Lutz Hamel and Joseph Goguen for an earlier version of this work.

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

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, a proof assistant for first order hidden logic, which also generates websites that document its proofs. Kumo uses BOBJ, not OBJ3.
- FOOPS, a declarative object oriented language built on top of OBJ3.
- TOOR, a requirements management system built on top of FOOPS.
- Eqlog, a logic programming language, implemented by enriching OBJ3 with order sorted unification and backtracking.
- OOZE, an object oriented version of Z built on top of FOOPS.
- 2OBJ, a theorem prover (for any user definable logic) built using OBJ3.

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:

*Conditional Circular Coinductive Rewriting*, by Joseph Goguen, Kai Lin and Grigore Rosu, slides for a lecture given at the**16th Workshop on Algebraic Development Techniques**, Frauenchiemsee, Germany, 24-27 September 2002. (Note: You may have to reorient to "seascape".) See also the two page abstract,*Conditional Circular Coinductive Rewriting*, by the same authors, for a paper in preparation, extending BOBJ's circular coinductive rewriting algorithm to conditional equations, and allowing "splits" for case analyses.

*Web-based Support for Cooperative Software Engineering*, by Joseph Goguen and Kai Lin. In**Annals of Software Engineering**, volume 12, 2001, a special issue on multimedia software engineering, edited by Jeffrey Tsai. A gzipped postscript version is also available. This is an overview of the Tatami project, featuring version 4 of the Kumo proof assistant and website generator, and focusing on its design decisions, its use of multimedia web capabilities, and its integration of formal and informal methods for software development in a distributed cooperative environment.*An Overview of the Tatami Project*, by Joseph Goguen, Kai Lin, Grigore Rosu, Akira Mori and Bogdan Warinschi, to appear in**Cafe: An Industrial-Strength Algebraic Formal Method**, edited by Kokichi Futatsugi, Tetsuo Tamai and Ataru Nakagawa, Elsevier, 2000. This paper is a high level snapshop of the UCSD Tatami project as of late November 1999. See also the one page summary of progress on our NSF grant up to October 1999,*Hidden Algebra and Concurrent Distributed Software*, in**Software Engineering Notes**, volume 25, number 1, January 2000.*A Protocol for Distributed Cooperative Work*, by Joseph Goguen and Grigore Rosu, in**Proceedings, Workshop on Distributed Systems**, Iasi, Romania, September 1999, and to appear in Springer Electronic Notes in Computer Science, Volume 28. Contains a concise summary of the previous version of hidden algebra, and applies it to the correctness of a novel internet broadcast protocol designed to support synchronous distributed cooperative proving.*Tools for Distributed Cooperative Engineering*, by Joseph Goguen, Kai Lin, Akira Mori and Grigore Rosu. Describes how the Tatami system and the Kumo proof assistant and website generator integrate formal and informal methods for software development, in a distributed cooperative environment. A verification step can be supported by the scan of and envelope back, a diagram or applet, as well as a fully formal subproof. In**Proceedings, CafeOBJ Symposium**(26-29 April 1998, Kyoto, Japan).*Distributed Cooperative Formal Methods Tools*, by Joseph Goguen, Kai Lin, Akira Mori, Grigore Rosu and Akiyoshi Sato. Overview of Tatami project tools and methods, including hidden algebra and algebraic semiotics, with examples.**Proceedings, Automated Software Engineering**(Lake Tahoe NV, 3-5 Nov 1997), IEEE, pages 55-62.*Algebraic Semiotics, ProofWebs and Distributed Cooperative Proving*, by Joseph Goguen, Akira Mori and Kai Lin. Describes the Tatami ProofWeb data structure and the Kumo proof assistant and website generator system, plus methods from semiotics used in their design, with examples. In**Proceedings, User Interfaces for Theorem Provers**(Sophia Antipolis, France, 1-2 Sept 1997), pages 25-34.*The Tatami System Design and its Motivation*, by Joseph Goguen, is a very brief informal description of the for the Tatami system, with some motivation, now rather outdated.*Social and Semiotic Analyses for Theorem Prover User Interface Design*, by Joseph Goguen, in**Formal Aspects of Computing**, volume 11, pages 272-301, 1999. Presents a systematic justification of the style guidelines for the proof websites generated by Kumo, based on algebraic semiotics, narratology, cognitive science, etc.

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