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

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)
           
 


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

The ESC/Java2 Project Homepage