Uses of Class
org.jmlspecs.checker.JmlSpecQuantifiedExpression

Packages that use JmlSpecQuantifiedExpression

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 JmlSpecQuantifiedExpression in org.jmlspecs.checker

Methods in org.jmlspecs.checker that return JmlSpecQuantifiedExpression

JmlSpecQuantifiedExpression

JmlParser.jmlSpecQuantifiedExprRest(TokenReference sourceRef)

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

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

Uses of JmlSpecQuantifiedExpression in org.jmlspecs.jmldoc.jmldoc_142

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

void	SpecWriter.visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)

Uses of JmlSpecQuantifiedExpression in org.jmlspecs.jmlrac

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

void	RacPrettyPrinter.visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self) Prints a JML specification quantified expression.
void	TransExpression.visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self) Translates a JML quantified expression.
void	TransExpression2.visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self)
protected void	TransExpression2.translateSpecQuantifiedExpression(TransExpression2 t, JmlSpecQuantifiedExpression self)
void	TransPostcondition.visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self) Translates the given JML quantified expression.
void	TransPostExpression2.visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self) Translates the given JML quantified expression.

Uses of JmlSpecQuantifiedExpression in org.jmlspecs.jmlrac.qexpr

Fields in org.jmlspecs.jmlrac.qexpr declared as JmlSpecQuantifiedExpression

protected JmlSpecQuantifiedExpression	Translator.quantiExp taget quantified expression to translate
private JmlSpecQuantifiedExpression	TransQuantifiedExpression.quantiExp quantified expression to be translated.

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

void	AbstractExpressionVisitor.visitJmlSpecQuantifiedExpression(JmlSpecQuantifiedExpression self) Visits the given spec quantified expression, self.
static StaticAnalysis	StaticAnalysis.getInstance(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp) Returns an instance of StaticAnalysis, that translates JML quantified expressions into Java source code.

Constructors in org.jmlspecs.jmlrac.qexpr with parameters of type JmlSpecQuantifiedExpression

Translator(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
Construct a TransQuantifiedExpression object.

StaticAnalysis(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
Constructs a StaticAnalysis object.

StaticAnalysis.SetBased(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
Constructs a SetBased object.

StaticAnalysis.IntervalBased(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
Constructs a IntervalBased object.

StaticAnalysis.EnumerationBased(VarGenerator varGen, RacContext ctx, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
Constructs a EnumerationBased object.

TransQuantifiedExpression(VarGenerator varGen, RacContext context, JmlSpecQuantifiedExpression expr, String resultVar, AbstractExpressionTranslator transExp)
Constructs a new instance.