groovy.contracts.Requires (precondition), @Ensures (postcondition), @Invariant (class invariant). Postconditions can access result and old() values.
| Annotation Type | Description |
|---|---|
| Contracted | |
| Decreases | Specifies a termination measure for a loop. |
| Ensures | |
| EnsuresConditions | Represents multiple postconditions. |
| Invariant | |
| Invariants | Represents multiple invariants |
| 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 | Represents multiple preconditions. |