Uses of Class
escjava.ast.Spec

Packages that use Spec

escjava.ast
escjava.translate

Uses of Spec in escjava.ast

Fields in escjava.ast declared as Spec

Spec

Call.spec

Methods in escjava.ast that return Spec

static Spec

Spec.make(DerivedMethodDecl dmd, ExprVec targets, ExprVec specialTargets, java.util.Hashtable preVarMap, ExprVec preAssumptions, ConditionVec pre, ExprVec postAssumptions, ConditionVec post, boolean modifiesEverything, java.util.Set postconditionLocations)

Methods in escjava.ast with parameters of type Spec

abstract java.lang.Object	VisitorArgResult.visitSpec(Spec x, java.lang.Object o)
abstract void	Visitor.visitSpec(Spec x)
void	EscPrettyPrint.printSpec(java.io.OutputStream o, int ind, Spec spec)

Uses of Spec in escjava.translate

Methods in escjava.translate that return Spec

static Spec	GetSpec.getSpecForCall(RoutineDecl rd, FindContributors scope, Set predictedSynTargs)
static Spec	GetSpec.getSpecForInline(RoutineDecl rd, FindContributors scope)
static Spec	GetSpec.getSpecForBody(RoutineDecl rd, FindContributors scope, Set synTargs, java.util.Hashtable premap)
private static Spec	GetSpec.getCommonSpec(RoutineDecl rd, FindContributors scope, java.util.Hashtable premap)
private static Spec	GetSpec.trMethodDecl(DerivedMethodDecl dmd, java.util.Hashtable premap) Translates a MethodDecl to a Spec.
private static Spec	GetSpec.extendSpecForCall(Spec spec, FindContributors scope, Set predictedSynTargs) Implements ExtendSpecForCall, section 7.3 of ESCJ 16.
private static Spec	GetSpec.extendSpecForBody(Spec spec, FindContributors scope, Set synTargs) Implements ExtendSpecForBody, section 7.4 of ESCJ 16.

Methods in escjava.translate with parameters of type Spec

private static Spec	GetSpec.extendSpecForCall(Spec spec, FindContributors scope, Set predictedSynTargs) Implements ExtendSpecForCall, section 7.3 of ESCJ 16.
private static Spec	GetSpec.extendSpecForBody(Spec spec, FindContributors scope, Set synTargs) Implements ExtendSpecForBody, section 7.4 of ESCJ 16.
private static void	GetSpec.addInvariantBody(InvariantInfo ii, Spec spec, Set synTargs) Extend spec, in a way appropriate for checking the body of a method or constructor, to account for invariant ii.J declared in class ii.U.
private static ParamAndGlobalVarInfo	GetSpec.collectParamsAndGlobals(Spec spec, FindContributors scope) Collects the parameters of spec.args and the static fields in scope, whose types are class types.
static GuardedCmd	GetSpec.surroundBodyBySpec(GuardedCmd body, Spec spec, FindContributors scope, Set syntargets, java.util.Hashtable premap, int locEndCurlyBrace) Returns a command that first does an assume for each precondition in spec, then does body, then checks the postconditions of spec, and finally checks the modifies constraints implied by spec.
private static void	GetSpec.checkModifiesConstraints(Spec spec, FindContributors scope, Set syntargets, java.util.Hashtable premap, int loc, StackVector code)