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 Invariant iants. |
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. |