Uses of Class
org.jmlspecs.jmlrac.qexpr.NonExecutableQuantifierException

Packages that use NonExecutableQuantifierException

org.jmlspecs.jmlrac.qexpr

Translates JML quantified expressions into Java source code to evaluate them at runtime.

Uses of NonExecutableQuantifierException in org.jmlspecs.jmlrac.qexpr

Methods in org.jmlspecs.jmlrac.qexpr that throw NonExecutableQuantifierException

RacNode	QInterval.translate(VarGenerator varGen, String lowerVar, String upperVar, AbstractExpressionTranslator transExp) Return Java source code that, if executed, evaluates the quantfied interval, i.e., its lower and upper bound values.
static QSet	QSet.build(JExpression expr, String var) Returns a new qset built from a JML expression and a quantified variable.
private static QSet	QSet.calculate(JExpression expr, String var) Returns the qset of an expression expr with respect to the quantified variable var.
abstract RacNode	QSet.translate(VarGenerator varGen, String resultVar, AbstractExpressionTranslator transExp) Returns Java source code that computes the qset represented by this object.
RacNode	QSet.Top.translate(VarGenerator varGen, String resultVar, AbstractExpressionTranslator transExp) Return Java source code that computes the qset represented by this object.
RacNode	QSet.Leaf.translate(VarGenerator varGen, String resultVar, AbstractExpressionTranslator transExp) Return Java source code that computes the qset represented by this object.
RacNode	QSet.Union.translate(VarGenerator varGen, String resultVar, AbstractExpressionTranslator transExp) Return Java source code that computes the qset represented by this object.
RacNode	QSet.Intersection.translate(VarGenerator varGen, String resultVar, AbstractExpressionTranslator transExp) Return Java source code that computes the qset represented by this object.
abstract RacNode	Translator.translate() Translate a JML quantified expression into Java source code and return the result.
abstract RacNode	Translator.generateLoop(RacNode body) Returns a loop code that evaluates the given body with the quantified variable bound to each possible value of the range.
RacNode	StaticAnalysis.translate() Translate a JML quantified expression into Java source code and return the result.
private RacNode	StaticAnalysis.translateForAll() Return Java source code for evaluating a JML quantified expression of a univeral quantifier.
private RacNode	StaticAnalysis.translateExists() Return Java source code for evaluating a JML quantified expression of an existential quantifier.
private RacNode	StaticAnalysis.translateSum() Return Java source code for evaluating a JML quantified expression of a generalized quantifier \sum.
private RacNode	StaticAnalysis.translateProduct() Return Java source code for evaluating a JML quantified expression of a generalized quantifier \product.
private RacNode	StaticAnalysis.translateMin() Return Java source code for evaluating a JML quantified expression of a generalized quantifier \min.
private RacNode	StaticAnalysis.translateMax() Return Java source code for evaluating a JML quantified expression of a generalized quantifier \max.
private RacNode	StaticAnalysis.translateNumOf() Returns code for evaluating numerical quantifiers\num_of.
private RacNode	StaticAnalysis.transForAllOrExists() Returns Java source code for evaluating the JML quantified expression, which is either a universal or existential quantifier.
private RacNode	StaticAnalysis.transSumOrProduct() Returns Java source code for evaluating the JML quantified expression, which is a generalized quantifier \sum or \product.
private RacNode	StaticAnalysis.transMinOrMax() Returns Java source code for evaluating the JML quantified expression, which is a generalized quantifier \min or \max.
RacNode	StaticAnalysis.generateLoop(RacNode body) Returns a loop code that evaluates the given body with the quantified variable bound to each possible value of the range.
protected abstract RacNode	StaticAnalysis.generateLoop(JVariableDefinition varDef, JExpression qexpr, String cond, RacNode result) Returns a loop code evaluating the body of the quantified predicate.
protected RacNode	StaticAnalysis.SetBased.generateLoop(JVariableDefinition varDef, JExpression qexpr, String cond, RacNode result) Returns Java source code for evaluating quantified expressions using the QSet-based translation.
protected RacNode	StaticAnalysis.IntervalBased.generateLoop(JVariableDefinition varDef, JExpression pred, String cond, RacNode result) Returns a loop code for evaluating quantified expressions using the interval-based analysis.
protected RacNode	StaticAnalysis.EnumerationBased.generateLoop(JVariableDefinition varDef, JExpression qexpr, String cond, RacNode result) Returns Java source code for evaluating quantified expressions using the QSet-based translation.
RacNode	TransQuantifiedExpression.generateLoop(RacNode node) Tanslates a JML quantified expression into Java source code that, if executed, evaluates the given statement, node for each combination of bound variables of the quantified expression.