|
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 CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectescjava.translate.UniqName
This class provides methods for unique-ifying names, as described
in ESCJ 23b, "Unique names in ESC/Java".
Methods suffixToString
and suffixToLoc
call
private method parseSuffix
whose out-parameters are stored
in some static fields of this class, these methods are not thread safe.
(To make them thread safe, these numbers could be returned in a
newly allocated array.)
Field Summary | |
private static int |
autoBoundVariable
Use this location *only* in declarations of automatically generated bound variables. |
private static int |
idDefaultSuffixFile
Sets the "default suffix file to be that of location loc , or to none if loc is the null location.
|
private static java.util.Hashtable |
mapObjStr
* Ensuring unique names for variables: * * |
private static java.util.Hashtable |
mapStrObj
|
private static int |
psout0
|
private static int |
psout1
|
private static int |
psout2
|
static int |
specialVariable
Use this location *only* in declarations of special variables (see case 4 of ESCJ 23b for the complete list of these). |
static int |
temporaryVariable
Use this location *only* in declarations of temporary variables (see case 6 of ESCJ 23b for rules on the names allowed for these). |
Constructor Summary | |
UniqName()
|
Method Summary | |
static java.lang.String |
locToSuffix(int loc)
Convert a location into a printable string suitable for use as a suffix in unique-ifying a name declared at loc .
|
static java.lang.String |
locToSuffix(int loc,
boolean useDefault)
|
static LocalVarDecl |
newBoundThis()
Returns a new bound variable for use in quantifying over "this" in an invariant. |
static LocalVarDecl |
newBoundVariable(char prefix)
Returns a new bound variable for use in a quantificiation, where we do not wish to or cannot associate the variable with an existing VariableAccess. |
static LocalVarDecl |
newBoundVariable(java.lang.String name)
Private routine to create a new bound variable for use in a quantificiation, where we do not wish to or cannot associate the variable with an existing VariableAccess. |
static LocalVarDecl |
newIntermediateStateVar(GenericVarDecl vd,
java.lang.String suffix)
|
static LocalVarDecl |
newIntermediateStateVar(VariableAccess v,
java.lang.String suffix)
Returns a new intermediate-state variable associated with an existing VariableAccess. |
private static boolean |
parseSuffix(java.lang.String suffix,
boolean recoverable)
Parses suffix , which is expected to have one of the forms
Number "." |
static void |
resetUnique()
Reset the |
static void |
setDefaultSuffixFile(int loc)
|
static int |
suffixToLoc(java.lang.String suffix)
Returns the location corresponding to suffix .
|
static int |
suffixToLoc(java.lang.String suffix,
boolean recoverable)
Returns the location corresponding to suffix , if any,
and the null location if suffix is not a valid suffix.
|
static java.lang.String |
suffixToString(java.lang.String suffix)
Convert a location suffix string into a printable string that describes the location. |
static java.lang.String |
type(Type t)
Returns the unique-ification of the type t . |
static java.lang.String |
variable(GenericVarDecl v)
Returns the unique-ification of the variable v . |
private static java.lang.String |
verifyUnique(GenericVarDecl o,
java.lang.String s)
|
Methods inherited from class java.lang.Object |
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait |
Field Detail |
private static int idDefaultSuffixFile
loc
, or to none if loc
is the null location.
The default suffix file is used in the converting of a location to
a suffix and back.
private static int psout0
private static int psout1
private static int psout2
public static final int specialVariable
public static final int temporaryVariable
private static final int autoBoundVariable
private static java.util.Hashtable mapObjStr
private static java.util.Hashtable mapStrObj
Constructor Detail |
public UniqName()
Method Detail |
public static void setDefaultSuffixFile(int loc)
public static java.lang.String locToSuffix(int loc)
loc
.
Precondition: loc
should be a valid non-null location.
Postcondition: \result != null
public static java.lang.String locToSuffix(int loc, boolean useDefault)
public static int suffixToLoc(java.lang.String suffix)
suffix
.
Requires suffix
to be a valid suffix.
public static int suffixToLoc(java.lang.String suffix, boolean recoverable)
suffix
, if any,
and the null location if suffix
is not a valid suffix.
Requires recoverable
or that suffix
is
a valid suffix.
public static java.lang.String suffixToString(java.lang.String suffix)
Precondition: suffix
should be a string previously
returned by locToSuffix
, and the default suffix
file should be the same as it was when the corresponding
locToSuffix
was called.
Not thread safe.
private static boolean parseSuffix(java.lang.String suffix, boolean recoverable)
suffix
, which is expected to have one of the forms
idDefaultSuffixFile
.
The third form indicates a stream number, where the location that
was converted into this suffix string was a whole-file location
(this occurs if the location refers to a place in a .class file).
This method uses psout0
, psout1
, and
psout2
as out parameters. The will contain the values
of the stream ID, line number, and column number of the location parsed
from the suffix, or the stream ID and two 0's if the suffix has
the third form.
If recoverable
is true
, then this method
can be called even if suffix
is not known to be a valid
suffix. If it isn't, false
is returned. If
suffix
is a valid suffix, then true
is
returned.
Not thread safe (since global variables are used to contain out parameters).
public static java.lang.String type(Type t)
t
. Handles case 7 of ESCJ 23b.
public static LocalVarDecl newBoundVariable(char prefix)
See newBoundThis() for an important exceptional case, though.
The resulting name will be of the form "
(This partially handles case 3 of ESCJ 23b.)
public static LocalVarDecl newBoundThis()
The resulting name will be of the form "brokenObj". (This partially handles case 3 of ESCJ 23b.)
public static LocalVarDecl newBoundVariable(java.lang.String name)
This handles case 3 of ESCJ 23b.
public static LocalVarDecl newIntermediateStateVar(VariableAccess v, java.lang.String suffix)
The resulting name will be of the form
This handles case 15 of ESCJ 23b.
public static LocalVarDecl newIntermediateStateVar(GenericVarDecl vd, java.lang.String suffix)
public static java.lang.String variable(GenericVarDecl v)
v
. Handles cases 3, 4, 6, 10, 11, 12, 13 and 15 of ESCJ 23b.
public static void resetUnique()
private static java.lang.String verifyUnique(GenericVarDecl o, java.lang.String s)
|
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 CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |