Package groovy.contracts

package groovy.contracts

Design-by-contract (DbC) support with compile-time assertion generation.

Stable annotations:

• @Requires – method precondition
• @Ensures – method postcondition; closures may reference result and old
• @Invariant – class invariant, also usable as a loop invariant on for / while / do-while loops
• @Contracted – package- or class-level opt-in marker that enables contract processing

Incubating in 6.0.0 (semantics may evolve in a subsequent 6.x release):

• @Modifies – frame condition declaring which fields and parameters a method may modify
• @Decreases – a termination measure (a strictly-decreasing, well-founded variant) for a loop (per iteration) or a recursive method (per recursive re-entry)

Annotation Interfaces

Class	Description
Contracted	Package-level and class-level annotation indicating that the package is enabled for class-invariants, pre- and post-conditions.
Decreases	Specifies a termination measure, either for a loop or for a (recursive) method.
Ensures	Represents a method postcondition.
EnsuresConditions	Container annotation for multiple Ensures postconditions on the same target.
Invariant	Represents a class-invariant or a loop 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	Represents a method precondition.
RequiresConditions	Container annotation for multiple Requires preconditions on the same target.