# Built-in auxiliary type checkers

version 6.0.0-alpha-1

## 1. Introduction

Groovy’s static nature includes an extensible type-checking mechanism. This mechanism allows users to selectively strengthen or weaken type checking as needed to cater for scenarios where the standard type checking isn’t sufficient.

In addition to allowing you to write your own custom checkers, Groovy offers a suite of built-in type checkers that provide additional compile-time verification for specific concerns:

Checker | What it does
--- | ---
RegexChecker | Validates regex patterns at compile time — no more `PatternSyntaxException` at runtime
    assert 'Apple' =~ /(a|A)./    //  okay
    assert 'apple' =~ /(a|A./     //  compile error: unclosed group
FormatStringChecker | Validates `printf`/`format` specifiers against argument types — catches mismatches at compile time
    String.format('%d: %s', 42, 'ok')  //  okay
    String.format('%d: %s', 'x', 42)   //  IllegalFormatConversion: d != String
NullChecker | Detects potential null dereferences using annotations and optional flow analysis
    if (name != null) name.size()   //  null guard
    name?.size()                    //  safe navigation
    name.size()                     //  potential null dereference
ModifiesChecker | Verifies methods only modify declared fields — humans and AI know what changed and what didn’t
    @Modifies({ this.balance })
    void deposit(n) { balance += n }   //  balance is declared

    @Modifies({ })
    void withdraw(n) { balance -= n }  //  balance not in @Modifies
PurityChecker | Enforces that `@Pure` methods have no side effects, with configurable strictness
    @Pure int twice() { value * 2 }  //  reads only
    @Pure int bad()   { count++ }    //  field mutation

These checkers work with annotations from multiple libraries (JSpecify, JetBrains, Checker Framework, and others) — matching by simple name so you can use whichever annotation library your project already depends on.

### 1.1. Why these checkers matter

In a world which seems to be having an ever-increasing focus on AI, here are numerous reasons you might want to make liberal use of checkers and their annotations:

- The checker declarations and associated annotations, along with other Groovy annotations used with AST transforms, e.g. `@Invariant` from `groovy-contracts`, form a declarative specification of program behavior. This specification replaces "read the body" reasoning allowing humans and AI to understand system behavior at scale.

- When an AI agent generates or modifies code, no human may fully understand the result. Type checkers act as a compile-time safety net on what those programs can do.

- If we can treat our systems as composable black boxes each with well specified behavior we can more easily start to apply compositional reasoning to our systems.

- Groovy’s dynamic features (metaprogramming, runtime dispatch, invokeMethod) are powerful but can make static reasoning hard. AI models can hallucinate about what dynamic code does. Type checkers let teams selectively fill in the missing gaps in static reasoning, that AI would otherwise struggle with.

- As AI agents increasingly write, review, and deploy code autonomously, we need machine-checkable invariants which form trust boundaries in agentic workflows.

As an example, let’s explore how combining some checkers and design-by-contract annotations allow both humans and AI to reason about method behavior without reading method implementations. Consider this annotated class:

    @Invariant({ balance >= 0 })
    class Account {
        BigDecimal balance = 0
        List<String> log = []

        @Requires({ amount > 0 })
        @Ensures({ balance == old.balance + amount })
        @Modifies({ [this.balance, this.log] })
        void deposit(BigDecimal amount) {
            balance += amount
            log.add("deposit $amount")
        }

        @Requires({ amount > 0 && amount <= balance })
        @Ensures({ balance == old.balance - amount })
        @Modifies({ [this.balance, this.log] })
        void withdraw(BigDecimal amount) {
            balance -= amount
            log.add("withdraw $amount")
        }

        @Pure
        BigDecimal available() { balance }
    }

When analyzing a sequence of calls:

    account.deposit(100)
    account.withdraw(30)
    def bal = account.available()

With annotations, each call is a self-contained specification — 3 linear reasoning steps:

1. `deposit(100)`: `@Requires` met (100 > 0), `@Ensures` gives `balance == old + 100`, `@Modifies` proves only `balance` and `log` changed

2. `withdraw(30)`: `@Requires` met (30 > 0, 30 ⇐ 100), `@Ensures` gives `balance == 100 - 30 = 70`, `@Modifies` proves `withdraw` didn’t undo the deposit

3. `available()`: `@Pure` proves no side effects — just returns `balance` (70)

This is human and AI reasoning that scales!

Without annotations, the analyzer must read every method body, verify what each one modifies (2 fields × 3 calls = 6 "did this change?" questions), re-verify earlier state after later calls, and check whether `available()` has hidden side effects. This grows as O(fields × calls × call_depth).

### 1.2. Using the checkers

In the examples which follow, we explicitly show declaring the type checker to use. Groovy’s compiler customization mechanisms allow you to simplify application of such checkers, e.g. make it apply globally using a compiler configuration script, as just one example.

## 2. Checking Regular Expressions

A regular expression (regex) defines a search pattern for text. The pattern can be as simple as a single character, a fixed string, or a complex expression containing special characters describing a pattern. The JDK has special regex classes and Groovy adds some special syntactic sugar and functionality on top of the JDK classes.

Here is an example the checks that the String 'Foo' matches a regular expression:

    assert 'foo'.matches(/[Ff].{2}\b/)

The regex pattern is made up of three parts:

- `[Ff]` is a character class matching upper or lowercase 'f',

- `.{2}` means exactly two occurrences of the `.` character class which matches any character

- `\b` matches a word boundary

There are more options we could add here such as grouping, lookahead and look-behind, to name just a few. With so many options and special characters, it isn’t hard to create an invalid regular expression pattern. Such invalid patterns are typically found at runtime with a runtime exception.

The goal of the `RegexChecker` is to find such errors at compile-time. If compilation of the expressions succeeds, they are guaranteed not to fail at runtime.

### 2.1. Typical usage

The previous example can be type checked as follows:

    @TypeChecked(extensions='groovy.typecheckers.RegexChecker')
    static main(args) {
        assert 'foo'.matches(/[Ff].{2}\b/)
    }

If you have many examples where such checking is desirable, you could consider automatically adding this extension to your compilation process.

### 2.2. Covered methods

The methods which are checked include:

`java.util.regex.Pattern`
    static Pattern compile(String regex)
    static Pattern compile(String regex, int flags)
    static boolean matches(String regex, CharSequence input)
`java.util.regex.Matcher`
    String group(int group)
    matcher[matchCount][groupCount]  // getAt shorthand
Operators
    ~/regex/                 // pattern operator
    'string' =~ /regex/      // find operator
    'string' ==~ /regex/     // (exact) match operator

The RegexChecker will check any method calls listed above. It might find such methods when they involve explicit static method calls or when the receiver’s type can be inferred.

The regular expression must be a constant-like String. Any group-count values must be a constant-like integer. By constant-like, we mean, either an explicit String literal, or a field with an initializer expression or a local variable with an initializer expression. These possibilities are shown in the following code, which contains 3 regular expressions:

    static final String TWO_GROUPS_OF_THREE = /(...)(...)/  (1)

    @TypeChecked(extensions='groovy.typecheckers.RegexChecker')
    static main(args) {
        var m = 'foobar' =~ TWO_GROUPS_OF_THREE  //  (2)
        assert m.find()
        assert m.group(1) == 'foo'
        assert m.group(2) == 'bar'  (3)

        var pets = ['cat', 'dog', 'goldfish']
        var shortNamed = ~/\w{3}/  (4)
        assert pets.grep(shortNamed) == ['cat', 'dog']  (5)

        assert Pattern.matches(/(\d{4})-(\d{1,2})-(\d{1,2})/, '2020-12-31')  (6)
    }

1 | A constant String regex
2 | Using the constant regex with the find operator
3 | Checking the matcher’s second group
4 | A local variable containing a regex pattern
5 | Using the pattern with grep
6 | An API call passing a String literal regex

### 2.3. Errors detected

Luckily, in the above example, we made no errors in our regex definitions, and the code compiles and executes successfully.

If however, we did make certain errors in those definitions, then we would expect the potential of runtime errors. Using `RegexChecker`, we can find certain kinds of errors during compilation. Let’s look at some examples.

Suppose at ❸ we looked for the third group instead of the second:

    assert m.group(3) == 'bar'

We would see the following error at compile-time:

    [Static type checking] - Invalid group count 3 for regex with 2 groups

Alternatively, suppose at ❹ we accidentally left off the closing curly brace:

    var shortNamed = ~/\w{3/

We would see the following error at compile-time:

    [Static type checking] - Bad regex: Unclosed counted closure near index 4

Alternatively, suppose at ❻ we accidentally left off the closing round bracket for the last (day of month) group:

    assert Pattern.matches(/(\d{4})-(\d{1,2})-(\d{1,2}/, '2020-12-31')

We would see the following error at compile-time:

    [Static type checking] - Bad regex: Unclosed group near index 26

Over-and-above these examples, detected errors include:

- Bad class syntax

- Bad named capturing group

- Dangling meta character

- Empty character family

- Illegal character range

- Illegal repetition

- Illegal/unsupported escape sequence

- Look-behind group does not have an obvious maximum length

- Unexpected character

- Unclosed character family

- Unclosed character class

- Unclosed counted closure

- Unclosed group

- Unknown character property name

- Unknown Unicode property

- Unknown group type

- Unknown inline modifier

- Unknown character name

- Unmatched closing ')'

## 3. Checking Format Strings

The `format` methods in `java.util.Formatter`, and other similar methods, support formatted printing in the style of C’s `printf` method with a format string and zero or more arguments.

Let’s consider an example which produces a string comprised of three terms:

- a floating-point representation (`%f`) of PI (with 2 decimal places of precision),

- the hex representation (`%X`) of 15 (as two uppercase digits with a leading 0),

- and the Boolean (`%B`) `True` (in uppercase).

The assertion checks our expectations:

    assert String.format('%4.2f %02X %B', Math.PI, 15, true) == '3.14 0F TRUE'

This is a powerful method supporting numerous conversions and flags. If the developer supplies incorrect conversions or flags, they will receive one of numerous possible runtime errors. As examples, consider the following mistakes and resulting runtime exceptions:

- supplying a String as the parameter for either of the first two arguments results in an `IllegalFormatConversionException`,

- leaving out the last argument results in a `MissingFormatArgumentException`,

- supplying the leading zero flag for the Boolean parameter results in a `FlagsConversionMismatchException`.

The goal of the `FormatStringChecker` is to eliminate a large number of such runtime errors. If the API call passes type checking, it will be guaranteed to succeed at runtime.

### 3.1. Typical usage

Here is an example of correctly using some of these methods with type checking in place:

    @TypeChecked(extensions='groovy.typecheckers.FormatStringChecker')
    static main(args) {
        assert String.format('%x', 1023) == '3ff'
        assert String.format(Locale.US, '%x', 1024) == '400'
        assert sprintf('%s%s', 'foo', 'bar') == 'foobar'
        assert new Formatter().format('xy%s', 'zzy').toString() == 'xyzzy'
        def baos = new ByteArrayOutputStream()
        new PrintStream(baos).printf('%-4c|%6b', 'x' as char, true)
        assert baos.toString() == 'x   |  true'
    }

Over and above these methods, if you have your own method of this style, you can annotate it with `@FormatMethod`, and it will also be checked.

    @FormatMethod
    static String log(String formatString, Object... args) {
        sprintf(formatString, args)
    }

    @TypeChecked(extensions='groovy.typecheckers.FormatStringChecker')
    static main(args) {
        assert log('%x', 1023) == '3ff'
        assert log('%x', 1024) == '400'
    }

You can use the `FormatMethod` annotation provided in the `groovy-typecheckers` module or the similarly named annotation from the Java-based checker framework.

### 3.2. Covered methods

The format string methods have the following characteristics:

- The first argument must be of type `java.util.Locale` or `java.lang.String`.

- If the first argument is of type `Locale`, the second argument must be of type `String`.

- The `String` argument is treated as a format string containing zero or more embedded format specifiers as well as plain text. The format specifiers determine how the remaining arguments will be used within the resulting output.

The `FormatStringChecker` ensures that the format string is valid and the remaining arguments are compatible with the embedded format specifiers.

The methods which are checked include:

`java.lang.String`
    static String format(String format, Object... args)
    static String format(Locale l, String format, Object... args)
    String formatted(Object... args)  // JDK15+
`java.util.Formatter`
    String format(String format, Object... args)
    String format(Locale l, String format, Object... args)
`java.io.PrintStream`
    PrintStream printf(String format, Object... args)
    PrintStream printf(Locale l, String format, Object... args)
DGM methods
    printf(String format, Object... args)
    printf(Locale l, String format, Object... args)
    sprintf(String format, Object... args)
    sprintf(Locale l, String format, Object... args)

The format string checker looks for a constant literal format string. For arguments, it also looks for constant literals or otherwise makes checks based on inferred type. When looking for constants, the checker will find inline literals, local variables with a constant initializer, and fields with a constant initializer. Here are some examples:

    static final String FIELD_PATTERN = '%x'
    static final int FIELD_PARAM = 1023

    @TypeChecked(extensions='groovy.typecheckers.FormatStringChecker')
    static main(args) {
        assert sprintf('%x', 1024) == '400'  (1)

        assert sprintf(FIELD_PATTERN, FIELD_PARAM) == '3ff'  (2)

        var local_var_pattern = '%x'
        var local_var_param = 1022
        assert sprintf(local_var_pattern, local_var_param) == '3fe'  (3)

        assert sprintf('%x%s', theParam(), 'a' + 'b') == '3fdab'  (4)
    }

    static int theParam() { 1021 }

1 | Constant literals
2 | Fields with an initializer
3 | Local variables with an initializer
4 | Checking of the parameter will be based on inferred type

### 3.3. Errors detected

Here are some examples of the kinds of errors detected.

- The arguments much match the type of the format classifier, e.g. we can’t use the character classifier with a boolean argument:

      sprintf '%c', true

  We would see the following error at compile-time:

      [Static type checking] - IllegalFormatConversion: c != java.lang.Boolean

- We shouldn’t specify precision for non-scientific arguments, e.g. we shouldn’t expect 7 decimal places of precision for an integral value:

      String.format('%1.7d', 3)

  We would see the following error at compile-time:

      [Static type checking] - IllegalFormatPrecision: 7

- We should specify only known format specifier conversions, e.g. `v` isn’t known:

      System.out.printf('%v', 7)

  We would see the following error at compile-time:

      [Static type checking] - UnknownFormatConversion: Conversion = 'v'

The complete list of errors detected include:

- duplicate format flags

- illegal format flags

- illegal format precision values

- unknown format conversions

- illegal format conversions

- format flags conversion mismatches

- missing arguments

## 4. Checking Null Safety (Incubating)

Null pointer dereferences are one of the most common sources of runtime errors. The `NullChecker` performs compile-time null-safety analysis, detecting potential null dereferences and null-safety violations before code is executed.

Languages like Kotlin and Swift distinguish nullable and non-nullable types throughout the type system, eliminating null errors by construction. Groovy takes a more pragmatic approach: flow analysis can catch many null issues without annotations (in `strict` mode), and `@Nullable`/`@NonNull` annotations provide additional precision where needed. This lets you adopt null safety incrementally — annotate the critical boundaries first, and let flow analysis handle the rest.

Two modes are provided:

- `NullChecker` — Annotation-based: Checks code annotated with `@Nullable` and `@NonNull` (or equivalent) annotations.

- `NullChecker(strict: true)` — Annotation-based + flow-sensitive: Includes all checks from `NullChecker` plus flow-sensitive tracking through assignments and control flow, detecting potential null dereferences even in unannotated code.

For code bases with a mix of strictness requirements, apply `NullChecker` to relaxed code and `NullChecker(strict: true)` to strict code via per-class or per-method `@TypeChecked` annotations.

### 4.1. Typical usage

Here is an example showing a method that safely handles a `@Nullable` parameter:

    @TypeChecked(extensions='groovy.typecheckers.NullChecker')
    int safeLength(@Nullable String text) {
        if (text != null) {
            return text.length()    // ok: null guard
        }
        return -1
    }

    assert safeLength('hello') == 5
    assert safeLength(null) == -1

The checker verifies that `text` is only dereferenced inside the null guard. Without the `if (text != null)` guard, the checker would report a compile-time error.

### 4.2. Supported annotations

The checker recognizes nullability annotations by their simple name, so annotations from any package are supported. The following annotation names are recognized:

Nullable | `@Nullable`, `@CheckForNull`, `@MonotonicNonNull`
Non-null | `@NonNull`, `@NotNull`, `@Nonnull`
Non-null by default (class-level) | `@NonNullByDefault`, `@NullMarked`, `@ParametersAreNonnullByDefault`
Opt-out (class-level) | `@NullUnmarked`

The annotation classes must be on the compile classpath so the Groovy compiler can resolve them. Since the checker matches by simple name, you are free to choose any annotation library:

- JSpecify: `@Nullable` / `@NullMarked` / `@NullUnmarked`

- `javax.annotation.Nullable` / `javax.annotation.Nonnull` (JSR-305)

- `org.jetbrains.annotations.Nullable` / `org.jetbrains.annotations.NotNull`

- `edu.umd.cs.findbugs.annotations.Nullable` / `edu.umd.cs.findbugs.annotations.NonNull`

- `org.checkerframework.checker.nullness.qual.Nullable` / `org.checkerframework.checker.nullness.qual.NonNull`

If you prefer not to add an external dependency, you can define your own minimal annotations:

    import java.lang.annotation.*

    @Target([ElementType.PARAMETER, ElementType.METHOD, ElementType.FIELD])
    @Retention(RetentionPolicy.CLASS)
    @interface Nullable {}

    @Target([ElementType.PARAMETER, ElementType.METHOD, ElementType.FIELD])
    @Retention(RetentionPolicy.CLASS)
    @interface NonNull {}

The following class-level annotations are also recognized:

- `@NullMarked` (JSpecify) — when applied to a class, all parameters, return types, and fields are treated as `@NonNull` unless explicitly annotated `@Nullable`. Use `@NullUnmarked` on a nested class to opt out of this default.

- `@NonNullByDefault` (SpotBugs, Eclipse JDT) — same semantics as `@NullMarked`.

- `@ParametersAreNonnullByDefault` (JSR-305) — when applied to a class, all non-primitive parameters are treated as `@NonNull` unless explicitly annotated `@Nullable`.

- `@groovy.transform.NullCheck` — when applied to a method or class, all non-primitive parameters are treated as effectively `@NonNull` (unless explicitly annotated `@Nullable`). This provides compile-time null checking complementing the runtime checks that `@NullCheck` generates.

### 4.3. Null-safe access patterns

The checker recognizes several patterns for safely working with nullable values.

Safe navigation using the `?.` operator:

    @TypeChecked(extensions='groovy.typecheckers.NullChecker')
    String greet(@Nullable String name) {
        name?.toUpperCase()                          // ok: safe navigation
    }

    assert greet('world') == 'WORLD'
    assert greet(null) == null

Null guards using `if (x != null)`:

    @TypeChecked(extensions='groovy.typecheckers.NullChecker')
    String process(@Nullable String input) {
        if (input != null) {
            return input.toUpperCase()              // ok: null guard
        }
        return 'default'
    }

Early exit using `if (x == null) return` or `throw`:

    @TypeChecked(extensions='groovy.typecheckers.NullChecker')
    String process(@Nullable String input) {
        if (input == null) return 'default'        // early exit
        input.toUpperCase()                        // ok: input is non-null here
    }

Ternary and elvis expressions: in flow-sensitive mode (`NullChecker(strict: true)`), the checker examines both branches of ternary (`condition ? a : b`) and elvis (`x ?: fallback`) expressions. If either branch can be null, the result is treated as nullable. The elvis assignment `x ?= nonNullValue` clears any nullable state on `x`.

### 4.4. Errors detected

Here are some examples of the kinds of errors detected.

- Dereferencing a `@Nullable` variable without a null check:

      def greet = { @Nullable String name ->
          name.toUpperCase()                     // potential null dereference
      }

  We would see the following error at compile-time:

      [Static type checking] - Potential null dereference: 'name' is @Nullable

- Passing `null` to a `@NonNull` parameter:

      @TypeChecked(extensions='groovy.typecheckers.NullChecker')
      class Greeter {
          static String greet(@NonNull String name) {
              name.toUpperCase()
          }
          static void main(String[] args) {
              greet(null)                              // cannot pass null
          }
      }

  We would see the following error at compile-time:

      [Static type checking] - Cannot pass null to @NonNull parameter 'name' of 'greet'

- Returning `null` from a `@NonNull` method:

      @TypeChecked(extensions='groovy.typecheckers.NullChecker')
      class Greeter {
          @NonNull static String greet() {
              return null                              // cannot return null
          }
      }

  We would see the following error at compile-time:

      [Static type checking] - Cannot return null from @NonNull method 'greet'

- Assigning `null` to a `@NonNull` field:

      @TypeChecked(extensions='groovy.typecheckers.NullChecker')
      class Config {
          @NonNull String name
          void clear() {
              name = null                              // cannot assign null
          }
      }

  We would see the following error at compile-time:

      [Static type checking] - Cannot assign null to @NonNull variable 'name'

- Dereferencing the return value of a `@Nullable` method:

      @TypeChecked(extensions='groovy.typecheckers.NullChecker')
      class UserService {
          @Nullable static String findUser() { null }
          static void main(String[] args) {
              findUser().toUpperCase()                  // may return null
          }
      }

  We would see the following error at compile-time:

      [Static type checking] - Potential null dereference: 'findUser()' may return null

### 4.5. @MonotonicNonNull and @Lazy

The `@MonotonicNonNull` annotation is useful for lazy initialization patterns. A field annotated with `@MonotonicNonNull` starts as `null` but once assigned a non-null value, it must remain non-null. The checker treats such fields as nullable (requiring null checks before use) but prevents re-assignment to `null` after initialization:

    @TypeChecked(extensions='groovy.typecheckers.NullChecker')
    class LazyService {
        @MonotonicNonNull String cachedValue

        String getValue() {
            if (cachedValue != null) {
                return cachedValue.toUpperCase()    // ok: null guard
            }
            cachedValue = 'computed'
            return cachedValue.toUpperCase()        // ok: just assigned non-null
        }
    }

Re-assigning `null` to a `@MonotonicNonNull` field after it has been set is an error:

    void reset() {
        value = "hello"
        value = null                             // cannot re-null
    }

We would see the following error at compile-time:

    [Static type checking] - Cannot assign null to @MonotonicNonNull variable 'value' after non-null assignment

Groovy’s `@Lazy` annotation is recognized as an implicit `@MonotonicNonNull`. A `@Lazy` field starts as `null` internally but once its generated getter initializes it, it stays non-null — exactly the monotonic non-null contract. Since `@Lazy` generates a getter that handles initialization automatically, property access to a `@Lazy` field is always safe and will not trigger null dereference warnings. The monotonic guarantee means the checker will also prevent re-assignment to `null` on the backing field after initialization.

### 4.6. Integration with @NullCheck

Groovy’s `@NullCheck` annotation generates runtime null checks for method parameters. When the null checkers see `@NullCheck` on a method or class, they treat all non-primitive parameters as effectively `@NonNull`, catching violations at compile time before they would fail at runtime:

    @NullCheck
    @TypeChecked(extensions='groovy.typecheckers.NullChecker')
    class Greeter {
        static String greet(String name) {
            "Hello, $name!"
        }
        static void main(String[] args) {
            greet(null)                              // caught at compile time
        }
    }

We would see the following error at compile-time:

    [Static type checking] - Cannot pass null to @NonNull parameter 'name' of 'greet'

Parameters explicitly annotated `@Nullable` override the `@NullCheck` behavior for the purpose of the null checkers (though `@NullCheck` will still generate a runtime check for those parameters).

### 4.7. Integration with @NonNullByDefault

Class-level `@NonNullByDefault` (from SpotBugs, Eclipse JDT, or your own definition) makes all parameters, return types, and fields in a class effectively `@NonNull`. Members explicitly annotated `@Nullable` override this default. Similarly, `@ParametersAreNonnullByDefault` (JSR-305) applies only to parameters.

    @NonNullByDefault
    @TypeChecked(extensions='groovy.typecheckers.NullChecker')
    class UserService {
        String name

        static String greet(String name) {
            "Hello, $name!"
        }

        static void main(String[] args) {
            greet(null)                              // compile error: params are @NonNull
        }
    }

We would see the following error at compile-time:

    [Static type checking] - Cannot pass null to @NonNull parameter 'name' of 'greet'

### 4.8. Integration with @Requires and @Ensures

When `groovy-contracts` is on the classpath, `NullChecker` recognises null-safety facts expressed through Design-by-Contract annotations. Top-level `x != null` conjuncts inside a `@Requires` closure mark the corresponding parameter as effectively `@NonNull`; a `result != null` conjunct inside an `@Ensures` closure marks the method return the same way. Both orderings (`x != null` and `null != x`) are recognised. Disjunctions (`||`) are deliberately not used for inference, since they do not establish non-nullness of any individual operand.

    @TypeChecked(extensions='groovy.typecheckers.NullChecker')
    class Greeter {
        @Requires({ name != null })
        static String greet(name) { "Hello, $name!" }

        static void main(String[] args) {
            greet(null)                              // caught at compile time
        }
    }

We would see the following error at compile-time:

    [Static type checking] - Cannot pass null to @NonNull parameter 'name' of 'greet'

The same applies on the return side with `@Ensures`:

    @TypeChecked(extensions='groovy.typecheckers.NullChecker')
    class Greeter {
        @Ensures({ result != null })
        String greet() {
            return null                              // caught at compile time
        }
    }

We would see the following error at compile-time:

    [Static type checking] - Cannot return null from @NonNull method 'greet'

This coexists with explicit `@NonNull` annotations: a method marked `@NonNull` that also carries any `@Ensures` postcondition, or that lives in a class with an `@Invariant` class invariant, still has its literal `return null` statements flagged. Without this coordination, the `groovy-contracts` AST transform would rewrite the return statement before the type-checking pass runs, hiding the literal from the checker. The runtime postcondition continues to guard non-literal cases.

### 4.9. Flow-sensitive mode with strict option

`NullChecker` only flags issues involving annotated code. `NullChecker(strict: true)` adds flow-sensitive tracking, detecting potential null dereferences in unannotated code by tracking nullability through variable assignments and control flow:

With `NullChecker(strict: true)`, the following code would be flagged:

    def x = null
    x.toString()                             // x may be null

We would see the following error at compile-time:

    [Static type checking] - Potential null dereference: 'x' may be null

Reassigning a non-null value clears the nullable state:

    @TypeChecked(extensions='groovy.typecheckers.NullChecker(strict: true)')
    static main(args) {
        def x = null
        x = 'hello'
        assert x.toString() == 'hello'           // ok: reassigned non-null
    }

The complete list of errors detected include:

- assigning `null` to a `@NonNull` field or variable (including implicit `@NonNull` from `@NonNullByDefault`)

- passing `null` or a `@Nullable` value to a `@NonNull` parameter (including implicit `@NonNull` from `@NullCheck`, `@NonNullByDefault`, or `@ParametersAreNonnullByDefault`)

- returning `null` or a `@Nullable` value from a `@NonNull` method (including implicit `@NonNull` from `@NonNullByDefault`)

- dereferencing a `@Nullable` variable without a null check or safe navigation

- dereferencing the return value of a `@Nullable` method without a null check

- re-assigning `null` to a `@MonotonicNonNull` or `@Lazy` field after initialization

- dereferencing a variable known to be null through flow analysis (`strict` mode only)

| For complementary null-related checks such as detecting broken null-check logic, unnecessary null guards before `instanceof`, or `Boolean` methods returning `null`, consider using CodeNarc's null-related rules alongside these type checkers.

## 5. Checking @Modifies Frame Conditions (Incubating)

The `ModifiesChecker` verifies that method bodies comply with their `@Modifies` frame condition declarations from the `groovy-contracts` module. It checks that methods only modify the fields and parameters they declare, helping both humans and AI reason about what a method changes — and crucially, what it does not.

Frame conditions are a well-established concept in formal verification. Dafny’s `modifies` clause and JML’s `assignable` clause serve the same purpose — declaring what a method may change so that everything else is known to be preserved. Groovy’s `@Modifies` brings this idea to the JDK ecosystem in a pragmatic, opt-in form. For projects already using JetBrains annotations, the checker also recognises `@Contract(mutates = "…​")` which expresses similar semantics.

This checker is opt-in and only activates for methods annotated with `@Modifies`:

    @TypeChecked(extensions = 'groovy.typecheckers.ModifiesChecker')
    class InventoryItem {
        int quantity = 0
        int reserved = 0

        @Modifies({ [this.quantity, this.reserved] })
        void restock(int amount) {
            quantity += amount       // OK: quantity is declared
            reserved = 0             // OK: reserved is declared
        }
    }

### 5.1. What the checker verifies

#### 5.1.1. Direct field assignments

Assignments to fields (via `this.field = …​`, `field = …​`, `field++`, `field += …​`) must target fields listed in `@Modifies`. Local variable assignments are always allowed.

    @Modifies({ this.count })
    void increment() {
        count++            // OK: count is declared
        def temp = count   // OK: local variable
    }

    @Modifies({ this.count })
    void broken() {
        other = 5          // ERROR: 'other' not declared in @Modifies
    }

#### 5.1.2. Method calls on `this`

When a method calls another method on `this`, the checker verifies compatibility:

- If the callee has `@Modifies`, its frame must be a subset of the caller’s frame.

- If the callee is annotated `@Pure`, the call is always safe.

- If the callee’s name is in a known-safe list (e.g., `toString`, `hashCode`), the call is allowed.

- Otherwise, a warning is produced.

    @Modifies({ [this.items, this.count] })
    void addItem(String item) {
        doAdd(item)                  // OK if doAdd has compatible @Modifies
        def n = currentCount()       // OK if currentCount() is @Pure
    }

#### 5.1.3. Method calls on parameters and variables

When a method calls a method on a variable or parameter:

- If the receiver is in the `@Modifies` set, any call is allowed (the contract declares the caller may modify it).

- If the receiver is not in the `@Modifies` set, the checker determines whether the call is non-mutating using a layered approach:

  1. Immutable receiver type: calls on `String`, `Integer`, `BigDecimal`, `LocalDate`, etc. are always safe.

  2. `@Pure` method: if the called method is annotated `@Pure`, it is safe.

  3. Known-safe method name: a curated whitelist of non-mutating method names including `size`, `get`, `contains`, `isEmpty`, `toString`, `iterator`, `stream`, `toList`, etc.

  4. Unknown: a warning is produced suggesting the method may modify the receiver.

    @Modifies({ this.count })
    void countItems(List items) {
        count = items.size()         // OK: size() is known-safe
        count = items.toString().length()  // OK: String is immutable
    }

    @Modifies({ list1 })
    void process(List list1, List list2) {
        list1.add('x')               // OK: list1 is in @Modifies
        list2.size()                  // OK: size() is known-safe
        list2.clear()                 // WARNING: clear() may modify list2
    }

### 5.2. Supported annotations from other libraries

The `ModifiesChecker` recognises purity and frame condition annotations from multiple libraries by simple name:

Annotation | Library | Semantics
--- | --- | ---
`@Pure` | Groovy, Checker Framework, Xtext | Implies `@Modifies({})`— no field mutations
`@SideEffectFree` | Checker Framework | Implies `@Modifies({})`— no field mutations
`@Contract(pure = true)` | JetBrains Annotations | Implies `@Modifies({})`— works with CLASS retention
`@Contract(mutates = "…​")` | JetBrains Annotations | Parsed as a frame condition on callees (see below)

#### 5.2.1. @Contract(mutates) support

When a callee has `@Contract(mutates = "…​")`, the checker parses the mutates string to determine what the callee modifies:

- `mutates = ""`— callee mutates nothing (equivalent to `@Pure`)

- `mutates = "this"`— callee mutates its receiver

- `mutates = "param1"`— callee mutates its first parameter

- `mutates = "this,param1"`— callee mutates both

The checker maps `param1`, `param2`, etc. to the actual arguments at the call site and warns if a mutated argument is not in the caller’s `@Modifies` set:

    @Modifies({ this.items })
    void process() {
        addToList(items, 'x')   // OK: items is in @Modifies
        addToList(other, 'x')   // WARNING: other is not in @Modifies
    }

    @Contract(mutates = "param1")
    static void addToList(List list, String item) { list.add(item) }

### 5.3. Interaction with other contract annotations

The `ModifiesChecker` works alongside the other design-by-contract annotations to provide a complete specification for modular reasoning:

- `@Requires` declares what must be true before a call

- `@Ensures` declares what is guaranteed after a call

- `@Modifies` declares what may change (and implicitly, what does not)

- `@Pure` declares a method has no side effects

Together, these annotations allow analysis of method call sequences without reading method bodies — each method becomes a self-contained specification.

## 6. Checking @Pure Purity (Incubating)

The `PurityChecker` verifies that `@Pure` methods have no side effects. By default, strict purity is enforced. The `allows` option declares which effect categories are tolerated.

Languages like Haskell enforce purity through the type system — all side effects must be expressed via IO and State monads, making impure code structurally impossible. Frege (a Haskell dialect for the JVM) takes the same approach. This is powerful but requires incorporating these patterns into your application’s type hierarchies, which can be impractical when integrating with JDK libraries that don’t follow these conventions.

Groovy’s `PurityChecker` provides an opt-in way to achieve similar levels of reasoning about method purity while staying pragmatic about the JDK ecosystem. The `allows` option acknowledges that real-world "pure" methods sometimes log or emit metrics — effects that don’t affect program correctness but would violate strict Haskell-style purity.

### 6.1. Basic usage

    // Strict: no side effects at all
    @TypeChecked(extensions = 'groovy.typecheckers.PurityChecker')
    class Calculator {
        @Pure
        int add(int a, int b) { a + b }              // OK: no effects

        @Pure
        int broken() { count++; return count }         // ERROR: field mutation
    }

### 6.2. Effect categories

The `allows` option accepts a `|`-separated list of effect categories:

    @TypeChecked(extensions = 'groovy.typecheckers.PurityChecker(allows: "LOGGING|METRICS")')

Category | What it allows | Examples
--- | --- | ---
`LOGGING` | Calls to logging frameworks and `println`/`print` | `log.debug(…​)`, `println(…​)`, `System.out.println(…​)`
`METRICS` | Calls to metrics instruments | Micrometer counters/timers, OpenTelemetry metrics
`IO` | File, network, database, and console I/O | `new File(…​)`, `Files.readAllLines(…​)`, JDBC calls
`NONDETERMINISM` | Time-dependent, random, and environment-dependent calls | `System.nanoTime()`, `Math.random()`, `new Date()`, `UUID.randomUUID()`

### 6.3. Supported annotations

The checker recognises purity annotations from multiple libraries by simple name:

Annotation | Library | Semantics
--- | --- | ---
`@Pure` | Groovy, Checker Framework, Xtext | Strict purity (side-effect-free + deterministic)
`@SideEffectFree` | Checker Framework | No mutations, but non-determinism is implicitly allowed
`@Contract(pure = true)` | JetBrains Annotations | Strict purity (works with CLASS retention)
`@Memoized` | Groovy | Effectively pure (checked for side effects)

Annotations are matched by simple name, so `@Pure` from any package is recognised. The `@Contract` annotation is checked for its `pure` attribute being `true`.

### 6.4. How calls are classified

The checker uses a layered approach to determine if a call is pure:

1. Callee has `@Pure`, `@SideEffectFree`, or `@Contract(pure = true)`— the call is pure

2. Callee has `@Memoized`— the call is effectively pure

3. Receiver type is immutable (String, Integer, BigDecimal, etc.) — all calls are pure

4. Method is in the known-pure list (`size`, `get`, `contains`, `isEmpty`, `toString`, etc.) — pure

5. Call matches an effect category— error unless that category is in `allows`

6. None of the above— warning: purity cannot be verified

### 6.5. Reasoning guarantees

The `allows` declaration is machine-readable, enabling both humans and AI to derive precise guarantees about `@Pure` methods:

Property | strict | +LOGGING | +METRICS | +IO | +NONDETERMINISM
--- | --- | --- | --- | --- | ---
No field mutations | Yes | Yes | Yes | Yes | Yes
Can carry forward state across call | Yes | Yes | Yes | Yes | Yes
Deterministic (same inputs → same output) | Yes | Yes | Yes | Yes | No
Can cache/memoize result | Yes | Yes | Yes | Yes | No
Can reorder call freely | Yes | Yes | Yes | No | Yes
Can eliminate dead call | Yes | No | No | No | Yes
No observable output | Yes | No | No | No | Yes

Each column represents a different `allows` configuration. For example, a `@Pure` method under `PurityChecker(allows: "LOGGING")` is guaranteed to have no field mutations, be deterministic, and be safely reorderable — but may produce log output, so dead call elimination would lose that output.

### 6.6. Examples

Strict purity (default):

    @TypeChecked(extensions = 'groovy.typecheckers.PurityChecker')
    class MathUtils {
        @Pure
        int square(int x) { x * x }                             // OK

        @Pure
        long timestamp() { System.nanoTime() }                   // ERROR: non-deterministic

        @Pure
        int logged(int x) { println("x=$x"); x * 2 }            // ERROR: logging
    }

Allowing logging:

    @TypeChecked(extensions = 'groovy.typecheckers.PurityChecker(allows: "LOGGING")')
    class Service {
        @Pure
        int compute(int x) {
            println("computing $x")          // OK: logging allowed
            return x * x
        }

        @Pure
        long getTime() { System.nanoTime() } // ERROR: non-deterministic (not allowed)
    }

Allowing logging and non-determinism:

    @TypeChecked(extensions = 'groovy.typecheckers.PurityChecker(allows: "LOGGING|NONDETERMINISM")')
    class Diagnostics {
        @Pure
        String snapshot(Map state) {
            println("snapshot at ${System.nanoTime()}")   // OK: both allowed
            return state.toString()
        }
    }

### 6.7. What the checker detects

The checker flags:

- Direct field assignments on `this` (`this.x = …​`, `x++` where `x` is a field)

- Property assignments on parameters and local variables (`param.x = 1`)

- Calls to methods not known to be pure

- Calls matching effect categories (logging, metrics, I/O, non-determinism) unless allowed

- Construction of non-deterministic or I/O types

The checker does not currently detect:

- Mutation through aliases (`def ref = this.list; ref.clear()`)

- Deep heap mutation (`this.items.get(0).setName("x")`)

- Mutation via chained property access (`a.b.c = 1`)

- Side effects within closures passed to higher-order methods

These limitations are acceptable for an opt-in checker — the common cases are caught, and unverifiable calls produce warnings.

### 6.8. Relationship to @Modifies and ModifiesChecker

`@Pure` implies `@Modifies({})`— a method with no field mutations. The `ModifiesChecker` recognises `@Pure` and verifies the no-mutation guarantee. The `PurityChecker` goes further, verifying additional purity properties (no impure calls, no I/O, etc.).

Both checkers can be used independently or together:

    // Just frame conditions
    @TypeChecked(extensions = 'groovy.typecheckers.ModifiesChecker')

    // Just purity
    @TypeChecked(extensions = 'groovy.typecheckers.PurityChecker')

    // Both -- ModifiesChecker handles @Modifies, PurityChecker handles @Pure
    @TypeChecked(extensions = ['groovy.typecheckers.ModifiesChecker',
                               'groovy.typecheckers.PurityChecker'])