Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

## escjava.translate
Class UniqName

    java.lang.Object
      escjava.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
  - Number "." Number "." Number
  - Number "." Number
  - Number ".."
  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)

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| 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

The ESC/Java2 Project Homepage