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