This module provides contract annotations that support the specification of class-invariants, pre- and post-conditions on Groovy classes and interfaces, loop invariants on for, while, and do-while loops, and frame conditions declaring which fields a method may modify. Special support is provided so that post-conditions may refer to the old value of variables or to the result value associated with calling a method.

1. Applying @Invariant, @Requires and @Ensures

With Groovy contracts in your classpath, contracts can be applied on a Groovy class or interface by using one of the annotations found in the groovy.contracts package.

package acme

import groovy.contracts.*

@Invariant({ speed() >= 0 })
class Rocket {
    int speed = 0
    boolean started = true

    @Requires({ isStarted() })
    @Ensures({ old.speed < speed })
    def accelerate(inc) { speed += inc }

    def speed() { speed }
}

def r = new Rocket()
r.accelerate(5)

2. Enabling contracts with @Contracted

Contract processing is opt-in. By default, classes that simply mention the contract annotations will have them processed; the @Contracted marker is used when you want to make the opt-in explicit at the package level, or when you want to apply contract processing to a type that doesn’t itself carry any contract annotations (for example, an empty class whose contract comes entirely from inherited interfaces).

@Contracted may be placed on a package declaration (in a package-info.groovy / package-info.java) to enable contract processing across every type in that package:

@Contracted
package com.acme.banking

import groovy.contracts.*

or on an individual type:

@Contracted
class Account { /* ... */ }

Once enabled, runtime assertion checking still honours the JVM’s -ea / -da flags; @Contracted controls whether the AST transforms generate assertion code at compile time, not whether the resulting assertions execute at run time.

3. More Features

Groovy contracts supports the following feature set:

  • definition of class invariants, pre- and post-conditions via @Invariant, @Requires and @Ensures

  • definition of loop invariants on for, while, and do-while loops via @Invariant

  • declaration of frame conditions (which fields a method may modify) via @Modifies

  • declaration of loop and recursion termination measures via @Decreases

  • inheritance of class invariants, pre- and post-conditions of concrete predecessor classes

  • inheritance of class invariants, pre- and post-conditions in implemented interfaces

  • usage of old and result variable in post-condition assertions

  • assertion injection in Plain Old Groovy Objects (POGOs)

  • human-readable assertion messages, based on Groovy power asserts

  • enabling contracts at package- or class-level with @Contracted

  • enable or disable contract checking with Java’s -ea and -da VM parameters

  • annotation contracts: a way to reuse reappearing contract elements in a project domain model

  • detection of circular assertion method calls

4. The Stack Example

Currently, Groovy contracts supports 3 annotations: @Invariant, @Requires and @Ensures – all of them work as annotations with closures, where closures allow you to specify arbitrary code pieces as annotation parameters:

import groovy.contracts.*

@Invariant({ elements != null })
class Stack<T> {

    List<T> elements

    @Ensures({ is_empty() })
    def Stack()  {
        elements = []
    }

    @Requires({ preElements?.size() > 0 })
    @Ensures({ !is_empty() })
    def Stack(List<T> preElements)  {
        elements = preElements
    }

    boolean is_empty()  {
        elements.isEmpty()
    }

    @Requires({ !is_empty() })
    T last_item()  {
        elements.get(count() - 1)
    }

    def count() {
        elements.size()
    }

    @Ensures({ result == true ? count() > 0 : count() >= 0  })
    boolean has(T item)  {
        elements.contains(item)
    }

    @Ensures({ last_item() == item })
    def push(T item)  {
       elements.add(item)
    }

    @Requires({ !is_empty() })
    @Ensures({ last_item() == item })
    def replace(T item)  {
        remove()
        elements.add(item)
    }

    @Requires({ !is_empty() })
    @Ensures({ result != null })
    T remove()  {
        elements.remove(count() - 1)
    }

    String toString() { elements.toString() }
}

def stack = new Stack<Integer>()

The example above specifies a class-invariant and methods with pre- and post-conditions. Note, that preconditions may reference method arguments and post-conditions have access to the method’s result with the result variable and old instance variables values with old.

Indeed, Groovy AST transformations change these assertion annotations into Java assertion statements (can be turned on and off with a JVM param) and inject them at appropriate places, e.g. class-invariants are used to check an object’s state before and after each method call.

5. Annotation closure rules

  • Invariants should reference class fields only.

  • Preconditions may reference class fields and arguments.

  • Postconditions may reference class fields, arguments, the result and the old value of class fields using the syntax old.fieldname.

Old values of class fields will only be stored where Groovy contracts knows how to make a copy. Currently, this means fields with a Cloneable class type, primitives, the primitive wrapper types, BigInteger, BigDecimal, and G/Strings.

6. Use within scripts

Currently, Groovy contracts intentionally doesn’t support scripts, but you can use them with JEP-445 compatible scripts from Groovy 5 as shown in this example:

import groovy.contracts.*
import org.apache.groovy.contracts.*
import static groovy.test.GroovyAssert.shouldFail

@Requires({ arg > 0 })
@Ensures({ result < arg })
def sqrt(arg) { Math.sqrt(arg) }

def main() {
    assert sqrt(4) == 2
    shouldFail(PreconditionViolation) { sqrt(-1) }
}

You could even place an @Invariant annotation on the main method and it will be moved to the generated script class.

7. Loop Invariants

In addition to class-level invariants, @Invariant can be placed directly on for, while, and do-while loops. A loop invariant is a condition that must hold at the start of each iteration. If the condition is violated, a LoopInvariantViolation (a subclass of AssertionError) is thrown.

This is inspired by design-by-contract constructs found in languages like Dafny and Eiffel.

7.1. For loop

import groovy.contracts.Invariant

int sum = 0
@Invariant({ 0 <= i && i <= 4 })
for (int i in 0..4) {
    sum += i
}
assert sum == 10

7.2. While loop

import groovy.contracts.Invariant

int n = 10
@Invariant({ n >= 0 })
while (n > 0) {
    n--
}
assert n == 0

7.3. Multiple invariants

Multiple @Invariant annotations can be stacked on a single loop, and each condition is checked independently at the start of every iteration:

import groovy.contracts.Invariant

int sum = 0
@Invariant({ sum >= 0 })
@Invariant({ sum <= 100 })
for (int i in 1..5) {
    sum += i
}
assert sum == 15

7.4. Rules for loop invariant closures

  • The closure should be a boolean expression (or multiple expressions).

  • The closure may reference any variables visible in the enclosing scope, including the loop variable.

  • Assignment operators and state-changing postfix/prefix operators are not supported inside the closure.

8. Termination with @Decreases

@Decreases declares a termination measure (a variant): a value that must strictly decrease through a well-founded sequence, guaranteeing progress towards termination. It applies in two places:

  • on a loop (for/while/do-while) — the measure must decrease on every iteration; and

  • on a method — the measure must decrease on every recursive re-entry.

In both cases the closure must yield a value whose successive values form a strictly decreasing, well-founded sequence. Two value shapes are supported:

  • A single Comparable value — usually numeric — that strictly decreases on every iteration. If the value is also a Number, it must additionally remain non-negative.

  • A List of Comparable elements, compared lexicographically: the first position at which consecutive values differ must show a strict decrease, and earlier positions must be equal. This is the natural way to express termination for nested loops (e.g. `[i, j]`).

If the variant fails to decrease (or a numeric scalar variant becomes negative), a LoopVariantViolation is thrown for a loop and a RecursionVariantViolation for a method (both subclasses of AssertionError).

This is inspired by similar constructs in design-by-contract languages such as Dafny and Eiffel.

@Decreases is incubating in Groovy 6.0.0. The contract — in particular the scalar non-negativity rule and the lexicographic shape for List variants — may be relaxed or extended in a future release based on usage feedback.

8.1. While loop

import groovy.contracts.Decreases

int n = 10
@Decreases({ n })
while (n > 0) {
    n--
}
assert n == 0

8.2. For loop

import groovy.contracts.Decreases

int remaining = 5
@Decreases({ remaining })
for (int i = 0; i < 5; i++) {
    remaining--
}
assert remaining == 0

8.3. Lexicographic (tuple) variants

For nested loops where no single counter strictly decreases on every iteration, return a List whose elements form a tuple compared lexicographically. In the example below the outer counter stays equal while the inner one decreases, then the outer one decreases and the inner one is allowed to reset:

import groovy.contracts.Decreases

int outer = 2, inner = 3
@Decreases({ [outer, inner] })
while (outer > 0) {
    if (inner > 0) {
        inner--
    } else {
        outer--
        inner = 3
    }
}
assert outer == 0

8.4. Recursive methods

On a method, the measure is a function of the method’s parameters and must strictly decrease on every recursive re-entry — the recursion analogue of a loop variant. At runtime the value is captured on entry and compared against the nearest enclosing invocation of the same method (per thread); a non-decreasing or negative measure throws a RecursionVariantViolation, turning a non-terminating recursion into an immediate, localised error rather than a StackOverflowError:

import groovy.contracts.Decreases

@Decreases({ n })                       // strictly decreases on every recursive call
int factorial(int n) {
    n <= 1 ? 1 : n * factorial(n - 1)
}
assert factorial(5) == 120

The bookkeeping is per method and per thread, so it also handles mutual recursion (each participant must decrease its own measure on its own re-entry) and recursion through callbacks. Like @Requires/@Ensures, a method @Decreases is inherited: an override that does not redeclare it inherits its parent’s measure (with the parent’s parameter names re-mapped to the override’s); an override may declare its own @Decreases to refine it.

8.5. Rules for @Decreases closures

  • The closure must return a Comparable value or a List of Comparable elements.

  • For a loop, the value is evaluated at the start and end of each iteration; for a method, on each entry. The new value must be strictly less than the previous one (lexicographically, for List variants).

  • For numeric scalar variants, the value must also remain >= 0. This non-negativity rule does not apply to non-Number Comparable values (e.g. `String`) or to List variants.

  • A loop measure may reference any variable visible in the enclosing scope; a method measure is over the method’s parameters (it is evaluated on entry, so it cannot reference the method’s result).

  • Checks honour the JVM’s -ea/-da assertion configuration for the enclosing class, as preconditions and postconditions do.

  • Recursion measure inheritance currently requires the parent to be compiled in the same unit; an override of a method from a precompiled (binary) supertype is not yet instrumented.

9. Unwoven preconditions

By default @Requires weaves its assertion: a violating caller observes a PreconditionViolation. Real methods often already enforce their obligations — a hand-written guard, an Objects.requireNonNull, Guava’s Preconditions — and adding a woven @Requires on top would double the check and change the exception a violating caller observes. Two members, shared with @ThrowsIf, cover this:

  • woven = false — no assertion is generated. The annotation remains the caller’s documented obligation, consumable by readers and tools (a verifier discharges it at call sites regardless of where enforcement lives); a violating caller observes whatever the existing enforcement does. An unwoven precondition never contributes to generated assertions, including the inherited precondition weaving of overriding methods.

  • direct — pure information, no effect on bytecode, ignored (implicitly true) for woven preconditions: true (default) says a hand-written check enforces the obligation in this body; false says the enforcement lives in code the method executes (a validator call, possibly transitive), so there is no check to find in this body. Most users never set it.

import groovy.contracts.Requires
import static groovy.test.GroovyAssert.shouldFail

class Greeter {
    // the obligation is already enforced by requireNonNull: the annotation documents it,
    // no assertion is generated, and a violating caller sees the library's NPE
    @Requires(value = { name != null }, woven = false, direct = false)
    static String greet(String name) {
        Objects.requireNonNull(name)
        "Hello, $name!"
    }
}

assert Greeter.greet('World') == 'Hello, World!'
shouldFail(NullPointerException) { Greeter.greet(null) }   // the enforcement, untouched

The members are per-annotation, so repeated preconditions mix modes — woven arms are asserted, unwoven arms are left to their existing enforcement:

import groovy.contracts.Requires
import org.apache.groovy.contracts.PreconditionViolation
import static groovy.test.GroovyAssert.shouldFail

class Adjuster {
    @Requires({ amount <= 1000 })                              // woven: asserted
    @Requires(value = { amount >= 0 }, woven = false)          // enforced in the body
    static int adjust(int amount) {
        if (amount < 0) throw new IllegalArgumentException('negative')
        amount
    }
}

assert Adjuster.adjust(5) == 5
shouldFail(PreconditionViolation) { Adjuster.adjust(2000) }        // the woven arm
shouldFail(IllegalArgumentException) { Adjuster.adjust(-1) }       // the body's own guard

Choosing between an unwoven @Requires and a @ThrowsIf over the same guard is a statement of intent: @Requires says a violating call is the caller’s bug (callers may not rely on the violation behaviour); @ThrowsIf says the throw is defined behaviour callers may rely on and catch. Both are spellable over the identical requireNonNull body — they are different claims.

The woven and direct members of @Requires are incubating in Groovy 6.0.0 and may be refined in a future release based on usage feedback.

10. Exceptional contracts with @ThrowsIf

@ThrowsIf declares a method’s exceptional contract: the method throws the given exception when the given condition holds on entry. It is the exceptional counterpart of @Requires — a precondition says the caller must not do this (violating it is the caller’s bug), whereas a @ThrowsIf arm says this input is handled, by throwing: it is defined behaviour, part of the contract, that callers may rely on (and catch). Guard clauses of this shape are among the most common contract-shaped code written by hand (if (b == 0) throw …​, Objects.requireNonNull(y), Guava’s Preconditions); @ThrowsIf makes that behaviour a first-class, machine-readable annotation. The condition is a closure over the method’s parameters, using the same conventions as @Requires, and the annotation is repeatable — each arm pairs one condition with one exception type.

The contract is read as an iff: the method throws a matching exception exactly when some arm’s condition holds. Two attributes generate code; the others are runtime-retained metadata for readers and tools (documentation generators, static analysers, verifiers, AI coding agents):

Member Effect on generated code

woven

true (default): the guard — if (cond) throw new E(…​) — is inserted at method entry (the general form of the pattern groovy.transform.NullCheck provides for the null-check special case). false: nothing is generated — the throw already exists.

checked

true: a verification wrapper is generated (see below). false (default): nothing.

exception

The type the woven guard constructs (it should provide a (String) constructor, as the standard exceptions do), and the type the checked wrapper matches escaping throws against.

exhaustive

Nothing on its own. Under checked = true it gates the escaping-throw check: false says the method may throw the same exception for other, unlisted reasons, so escaping throws are never judged.

direct

Nothing, ever — pure information: true (default) says a hand-written throw statement lives in this body; false says the exception arises from code the method executes (a call, possibly transitive, or a runtime operation), so there is no throw statement in this body to find. Ignored (implicitly true) for woven arms. This is documentation for a human reader but exists primarily for tools - if you are not using a tool that needs it, you can safely ignore it.

10.1. Woven guards

With the defaults, the annotation is the guard:

import groovy.contracts.ThrowsIf
import static groovy.test.GroovyAssert.shouldFail

class Calculator {
    @ThrowsIf(value = { b == 0 }, exception = ArithmeticException)
    static int divide(int a, int b) { a.intdiv(b) }
}

assert Calculator.divide(4, 2) == 2
shouldFail(ArithmeticException) { Calculator.divide(1, 0) }   // the woven guard

On a constructor whose first statement is an explicit super(…​) or this(…​) call, the guard is inserted immediately after that call, which must stay first — a (current) language constraint.

10.2. Documenting an existing throw

With woven = false nothing is generated; the annotation is checkable documentation of a guard that is already there:

import groovy.contracts.ThrowsIf
import static groovy.test.GroovyAssert.shouldFail

class MathUtil {
    @ThrowsIf(value = { n < 0 }, exception = IllegalArgumentException, woven = false)
    static int fact(int n) {
        if (n < 0) throw new IllegalArgumentException('negative')   // the guard is already here
        n <= 1 ? 1 : n * fact(n - 1)
    }
}

assert MathUtil.fact(4) == 24
shouldFail(IllegalArgumentException) { MathUtil.fact(-1) }

When the throw originates in code the method merely calls (a third-party library), add direct = false — there is no throw statement in this body to find, and weaving a wrong claim about invoked code would silently change behaviour, which is why such arms are never woven:

import groovy.contracts.ThrowsIf

class Wrapper {
    @ThrowsIf(value = { s == null }, exception = NullPointerException, woven = false, direct = false)
    static Object describe(Object s) {
        Objects.requireNonNull(s)   // the library throws; the annotation records the contract
        "value: $s"
    }
}

assert Wrapper.describe('x') == 'value: x'

Most users never set direct: the defaults are right for woven arms and hand-written guards alike, and the usual prompt to add direct = false is a verification or analysis tool reporting that it cannot find the promised throw in the body.

10.3. Runtime checking

Weaving implements the contract; checked = true additionally verifies it at runtime, in the same assertion style as @Ensures: on a normal return, no non-woven arm’s condition may have held on entry (must-throw), and an escaping exception matching some arm’s type must be justified by a matching arm’s condition having held (only-when — checked only for exhaustive arm-sets). A broken implementation raises ThrowsIfViolation — never the declared exception, which is defined behaviour delivered at entry; a justified throw always propagates untouched:

import groovy.contracts.ThrowsIf
import org.apache.groovy.contracts.ThrowsIfViolation
import static groovy.test.GroovyAssert.shouldFail

class Broken {
    // the body SHOULD throw when n < 0 but does not — a broken implementation,
    // reported as a violation (never the declared exception)
    @ThrowsIf(value = { n < 0 }, exception = IllegalArgumentException, woven = false, checked = true)
    static int identity(int n) { n }
}

assert Broken.identity(5) == 5
shouldFail(ThrowsIfViolation) { Broken.identity(-5) }

checked is set-level: if any arm is checked, the whole arm-set is checked — every non-woven arm is must-throw checked, and every arm serves as an only-when justifier.

10.4. Rules for @ThrowsIf closures

  • The closure is a boolean expression over the method’s parameters (the same conventions as @Requires; it cannot reference result or old).

  • Multiple arms are independent must-throws; the only-when direction is a property of the whole arm-set. One exhaustive = false arm disclaims it for the set.

  • Exhaustiveness is (at most) over the conditions for the exception types mentioned, never over exception types: declaring an ArithmeticException arm says nothing about whether the method can throw anything else.

  • No claim, however exhaustive, reasons about VM resource conditions: an OutOfMemoryError or StackOverflowError is outside contract semantics, and the checked wrapper passes any VirtualMachineError through unjudged.

  • When both apply on the same input, a @Requires violation is reported first (PreconditionViolation): the caller’s obligation is judged before the method’s defined behaviour.

@ThrowsIf is incubating in Groovy 6.0.0. The attribute set — in particular the direct metadata member and the set-level checked rule — may be refined in a future release based on usage feedback.

11. Frame Conditions with @Modifies

The @Modifies annotation declares which fields or parameters a method is allowed to modify. All other state is implicitly declared unchanged. This is known as a frame condition in design-by-contract terminology, inspired by similar constructs in Dafny and JML.

@Modifies does not generate runtime assertion code — it serves as a specification for humans and tools (including AI) to reason about what a method changes.

11.1. Basic usage

Use this.fieldName to declare that a field may be modified:

@Modifies({ this.items })
void addItem(String item) {
    items.add(item)
}

For multiple fields, use a list expression:

@Modifies({ [this.items, this.count] })
void addAndCount(String item) {
    items.add(item)
    count++
}

Or use multiple @Modifies annotations (via @Repeatable):

@Modifies({ this.items })
@Modifies({ this.count })
void addAndCount(String item) { ... }

11.2. Parameter references

Method parameters can also be declared as modifiable:

@Modifies({ arr })
void fillArray(int[] arr) {
    for (int i = 0; i < arr.length; i++) {
        arr[i] = i
    }
}

11.3. Interaction with @Ensures

When both @Modifies and @Ensures are present on a method, a compile-time check ensures that the old variable in the postcondition only references fields declared in @Modifies. Referencing a field via old that is not in the modification set produces a compile error:

@Modifies({ this.items })
@Ensures({ old -> old.items.size() < items.size() })  // OK: items is declared
void addItem(String item) { ... }

@Modifies({ this.items })
@Ensures({ old -> old.count == count })  // ERROR: count not declared in @Modifies
void addItem(String item) { ... }

11.4. Compile-time validation

The @Modifies annotation validates at compile time that:

  • Field references (this.fieldName) refer to fields that exist on the class.

  • Parameter references refer to actual parameters of the method.

  • If @Ensures is also present, old.fieldName references only access fields declared in @Modifies.

11.5. Rules for @Modifies closures

  • The closure must contain a single field reference (this.field), parameter reference (param), or a list of such references.

  • Field references use the this.fieldName syntax.

  • Parameter references use the bare parameter name.

  • The closure is not executed at runtime — it is only analyzed at compile time.

11.6. Verifying method bodies with ModifiesChecker

While @Modifies alone is a compile-time-checked specification (validating field/parameter existence and @Ensures consistency), it does not verify the method body itself. For that, the groovy-typecheckers module provides the ModifiesChecker type checking extension:

@TypeChecked(extensions = 'groovy.typecheckers.ModifiesChecker')

When enabled, the checker verifies that method bodies only modify fields declared in @Modifies, and that method calls on non-modifiable receivers use only non-mutating operations. See the Type Checkers documentation for details.