@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target(ElementType.TYPE)
@Incubating
public @interface Decreases

Specifies a termination measure for a loop. The closure must return a Comparable value that strictly decreases on every iteration and remains non-negative (i.e., >= 0 for numeric types).

At runtime, the expression is evaluated at the start and end of each iteration. A LoopVariantViolation is thrown if:

• the value did not decrease, or
• the value became negative.

Example:

 int n = 10
 @Decreases({ n })
 while (n > 0) {
     n--
 }
 

Since:

6.0.0

See Also:

Invariant