Package groovy.contracts

Annotation Interface Decreases

@Documented @Retention(RUNTIME) @Target({TYPE,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:

  • Required Element Summary

    Required Elements
    Modifier and Type
    Required Element
    Description
    Class
    value
    Returns the closure class that computes the variant value.

  • Element Details

    • value

      Class value
      Returns the closure class that computes the variant value.
      Returns:
      the generated closure class backing the variant expression