CMU 15-671Models of Software SystemsFall 1995
Mod7 Counter Satisfies Days
Garlan & Wing Handout 10 9 October 1995
Here's a simple example to show how an ``integer mod-7'' counter state machine satisfies a ``days of the week'' machine. Both the abstract and concrete machines have a finite number of states, a finite number of transitions, and infinite traces. My proof of correctness uses an abstraction function that is one-to-one.