Package org.apache.groovy.contracts.domain

Class LoopInvariant

java.lang.Object

org.apache.groovy.contracts.domain.Assertion<LoopInvariant>

org.apache.groovy.contracts.domain.LoopInvariant

public class LoopInvariant
extends Assertion<LoopInvariant>

A loop-invariant assertion that must hold at the start of each iteration.

Since:

6.0.0

Field Summary

Fields

Modifier and Type	Field	Description
static final LoopInvariant	DEFAULT	Shared invariant instance representing an unconstrained loop invariant.

Constructor Summary

Constructors

Constructor	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.

Method Summary

Methods inherited from class org.apache.groovy.contracts.domain.Assertion

and, booleanExpression, or, originalBlockStatement, renew

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Details

DEFAULT

public static final LoopInvariant DEFAULT

Shared invariant instance representing an unconstrained loop invariant.

Constructor Details

LoopInvariant

public LoopInvariant()

Creates a loop invariant that defaults to true.

LoopInvariant

public LoopInvariant(BlockStatement blockStatement,
 BooleanExpression booleanExpression)

Creates a loop invariant from the supplied source block and boolean expression.

Parameters:

blockStatement - the original invariant block

booleanExpression - the normalized invariant expression