EmptySet;
static int nPendingRequests = 0;
[StateInvariant]
static bool IsConsisitent()
{
return pendingRequests.Count == nPendingRequests;
}
}
}
If the target of an [StateInvariant] attribute is a method, it is possible for the
method to be a static method or an instance method. In the case of an instance
method, the state invariant is said to hold if the return value is true for all reachable
instances of the class. The return type must be System.Boolean.
A.1.8 State filters
A state filter is a Boolean condition that indicates that a state, although valid, should
be excluded from exploration. The [StateFilter] attribute indicates that its target
method, property, or field is a state filter. A value of true indicates that the state will
be included; false means exclusion from exploration.
namespace MyModelProgram
{
static class Contract
Appendices 291
{
static Set
pendingRequests = Set.EmptySet;
[StateFilter]
static bool LimitNumberOfRequests()
{
return pendingRequests.Count < 4;
}
}
}
State filters are often used in conjuction with a [Feature] attribute so that they
may selectively applied.
A.1.9 State properties
The [StateProperty] attribute indicates additional information that may be used by
the exploration algorithm when deciding which states to explore. It may be applied
to a method, property, or field. Properties are named.
Pages:
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379