Uses of Class
org.jmlspecs.jml4.rac.quantifiedexpression.RacContext

Packages that use RacContext

org.jmlspecs.jml4.rac.quantifiedexpression

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

Methods in org.jmlspecs.jml4.rac.quantifiedexpression that return RacContext

static RacContext	RacContext.createNegative() Returns a new negative context.
static RacContext	RacContext.createNeutral() Returns a new neutral context.
static RacContext	RacContext.createOpposite(RacContext ctx) Returns a new context that has the opposite polarity to the given context, but with the same status.
static RacContext	RacContext.createPositive() Returns a new positive context.

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

static RacContext	RacContext.createOpposite(RacContext ctx) Returns a new context that has the opposite polarity to the given context, but with the same status.
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.

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

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