|
Annotation Types Summary |
| Also |
A Container for multiple SpecCase-annotations. |
| Helper |
The Helper-annotation is a marker for
non-public methods. |
| Invariant |
The class invariant assertion. |
| InvariantDefinitions |
A container-annotation for Invariantiants. |
| Length |
A parameter annotation which is used to
specify the length/size of an array, the size of any subtype of
the superinterface Collection, and for the length
of Strings. |
| Max |
Defines an upper bound of a numeric parameter. |
| Min |
Defines a lower bound of a numeric parameter. |
| Model |
The definition of the model variable
which consists of a Model.name() and
a Model.type(). |
| ModelDefinitions |
A Container-annotation for multiple Model-variable
definitions. |
| Name |
Is used to define the specification name of a method or
constructor parameter. |
| NonNull |
This annotation can be used to express that
a parameter or a field is not allowed to be null. |
| Post |
A post-condition. |
| Pre |
The Pre-annotation implements a
pre-condition. |
| Pure |
Expresses that a method is side-effect free
or that a type is immutable. |
| Range |
This annotation is used to specify the range
of numeric parameters. |
| Represents |
The represents clause is used to bind a value to a
model variable. |
| RepresentsDefinitions |
A Container-annotation for model-variable
representations. |
| SpecCase |
The SpecCase-annotation can be used to specify the
behaviour of a method or constructor. |