# Groovy Contracts – design by contract support for Groovy

version 6.0.0-alpha-1

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

- 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 @AssertionsEnabled

- 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

## 3. 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.

## 4. 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.

## 5. 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.

## 6. 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.

### 6.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

### 6.2. While loop

    import groovy.contracts.Invariant

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

### 6.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

### 6.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.

## 7. 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.

### 7.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) { ... }

### 7.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
        }
    }

### 7.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) { ... }

### 7.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`.

### 7.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.

### 7.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.