Stable annotations:
Incubating in 6.0.0 (semantics may evolve in a subsequent 6.x release):
| Annotation Type | Description |
|---|---|
| Contracted | |
| Decreases | Specifies a termination measure, either for a loop or for a (recursive) method. |
| Ensures | |
| EnsuresConditions | Container annotation for multiple Ensures postconditions on the same target. |
| Invariant | |
| Invariants | Container annotation for multiple Invariant declarations on the same type. |
| Modifies | Declares the frame condition for a method: the set of fields and parameters that the method is allowed to modify. |
| ModifiesConditions | Container for multiple Modifies annotations on the same method. |
| Requires | |
| RequiresConditions | Container annotation for multiple Requires preconditions on the same target. |