Kumo, BOBJ, and Behavioral
Good implementations often fail to strictly satisfy their specifications,
but instead satisfy them only "behaviorally," in the sense of appearing to
satisfy them under all members of a certain set of "experiments".
Consequently behavioral specifications and behavioral proofs can often be
simpler than ordinary specs and proofs. BOBJ is a new member of the OBJ
family, which supports behavioral algebraic specification by providing a
language, an interpreter, and some algorithms, while the Kumo system extends
this to first order behavioral logic, and in addition, generates interactive
websites that document the proofs that it produces. We give overviews of BOBJ
and Kumo, and of hidden algebra, which is the formal foundation for these
systems, using a number of examples; we also describe some principles used in
building these systems, including parameterized programming and algebraic
The purpose is to introduce the following:
- The BOBJ language and system, including its design, its implementation,
and its practical use.
- The Kumo system, including its design principles, its implementation,
and its practical use.
- The motivation for, and some basics of, the algebraic approach to
behavioral specification and verification, especially for distributed
- Some motivation for and basics of algebraic semiotics, in connection
with the design of the websites that are generated by Kumo.
- Basic algebraic specification: signatures, equations, algebras,
deduction, specifications, satisfaction, and modules, with many examples in
- Implementation of algebraic specification by term rewriting in BOBJ.
- Structured semi-formal proofs in BOBJ, with examples, including
- Behavioral specification: experiments, contexts, algebras, satisfaction,
and coinduction, with examples in BOBJ.
- First order behavioral logic, and its implementation in Kumo, with
- Design principles of BOBJ and Kumo, especially parameterized programming,
and the combination of initial, loose, and behavioral specification.
- Algebraic semiotic principles for the user interface design of Kumo.
- The Kumo examples homepage, at http://www.cs.ucsd.edu/groups/tatami/kumo/exs/,
provides a leisurely stroll through a number of interactive examples, forming
a tutorial on Kumo and hidden algebra, motivating the use of a behavioral
approach, and introducing some basics of the theory.
- The BOBJ homepage, at http://www.cs.ucsd.edu/groups/tatami/bobj/,
has links to a number of interesting examples, illustrating features of BOBJ,
especially coinduction, cobases, and the circular coinductive rewriting
- More theoretical material on hidden algebra may be found on the hidden
algebra homepage, at http://www.cs.ucsd.edu/users/goguen/projs/halg.html.
- Finally, some cognitive and social science principles that drove the
design of Kumo (and to a lesser extent, of BOBJ), including the sociology of
proving and algebraic semiotics, are discussed in the web essay What is a
proof? and on the algebraic semiotics homepage, at http://www.cs.ucsd.edu/users/goguen/papers/proof.html,
- Web-based Support for Cooperative Software Engineering, by Joseph
Goguen and Kai Lin, Annals of Software Engineering, volume 12, 2001, a
special issue on multimedia software engineering, edited by Jeffrey Tsai.
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. Available at http://www.cs.ucsd.edu/users/goguen/pps/taiwanj.ps.
- What is a Proof? by Joseph Goguen. An informal essay written for
the UCSD user interface design course, which uses philosophy and sociology of
mathematics to motivate the unusual notion of proof used in Kumo. Available
- Circular Coinductive Rewriting by Joseph Goguen, Grigore Rosu and Kai Lin, in Proceedings, Automated
Software Engineering '00 (Grenoble France), September 2000, IEEE, pages
123-131. Using many examples, this paper introduces the BOBJ system for
behavioral specification and computation, and its surprisingly powerful
circular coinductive rewriting algorithm for behavioral equalities, combining
behavioral rewriting with circular coinduction. Available at http://www.cs.ucsd.edu/users/goguen/ps/ccrw.ps.
- Behavioral and Coinductive Rewriting, by Joseph Goguen, Kai Lin,
and Grigore Rosu. Keynote address, in Proceedings, Rewriting Logic
Workshop, 2000 (Kanazawa, Japan), edited by Kokichi Futatsugi, Japan
Advanced Institute of Science and Technology, September 2000, pages 1-22. An
informal summary, with simulated behavioral rewriting via standard rewriting,
and circular coinductive rewriting. Available at http://www.cs.ucsd.edu/users/goguen/ps/rwl00.ps.gz.
- A Protocol for Distributed Cooperative Work, by Joseph Goguen and
Grigore Rosu, in
Proceedings, Workshop on Distributed Systems (Iasi, Romania), September
1999, and in Springer Electronic Notes in Computer Science, Volume 28,
1999, pages 1-22. Contains a concise summary of an earlier version of hidden
algebra, and applies it to proving correctness of a novel internet broadcast
protocol for synchronous distributed cooperative proving. Available at http://www.cs.ucsd.edu/users/goguen/ps/iasi.ps.gz.
- Hidden Algebra for Software Engineering, by Joseph Goguen, in
Combinatorics, Computation and Logic, Proceedings, Conference on
Discrete Mathematics and Theoretical Computer Science, (University of
Auckland, New Zealand, 18-21 January 1999), edited by Cristian Calude and Michael
Dinneen, Australian Computer Science Communications, Volume 21, Number
3, Springer, pages 35-59, 1999 (keynote address). A gentle but somewhat out
of date introduction to hidden algebra, with simple examples, much motivation,
and some history. Available at http://www.cs.ucsd.edu/users/goguen/pps/dmtcs.ps.