After thinking about the problem, we might say that it would be sufficient to
explore the Counter model program with just five input values 0, 1, 2, 3, and 4. We
might justify this by saying that these values are representative of typical inputs and
that after examining the logic, we see that other values would not produce additional
states.
If we are willing to restrict the scope of our analysis in this way then we can use
the Domain attribute that was introduced on page 81 to create a finitely branching
model program:
namespace Counter
{
static class Contract
{
static int counter = 0;
static readonly Set
inputs = new Set(0, 1, 2, 3, 4);
[Action]
static void ModularIncrement([Domain("inputs")] int x)
{ counter = (counter + x) % 5; }
}
}
Adding a Domain attribute gives us an explorable model program with five possible
actions in each state.2 Unfortunately, this approach introduces a new problem. What
2 Although we don??™t make use of it in this example, it is possible to make the domain depend on
the current state. To do this, you would just give the domain as a static method that references
one or more state variables to compute the set of values returned.
Systems with Complex State 185
relation does the modified model program have to the original? Mixing parameter
restrictions inline with our model confuses the contract (the system??™s specified
behavior) with a scenario (a particular situation of interest for analysis or testing).
Pages:
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253