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:
- some are used for data values (e.g., of attributes), as in the algebraic
approach to data types; and
- others are used for states, as in the algebraic approach to abstract
machines.
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.
- Behavioral and non-behavioral operations are distinguished; the former
are called congruent.
- Behavioral operations may have more than one hidden argument.
- Cobases can be used in coinduction, dual to the notion of basis
for induction; when well chosen, they can greatly simplify proofs.
- Automatic cobasis generation is provided (though users can also
define their own), using congruence criteria that take account of the
special role of the untupling operation in concurrent connection.
- Rules for equational deduction and coinduction have been developed for
these generalizations.
- An institution has been developed for hidden algebra to captures all
these generalizations; it differs from prior institutions in treating
congruent operations as sentences rather than as part of the signature.
- Circular coinductive rewriting has significantly extended the
power of coinductive proofs, by combining coinduction, hidden rewriting, and
cobasis generation.
- A Case analysis capability has been added to the circular
coinductive rewriting algorithm.
The bullets below concern the BOBJ
implementation, which has all of the above, plus the following:
- Cobases are treated as first class citizens (i.e., they can be declared
and named).
- Sort declarations, a feature of order sorted algebra that allows the
equational definition of subsorts, are supported.
- Second order parameterized programming is implemented, including
parameterized views, and passing parameterized modules as parameters.
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
- Behavioral Verification of Distributed
Concurrent Systems with BOBJ, by Joseph Goguen and Kai Lin. Text of
keynote lecture for Conference on
Quality Software, Dallas TX, 5-6 November 2003. In Proceedings,
Conference on Quality Software, IEEE Press 2003, pages 216-235. Some slides are also available, although they are
much more technical than the talk that was actually given. The paper proves
correctness of the alternating bit protocol making strong use of recent
features of BOBJ, especially conditional
circular coinductive rewriting with case analysis. An early version of this
paper is A Hidden Proof of the Alternating Bit
Protocol, by Kai Lin and Joseph Goguen.
See also the brief early web note Correctness of the Alternating Bit
Protocol, and proof sketch for the Petersen Critical Section Algorithm.
- Semiotic Morphisms, Representations, and
Blending for User Interface Design, by Joseph Goguen. Keynote
lecture, in Proceedings,
AMAST Workshop on Algebraic Methods in Language Processing, AMAST
Press, 2003, pages 1-15 (held Verona, Italy, 25 - 27 August 2003). This
paper extends algebraic semiotics to handle interaction by using hidden
algebra; some examples are given in detail. A pdf
version of the paper, and the slides
for the talk are also available (you may have to change the orientation to
swap landscape).
- Conditional Circular Coinductive
Rewriting with Case Analysis, by Joseph Goguen, Kai Lin and Grigore
Rosu, in Recent Trends in Algebraic Development Techniques,
Springer Lecture Notes in Computer Science, volume 2755, 2004, pages 216-232;
proceedings of 16th Workshop on
Algebraic Development Techniques, Frauenchiemsee, Germany, 24-27
September 2002. Slides for the lecture version are also available, Conditional Circular Coinductive Rewriting
(Note: You may have to reorient to "seascape"), as is the two page abstract,
Conditional Circular Coinductive
Rewriting, by the same authors. This paper extends BOBJ's circular
coinductive rewriting algorithm to conditional equations and "splits" for
case analyses. Postscript version also
available. Note: This version does not have proofs.
- A Hidden Herbrand Theorem: Combining the
Object, Logic and Functional Paradigms, by Joseph Goguen, Grant Malcolm, and Tom Kemp,
Journal of Logic and Algebraic Programming, Volume 51, 2002, pages
1-41. Shows how to combine the logic and object paradigms using hidden
algebra with existential quantifiers. This is a journal version of a paper
in Principles of Declarative Programming, edited by Catuscia
Palamidessi, Hugh Glaser and Karl Meinke (Proceedings of PLIP/ALP'98
[Programming Languages, Implementations, Logics and Programs / Algebraic and
Logic Programming], Pisa, Italy, 14-19 September 1998), Springer Lecture
Notes in Computer Science, Volume 1490, pages 445-462. (The paper was
completed in 2001, and uses an older version of hidden algebra.) Compressed postscript and postscript versions are also available.
- Web-based Support for Cooperative
Software Engineering, by Joseph Goguen and Kai Lin. To in Annals of Software
Engineering, volume 12, 2001, a special issue on multimedia software
engineering, edited by Jeffrey Tsai. An pdf
version is also available. 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. The paper is a revised and expanded
version of the paper Web-based Multimedia
Support for Distributed Cooperative Software Engineering, by Joseph Goguen and Kai Lin, which
appeared in Proceedings, International Symposium on Multimedia Software
Engineering, edited by Jeffrey Tsai and Po-Jen Chuang, IEEE Press, pages
25-32; this meeting was held in Taipai, Taiwan, December 2000.
- 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. A somewhat informal summary, including simulating
behavioral rewriting with standard rewriting, and circular coinductive
rewriting; the latter is a surprisingly effective algorithm for proving
behavioral equalities.
- 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 proving behavioral
equalitites, which combines behavioral rewriting with circular coinduction.
There is also a compressed postscript version.
- Circular Coinduction by Grigore Rosu and Joseph
Goguen, in Proceedings, International Joint Conference on Automated
Deduction, Sienna, June 2001. This paper provides the full proof of
correctness of circular coinduction, and draws some consequences, including
various congruence criteria.
- Slides for a lecture Towards the
Automation of Behavioral Reasoning, given by Joseph Goguen at a
meeting of IFIP WG 1.3
(Foundations of System Specification), at Stanford University on 30 June 2000;
based on joint work with Kai Lin and Girgore Rosu, the slides summarize recent
work on hidden algebra, especially the paper Circular Coinductive Rewriting by Joseph Goguen,
Kai Lin, and Girgore Rosu.
- An Overview of the Tatami Project,
by Joseph Goguen, Kai Lin, Grigore Rosu, Akira Mori and Bogdan Warinschi, in
Cafe: An Industrial-Strength Algebraic Formal Method, edited by Kokichi
Futatsugi, Tetsuo Tamai and Ataru Nakagawa, Elsevier, 2000, pages 61-78. This
paper is a high level snapshop of the UCSD Tatami
project as of late November 1999.
- Hidden Algebra and Concurrent Distributed
Software, in Software
Engineering Notes, volume 25, number 1, page 51, January 2000. A one
page summary of progress on our NSF grant up to mid October 1999.
- A Protocol for Distributed Cooperative
Work, by Joseph Goguen and Grigore Rosu, in Proceedings,
Workshop on Distributed Systems (Iasi, Romania), September 1999, and in
Elsevier Electronic Notes in Computer Science, Volume 28, 1999, pages
1-22. Contains a concise summary of the previous version of hidden algebra,
and applies it to the correctness of a novel internet broadcast protocol
designed to support synchronous distributed cooperative proving. Final
revision 27 July 1999.
- Hiding More of Hidden Algebra, by
Joseph Goguen and Grigore Rosu , in FM`99 - Formal
Methods, Proceedings of World Congress on Formal Methods (Toulouse,
France, August 1999), Springer Lecture Notes in Computer Science, Volume 1709,
pages 1704-1719. New results relating information hiding to hidden algebra,
and some compelling examples of behavioral operations with multiple hidden
arguments.
- Hidden Congruent Deduction, by Grigore Rosu and Joseph Goguen, in
Automated Deduction in Classical and Non-Classical Logics, edited by
Ricardo Caferra and Gernot Salzer, Lecture Notes in Artificial Intelligence,
Volume 1761, pages 252-267, 2000. Preliminary version in Proceedings,
First-Order Theorem Proving - FTP'98, edited by Ricardo Caferra and Gernot
Salzer, Technische Universitat Wien, pages 213-223, 1998 (proceedings of a
workshop held at Schloss Wilhelminenberg, Vienna, November 23-25, 1998). The
complete proceedings are available
on the web, and by ftp. This
paper extended all the main notions and results of hidden algebra to
operations that may have more than one hidden argument, and also introduced
the notion of cobasis, gave criteria for operations to be congruent, and
introduced more powerful rules of deduction.
- Hidden Algebra for Software
Engineering, 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 compressed postscript version is also available. A
gentle introduction to hidden algebra, with simple examples, much motivation,
and some history. Completed 8 November 1998.
- A Hidden Agenda, by Joseph Goguen and Grant
Malcolm, Theoretical Computer Science, vol 245, no 1, pages 55-101,
August 2000, special issue on Algebraic Engineering, edited by Chrystopher
Nehaniv and Masami Ito; a compressed postscript
version is also available. This is an early basic paper on hidden
algebra, treating coinduction, nondeterminism, concurrency and more. An even
earlier version is UCSD Technical Report
CS97-538, April 1997, and an obsolete abstract is in Proceedings
of Workshop on New Mathematics for Computer Science, in Conference on
Intelligent Systems: A Semiotic Perspective (National Institute of Standards
and Technology, Gaithersberg MD, 20-23 Oct 1996) pages 159-167. Last modified
29 January 1999.
- Hidden Coinduction, by Joseph Goguen and Grant
Malcolm, in Mathematical Structures in Computer Science, 9, number
3, pages 287-319, June 1999; this is a sister paper to A Hidden
Agenda.
- Hidden Algebraic Engineering, by
Joseph Goguen, in Algebraic Engineering, edited by Chrystopher Nehaniv
and Masami Ito, World Scientific, 1999, pages 17-36; also UCSD Technical
Report CS97-569, December 1997, and preliminary version in Proceedings,
Conference on Semigroups and Algebraic Engineering, edited by Chrystopher
Nehaniv (Aizu-Wakamatsu, Japan, 24-26 Mar 1997). This is a gentle
introduction to the original version of hidden algebra, with some examples and
much motivation.
- Towards an Algebraic Semantics for the
Object Paradigm, by Joseph Goguen and Rãzvan Diaconescu, in
Recent Trends in Data Type Specification, Proceedings of the 9th
Workshop on Abstract Data Types (Caldes de Malevella, Spain, 28 October 1992),
edited by Hartmut Ehrig and Fernando Orejas, Springer, Lecture Notes in
Computer Science, Volume 785, 1994, pages 1-29. Although this is an early
paper on hidden algebra, it includes an approach to inheritance, and details
of the categorical concurrent connection construction.
Background information on universal algebra and category theory can be
obtained from the following:
- Algebraic Semantics of Imperative
Programs, by Joseph Goguen and Grant Malcolm (MIT Press, 1996).
Contains entry level introductions to universal algebra and the OBJ3 language.
The paper An Executable Course in the
Algebraic Semantics of Imperative Programs discusses some pedagogical
innovations of this book.
- Two chapters from Theorem proving and Algebra, by Joseph Goguen, to
be published by MIT Press: Chapter 1, the Introduction and Chapter 8, First Order Logic, plus the References and the Table of
Contents. Chapter 8 is an elegant algebraic exposition of first order
logic, proof planning and induction; the treatment of induction is unusually
general. This book provides a systematic exposition of universal algebra and
its applications in computer science.
- Introducing OBJ, in Software
Engineering with OBJ: algebraic specification in action, edited by Joseph
Goguen and Grant Malcolm, Kluwer, 2000, pages 3-167. The OBJ3 user manual;
complete explanation of the language with many examples. (Revised and
extended in August 1999.)
- A Categorical Manifesto, in
Mathematical Structures in Computer Science, Volume 1, Number 1, March
1991, pages 49-67. Intuitive motivation for all the basic concepts of
category theory, with many computer science examples.
- What is Unification?, in
Resolution of Equations in Algebraic Structures, Volume 1: Algebraic
Techniques, edited by Maurice Nivat and Hassan Ait-Kaci (Academic Press,
1989) pages 217-261. An introductory exposition of some basic categorical
concepts.
- Stretching First order Equational Logic:
Proofs with Partiality, Subtypes and Retracts, in Proceedings,
International Workshop on First Order Theorem proving (Schloss Hagenbert,
Austria, 27-28 October 1997). Watch retracts at work and at play! See how
cute and useful they can be!
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.
- 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.)
- 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.
- 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.
- 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.
- Here are the complete proofs
for all three inductive properties of lists, including the two lemmas
that are needed to establish the main goal.
- 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.
- A behavioral refinement proof of the correctness of implementing sets with
lists, using attribute coinduction.
- 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.
- 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.
- 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
-
Incompleteness of Behavioral Abstraction, by Sam Buss and Grigore Rosu, in Proceedings,
Coalgebraic Methods in Computer Science (CMCS'00), Berlin, Volume 33,
Electronic Notes in Theoretical Computer Science, Springer, 2000.
-
Equational Axiomatizability for Coalgebra, by Grigore Rosu, in Theoretical Computer
Science, vol. 260, no 1/2, 2001. This is a revised version of a more
hidden algebra oriented paper, A
Birkhoff-like Axiomatizability Result for Hidden Algebra and
Coalgebra, Electronic Notes in Theoretical Computer Science
(Proceedings of CMCS '98, Lisbon, Portugal), Volume 11, 1998.
-
Behavioral Coinductive Rewriting, by Grigore Rosu, in Proceedings
OBJ/CafeOBJ/Maude Workshop at Formal Methods 99, Toulouse, France,
August 1999, pages 179-196.
-
Grothendieck Institutions, by Rãzvan Diaconescu, IMAR
Preprint 2-2000, ISSN 250-3638. Submitted to Journal of Applied
Categorical Structures.
-
Logical Foundations of CafeOBJ, by Rãzvan Diaconescu and Kokichi
Futatsugi. Submitted to Theoretical Computer Science. An overview of
the mathematical foundations of CafeOBJ, including its institutions.
-
CafeOBJ Jewels, by Rãzvan Diaconescu, Kokichi Futatsugi and Shusaku
Iida, in Cafe: An Industrial-Strength Algebraic Formal Method, edited
by Kokichi Futatsugi, Tetsuo Tamai and Ataru Nakagawa, Elsevier, 2000, pages
33-60. An overview of the main features and methodologies of CafeOBJ via a
collection of examples.
- Behavioural Coherence
in Object-Oriented Algebraic Specification, by Rãzvan
Diaconescu and Kokichi Futatsugi, J. Universal Computer Science,
6(1):74-96, Springer, 2000. Extends hidden algebra formalism with
behaviourally coherent operations.
- CafeOBJ Report:
The Language, Proof Techniques, and Methodologies for Object-Oriented
Algebraic Specification, by Rãzvan Diaconescu and Kokichi
Futatsugi, Volume 6 of AMAST series in Computing, World Scientific, 1998.
Contains the formal definition and semantics of CafeOBJ.
Some Future
Research
- There is not yet any systematic exposition of hidden order sorted
algebra; we would like to write a book on this topic; probably some
additional research is also needed.
- We would like to implement the active constraint object paradigm
that is described in A Hidden Herbrand
Theorem: Combining the Object, Logic and Functional Paradigms, by
Joseph Goguen, Grant Malcolm,
and Tom Kemp, in Journal of Logic and Algebraic Programming,
Volume 51, 2002, pages 1-41.
- Circular Coinductive Rewriting
with Case Analysis is very powerful, but the implementation needs to
provide users with feedback when cases fail, since this may be due to the
case being true but not provable without further lemmas.
Some Other
Links
- See the Behavior
Homepage for a list of all members of the Behavior Discussion List,
with links to their homepages whenever we could find them.
- Website of Grigore Rosu, at
University of Illinois, Urbana-Champaign.
- CafeOBJ is a new generation
algebraic specification language being developed in Japan with support from IPA (Japan). CafeOBJ supports hidden
algebra. The CafeOBJ project is lead by Prof Kokichi Futatsugi of JAIST (Japan). More information about
CafeOBJ, including its "cafeteria" mailing list, is available at the UCSD mirror site of the CafeOBJ homepage at Japan Advanced
Institute of Science and Technology (JAIST).
- Website of Grant Malcolm,
at the University of Liverpool.
- Website of Razvan Diaconescu at
Institute of Mathematics of the Romanian Academy; neat stuff on the constraint
paradigm, behavioral rewriting logic, and more.
- Website on algebraic
semantics at Oxford, including links for work of Grant Malcolm, Corina
Cirstea, James Worrell, Simone Veglioni, Sula Ma, and Andrew Stevens.
- Website of Horst Reichel
at Dresden; neat stuff on coalgebraic semantics for the object paradigm.
- Website of Peter Padawitz at
Universitaet Dortmund, Germany; behavioral deduction and declarative
programming in his "swinging
types" framework.
- Website of Bart Jacobs at
Nijmegen, the Netherlands (formerly CWI, Amsterdam); more neat stuff on
coalgebraic semantics for the object paradigm, and also for hybrid systems.
- Website of Oscar Nierstrasz
at Bern, Switzerland (formerly at Geneva); much interesting information and
links on object oriented systems and software composition.
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