What's New on this site   -   and What's Cool on the web
The Tatami Project
LINKS for a Hidden World -- using Kumo  and   BOBJ
("LINKS" could be an acronym for something like "Library Information Network Knowledge System".)
The Tatami system supports distributed cooperative design, specification and validation of (software and/or hardware) systems, especially distributed concurrent systems. The Tatami system integrates formal with informal methods, has an online tutorial capability, runs over the web, and is intended to be useful to ordinary software engineers. The underlying formal logic is first order logic with atoms from hidden (order sorted) algebra. User interface design has been guided by algebraic semiotics and narratology, which are respectively the theories of signs and of stories.
Note: "Tatami" are natural fiber mats used in traditional Japanese buildings. The size of a room is measured by the number of tatami on its floor, where each tatami is a rectangle about 5 by 3 feet. Thus a 2 tatami room, like a 2 tatami proof, is pretty small, an 8 tatami room (or proof) is ok, but a 12 tatami room (or proof) is getting large, and should probably be subdivided. Tatami are cool, refreshing and aromatic; we hope you will find this metaphor helpful when creating and browsing proofs.


The figure above suggests how the Tatami system works; some components are clickable for further detail. The main components are the Kumo proof assistant and website generator ("kumo" is a Japanese word for spider), the tatami protocol, the barista generic proof server, the tatami database, the BOBJ behavioral specification language, and one or more proof engines, each with a server (the current implementation uses a slightly old version of BOBJ). Kumo assists multiple distributed users with design and validation, and automatically generates websites to document their work. Kumo reads commands written in the Duck language, reads specifications in the BOBJ language, checks proofs using proof engines, and then generates "proofweb" data structures in XML, which are then translated into HTML for proof documentation, based on the tatami conventions. Information is broadcast to other sites using the tatami protocol, and all local tatami databases (including truth values) are updated locally. Any standard web browser can be used to view the websites generated by Kumo, and to execute the proof scores on remote proof engines via barista servers.

We do not aspire to mechanize proofs like those of which mathematicians are justly so proud, but rather to provide support that is useful to practicing engineers for design, specification and validation. We also do not aspire to build powerful theorem provers to compete with existing provers like HOL, Nqthm, PVS and Otter; instead, we intend to re-use them.

For more detail, see Web-based Support for Cooperative Software Engineering, by Joseph Goguen and Kai Lin, in Annals of Software Engineering, volume 12, 2001; a pdf version is also available. See also the brief summary of results as of Sept. 2001, the brief report by Prof. Rod Burstall, and the one page progress summary for our NSF grant up to October 1999, Hidden Algebra and Concurrent Distributed Software, which appeared in Software Engineering Notes. A description of the previous Tatami system design appears in An Overview of the Tatami Project, which appeared in Cafe: An Industrial-Strength Algebraic Formal Method, edited by Kokichi Futatsugi, Tetsuo Tamai and Ataru Nakagawa, Elsevier, 2000, pages 61-78. Many further details are given in papers listed below.

Examples

A number of websites generated by Kumo have been organized to form a tutorial on our approach and some of its underlying technologies, including website generation, website design principles, proof by reduction, first order proof planning, hidden algebra (especially coinduction), interactive browsing, executing proof scores on remote proof servers, interactive Java applets illustrating key concepts of specifications and verifications, web-based tutorials on first order logic and hidden algebra, and explanation web pages for specs and major proof steps. (Of course, many proofs do not admit a picture or applet to illustrate the main ideas, or even of the result.) These websites were all generated completely automatically by Kumo, of course using files supplied by the user for specifications, explanations and goals. The use of Kumo guarantees that these proofs are completely formally correct. The Kumo demos homepage gives further information about Kumo and these examples:

  1. An inductive proof that 1+...+ n = n(n+1) / 2. This will give you a chance to explore Kumo's navigation and display conventions on a simple example.
  2. A coinductive proof of a behavioral property of a simple flag object. This illustrates some basics of hidden algebra on a very simple example, including an especially clear explanation of the need for behavioral properties.
  3. Two proofwebs for some familiar inductive properties of lists. The first was generated by a duck score written at the beginning of this effort; it is striking that the lemmas needed to complete the proof can be deduced from the way that successive proof attempts fail. The second proofweb succeeds, and was generated by a duck score derived from the first just by reordering its goals so that the lemmas that were found necessary are proved first.
    1. This early attempt at proving that the reverse of the reverse of a list is the original list, takes a direct approach, and its explanations emphasize the way that the two lemmas that are needed to complete the proof can be deduced from the output produced by unsuccessful proof attempts; one of these lemmas is the associativity of append.
    2. Here are the complete proofs for all three inductive properties of lists, including the two lemmas that are needed to establish the main goal.
  4. A coinductive proof of the behavioral correctness of the array-with-pointer implementation of stack. This behavioral refinement proof requires introducing a non-trivial lemma, which can also be inferred from a prior proof attempt that fails without it.
  5. A behavioral refinement proof of the correctness of implementing sets with lists, using attribute coinduction.
  6. A simple inductive proof of a formula for the sum of the squares of the first n natural numbers. This example is deliberately very spare, and in particular has no explanations, in order to illustrate the default conventions that Kumo uses when a user supplies only the absolute minimum input.
  7. A detailed proof that the square root of 2 is irrational, illustrating the first order capabilities of Kumo. Note that this uses and proves many auxiliary lemmas; see the directory listing. Note that no explanations have as yet been provided for this proof or its parts.
The first example proves a simple formula about natural numbers, illustrating the use of simple first order logic and induction. The second example proves a simple property of a very simple software object, a flag, and illustrates some basic concepts of hidden algebra, including behavioral properties and coinduction. The third example proves the correctness of implementing a stack with a pointer and an array; this is more complex than the previous example, and uses more sophisticated coinduction techniques for refinement. The first and fourth examples use induction, but the fourth is considerably more complex, since it involves several inductive lemmas. The fifth example has a different flavor, because it uses operations with multiple hidden arguments. The seventh is a proof by contradiction, making heavy use of first order logic; it is quite different from other examples, and demonstrates the power of Kumo as a proof assistant.

For those who are interested in earlier stages of our research, we built a number of demo websites by hand, in order to explore the underlying principles and technologies. See the handmade demos homepage, which contains the following:

  1. An inductive proof that 1+...+ n = n(n+1) / 2.
  2. A coinductive proof of a behavioral property of a simple flag object.
  3. A coinductive proof of correctness of implementing stack by pointer and array.
  4. A large compiler correctness proof using both induction and coinduction, with a complex specification and many lemmas.
One noticable difference from the new Kumo generated proofs is that they lack a status window popup; however, this will eventually be added; the new Kumo websites also have better format and other features. The fourth example is a compiler correctness proof that uses both induction and coinduction, with complex specifications and many lemmas; this industrial scale example also illustrates how proofs that are partly informal can be supported.

An intermediate stage between the examples produced by the current Kumo system and the hand made examples, is represented by the examples in the old Kumo demos homepage:

  1. An inductive proof that 1+...+ n = n(n+1) / 2.
  2. A coinductive proof of a behavioral property of a simple flag object.
  3. A proof of behavioral correctness of the array-with-pointer implementation of stack, using coinduction.
  4. An inductive proof that the reverse of the reverse of a list is the list, with some lemmas, including that append is associative.
  5. A behavioral refinement proof of the correctness of implementing sets with lists, using attribute coinduction.
  6. A first order logic proof that the square root of 2 is irrational.
  7. An inductive proof of a formula for the sum of the squares of the first n natural numbers.
  8. A coinductive correctness proof for the tatami protocol, which maintains the consistency of distributed cooperative proofs that are built using the Tatami system.
We believe that the newer Kumo user interface is better, and in addition, we have taken advantage of improved logical capabilites in Kumo in the proofs in the new Kumo demos homepage.
Organization

This project is supported by the National Science Foundation, and was previously supported by the CafeOBJ Project at JAIST (Japan Advanced Institute of Science and Technology), organized by Prof. Kokichi Futatsugi of JAIST. See also the UCSD CafeOBJ homepage and the IPA (Japan) homepage. Other participants in the CafeOBJ project included: Mitsubishi Research Institute, NEC, SRA and Unisys in Japan; SRI International in Menlo Park, California; the Technical University of Munich in Germany; and the University of Paris at Orsay.

Personnel Visitors include: Alumni and close friends of the project include:
More details

The use of web technologies to display designs and validations of software systems is novel, as is the use of algebraic semiotics for interface design; see Social and Semiotic Analyses for Theorem Prover User Interface Design for details of how designs for the status window were improved by using semiotic morphisms. Examples in the library range from simple illustrations of basic techniques to large scale validations of real running systems, so that the novice can gradually become more expert. The formal proofs use hidden algebra and various kinds of coinduction, which are believed easier to apply than more traditional approaches like process algebra and transition systems, because they exploit algebraic laws about methods and attributes that are not available in these methods. The BOBJ language is used both for specifications and as a proof engine, to dispose of the boring details of proofs. BOBJ is a behavioral extension of the specification aspect of OBJ3.

The following material related to this project is available:

More links
Some Software Used in the Kumo System
To the UCSD Meaning and Computation Lab homepage
To the research projects homepage
Maintained by Joseph Goguen
Largely written by May 2002; somewhat updated March 2005