If a name is not given in the
attribute, the property name defaults to the target name.
namespace MyModelProgram
{
static class Contract
{
static Set
pendingRequests = Set.EmptySet;
[StateProperty("NumberOfRequests")]
static int RequestCount()
{
return pendingRequests.Count;
}
}
}
A.1.10 Requirements
It is sometimes useful to document the link between the elements of amodel program
and a natural language requirements document. We use an attribute in the form
[Requirement("string")] for this purpose. The string string provides traceability
back to an external requirement source.
292 Modeling Library Reference
Requirement strings are printed in error contexts such as conformance failures
and state invariant violations. They can also be used to check for coverage of requirements.
The [Requirement] attribute may be applied to any .NET attributable element.
More than one [Requirement] attribute may be provided for an entity.
static class Bar
{
[Requirement("XYZ spec 3.2.4: Foo parameter must be nonnegative")]
static void FooEnabled(int x)
{
return x > 0;
}
[Action]
static void Foo(int x) { /* ... */ }
}
A.2 Data types
A.2.1 Compound value
CompoundValue
Base class for data records with structural equality.
Syntax
public abstract class CompoundValue : AbstractValue, IComparable
Methods
CompareTo(Object)
Term order. Comparison is based on type and recursively on fields.
Pages:
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380