@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.CONSTRUCTOR, ElementType.METHOD})
@Incubating
@Repeatable(ModifiesConditions.class)
public @interface Modifies

Declares the frame condition for a method: the set of fields and parameters that the method is allowed to modify. All other state is implicitly declared unchanged.

The closure value lists the modifiable targets as field references (this.fieldName) or parameter references (paramName). Multiple targets can be specified using a list:

   @Modifies({ this.items })
   void addItem(Item item) { ... }

   @Modifies({ [this.items, this.count] })
   void addAndCount(Item item) { ... }
 

Multiple @Modifies annotations can also be used (via Repeatable):

   @Modifies({ this.items })
   @Modifies({ this.count })
   void addAndCount(Item item) { ... }
 

When both @Modifies and Ensures are present on a method, the old variable in the postcondition may only reference fields declared in @Modifies. A compile error is reported otherwise.

@Modifies does not generate runtime assertion code. It serves as a specification for humans and tools (including AI) to reason about method behavior.

Since:

6.0.0

See Also:

Ensures

Requires