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

escjava.translate
Class UniqName

java.lang.Object
  extended byescjava.translate.UniqName

public final class UniqName
extends java.lang.Object

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 -uniqueness-ensuring mechanism.
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

idDefaultSuffixFile

private static int idDefaultSuffixFile
Sets the "default suffix file to be that of location 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.


psout0

private static int psout0

psout1

private static int psout1

psout2

private static int psout2

specialVariable

public static final int specialVariable
Use this location *only* in declarations of special variables (see case 4 of ESCJ 23b for the complete list of these).


temporaryVariable

public static final 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).


autoBoundVariable

private static final int autoBoundVariable
Use this location *only* in declarations of automatically generated bound variables. (See case 3 of ESCJ 23b for rules on the names allowed for these).


mapObjStr

private static java.util.Hashtable mapObjStr
* Ensuring unique names for variables: * *


mapStrObj

private static java.util.Hashtable mapStrObj
Constructor Detail

UniqName

public UniqName()
Method Detail

setDefaultSuffixFile

public static void setDefaultSuffixFile(int loc)

locToSuffix

public 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.

Precondition: loc should be a valid non-null location.

Postcondition: \result != null


locToSuffix

public static java.lang.String locToSuffix(int loc,
                                           boolean useDefault)

suffixToLoc

public static int suffixToLoc(java.lang.String suffix)
Returns the location corresponding to suffix. Requires suffix to be a valid suffix.


suffixToLoc

public 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. Requires recoverable or that suffix is a valid suffix.


suffixToString

public static java.lang.String suffixToString(java.lang.String suffix)
Convert a location suffix string into a printable string that describes the location.

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.


parseSuffix

private static boolean parseSuffix(java.lang.String suffix,
                                   boolean recoverable)
Parses suffix, which is expected to have one of the forms The first form indicates a stream ID, a line number (1-based), and and column number (0-based). The second form indicates a line number and a column number, where the implicit stream ID number is 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).


type

public static java.lang.String type(Type t)
Returns the unique-ification of the type t.

Handles case 7 of ESCJ 23b.


newBoundVariable

public 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.

See newBoundThis() for an important exceptional case, though.

The resulting name will be of the form "".

(This partially handles case 3 of ESCJ 23b.)


newBoundThis

public static LocalVarDecl newBoundThis()
Returns a new bound variable for use in quantifying over "this" in an invariant.

The resulting name will be of the form "brokenObj". (This partially handles case 3 of ESCJ 23b.)


newBoundVariable

public 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.

This handles case 3 of ESCJ 23b.


newIntermediateStateVar

public static LocalVarDecl newIntermediateStateVar(VariableAccess v,
                                                   java.lang.String suffix)
Returns a new intermediate-state variable associated with an existing VariableAccess.

The resulting name will be of the form :, where is the location of the variable reference in the given VariableAccess if available, and the location of the variable declaration otherwise.

This handles case 15 of ESCJ 23b.


newIntermediateStateVar

public static LocalVarDecl newIntermediateStateVar(GenericVarDecl vd,
                                                   java.lang.String suffix)

variable

public static java.lang.String variable(GenericVarDecl v)
Returns the unique-ification of the variable v.

Handles cases 3, 4, 6, 10, 11, 12, 13 and 15 of ESCJ 23b.


resetUnique

public static void resetUnique()
Reset the -uniqueness-ensuring mechanism.


verifyUnique

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

The ESC/Java2 Project Homepage