Diverging Counter

This example has two purposes. One is to give another example of an invariant. The other is to give an example of a state machine with more than one state variable. The invariant property captures an invariant relationship that we want to maintain between these two state variables.

Here's a two-integer counter with state variables, x and y, whose values get further and further apart as you poke the machine.

Here's a description of the DivergingCounter:

DivergingCounter = (



=

1

 pokeĒ(i: int)

           		 pre i > 0

           		 post    

).

Notice that all the states drawn above are legitimate initial states. So is the state where x and y are both initialized to 0.

The invariant maintained by DivergingCounter is:

Can you prove it?