• Abstract
• Objectives
• Topics
• Web Resources
• Some Literature

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

The purpose is to introduce the following:

1. The BOBJ language and system, including its design, its implementation, and its practical use.
2. The Kumo system, including its design principles, its implementation, and its practical use.
3. The motivation for, and some basics of, the algebraic approach to behavioral specification and verification, especially for distributed concurrent systems.
4. Some motivation for and basics of algebraic semiotics, in connection with the design of the websites that are generated by Kumo.

1. Basic algebraic specification: signatures, equations, algebras, deduction, specifications, satisfaction, and modules, with many examples in BOBJ.
2. Implementation of algebraic specification by term rewriting in BOBJ.
3. Structured semi-formal proofs in BOBJ, with examples, including induction.
4. Behavioral specification: experiments, contexts, algebras, satisfaction, and coinduction, with examples in BOBJ.
5. First order behavioral logic, and its implementation in Kumo, with examples.
6. Design principles of BOBJ and Kumo, especially parameterized programming, and the combination of initial, loose, and behavioral specification.
7. Algebraic semiotic principles for the user interface design of Kumo.

1. 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.
2. 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 algorithm.
3. 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.
4. 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, and http://www.cs.ucsd.edu/users/goguen/projs/semio.html, respectively.

1. 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.
    
2. 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 at http://www.cs.ucsd.edu/users/goguen/papers/proof.html.
    
3. 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.
    
4. 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.
    
5. 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.
    
6. 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.