public class LoopInvariantASTTransformation
extends Object
implements ASTTransformation Handles Invariant annotations placed on loop statements (for,
while, do-while). The invariant closure is evaluated as an
assertion at the start of each loop iteration.
When @Invariant is placed on a class (its original usage), this
transform returns immediately, letting the existing global contract pipeline
handle it.
Example:
int sum = 0
@Invariant({ 0 <= i && i <= 4 })
for (int i in 0..4) {
sum += i
}