**Doubly Reversed Flag**

We are given a flag that may be up or down, like on an old fashioned mail box, with methods to put the flag up, put it down, and reverse it. There is just one attribute (namely up?) showing whether the flag is up or down; see the Java applet (due to Grant Malcolm) and OBJ3 specification below.

th FLAG is sort Flag .
ops (up_)(dn_)(rev_) : Flag -> Flag .
op up?_ : Flag -> Bool .
var F : Flag .
eq up? up F = true .
eq up? dn F = false .
eq up? rev F = not up? F .
endth

We want to show that if we reverse the flag twice, then the flag returns to its original state, i.e., we want to show that for all flags
F
,
rev rev F = F .

Unfortunately, this equation is
**not satisfied**
by all models (i.e., implementations) of
FLAG
! For example, consider the model whose states are natural numbers, and whose operations are defined as follows:
obj NFLAG is pr EVENAT *(sort Nat to Flag) .
ops (up_)(dn_)(rev_) : Flag -> Flag .
op up?_ : Flag -> Bool .
var F : Flag .
eq up F = 2 * F .
eq dn F = 2 * F + 1 .
eq rev F = F + 1 .
eq up? F = even(F) .
endo

where
EVENAT
denotes the natural numbers with an
even
operation. Here, the equation is not satisfied because
rev rev F = F + 2 .

For another example, consider the model whose states are "histories" that is, sequences of all methods (i.e., messages) received so far. Then the state after a double reversal of
F
is the sequence
rev rev F
, which does not equal the sequence
F
. Such an implementation (or one a little simpler) would be needed if some other attributes were required, such as the number of methods received, or the last method received.

Actually, there is
*only one*
implementation (up to isomorphism) where the equation is actually true of all reachable states! There are infinitely many other implementations where the equation is literally false, but always
*appears to be true*
. This means that the equation is
**observationally**
or
**behaviorally satisfied**
by
M
, which we write as
M (F : Flag) rev rev F = F

even though
M (F : Flag) rev rev F = F

(ordinary satisfaction) does not hold. Thus, we have to use a technique that allows us to prove
behavioral satisfaction
, not just ordinary satisfaction. This is why we use
coinduction
. This situation is actually very common: software engineers often write clever code that doesn't really satisfy its specification, but does always "appear to" to satisfy it.
Flags are about the simplest non-trivial example of coinduction we could find, but if you are not already familiar with
hidden algebra
and
coinduction
, you will have some work to do before you can follow our proof. In that case, you should do some background reading, and start with some proofs using more familiar techniques, such as induction; the
tatami project homepage
would be a good place to start, especially its links to the hidden algebra tutorial.

*This text was written by Joseph Goguen in May 1996.*

To the first tatami (i.e., proof) page.

To the duck source file.

To the Kumo demos homepage.

To the Tatami Project homepage.

To the UCSD Meaning and Computation Group homepage.

*This page was generated by Kumo on Fri Jul 02 14:09:27 PDT 1999.*