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
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 as defined in the following:
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) . endowhere EVENAT denotes the natural numbers with an even operation; see the applet below (due to Akira Mori). 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; see the applet below (due to Akira Mori). 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.
M (F : Flag) rev rev F = Feven 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".
This flag example is about the simplest non-trivial example for coinduction we could think of, 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; you might also start with proofs using more familiar techniques, such as induction.