|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV NEXT | FRAMES NO FRAMES |
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)
|
|
ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved |
||||||||||
PREV NEXT | FRAMES NO FRAMES |