Paul King created GROOVY-12477:
----------------------------------
Summary: @Modifies with an empty or no list isn't working correctly
Key: GROOVY-12477
URL: https://issues.apache.org/jira/browse/GROOVY-12477
Project: Groovy
Issue Type: Bug
Components: groovy-contracts, groovy-typecheckers
Reporter: Paul King
Assignee: Paul King
h3. Problem
There is no working way to declare that a method modifies nothing with
{{@Modifies}}. The forms a user would reach for are either rejected or silently
treated as if the method had no {{@Modifies}} at all.
With {{@TypeChecked(extensions = 'groovy.typecheckers.ModifiesChecker')}} on a
method whose body is {{balance -= n}}:
||Form||Result||
|{{@Modifies({ this.other })}}|Error: {{'balance' is not declared in
@Modifies}} (correct)|
|{{@Modifies({ [] })}}|*Compiles; nothing is checked*|
|{{@Modifies({})}}|Error: {{@Modifies closure must contain a field reference,
parameter reference, or list of references}}|
|{{@Modifies}}|*Compiles; nothing is checked*|
{code:groovy}
import groovy.contracts.Modifies
import groovy.transform.TypeChecked
@TypeChecked(extensions = 'groovy.typecheckers.ModifiesChecker')
class Account {
int balance
@Modifies({ [] })
void withdraw(int n) { balance -= n } // expected: error, actual: compiles
}
{code}
h3. Cause
* {{ModifiesASTTransformation}} stores the {{groovy.contracts.modifiesFields}}
metadata only when the set is non-empty. An empty list therefore leaves no
metadata. {{ModifiesChecker}} reads missing metadata as "no {{@Modifies}},
nothing to check". {{ModifiesEnsuresValidationTransformation}} returns early on
an empty set too, so {{old.x}} in an {{@Ensures}} is not validated either.
* An empty closure body is rejected because exactly one statement is required.
* {{Modifies.value()}} has no default, so a bare {{@Modifies}} should be a
missing-member error. The transform replaces {{value}} with {{Object.class}}
unconditionally, which hides the missing member.
The intent that "nothing" be expressible is already in the docs and the
checker. The type checkers guide says {{@Pure}}, {{@SideEffectFree}} and
{{@Contract(pure = true)}} each imply {{@Modifies({})}}, and
{{ModifiesChecker}} substitutes an empty frame for them. A user cannot write
that form themselves.
h3. Proposed fix
* {{@Modifies({})}} and {{@Modifies({ [] })}} both declare an empty frame: the
method modifies no fields or parameters. The metadata is always stored, even
when empty, so an empty frame is distinguishable from no annotation.
* A bare {{@Modifies}} is a compile error. A frame condition is a claim the
checker enforces, so "modifies nothing" should be explicit rather than inferred
from a marker that could equally be read as "modifies something unspecified".
* With an empty frame, {{@Ensures}} may not reference {{old.<field>}},
consistent with the existing rule that {{old}} may only reference fields
declared in {{@Modifies}}.
* The contracts user guide states the empty-frame form.
Both modules are {{@Incubating}}, so the tightening is low cost. The only
existing code that changes behaviour is code using {{@Modifies({ [] })}} or a
bare {{@Modifies}} and relying on it being unchecked.
--
This message was sent by Atlassian Jira
(v10.3.26#10030026)
