Uses of Class
org.jmlspecs.jml4.rac.PostStateExpressionTranslator

Packages that use PostStateExpressionTranslator

org.jmlspecs.jml4.rac
org.jmlspecs.jml4.rac.quantifiedexpression

Uses of PostStateExpressionTranslator in org.jmlspecs.jml4.rac

Subclasses of PostStateExpressionTranslator in org.jmlspecs.jml4.rac

class	ConstraintTranslator Translates constraint clauses to history constraint checking methods.
class	ExceptionalPostconditionTranslator Translate the exceptional postcondition of a method or constructor.
class	PostconditionTranslator
class	PreconditionTranslator Translates the precondition of a method or constructor into RAC code.

Uses of PostStateExpressionTranslator in org.jmlspecs.jml4.rac.quantifiedexpression

Fields in org.jmlspecs.jml4.rac.quantifiedexpression declared as PostStateExpressionTranslator

PostStateExpressionTranslator

QuantifiedExpressionTranslator.transExp translator for translating subexpressions

Methods in org.jmlspecs.jml4.rac.quantifiedexpression with parameters of type PostStateExpressionTranslator

static StaticAnalysis	StaticAnalysis.getInstance(VariableGenerator varGen, RacContext ctx, JmlQuantifiedExpression expr, java.lang.String resultVar, PostStateExpressionTranslator transExp, RacResult racResult, SourceTypeBinding typeBinding) Returns an instance of StaticAnalysis, that translates JML quantified expressions into Java source code.
java.lang.String	QInterval.translate(VariableGenerator varGen, java.lang.String lowerVar, java.lang.String upperVar, PostStateExpressionTranslator transExp) Return Java source code that, if executed, evaluates the quantfied interval, i.e., its lower and upper bound values.

Constructors in org.jmlspecs.jml4.rac.quantifiedexpression with parameters of type PostStateExpressionTranslator

QuantifiedExpressionTranslator(VariableGenerator varGen, RacContext context, JmlQuantifiedExpression expr, java.lang.String resultVar, PostStateExpressionTranslator transExp, RacResult racResult, SourceTypeBinding typeBinding)
Constructs a new instance.