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.
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:
Note that EC, RES, and XRES may now be followed by :L, where previously (in ESCJ 23b) this was not possible.
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 |