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
}
| Type Params | Return Type | Name and description |
|---|---|---|
|
public void |
visit(ASTNode[] nodes, SourceUnit source)Rewrites a loop-level Invariant annotation into assertion checks injected at the start of the loop body. |
Rewrites a loop-level Invariant annotation into assertion checks injected at the start of the loop body.
nodes - the annotated AST nodes supplied by the compilersource - the current source unit