Download ESC/Java User's Manual

expression of type \TYPE. If E denotes an array type T[], then \elemtype(E) denotes T. Otherwise the value
of \elemtype(E) is unspecified.
3.2.3 Subtype: <:
An expression of the form S <: T where S and T are specification expressions of type \TYPE is a specification
expression of type boolean. It denotes that S is a subtype of T (including the case where S is equal to T). The
operator <: has the same binding power as the relational operators <, >, <=, and >=.
3.2.4 Examples involving \TYPE, \type, \typeof, \elemtype, and <:
Suppose file T.java contains the following declaration
class T {
//@ requires a != null && 0 <= i & i < a.length;
static void storeObject(T[] a, int i, T x) {
a[i] = x;
}
...
When checking the body of the storeObject method, ESC/Java will produce an ArrayStore warning
(section 4.1) for the assignment
a[i] = x;
The problem is that, so far as ESC/Java can tell, the actual type of a at the time of the call might be S[], where S
is some proper subtype of T, and x might not be of type S. Consequently, the attempt to store x into a[i] might
give rise to an ArrayStoreException [JLS, 10.10, 15.25.1], which ESC/Java treats as an error.
The ArrayStoreException cannot arise in the method if the parameter a always has actual type exactly T[].
The programmer can express this intention with the pragma
//@ requires \elemtype(\typeof(a)) == \type(T);
or, equivalently, with the pragma
//@ requires \typeof(a) == \type(T[]);
Note that
//@ requires \typeof(a) == \type(T)[];
would not be legal, since the form N[] makes sense only when N is a specification type, not a specification
expression of type \TYPE.
A weaker, but still sufficient, precondition for avoiding the ArrayStoreException would be to require that the
array a merely have an actual element type adequate to hold the value of x. This precondition is expressed by
the pragmas
56 of 95