You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
a| Enforces that `@Pure` methods have no side effects, with configurable strictness
84
+
85
+
[listing,subs="+quotes,macros"]
86
+
----
87
+
@Pure int twice() { value * 2 } [.green]#// icon:check[] reads only#
88
+
@Pure int bad() { count++ } [.red]#// icon:times[] field mutation#
89
+
----
90
+
|===
91
+
92
+
These checkers work with annotations from multiple libraries (JSpecify, JetBrains,
93
+
Checker Framework, and others) -- matching by simple name so you can use whichever
94
+
annotation library your project already depends on.
95
+
96
+
=== Why these checkers matter
97
+
98
+
In a world which seems to be having an ever-increasing focus on AI,
99
+
here are numerous reasons you might want to make liberal use of checkers and their annotations:
100
+
101
+
* The checker declarations and associated annotations, along with other Groovy annotations
102
+
used with AST transforms, e.g. `@Invariant` from `groovy-contracts`, form a declarative
103
+
specification of program behavior. This specification replaces "read the body" reasoning allowing humans and AI to understand system behavior at scale.
104
+
* 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.
105
+
* 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.
106
+
* Groovy's dynamic features (metaprogramming, runtime dispatch, invokeMethod) are powerful
107
+
but can make static reasoning hard. AI models can hallucinate about what dynamic code does.
108
+
Type checkers let teams selectively fill in the missing gaps in static reasoning,
109
+
that AI would otherwise struggle with.
110
+
* As AI agents increasingly write, review, and deploy code autonomously, we need machine-checkable invariants which form trust boundaries in agentic workflows.
111
+
112
+
As an example, let's explore how combining some checkers and design-by-contract annotations
113
+
allow both humans and AI to reason about method behavior
114
+
without reading method implementations. Consider this annotated class:
115
+
116
+
[source,groovy]
117
+
----
118
+
@Invariant({ balance >= 0 })
119
+
class Account {
120
+
BigDecimal balance = 0
121
+
List<String> log = []
122
+
123
+
@Requires({ amount > 0 })
124
+
@Ensures({ balance == old.balance + amount })
125
+
@Modifies({ [this.balance, this.log] })
126
+
void deposit(BigDecimal amount) {
127
+
balance += amount
128
+
log.add("deposit $amount")
129
+
}
130
+
131
+
@Requires({ amount > 0 && amount <= balance })
132
+
@Ensures({ balance == old.balance - amount })
133
+
@Modifies({ [this.balance, this.log] })
134
+
void withdraw(BigDecimal amount) {
135
+
balance -= amount
136
+
log.add("withdraw $amount")
137
+
}
138
+
139
+
@Pure
140
+
BigDecimal available() { balance }
141
+
}
142
+
----
143
+
144
+
When analyzing a sequence of calls:
145
+
146
+
[source,groovy]
147
+
----
148
+
account.deposit(100)
149
+
account.withdraw(30)
150
+
def bal = account.available()
151
+
----
152
+
153
+
*With annotations*, each call is a self-contained specification -- 3 linear reasoning steps:
154
+
155
+
1. `deposit(100)`: `@Requires` met (100 > 0), `@Ensures` gives `balance == old + 100`,
156
+
`@Modifies` proves only `balance` and `log` changed
0 commit comments