Uses of Class
org.jmlspecs.checker.JmlInvariantForExpression

Packages that use JmlInvariantForExpression

org.jmlspecs.checker	Contains the source code for a parser and typechecker for JML annotations and java code.
org.jmlspecs.jmldoc.jmldoc_142
org.jmlspecs.jmlrac	Generates Java classes from JML specifications that check assertions at runtime.
org.jmlspecs.jmlrac.qexpr	Translates JML quantified expressions into Java source code to evaluate them at runtime.

Uses of JmlInvariantForExpression in org.jmlspecs.checker

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

void	JmlAbstractVisitor.visitJmlInvariantForExpression(JmlInvariantForExpression self)
abstract void	JmlVisitor.visitJmlInvariantForExpression(JmlInvariantForExpression self)
void	JmlVisitorNI.visitJmlInvariantForExpression(JmlInvariantForExpression self)
void	JmlExpressionChecker.visitJmlInvariantForExpression(JmlInvariantForExpression self) Checks visibility (and purity) of the given expression, self.

Uses of JmlInvariantForExpression in org.jmlspecs.jmldoc.jmldoc_142

Methods in org.jmlspecs.jmldoc.jmldoc_142 with parameters of type JmlInvariantForExpression

void	SpecWriter.visitJmlInvariantForExpression(JmlInvariantForExpression self)

Uses of JmlInvariantForExpression in org.jmlspecs.jmlrac

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

void	RacPrettyPrinter.visitJmlInvariantForExpression(JmlInvariantForExpression self) Prints a JML invariant for expression.
void	TransExpression.visitJmlInvariantForExpression(JmlInvariantForExpression self) Translates a JML invariant_for expression.
void	TransExpression2.visitJmlInvariantForExpression(JmlInvariantForExpression self) NOT SUPPORTED The \invariant_for operator returns true just when its argument satisfies the invariant of its static type.

Uses of JmlInvariantForExpression in org.jmlspecs.jmlrac.qexpr

Methods in org.jmlspecs.jmlrac.qexpr with parameters of type JmlInvariantForExpression

void	AbstractExpressionVisitor.visitJmlInvariantForExpression(JmlInvariantForExpression self) Visits the given \invariant_for expression, self.