Tatami Conventions
The style guidelines below have been developed for the proof websites
generated by Kumo, with the aim of making proofs much easier to understand
than is usual. To clarify the discussion, we distinguish between abstract
proofwebs and display proofwebs; the first contains only proof
information, while the second also includes display information. We will use
the word unit for any block of information of the same kind within a
display proofweb.
- A homepage is provided for each major proof part; these serve
to introduce and motivate the problem to be solved and the approach taken to
the solution.
- Tatami pages are the basic constituents of display proofwebs;
each tatami page has one or more proof units showing its inference
rule applications, interleaved with one or more explanation units; it is
feasible to have both on the same web page because there should only be a
small number of proof steps per page (about 7 non-automatic rules works
well). Tatami pages are also called "proof pages."
- The explanation units of tatami pages are prover-supplied
informal discussions of proof concepts, strategies, obstacles, etc.; these
may contain graphics, applets, and of course text.
- Tatami pages can be browsed in an order designed by the prover to be
helpful and interesting to the reader; if possible, these pages should tell a
story about how obstacles were overcome (or still remain); this order will be
called the narrative order. (See Notes on Narrative for
more information on the theory of narrative used here.)
- Major proof parts, including lemmas, have their own subwebsites, each
with the same structure as the main proof, including homepage and explanation
units. These appear in a separate dedicated persistent popup window.
- Tatami pages also have associated formal proof scores, which appear in
another separate popup window when summoned from a tatami page. It is
convenient to have a separate window because users usually want to look at
the proof and explanation at the same time as the proof score. Readers can
also request proof score execution, and the result is then displayed in the
same window as the score, so that one can easily alternate between them.
(The proof score is sent to an OBJ server and the result is returned for
display.)
- Major proof parts can have an optional closing page, to sum up important
results and lessons; these appear in the same window as their tatami pages.
- Formal proof steps are automatically linked to pre-existing tutorial
background pages; e.g., each application of induction is linked to a webpage
that explains the kind of induction used. Tutorial pages have their own
dedicated persistent popup window.
- A menu of open subgoals appears on each homepage, and error messages are
placed on appropriate pages. In database mode, a summary of this information
may be seen in the status window, which is a specialized popup that reports
any currently open subgoals.
These conventions have the effect of integrating proofs with the
information that is needed to motivate, understand and debug them; the
intention is to make proofs easier to do and to understand, and to display
information in a way that facilitates typical patterns of use.
The above material was taken from the overview paper Web-based Support for Cooperative Software
Engineering, by Joseph Goguen and Kai Lin, to appear in a special issue of Annals of
Software Engineering on multimedia software engineering, edited by Jeffrey
Tsai. An uncompressed postscript
version is also available. Systematic justifications for the Tatami
conventions, based on cognitive science, narratology, and algebraic semiotics,
may be found in this paper.
To the Tatami project homepage
Last modified: Thu Sep 27 11:24:11 PDT 2001