Coinduction is a powerful technique for proving behavioral properties of (systems of concurrent interacting) objects. It generalizes the notion of bisimulation introduced by David Park in late 70's for labeled transition systems, a proof technique for a semantic notion introduced earlier by Robin Milner. Here we formulate coinduction as a proof rule.

Technically, coinduction is used to show that an equation is behaviorally satisfied by (all models of) some hidden specification. Thus if E is a set of hidden -equations, our proof goal has the form

E (X) t1 = t2,where X is some set of variables with their types, and t1, t2 are terms of (the same) hidden sort.

A coinductive proof of this goal must provide the following:

- A relation R defined on -terms with variables from X, called the
**candidate relation**. - A signature , whose elements are called
**generators**. - A signature , whose elements are called
**selectors**.

- R is a hidden -congruence;
- R is a hidden -congruence; and
- t1 R t2;

- + + must be a decomposition of .
- Any elements of and that are
*derived*within their own signature can be omitted (this notion is defined, and the result is proved in "A Hidden Agenda"). - The candidate relation only needs to be defined on
**hidden**sorts, because in any case it must be the identity on visible sorts (this is implied by 1.). - There is a common
**default choice**, where consists of the methods in , where contains the attributes in , and where two terms are R-related iff all their attributes are equal. If this default choice is taken, then condition above is automatically satisfied, and in fact R is behavioral -equivalence. - If the equations satisfy a certain property (called "hidden completeness" -- see "A Hidden Agenda") then 2 property. is also automatically satisfied. It is sufficient for each equation to be of the form a(m(x)) = t(x), with m a method, a an attribute and t a term involving no methods.

[Next] [Prev] [Home] [BHome]

23 November 1996