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.