//////////////////////////////////////////

  Licensed to the Apache Software Foundation (ASF) under one
  or more contributor license agreements.  See the NOTICE file
  distributed with this work for additional information
  regarding copyright ownership.  The ASF licenses this file
  to you under the Apache License, Version 2.0 (the
  "License"); you may not use this file except in compliance
  with the License.  You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

  Unless required by applicable law or agreed to in writing,
  software distributed under the License is distributed on an
  "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY
  KIND, either express or implied.  See the License for the
  specific language governing permissions and limitations
  under the License.

//////////////////////////////////////////
ifndef::reldir_typecheckers[]
:reldir_typecheckers: .
endif::[]
:icons: font

= Built-in auxiliary type checkers

== 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:

[cols="3,10",options="header"]
|===
| Checker | What it does

| <<Checking Regular Expressions,RegexChecker>>
a| Validates regex patterns at compile time -- no more `PatternSyntaxException` at runtime

[listing,subs="+quotes,macros"]
----
assert 'Apple' =~ /(a\|A).*/    [.green]#// icon:check[] okay#
assert 'apple' =~ /(a\|A.*/     [.red]#// icon:times[] compile error: unclosed group#
----

| <<Checking Format Strings,FormatStringChecker>>
a| Validates `printf`/`format` specifiers against argument types -- catches mismatches at compile time

[listing,subs="+quotes,macros"]
----
String.format('%d: %s', 42, 'ok')  [.green]#// icon:check[] okay#
String.format('%d: %s', 'x', 42)   [.red]#// icon:times[] IllegalFormatConversion: d != String#
----

| <<Checking Null Safety (Incubating),NullChecker>>
a| Detects potential null dereferences using annotations and optional flow analysis

[listing,subs="+quotes,macros"]
----
if (name != null) name.size()   [.green]#// icon:check[] null guard#
name?.size()                    [.green]#// icon:check[] safe navigation#
name.size()                     [.red]#// icon:times[] potential null dereference#
----

| <<Checking @Modifies Frame Conditions (Incubating),ModifiesChecker>>
a| Verifies methods only modify declared fields -- humans and AI know what changed and what didn't

[listing,subs="+quotes,macros"]
----
@Modifies({ this.balance })
void deposit(n) { balance += n }   [.green]#// icon:check[] balance is declared#

@Modifies({ })
void withdraw(n) { balance -= n }  [.red]#// icon:times[] balance not in @Modifies#
----

| <<Checking @Pure Purity (Incubating),PurityChecker>>
a| Enforces that `@Pure` methods have no side effects, with configurable strictness

[listing,subs="+quotes,macros"]
----
@Pure int twice() { value * 2 }  [.green]#// icon:check[] reads only#
@Pure int bad()   { count++ }    [.red]#// icon:times[] 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.

=== 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:

[source,groovy]
----
@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:

[source,groovy]
----
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)_.

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

== 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:

[source,groovy]
----
include::../test/RegexCheckerTest.groovy[tags=intro_example,indent=0]
----

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.

=== Typical usage

The previous example can be type checked as follows:

[source,groovy]
----
include::../test/RegexCheckerTest.groovy[tags=checked_example,indent=0]
----

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

=== Covered methods

The methods which are checked include:

|===
a|`java.util.regex.Pattern`
[source,groovy]
----
static Pattern compile(String regex)
static Pattern compile(String regex, int flags)
static boolean matches(String regex, CharSequence input)
----
a|`java.util.regex.Matcher`
[source,groovy]
----
String group(int group)
matcher[matchCount][groupCount]  // getAt shorthand
----
a|Operators
[source,groovy]
----
~/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:

[source,groovy]
----
include::../test/RegexCheckerTest.groovy[tags=introduction_example,indent=0]
----
<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

=== 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 &#x2778; we looked for the third group instead of the second:

[source,groovy]
----
include::../test/RegexCheckerTest.groovy[tags=invalid_group_count,indent=0]
----

We would see the following error at compile-time:

----
include::../test/RegexCheckerTest.groovy[tags=invalid_group_count_message,indent=0]
----

Alternatively, suppose at &#x2779; we accidentally left off the closing curly brace:

[source,groovy]
----
include::../test/RegexCheckerTest.groovy[tags=unclosed_counted_closure,indent=0]
----

We would see the following error at compile-time:

----
include::../test/RegexCheckerTest.groovy[tags=unclosed_counted_closure_message,indent=0]
----

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

[source,groovy]
----
include::../test/RegexCheckerTest.groovy[tags=unclosed_group,indent=0]
----

We would see the following error at compile-time:

[source]
----
include::../test/RegexCheckerTest.groovy[tags=unclosed_group_message,indent=0]
----

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 ')'

== 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:

[source,groovy]
----
include::../test/FormatStringCheckerTest.groovy[tags=intro_example,indent=0]
----

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.

=== Typical usage

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

[source,groovy]
----
include::../test/FormatStringCheckerTest.groovy[tags=valid_format_string_example,indent=0]
----

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.

[source,groovy]
----
include::../test/FormatStringCheckerTest.groovy[tags=format_method_example,indent=0]
----

You can use the `FormatMethod` annotation provided in the `groovy-typecheckers`
module or the https://checkerframework.org/api/org/checkerframework/checker/formatter/qual/FormatMethod.html[similarly named] annotation from the Java-based https://checkerframework.org/[checker framework].

=== 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:

|===
a|`java.lang.String`
[source,groovy]
----
static String format(String format, Object... args)
static String format(Locale l, String format, Object... args)
String formatted(Object... args)  // JDK15+
----
a|`java.util.Formatter`
[source,groovy]
----
String format(String format, Object... args)
String format(Locale l, String format, Object... args)
----
a|`java.io.PrintStream`
[source,groovy]
----
PrintStream printf(String format, Object... args)
PrintStream printf(Locale l, String format, Object... args)
----
a|DGM methods
[source,groovy]
----
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:

[source,groovy]
----
include::../test/FormatStringCheckerTest.groovy[tags=valid_format_string_variations,indent=0]
----
<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

=== 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:
+
[source,groovy]
----
include::../test/FormatStringCheckerTest.groovy[tags=illegal_format_conversion,indent=0]
----
+
We would see the following error at compile-time:
+
[source]
----
include::../test/FormatStringCheckerTest.groovy[tags=illegal_format_conversion_message,indent=0]
----

* We shouldn't specify precision for non-scientific arguments, e.g. we shouldn't
expect 7 decimal places of precision for an integral value:
+
[source,groovy]
----
include::../test/FormatStringCheckerTest.groovy[tags=illegal_format_precision,indent=0]
----
+
We would see the following error at compile-time:
+
[source]
----
include::../test/FormatStringCheckerTest.groovy[tags=illegal_format_precision_message,indent=0]
----

* We should specify only known format specifier conversions, e.g. `v` isn't known:
+
[source,groovy]
----
include::../test/FormatStringCheckerTest.groovy[tags=unknown_format_conversion,indent=0]
----
+
We would see the following error at compile-time:
+
[source]
----
include::../test/FormatStringCheckerTest.groovy[tags=unknown_format_conversion_message,indent=0]
----

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

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

=== Typical usage

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

[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=intro_example,indent=0]
----

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.

=== 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:

* https://jspecify.dev/[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:

[source,groovy]
----
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` (https://jspecify.dev/[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.

=== Null-safe access patterns

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

*Safe navigation* using the `?.` operator:

[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=safe_navigation,indent=0]
----

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

[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=null_guard,indent=0]
----

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

[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=early_return,indent=0]
----

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

=== Errors detected

Here are some examples of the kinds of errors detected.

* Dereferencing a `@Nullable` variable without a null check:
+
[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=nullable_dereference,indent=0]
----
+
We would see the following error at compile-time:
+
[source]
----
include::../test/NullCheckerTest.groovy[tags=nullable_dereference_message,indent=0]
----

* Passing `null` to a `@NonNull` parameter:
+
[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=null_to_nonnull,indent=0]
----
+
We would see the following error at compile-time:
+
[source]
----
include::../test/NullCheckerTest.groovy[tags=null_to_nonnull_message,indent=0]
----

* Returning `null` from a `@NonNull` method:
+
[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=null_return,indent=0]
----
+
We would see the following error at compile-time:
+
[source]
----
include::../test/NullCheckerTest.groovy[tags=null_return_message,indent=0]
----

* Assigning `null` to a `@NonNull` field:
+
[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=nonnull_assign,indent=0]
----
+
We would see the following error at compile-time:
+
[source]
----
include::../test/NullCheckerTest.groovy[tags=nonnull_assign_message,indent=0]
----

* Dereferencing the return value of a `@Nullable` method:
+
[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=nullable_return_deref,indent=0]
----
+
We would see the following error at compile-time:
+
[source]
----
include::../test/NullCheckerTest.groovy[tags=nullable_return_deref_message,indent=0]
----

=== @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:

[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=monotonic_nonnull,indent=0]
----

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

[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=monotonic_reassign,indent=0]
----

We would see the following error at compile-time:

[source]
----
include::../test/NullCheckerTest.groovy[tags=monotonic_reassign_message,indent=0]
----

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.

=== 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:

[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=nullcheck_integration,indent=0]
----

We would see the following error at compile-time:

[source]
----
include::../test/NullCheckerTest.groovy[tags=nullcheck_integration_message,indent=0]
----

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

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

[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=nonnull_by_default,indent=0]
----

We would see the following error at compile-time:

[source]
----
include::../test/NullCheckerTest.groovy[tags=nonnull_by_default_message,indent=0]
----

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

[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=requires_integration,indent=0]
----

We would see the following error at compile-time:

[source]
----
include::../test/NullCheckerTest.groovy[tags=requires_integration_message,indent=0]
----

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

[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=ensures_integration,indent=0]
----

We would see the following error at compile-time:

[source]
----
include::../test/NullCheckerTest.groovy[tags=ensures_integration_message,indent=0]
----

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.

=== 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:

[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=flow_sensitive,indent=0]
----

We would see the following error at compile-time:

[source]
----
include::../test/NullCheckerTest.groovy[tags=flow_sensitive_message,indent=0]
----

Reassigning a non-null value clears the nullable state:

[source,groovy]
----
include::../test/NullCheckerTest.groovy[tags=flow_reassign,indent=0]
----

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)

NOTE: For complementary null-related checks such as detecting broken null-check logic,
unnecessary null guards before `instanceof`, or `Boolean` methods returning `null`,
consider using https://codenarc.org/[CodeNarc]'s null-related rules alongside these type checkers.

== 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`:

[source,groovy]
----
@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
    }
}
----

=== What the checker verifies

==== Direct field assignments

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

[source,groovy]
----
@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
}
----

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

[source,groovy]
----
@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
}
----

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

[source,groovy]
----
@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
}
----

=== Supported annotations from other libraries

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

[cols="2,2,3",options="header"]
|===
| 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)
|===

==== @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:

[source,groovy]
----
@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) }
----

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

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

=== Basic usage

[source,groovy]
----
// 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
}
----

=== Effect categories

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

[source,groovy]
----
@TypeChecked(extensions = 'groovy.typecheckers.PurityChecker(allows: "LOGGING|METRICS")')
----

[cols="1,3,3",options="header"]
|===
| 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()`
|===

=== Supported annotations

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

[cols="2,2,3",options="header"]
|===
| 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`.

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

=== Reasoning guarantees

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

[cols="3,1,1,1,1,1",options="header"]
|===
| 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.

=== Examples

*Strict purity (default):*

[source,groovy]
----
@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:*

[source,groovy]
----
@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:*

[source,groovy]
----
@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()
    }
}
----

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

=== 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:

[source,groovy]
----
// 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'])
----
