@Documented
@Retention(RetentionPolicy.RUNTIME)
@Target({ElementType.TYPE, ElementType.METHOD})
@Incubating
public @interface Decreases

Specifies a termination measure, either for a loop or for a (recursive) method. The closure must return a Comparable value that strictly decreases and remains non-negative (i.e., >= 0 for numeric types) — a well-founded measure.

On a loop (for/while/do-while) the expression is evaluated at the start and end of each iteration and must decrease per iteration; a LoopVariantViolation is thrown otherwise. The measure may also be a List compared lexicographically.

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

On a method the expression is a function of the method's parameters and must strictly decrease (and stay >= 0) on every recursive re-entry — a recursion termination measure. At runtime the value is captured on entry and compared against the nearest enclosing invocation of the same method (per thread); a RecursionVariantViolation is thrown if a recursive call fails to decrease it or it becomes negative, turning a non-terminating recursion into an immediate, localised error rather than a StackOverflowError.

 @Requires({ n >= 0 })
 @Ensures({ result >= n })
 @Decreases({ n })
 static int sumUp(int n) { n == 0 ? 0 : sumUp(n - 1) + n }
 

Since:

6.0.0

See Also:

Invariant