next up previous contents
Next: A simple example Up: Proof by induction Previous: Proof by induction   Contents

Induction over infinite sequences

Now, suppose we have a counter that ranges from zero to infinity. We can still prove by induction that any value i is eventually reached. To do this, we declare TYPE to be an ordset without an upper bound:

ordset TYPE 0..;

With this change, run the example. Now choose Verify All to verify that in fact the induction works, and that p[i] holds for all i. We've just proved a property of an infinite-state system by model checking.