This includes System.
Boolean and all enum types.
The domain attribute may be applied to instance methods to give the possible
values of the implicit this parameter of the instance method.
A.1.6 Accepting state conditions
Runs of a model program may terminate only in an accepting state. The predicates
that determine whether a given state is an accepting state are given by the
[AcceptingStateCondition] attribute. The target of this attribute may be a method,
field, or property.
An example of the use of this attribute is
namespace MyModelProgram
{
static class Contract
{
static Set
pendingRequests = Set.EmptySet;
[AcceptingStateCondition]
static bool NoPendingRequests()
{
return pendingRequests.IsEmpty;
}
}
}
290 Modeling Library Reference
If the target of an [AcceptingStateCondition] 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 is accepting if the condition holds for all reachable instances of
the class. The return type must be System.Boolean.
A.1.7 State invariants
It is possible to indicate conditions called state invariants that must hold in every
state. The failure of any state invariant indicates a modeling error.
The [StateInvariant] attribute indicates that the target method, field, or property
must hold in every state.
An example of the use of this attribute is
namespace MyModelProgram
{
static class Contract
{
static Set pendingRequests = Set.
Pages:
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378