[
https://issues.apache.org/jira/browse/GROOVY-12135?page=com.atlassian.jira.plugin.system.issuetabpanels:all-tabpanel
]
Paul King updated GROOVY-12135:
-------------------------------
Description:
h2. Summary
groovy-contracts covers Eiffel's *normal-behaviour* contracts — {{@Requires}},
{{@Ensures}}, {{@Invariant}} — and nothing exceptional. Yet one of the most
common contract-shaped code Groovy programmers write by hand is the *guard
clause*: test an argument, throw {{IllegalArgumentException}} /
{{NullPointerException}} / {{ArithmeticException}}. This proposes one
annotation to make that behaviour a first-class, machine-readable, optionally
*woven* contract:
{code:groovy}
@ThrowsIf(value = { b == 0 }, exception = ArithmeticException)
int divide(int a, int b) { a.intdiv(b) }
{code}
read as an *iff*: the method throws {{ArithmeticException}} _exactly when_ {{b
== 0}} — it must throw when the condition holds, and may not throw that
exception otherwise. With the default {{woven = true}}, groovy-contracts
*generates* the guard at method entry — the general form of a pattern Groovy
core already ships: {{groovy.transform.NullCheck}} weaves exactly this kind of
guard for the null-check special case (as does Lombok's {{@NonNull}} for Java).
The annotation is the implementation, not a comment about one.
h2. Motivation
# *The missing quadrant.* Design-by-Contract in the Eiffel lineage specifies
the happy path; exceptional behaviour is left to javadoc prose. JML closed this
gap for Java with {{signals}} clauses; groovy-contracts has no analogue. Guard
clauses are today boilerplate ({{if (b == 0) throw ...}},
{{Objects.requireNonNull\(y)}}, Guava {{Preconditions}}) — behaviour every
caller depends on, in a form no tool can consume.
# *A {{@Requires}} is the wrong tool for it.* A precondition says _the caller
must not do this_ — violating it is the caller's bug. A guard throw says _this
input is handled, by throwing_ — it is *defined behaviour* callers may rely on
(and catch). The JDK's own culture is overwhelmingly defined-throws, not
preconditions: {{Math.floorDiv}} on a zero divisor _throws_, by specification.
# *Machine-readable exceptional behaviour — the AI-agent case.* To answer "when
does this method throw?" a tool or AI coding agent must today parse javadoc
prose, traverse the body for guarded throw sites (transitively), or read
checked-exception signatures (types only, unchecked exceptions invisible). None
is reliable; javadoc rots silently. An {{@ThrowsIf}} arm is one structured line
— condition, type, direction — and because it is enforced, it cannot drift from
the code without failing a build.
# *It composes with verification but does not require it.* The design
originates in groovy-verify (an SMT-backed verifier on the {{@TypeChecked}}
extension SPI), which statically proves both directions of the iff — but every
feature proposed here has standalone runtime value.
h2. Proposed annotation
{code:groovy}
@Repeatable(ThrowsIfConditions)
@Retention(RetentionPolicy.RUNTIME)
@Target([ElementType.METHOD, ElementType.CONSTRUCTOR])
@interface ThrowsIf {
Class value() // the condition, a closure over the
parameters: { b == 0 }
Class exception() default Throwable // the exception type thrown when the
condition holds
boolean woven() default true // true: insert the guard-throw at
method entry;
// false: the body already implements
the throw
boolean trusted() default false // true: specification-only — the
throw originates in a
// third-party call; never woven
boolean exhaustive() default true // true: iff — the listed conditions
are the ONLY reasons a
// matching exception is thrown;
false: one-directional
// (JML signals-style) — sufficient,
no exhaustiveness claim
boolean checked() default false // true: verify the contract at
runtime in the assertion
// style of @Ensures — see Checking
below
}
{code}
with {{ThrowsIfConditions}} the standard repeatable container. Conditions
accept the same closure conventions as {{@Requires}} (bare free variables
resolve to parameters).
*Semantics.* An arm states two directions: *must-throw* (condition holds on
entry ⇒ the method throws, not returns) and *only-when* (the iff half, disabled
by {{exhaustive = false}}: a matching throw ⇒ some arm's condition held).
Multiple arms are independent must-throws; only-when is a property of the whole
arm-set. Two deliberate non-claims: no {{signals_only}} (an arm-set is
exhaustive over the _conditions for the types it mentions_, never over
exception _types_), and {{exhaustive = false}} exists because true iffs are
sometimes unstatable — {{Integer.parseInt}}'s full throw condition (malformed
_or_ out of range) is beyond a parameter closure, but {{s == null}} is a true
sufficient half.
h2. The three modes, by example
*Unwoven* ({{woven = false}}) — the body already implements the throw; the
annotation is checkable documentation:
{code:groovy}
@ThrowsIf(value = { n < 0 }, exception = IllegalArgumentException, woven =
false)
int fact(int n) {
if (n < 0) throw new IllegalArgumentException('negative')
...
}
{code}
*Trusted* ({{trusted = true}}) — the throw originates in a third-party call;
the author documents behaviour they do not implement and cannot weave (weaving
a wrong trusted spec would silently change behaviour — why {{trusted}} and
{{woven}} are distinct axes):
{code:groovy}
@ThrowsIf(value = { y == null }, exception = NullPointerException, trusted =
true)
Object myMethod(Object x, Object y) {
...
Objects.requireNonNull(y) // the library throws; the annotation records
the contract
...
}
{code}
Attributes are per-arm because real methods mix modes:
{code:groovy}
@ThrowsIf(value = { x == null }, exception = NullPointerException)
// woven for me
@ThrowsIf(value = { y == null }, exception = NullPointerException, woven =
false) // I already guard y
Object process(Object x, Object y) { ... }
{code}
h2. Checking — the runtime iff
Weaving *implements* the contract; {{checked = true}} additionally *verifies*
it at runtime, in the assertion style of {{@Ensures}}: on a normal return, no
unwoven arm's condition may have held on entry (must-throw), and an escaping
exception matching some arm's type must be justified by a matching arm's
condition having held (only-when — checked only for {{exhaustive}} arm-sets).
Conceptually:
{code:groovy}
boolean $c0 = <cond0>; ... // entry snapshot,
every arm
if ($c0) throw new E0(...) // woven arms, in
declaration order
Throwable $t = null
try { <original body> }
catch (Throwable caught) {
$t = caught
throw ThrowsIfSupport.onlyWhen(caught, [$c0, ...], [E0, ...], [texts],
allExhaustive)
} finally {
if ($t == null) ThrowsIfSupport.mustThrow([unwoven $ci ...], [texts]) //
normal return only
}
{code}
A broken implementation raises {{ThrowsIfViolation}} (an {{AssertionViolation}}
sibling of {{PostconditionViolation}}) — deliberately *never* the declared
exception, which is defined behaviour delivered at entry; a justified throw
always propagates to the caller untouched. Without {{checked}}, the runtime
enforces at most the must-throw half (by construction, for woven arms) — the
checked mode is what makes the iff real at runtime, symmetric with
{{@Requires}}/{{@Ensures}} being checked contracts rather than documentation. A
pleasant corollary: {{trusted + checked}} runtime-validates a third-party claim
— a wrong trusted specification is exposed, not silently believed. If any arm
is {{checked}}, the whole arm-set participates in the only-when justification.
h2. What users get with no verifier anywhere
* *Declarative guard clauses* — the boilerplate every service method opens with
becomes one line, with a consistent auto-derived message. Groovy core has
already accepted this pattern once: {{groovy.transform.NullCheck}} is precisely
a woven guard-throw, specialised to null checks — {{@ThrowsIf}} generalises it
to arbitrary conditions and exception types (Lombok's {{@NonNull}} is the same
precedent on the Java side).
* *A runtime-checked exceptional contract* — {{checked = true}} verifies both
directions of the iff in the same assertion style as {{@Ensures}}, including
validating {{trusted}} claims about third-party callees.
* *Exceptional behaviour as structured metadata* — RUNTIME-retained,
repeatable, reflectively consumable by doc generators, test generators, static
analysers, and AI coding agents.
* *A vocabulary distinction the ecosystem lacks* — {{@Requires}} = the caller's
obligation; {{@ThrowsIf}} = the method's defined exceptional behaviour. Callers
_may_ rely on a defined throw; they may _not_ rely on precondition-violation
behaviour.
h2. Evidence
The semantics are the stable survivor of several design rounds field-tested in
groovy-verify (observational vs generative weaving; a whole-method {{@Trusted}}
marker, rejected by the mixed-method case; iff-only, rejected by {{parseInt}}).
A pinned corpus exercises every direction — iff verification and both
refutation directions, mixed woven/unwoven methods, trusted arms including
vacuity detection, {{exhaustive = false}} tolerating unlisted throw reasons
while must-throw stays enforced — and a differential runtime rung
cross-validates proved contracts against real execution over an input grid. A
reference implementation targeting groovy-contracts directly accompanies this
issue: the annotation pair, a SEMANTIC_ANALYSIS local transform in the
{{@Decreases}} style (guard weaving in declaration order + the checked
wrapper), {{ThrowsIfSupport}} / {{ThrowsIfViolation}}, and 17 tests including
the {{@Requires}} interaction cases.
h2. Compatibility
Purely additive: a new annotation pair, no change to existing annotations or
weaving. The weaving-order question is settled empirically and pinned by tests:
the {{@Requires}} assertion weaves ahead of the {{@ThrowsIf}} prologue, so an
input violating both reports as {{PreconditionViolation}} (a caller bug is
judged first), and a precondition whose *evaluation* throws surfaces raw —
pre-body throws never reach the checked wrapper, so they cannot be misjudged as
contract violations ({{AssertionViolation}}s are additionally passed straight
through the checker as belt-and-braces).
h2. Open questions
# *Inheritance* — does an override inherit arms, and what is the Liskov rule
for exceptional contracts? Deliberately undesigned; gc's existing
{{@Requires}}/{{@Ensures}} inheritance semantics should drive it.
# *Default for {{checked}}* — {{false}} (opt-in overhead) as implemented, or
{{true}} for symmetry with {{@Requires}}/{{@Ensures}}, which check by default?
# *Naming* — {{@ThrowsIf}} reads one-directional while the default is an iff.
{{@Signals}} would be actively misleading (JML's {{signals}} is the converse
direction); {{@ThrowsIff}} is accurate but unpronounceable. {{@ThrowsIf}} +
documented iff default is the least-bad.
was:
h2. Summary
groovy-contracts covers Eiffel's *normal-behaviour* contracts — {{@Requires}},
{{@Ensures}}, {{@Invariant}} — and nothing exceptional. Yet one of the most
common contract-shaped code Groovy programmers write by hand is the *guard
clause*: test an argument, throw {{IllegalArgumentException}} /
{{NullPointerException}} / {{ArithmeticException}}. This proposes one
annotation to make that behaviour a first-class, machine-readable, optionally
*woven* contract:
{code:groovy}
@ThrowsIf(value = { b == 0 }, exception = ArithmeticException)
int divide(int a, int b) { a.intdiv(b) }
{code}
read as an *iff*: the method throws {{ArithmeticException}} _exactly when_ {{b
== 0}} — it must throw when the condition holds, and may not throw that
exception otherwise. With the default {{woven = true}}, groovy-contracts
*generates* the guard at method entry — the general form of a pattern Groovy
core already ships: {{groovy.transform.NullCheck}} weaves exactly this kind of
guard for the null-check special case (as does Lombok's {{@NonNull}} for Java).
The annotation is the implementation, not a comment about one.
h2. Motivation
# *The missing quadrant.* Design-by-Contract in the Eiffel lineage specifies
the happy path; exceptional behaviour is left to javadoc prose. JML closed this
gap for Java with {{signals}} clauses; groovy-contracts has no analogue. Guard
clauses are today boilerplate ({{if (b == 0) throw ...}},
{{Objects.requireNonNull\(y)}}, Guava {{Preconditions}}) — behaviour every
caller depends on, in a form no tool can consume.
# *A {{@Requires}} is the wrong tool for it.* A precondition says _the caller
must not do this_ — violating it is the caller's bug. A guard throw says _this
input is handled, by throwing_ — it is *defined behaviour* callers may rely on
(and catch). The JDK's own culture is overwhelmingly defined-throws, not
preconditions: {{Math.floorDiv}} on a zero divisor _throws_, by specification.
# *Machine-readable exceptional behaviour — the AI-agent case.* To answer "when
does this method throw?" a tool or AI coding agent must today parse javadoc
prose, traverse the body for guarded throw sites (transitively), or read
checked-exception signatures (types only, unchecked exceptions invisible). None
is reliable; javadoc rots silently. An {{@ThrowsIf}} arm is one structured line
— condition, type, direction — and because it is enforced, it cannot drift from
the code without failing a build.
# *It composes with verification but does not require it.* The design
originates in groovy-verify (an SMT-backed verifier on the {{@TypeChecked}}
extension SPI), which statically proves both directions of the iff — but every
feature proposed here has standalone runtime value.
h2. Proposed annotation
{code:groovy}
@Repeatable(ThrowsIfConditions)
@Retention(RetentionPolicy.RUNTIME)
@Target([ElementType.METHOD, ElementType.CONSTRUCTOR])
@interface ThrowsIf {
Class value() // the condition, a closure over the
parameters: { b == 0 }
Class exception() default Throwable // the exception type thrown when the
condition holds
boolean woven() default true // true: insert the guard-throw at
method entry;
// false: the body already implements
the throw
boolean trusted() default false // true: specification-only — the
throw originates in a
// third-party call; never woven
[open question 1]
boolean exhaustive() default true // true: iff — the listed conditions
are the ONLY reasons a
// matching exception is thrown;
false: one-directional
// (JML signals-style) — sufficient,
no exhaustiveness claim
}
{code}
with {{ThrowsIfConditions}} the standard repeatable container. Conditions
accept the same closure conventions as {{@Requires}} (bare free variables
resolve to parameters).
*Semantics.* An arm states two directions: *must-throw* (condition holds on
entry ⇒ the method throws, not returns) and *only-when* (the iff half, disabled
by {{exhaustive = false}}: a matching throw ⇒ some arm's condition held).
Multiple arms are independent must-throws; only-when is a property of the whole
arm-set. Two deliberate non-claims: no {{signals_only}} (an arm-set is
exhaustive over the _conditions for the types it mentions_, never over
exception _types_), and {{exhaustive = false}} exists because true iffs are
sometimes unstatable — {{Integer.parseInt}}'s full throw condition (malformed
_or_ out of range) is beyond a parameter closure, but {{s == null}} is a true
sufficient half.
h2. The three modes, by example
*Unwoven* ({{woven = false}}) — the body already implements the throw; the
annotation is checkable documentation:
{code:groovy}
@ThrowsIf(value = { n < 0 }, exception = IllegalArgumentException, woven =
false)
int fact(int n) {
if (n < 0) throw new IllegalArgumentException('negative')
...
}
{code}
*Trusted* ({{trusted = true}}) — the throw originates in a third-party call;
the author documents behaviour they do not implement and cannot weave (weaving
a wrong trusted spec would silently change behaviour — why {{trusted}} and
{{woven}} are distinct axes):
{code:groovy}
@ThrowsIf(value = { y == null }, exception = NullPointerException, trusted =
true)
Object myMethod(Object x, Object y) {
...
Objects.requireNonNull(y) // the library throws; the annotation records
the contract
...
}
{code}
Attributes are per-arm because real methods mix modes:
{code:groovy}
@ThrowsIf(value = { x == null }, exception = NullPointerException)
// woven for me
@ThrowsIf(value = { y == null }, exception = NullPointerException, woven =
false) // I already guard y
Object process(Object x, Object y) { ... }
{code}
h2. What users get with no verifier anywhere
* *Declarative guard clauses* — the boilerplate every service method opens with
becomes one line, with a consistent auto-derived message (Lombok-{{@NonNull}},
generalised to arbitrary conditions and exception types).
* *Exceptional behaviour as structured metadata* — RUNTIME-retained,
repeatable, reflectively consumable by doc generators, test generators, static
analysers, and AI coding agents.
* *A vocabulary distinction the ecosystem lacks* — {{@Requires}} = the caller's
obligation; {{@ThrowsIf}} = the method's defined exceptional behaviour. Callers
_may_ rely on a defined throw; they may _not_ rely on precondition-violation
behaviour.
h2. Evidence
The semantics are the stable survivor of several design rounds field-tested in
groovy-verify (observational vs generative weaving. A pinned corpus exercises
every direction — iff verification and both refutation directions, mixed
woven/unwoven methods, trusted arms including vacuity detection, {{exhaustive =
false}} tolerating unlisted throw reasons while must-throw stays enforced — and
a differential runtime rung cross-validates proved contracts against real
execution over an input grid. A reference implementation is available for
adoption: the annotation pair, the CONVERSION-phase weaving transform
(bare-closure normalisation + guard insertion, ~100 lines), and the test corpus.
h2. Compatibility
Purely additive: a new annotation pair, no change to existing annotations or
weaving. One documented decision needed on weaving order (guards vs
{{@Requires}} checks); the reference implementation inserts guards at method
entry after contract capture.
h2. Open questions
# *Packaging of {{trusted}}* — include in the first cut (upstream cost: one
weaving-skip branch), or hold back and upstream only {{value}} / {{exception}}
/ {{woven}} / {{exhaustive}}? Leaning include — documenting a dependency's
throw is a runtime-library use case, not a verification one.
# *Inheritance* — does an override inherit arms, and what is the Liskov rule
for exceptional contracts? Deliberately undesigned; gc's existing
{{@Requires}}/{{@Ensures}} inheritance semantics should drive it.
# *Runtime only-when monitoring* — an opt-in mode validating that an escaping
matching exception had a justifying arm. Real value, real overhead; suggest
deferring past v1.
# *Naming* — {{@ThrowsIf}} reads one-directional while the default is an iff.
{{@Signals}} would be actively misleading (JML's {{signals}} is the converse
direction); {{@ThrowsIff}} is accurate but unpronounceable. {{@ThrowsIf}} +
documented iff default is the least-bad.
> groovy-contracts: Add a ThrowsIf annotation
> -------------------------------------------
>
> Key: GROOVY-12135
> URL: https://issues.apache.org/jira/browse/GROOVY-12135
> Project: Groovy
> Issue Type: Improvement
> Reporter: Paul King
> Priority: Major
>
> h2. Summary
> groovy-contracts covers Eiffel's *normal-behaviour* contracts —
> {{@Requires}}, {{@Ensures}}, {{@Invariant}} — and nothing exceptional. Yet
> one of the most common contract-shaped code Groovy programmers write by hand
> is the *guard clause*: test an argument, throw {{IllegalArgumentException}} /
> {{NullPointerException}} / {{ArithmeticException}}. This proposes one
> annotation to make that behaviour a first-class, machine-readable, optionally
> *woven* contract:
> {code:groovy}
> @ThrowsIf(value = { b == 0 }, exception = ArithmeticException)
> int divide(int a, int b) { a.intdiv(b) }
> {code}
> read as an *iff*: the method throws {{ArithmeticException}} _exactly when_
> {{b == 0}} — it must throw when the condition holds, and may not throw that
> exception otherwise. With the default {{woven = true}}, groovy-contracts
> *generates* the guard at method entry — the general form of a pattern Groovy
> core already ships: {{groovy.transform.NullCheck}} weaves exactly this kind
> of guard for the null-check special case (as does Lombok's {{@NonNull}} for
> Java). The annotation is the implementation, not a comment about one.
> h2. Motivation
> # *The missing quadrant.* Design-by-Contract in the Eiffel lineage specifies
> the happy path; exceptional behaviour is left to javadoc prose. JML closed
> this gap for Java with {{signals}} clauses; groovy-contracts has no analogue.
> Guard clauses are today boilerplate ({{if (b == 0) throw ...}},
> {{Objects.requireNonNull\(y)}}, Guava {{Preconditions}}) — behaviour every
> caller depends on, in a form no tool can consume.
> # *A {{@Requires}} is the wrong tool for it.* A precondition says _the caller
> must not do this_ — violating it is the caller's bug. A guard throw says
> _this input is handled, by throwing_ — it is *defined behaviour* callers may
> rely on (and catch). The JDK's own culture is overwhelmingly defined-throws,
> not preconditions: {{Math.floorDiv}} on a zero divisor _throws_, by
> specification.
> # *Machine-readable exceptional behaviour — the AI-agent case.* To answer
> "when does this method throw?" a tool or AI coding agent must today parse
> javadoc prose, traverse the body for guarded throw sites (transitively), or
> read checked-exception signatures (types only, unchecked exceptions
> invisible). None is reliable; javadoc rots silently. An {{@ThrowsIf}} arm is
> one structured line — condition, type, direction — and because it is
> enforced, it cannot drift from the code without failing a build.
> # *It composes with verification but does not require it.* The design
> originates in groovy-verify (an SMT-backed verifier on the {{@TypeChecked}}
> extension SPI), which statically proves both directions of the iff — but
> every feature proposed here has standalone runtime value.
> h2. Proposed annotation
> {code:groovy}
> @Repeatable(ThrowsIfConditions)
> @Retention(RetentionPolicy.RUNTIME)
> @Target([ElementType.METHOD, ElementType.CONSTRUCTOR])
> @interface ThrowsIf {
> Class value() // the condition, a closure over the
> parameters: { b == 0 }
> Class exception() default Throwable // the exception type thrown when
> the condition holds
> boolean woven() default true // true: insert the guard-throw at
> method entry;
> // false: the body already
> implements the throw
> boolean trusted() default false // true: specification-only — the
> throw originates in a
> // third-party call; never woven
> boolean exhaustive() default true // true: iff — the listed conditions
> are the ONLY reasons a
> // matching exception is thrown;
> false: one-directional
> // (JML signals-style) — sufficient,
> no exhaustiveness claim
> boolean checked() default false // true: verify the contract at
> runtime in the assertion
> // style of @Ensures — see Checking
> below
> }
> {code}
> with {{ThrowsIfConditions}} the standard repeatable container. Conditions
> accept the same closure conventions as {{@Requires}} (bare free variables
> resolve to parameters).
> *Semantics.* An arm states two directions: *must-throw* (condition holds on
> entry ⇒ the method throws, not returns) and *only-when* (the iff half,
> disabled by {{exhaustive = false}}: a matching throw ⇒ some arm's condition
> held). Multiple arms are independent must-throws; only-when is a property of
> the whole arm-set. Two deliberate non-claims: no {{signals_only}} (an arm-set
> is exhaustive over the _conditions for the types it mentions_, never over
> exception _types_), and {{exhaustive = false}} exists because true iffs are
> sometimes unstatable — {{Integer.parseInt}}'s full throw condition (malformed
> _or_ out of range) is beyond a parameter closure, but {{s == null}} is a true
> sufficient half.
> h2. The three modes, by example
> *Unwoven* ({{woven = false}}) — the body already implements the throw; the
> annotation is checkable documentation:
> {code:groovy}
> @ThrowsIf(value = { n < 0 }, exception = IllegalArgumentException, woven =
> false)
> int fact(int n) {
> if (n < 0) throw new IllegalArgumentException('negative')
> ...
> }
> {code}
> *Trusted* ({{trusted = true}}) — the throw originates in a third-party call;
> the author documents behaviour they do not implement and cannot weave
> (weaving a wrong trusted spec would silently change behaviour — why
> {{trusted}} and {{woven}} are distinct axes):
> {code:groovy}
> @ThrowsIf(value = { y == null }, exception = NullPointerException, trusted =
> true)
> Object myMethod(Object x, Object y) {
> ...
> Objects.requireNonNull(y) // the library throws; the annotation records
> the contract
> ...
> }
> {code}
> Attributes are per-arm because real methods mix modes:
> {code:groovy}
> @ThrowsIf(value = { x == null }, exception = NullPointerException)
> // woven for me
> @ThrowsIf(value = { y == null }, exception = NullPointerException, woven =
> false) // I already guard y
> Object process(Object x, Object y) { ... }
> {code}
> h2. Checking — the runtime iff
> Weaving *implements* the contract; {{checked = true}} additionally *verifies*
> it at runtime, in the assertion style of {{@Ensures}}: on a normal return, no
> unwoven arm's condition may have held on entry (must-throw), and an escaping
> exception matching some arm's type must be justified by a matching arm's
> condition having held (only-when — checked only for {{exhaustive}} arm-sets).
> Conceptually:
> {code:groovy}
> boolean $c0 = <cond0>; ... // entry snapshot,
> every arm
> if ($c0) throw new E0(...) // woven arms, in
> declaration order
> Throwable $t = null
> try { <original body> }
> catch (Throwable caught) {
> $t = caught
> throw ThrowsIfSupport.onlyWhen(caught, [$c0, ...], [E0, ...], [texts],
> allExhaustive)
> } finally {
> if ($t == null) ThrowsIfSupport.mustThrow([unwoven $ci ...], [texts])
> // normal return only
> }
> {code}
> A broken implementation raises {{ThrowsIfViolation}} (an
> {{AssertionViolation}} sibling of {{PostconditionViolation}}) — deliberately
> *never* the declared exception, which is defined behaviour delivered at
> entry; a justified throw always propagates to the caller untouched. Without
> {{checked}}, the runtime enforces at most the must-throw half (by
> construction, for woven arms) — the checked mode is what makes the iff real
> at runtime, symmetric with {{@Requires}}/{{@Ensures}} being checked contracts
> rather than documentation. A pleasant corollary: {{trusted + checked}}
> runtime-validates a third-party claim — a wrong trusted specification is
> exposed, not silently believed. If any arm is {{checked}}, the whole arm-set
> participates in the only-when justification.
> h2. What users get with no verifier anywhere
> * *Declarative guard clauses* — the boilerplate every service method opens
> with becomes one line, with a consistent auto-derived message. Groovy core
> has already accepted this pattern once: {{groovy.transform.NullCheck}} is
> precisely a woven guard-throw, specialised to null checks — {{@ThrowsIf}}
> generalises it to arbitrary conditions and exception types (Lombok's
> {{@NonNull}} is the same precedent on the Java side).
> * *A runtime-checked exceptional contract* — {{checked = true}} verifies both
> directions of the iff in the same assertion style as {{@Ensures}}, including
> validating {{trusted}} claims about third-party callees.
> * *Exceptional behaviour as structured metadata* — RUNTIME-retained,
> repeatable, reflectively consumable by doc generators, test generators,
> static analysers, and AI coding agents.
> * *A vocabulary distinction the ecosystem lacks* — {{@Requires}} = the
> caller's obligation; {{@ThrowsIf}} = the method's defined exceptional
> behaviour. Callers _may_ rely on a defined throw; they may _not_ rely on
> precondition-violation behaviour.
> h2. Evidence
> The semantics are the stable survivor of several design rounds field-tested
> in groovy-verify (observational vs generative weaving; a whole-method
> {{@Trusted}} marker, rejected by the mixed-method case; iff-only, rejected by
> {{parseInt}}). A pinned corpus exercises every direction — iff verification
> and both refutation directions, mixed woven/unwoven methods, trusted arms
> including vacuity detection, {{exhaustive = false}} tolerating unlisted throw
> reasons while must-throw stays enforced — and a differential runtime rung
> cross-validates proved contracts against real execution over an input grid. A
> reference implementation targeting groovy-contracts directly accompanies this
> issue: the annotation pair, a SEMANTIC_ANALYSIS local transform in the
> {{@Decreases}} style (guard weaving in declaration order + the checked
> wrapper), {{ThrowsIfSupport}} / {{ThrowsIfViolation}}, and 17 tests including
> the {{@Requires}} interaction cases.
> h2. Compatibility
> Purely additive: a new annotation pair, no change to existing annotations or
> weaving. The weaving-order question is settled empirically and pinned by
> tests: the {{@Requires}} assertion weaves ahead of the {{@ThrowsIf}}
> prologue, so an input violating both reports as {{PreconditionViolation}} (a
> caller bug is judged first), and a precondition whose *evaluation* throws
> surfaces raw — pre-body throws never reach the checked wrapper, so they
> cannot be misjudged as contract violations ({{AssertionViolation}}s are
> additionally passed straight through the checker as belt-and-braces).
> h2. Open questions
> # *Inheritance* — does an override inherit arms, and what is the Liskov rule
> for exceptional contracts? Deliberately undesigned; gc's existing
> {{@Requires}}/{{@Ensures}} inheritance semantics should drive it.
> # *Default for {{checked}}* — {{false}} (opt-in overhead) as implemented, or
> {{true}} for symmetry with {{@Requires}}/{{@Ensures}}, which check by default?
> # *Naming* — {{@ThrowsIf}} reads one-directional while the default is an iff.
> {{@Signals}} would be actively misleading (JML's {{signals}} is the converse
> direction); {{@ThrowsIff}} is accurate but unpronounceable. {{@ThrowsIf}} +
> documented iff default is the least-bad.
--
This message was sent by Atlassian Jira
(v8.20.10#820010)
