public class LoopInvariant
extends Assertion
A loop-invariant assertion that must hold at the start of each iteration.
| Modifiers | Name | Description |
|---|---|---|
static LoopInvariant |
DEFAULT |
Shared invariant instance representing an unconstrained loop invariant. |
| Constructor and description |
|---|
LoopInvariant()Creates a loop invariant that defaults to true. |
LoopInvariant(BlockStatement blockStatement, BooleanExpression booleanExpression)Creates a loop invariant from the supplied source block and boolean expression. |
| Methods inherited from class | Name |
|---|---|
class Assertion |
and, booleanExpression, or, originalBlockStatement, renew |
Shared invariant instance representing an unconstrained loop invariant.
Creates a loop invariant that defaults to true.
Creates a loop invariant from the supplied source block and boolean expression.
blockStatement - the original invariant blockbooleanExpression - the normalized invariant expressionCopyright © 2003-2026 The Apache Software Foundation. All rights reserved.