All Implemented Interfaces and Traits:

ASTTransformation, CompilationUnitAware

public class LoopVariantASTTransformation
extends Object
implements ASTTransformation, CompilationUnitAware

Handles Decreases annotations placed on loop statements (for, while, do-while). The closure must return a value that strictly decreases on every iteration and remains non-negative.

The transformation injects code to:

1. Save the expression value at the start of each iteration.
2. Re-evaluate it at the end of the iteration.
3. Assert the value has strictly decreased.
4. Assert the value is non-negative.

Example:

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

Since:

6.0.0

See Also:

Decreases

VariantSupport

LoopVariantViolation