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

Package escjava.translate

Class Summary
AssocDeclClipPolicy  
ATarget Infers more precise loop targets.
AuxInfo  
AuxInfoLink  
CalcFreeVars  
Ejp  
ErrorMsg Provides printing of error messages to the user.
Frame  
Frame.ModifiesIterator This class enables iterating over the set of store-ref locations in a ModifiesGroupPragma.
GC  
GCSanity  
GetSpec Responsible for getting Spec for calls.
Helper  
InitialState This class provides two methods used in the generation of a verification condition for a method or constructor (see section 8 of ESCJ 16).
InlineConstructor  
InlineSettings  
Inner * This class contains a number of routines used in the * interpretation of Java 1.1 as Java 1.0
InvariantInfo * This class is used by collectInvariants and its callers, * extendSpecForCall and extendSpecForBody.
LabelInfoToString  
NoWarn Handles turning off warnings.
ParamAndGlobalVarInfo This class is used by collectParamsAndGlobalVars and its * caller, extendSpecForCall.
Purity  
RepHelper  
Substitute Responsible for performing substitutions in expressions.
Substitute.SetRef  
Suggestion This class generates possible ways to annotate a program to eliminate a given warning.
Targets Provides methods for computing various kinds of syntactic targets
TrAnExpr Translates Annotation Expressions to GCExpr.
Translate  
Translate.Strings  
UniqName This class provides methods for unique-ifying names, as described in ESCJ 23b, "Unique names in ESC/Java".
VcToString  
VcToStringPvs  
 


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