ESCJ 31: Naming, revised

By Rustan Leino and Todd Millstein, 28 Aug 1999.

This note describes revisions to the naming scheme used in ESC/Java, as described in ESCJ 23b.

Arbitrary-value variables

The random variables (arbitrary-value variables) had been used to represent arbitrary values of a certain variables. In particular, they were used

  1. as zero-equivalent value initially assigned to reference-typed or TYPE-typed instance fields inside a constructor, and
  2. as the new, arbitrary value of a variable modified as a result of a routine call.

Previously, the random variables had the form randomN, where N is a natural number (generated in sequence for subsequent random variables). Now, they have the respective forms:

  1. f@zero where f is the name of the instance field.
  2. If the modified variable is one of the special variables EC, RES, or XRES, then the name of the random variable is EC:L, RES:L, and XRES:L, where L is the location of the call. If the modified variable is not one of these special variables, then the name of the random variable is after@L, where again L is the location of the call.

Note that EC, RES, and XRES may now be followed by :L, where previously (in ESCJ 23b) this was not possible.

Temporary variables

The temporary (tmp) variables used as temporary variables for various purposes. Previously, they had the form tmpN, where N is a natural number (generated in sequence for subsequent temporary variables). Now they have one of the forms tmpN:L and tmpN!S:L, where N is as before a natural number, S is a suffix string (described below), and L is a location. The suffix S is used to provide more information in the name of the temporary variable. In general, the location L used on a temporary is the primary location (described below) of the source expression whose value the temporary variable holds. The primary location is some location within an expression that uniquely determines the expression. The following table explains the primary locations of expressions:

Temp holds value of: Suffix Primary location
unary operation   start location of the operator
~binary operation   start location of the operator
method invocation m(...) m location of (
E in switch (E) { ... switch start location of E
E in synchronized (E) { ... synchronized start location of E
arrayinit {E0, ... arrayinit location of {
new T[E] new!T[] location of new
new T(...) new!T location of (
G ? E0 : E1 cond location of ?
E0 && E1 cand location of &&
E0 || E1 cor location of ||
variable access x x location of x
result of x assignOp E when result is the new value of x x= location of assignOp
old value of x in x assignOp E old!x location of assignOp
field access o.f f location of f
result of o.f assignOp E when result is the new value of o.f f= location of assignOp
old value of o.f in o.f assignOp E old!f location of assignOp
array access a[i]   location of [
result of a[i] assignOp E when result is the new value of a[i] assignOp E   location of assignOp
old value of a[i] assignOp E old location of assignOp
value of object designator o in field access o.f, when this object designator needs to be protected in the course of performing read or write check od location associated with the corresponding read or write check

Legal Statement Privacy Statement