Uses of Class
org.jmlspecs.checker.JmlLoopInvariant

Packages that use JmlLoopInvariant

org.jmlspecs.checker	Contains the source code for a parser and typechecker for JML annotations and java code.
org.jmlspecs.jmlrac	Generates Java classes from JML specifications that check assertions at runtime.

Uses of JmlLoopInvariant in org.jmlspecs.checker

Fields in org.jmlspecs.checker declared as JmlLoopInvariant

private JmlLoopInvariant[]

JmlLoopStatement.loopInvariants

Methods in org.jmlspecs.checker that return JmlLoopInvariant

JmlLoopInvariant[]	JmlLoopStatement.loopInvariants()
JmlLoopInvariant[]	JmlParser.jmlLoopInvariantList()
JmlLoopInvariant	JmlParser.jmlLoopInvariant()

Methods in org.jmlspecs.checker with parameters of type JmlLoopInvariant

void	JmlAbstractVisitor.visitJmlLoopInvariant(JmlLoopInvariant self)
abstract void	JmlVisitor.visitJmlLoopInvariant(JmlLoopInvariant self)
void	JmlVisitorNI.visitJmlLoopInvariant(JmlLoopInvariant self)

Constructors in org.jmlspecs.checker with parameters of type JmlLoopInvariant

JmlLoopStatement(TokenReference where, JmlLoopInvariant[] loopInvariants, JmlVariantFunction[] variantFunctions, JStatement stmt, JavaStyleComment[] comments)
Constructs a new instance with the given arguments.

Uses of JmlLoopInvariant in org.jmlspecs.jmlrac

Methods in org.jmlspecs.jmlrac with parameters of type JmlLoopInvariant

void	RacPrettyPrinter.visitJmlLoopInvariant(JmlLoopInvariant self) Prints a JML loop invariant.
private RacNode	TransMethodBody.invariantCheckCode(JmlLoopInvariant[] invs) Returns code that checks the given loop invariants.
private JExpression	TransMethodBody.conjoinInvariants(JmlLoopInvariant[] invs) Conjoins the given loop invariants and returns the result.