Hidden Algebra Homepage
Contents
A Brief Overview of Hidden Algebra

Hidden algebra aims to give a semantics for software engineering, and in particular for concurrent distributed object systems, supporting correctness proofs that are as simple and mechanized as possible. This emphasis on effective proofs rather than semantic modelling is supported by taking a calculational approach based on equations, rather than one based on, for example, higher order logic, type theory, denotational semantics, or any particular kind of model or set theory, because equational proofs achieve maximal simplicity and mechanization, while still allowing adequate expressiveness. It is also convenient that the models of a hidden algebraic specification are precisely its possible implementations.

Hidden algebra effectively handles the most troubling features of large systems, including concurrency, distribution, nondeterminism, and local states, as well as the usual features of the object paradigm, including classes, subclasses (inheritance), attributes and methods, in addition to supporting logical variables (as in logic programming), abstract data types, generic modules and more generally, the very powerful module system of prameterized programming. Hidden algebra generalizes the process algebra and transition system approaches to include non-monadic operations, so that it can take advantage of equations involving methods and attributes parameterized by data; this extra power can also dramatically simplify proofs. Coinduction methods appear to be more effective for behavioral properties (including behavioral refinement) than any alternative of which we are aware, and moreover, they can be automated to a very significant degree.

The hidden algebra approach takes as basic the notion of observational abstraction, or more precisely, behavioral satisfaction: this means that hidden specifications characterize how objects (and systems) behave in response to a given set of experiments, rather than how they are implemented; this provides a version of what is called a behavioral type in the object oriented jargon, but which we prefer to call a hidden theory, behavioral theory, or hidden specification. A hidden correctness proof for a refinement (or implementation) shows that one hidden theory behaviorally satisfies another, in the sense that any model of the second theory yields a model of the first; however, the formal proof is algebraic, not model-based. Successive refinement of designs is a useful model of software development, which avoids the unproductive "semantic swamp" of verifying actual code.

The Kumo examples homepage is designed to serve as a basic tutorial for both hidden algebra and the Kumo system which implements it, but the following remarks may also be helpful. Sorts are used in two distinct ways in hidden algebra:

The latter give objects. These two uses for sorts are dual: induction is used to establish properties of data types; while coinduction is used to establish (behavioral) properties of objects with states. Similarly, initiality is important for data types, while finality is important for states. However, we do not insist that implementations of abstract machines (or objects) must be final; on the contrary, we accept any implementation that satisfies the given axioms. This is important because in general, the most efficient implementations are neither initial nor final, but somewhere between. Moreover, hidden algebra's generality is such that final models may not even exist (this is because we allow operations with multiple hidden arguments).

Because we use hidden sorts to specify classes of objects, order sorted algebra provides a very natural way to handle inheritance; it also allows specifying partial recursive functions, partially defined functions, subtypes of various kinds, error definition and recovery, coercions and multiple representations. The module system of parameterized programming gives us other forms of inheritance, plus all the power of higher order functional programming in a first order setting which makes both proofs and programming easier. The most important results in hidden algebra justify efficient proof techniques based on coinduction. We consider hidden algebra to be the natural next step in the evolution of algebraic specification.

Some relatively recent developments in coinduction are described in Behavioral Verification of Distributed Concurrent Systems with BOBJ, by Joseph Goguen and Kai Lin; there is also a postscript version; in particular, the BOBJ system c4rw algorithm for proving behavioral properties by a combination of behavioral rewriting with circular coinduction and case analysis is described; the main example is a correctness proof of the alternating bit protocol. A more detailed discussion of the algorithm may be found in Conditional Circular Coinductive Rewriting with Case Analysis, by Joseph Goguen, Kai Lin and Grigore Rosu, though most proofs are omitted there. (Detailed citations for these papers in given in the Brief Hidden Bibliography section below). The paper Specifying, Programming and Verifying with Equational Logic, to appear in Festschrift volume for Dov Gabbay, discusses mutual coinduction, and illustrates it with inductive proof schemes; two theoretical contributions are a new formalization of logical programming, and a new semantics for higher order modules. A postscript version is also available, as are versions in the much more voluminous format of the book, in pdf and postscript.

An interesting application to verifying the Kumo distributed proof protocol is given in A Protocol for Distributed Cooperative Work, by Joseph Goguen and Grigore Rosu, with a brief summary of the main definitions and results in an earlier framework. A relatively leisurely introduction to some main concepts is in Hiding More of Hidden Algebra by Joseph Goguen and Grigore Rosu.

A high level snapshot of the UCSD Tatami project as of late September 2000 may be found in Web-based Multimedia Support for Distributed Cooperative Software Engineering, by Joseph Goguen and Kai Lin; a snapshot as of November 1999, with more emphasis on the web-based user interface, may be found in An Overview of the Tatami Project, by Joseph Goguen and Kai Lin, Grigore Rosu, Akira Mori and Bogdan Warinschi; see also the one page summary of progress on our NSF grant up to mid October 1999, Hidden Algebra and Concurrent Distributed Software, in Software Engineering Notes, volume 25, number 1, page 51, January 2000.

A web-based tutorial on hidden algebra (though written for an early version of hidden algebra) is available, with pages on over 20 different topics, including links to background material on many sorted algebra and first order logic, although the version of hidden algebra used there is now out of date.

A Behavior Discussion List has been formed to facilitate progress on behavioral aspects of computer science and mathematics, including, but not limited to, versions of hidden algebra and behavioral equational logic, observational logic, and coalgebra, as well as systems that support them, such as CafeOBJ and Kumo. There is also a Behavior Homepage, which lists all members of the Behavior Discussion List, with links to their homepages whenever we could find them.

Hidden algebra is also implemented in CafeOBJ, a new generation algebraic specification system developed in Japan under the direction of Prof. Kokichi Futatsugi at Japan Advanced Inst of Science and Technology (JAIST). CafeOBJ preserves the distinctive useful features of OBJ3 with a different syntax, and adds new features for hidden algebra, rewriting logic, and their combinations with order sorted algebra. A somewhat more general version of hidden algebra is implemented in the BOBJ system, supporting circular coinductive rewriting with case analysis, automatic cobasis generation, and concurrent connection, for behavioral operations with multiple hidden arguments. The Kumo system provides theorem proving capability for full first order hidden logic, and in addition generates websites that document proofs done using it.

Latest Hidden Results

Hidden algebra has developed greater generality and more effective proof techniques through a series of steps, which are summarized in the bullets below, and are described in detail in our publications.

The bullets below concern the BOBJ implementation, which has all of the above, plus the following: The Kumo behavioral proof assistant and proof website generator is available over the web in browser mode; a number of examples plus some documentation can be found at the Kumo examples homepage; see the Online Interactive Examples section below for a list of all these examples. You can also get the (more or less) most recent version of BOBJ from the BOBJ ftp site.

A Brief Hidden Bibliography Background information on universal algebra and category theory can be obtained from the following:

Some Online Interactive Examples

The tatami project homepage gives a general introduction to the project, and includes links to the web-based interactive examples listed below. Although not all of these illustrate hidden algebra, it is advisable to visit them in the order given, since they were assembled as an integrated sequence for pedagogical purposes; these examples are linked to an online tutorial on hidden algebra (unfortunately an older version), which in turn is linked to background tutorials on first order logic and proof planning.

  1. An inductive proof that 1+...+ n = n(n+1)/2. This gives you a chance to explore Kumo's navigation and display conventions on a simple example. (Click on the "question mark" icon for navigation instructions.)
     
  2. A coinductive proof of a behavioral property of a simple flag object. This illustrates some basics of the hidden algebra approach on a very simple example; it includes an especially clear motivation for the necessity of 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 examining 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: No explanations have yet been provided.
     
  8. A coinductive correctness proof for the tatami protocol, which maintains the consistency of distributed cooperative proofs that are built using the tatami system (this was done using an older version of Kumo).
All these were generated by Kumo, which has been implemented by Kai Lin; Netscape 3.0 or later and some knowledge of hidden algebra will be needed to read them. Eventually the Java source code should be available for downloading via the Kumo homepage. Kumo is both a proof assistant and a proof website generator, though users must supply the specifications, goals, and explanations (if any). Using Kumo guarantees that the proofs are completely formally correct. Several of these examples also have illustrative Java applets, and there is live proof execution via a BOBJ server. Initial work on Kumo was supported by the large international CafeOBJ Project (see the CafeOBJ Press Release).

Some Related Papers on Other Sites
Some Future Research

Some Other Links
Return to the top of this page
To the research projects index page
Maintained by Joseph Goguen
Key Resource Award in Formal Methods given this site by Links2Go.
Last modified: Mon Oct 10 04:08:14 PDT 2005