We will show in Chapter 11 how to adapt our analysis techniques to cases like this.
In this chapter we??™ll focus on how to write model programs that benefit from the
descriptive power of richer structural data types.
It is also possible to write model programs that are not finitely branching. Surprisingly,
this does not necessarily mean that the number of states is unbounded. For
example, here is a model program with only five states that has (computationally)
infinite branching:
namespace Counter2
{
static class Contract
{
static int counter = 0;
[Action]
static void ModularIncrement(int x)
{ counter = (counter + x) % 5; }
}
}
This model program is infinitely branching because in every state there are an
???infinite??? (very large) number of integer values for the parameter x. There are only
five states because the modulus operator % in this example limits the counter to five
values.
The previous two examples illustrate one of the main differences between model
programs and finite state machines (FSMs). FSMs always have a finite number
of states and transitions, while model programs may represent systems with an
unbounded number of states and transitions.
You can understand this difference by analogy. Consider the relationship between
the string array type string[] and an enumerator of strings IEnumerator
.
Conceptually, the two types are similar, but the string array is a finite type that
provides a Length operation and random, indexed access.
Pages:
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222