ESCJ 7: ESC/Java Annotation Reference Manual
Last modified by rustan on 2 Sep 1997.
This is the ESC/Java annotations reference manual, an evolving document.
The keywords shown are not necessarily the final ones. Some things are
still to be written (TBW).
A specification expression is a side-effect free Java expression,
possibly containing quantifications.
New adjectives for instance variables
writable-deferred
An instance variable x in a class C can be declared with
the adjective writable-deferred. This makes x writable-deferred
in C. For every update of a designator o.f, where o
is of static type C, ESC/Java checks that f is not writable-deferred
in C. This check is done by a syntactic scan of the code being checked.
defined-if
A field x can be declared with the adjective defined-if
E, where E denotes some boolean specification expression
in which all free variables are (at least) as accessible to every client
as x is. For example, if x is declared as protected
in a class C, then every free variable in E must either be
protected or package and declared in a superclass of
C, or be public. ESC/Java checks that condition E
holds whenever x is read.
monitored-by
In a similar fashion, a field x can be declared with the adjective
monitored-by m, where m denotes a nonempty list
of specification expressions denoting objects. Each free variable in m
must be as accessible as x. If x is an instance variable,
this is allowed to occur in m.
A field x is allowed at most one monitored-by adjective.
If there is one, ESC/Java will do a check for each read or write of x.
For each read of x, ESC/Java checks that at least one of the the
non-null locks in m is in the locking set of the current
thread. For each write of x, ESC/Java checks that every lock in
m is either null or is in the locking set of the current
thread, and checks that at least one of the locks in m is non-null.
monitored
As a convenient shorthand, if f is an instance variable, the adjective
monitored is short for monitored-by this.
New class members
writable-deferred
A class C that extends a class B can declare writable-deferred
x; if x is a variable declared in a proper supertype
of C in such a way that C can read it (in other words, x
is not declared private), provided that x is writable-deferred
in B. The declaration makes x writable-deferred in C.
invariant
A class C that extends a class B can declare invariant
J;, where J is a boolean specification expression.
The annotation declares J as an object invariant of class C.
The free variables in J must either be fields declared in C,
or be fields that are declared in a proper supertype of C and that
are writable-deferred in B. Fields of fields are not allowed to
be mentioned. Also, all free variables in J must have the same protection
level. ((Footnote: This restriction can be dropped if we change our methodological
view of Java scoping/protection rules.))For example, they can all be private
or all be protected. The protection level of the invariant is
the same as that of the variables it mentions. For example, an object invariant
that mentions protected fields is said to be protected.
A class can have any number of object invariant declarations.
Let S denote a method body given in a class K and let
J denote an object invariant of a class C accessible to class
K. Then, ESC/Java will check that J holds for every C
object at every method invocation within S, at every call to a constructor
within S, and upon exit from S. ESC/Java will also assume
that J holds for every C object upon entry to S, upon
return from any method invocation within S, and upon return from
any constructor call within S.
There is an exception to the rule described in the previous paragraph.
If C is a subclass of K, S is the body of a constructor,
and the dynamic type of this is a subtype of C, then "every
C object" in the paragraph above should be replaced by "every C
object other than this". However, if K is C, then
ESC/Java will check that J holds for this upon exit from
S.
New adjectives for methods
Method specifications
A method m declared in a class C can have the following adjectives,
which together are referred to as the specification of m:
-
requires P
-
where P is a boolean specification expression that may mention as
free variables any parameter to m and any variable that is accessible
to all clients of m (here and throughout, parameter includes
this unless m is static)
-
modifies w
-
where w is a list of designator expressions accessible within
class C. A designator can be a static field, an expression o.f
where o is a modifies select expression, a[i] where
a is a modifies select expression denoting an array reference and
i is a modifies select expression denoting an integer, and a[]
where a is a modifies select expression denoting an array.
A modifies select expression has one of the following forms:
o, g, g', e.f, e.f', a[i], or
a[i]', where o is a parameter to m or the special
keyword result, g is a static field, and e, a,
and i are modifies select expression denoting an object with an
f field, an array, and an integer, respectively.
The keyword result denotes the result value of m, if
there is one. Primes indicate final values of fields and static values.
-
ensures Q
-
where Q is a boolean specification expression that may mention as
free variables any parameter to m, the special variable result,
and fields accessible to all clients of m. In addition, Q
may mention g', e.f', and a[i]' like in the modifies
clause.
-
raises (T t) Q
-
where T denotes a subclass of Throwable, t is a dummy
variable that can be used in Q to denote the exception being raised
by the method, and Q is as described in the previous paragraph,
except that it may contain t instead of result. The order
of raises annotations makes a difference in the same way that
catch phrases do in the Java try statement.
The precondition of m is the conjunction of all such Ps
and the postcondition of m is the conjunction of all such
Qs.
In any subclass D of C, a new implementation of m
is allowed to extend the specification of m with further modifies
o.f clauses, where o is this and f is a field
introduced in D.
The modifies list of m for a class T is the union
of all ws occurring in modifies w clauses for m
in any superclass of T, unioned with the expression e.f for
any term e.f' occurring in the postcondition of m, unioned
with the expression g for any term g' occurring in the postcondition
of m, and unioned with a[i] for any expression a[i]'
occurring in the postcondition. For example, if o.f'[i].h.k' occurs
in the postcondition, the modifies list will contain o.f and o.f'[i].h.k.
TBW: quantified variables occurring in the postcondition must get some
interpretation in the modifies list.
For an invocation of m on an object t of static type T,
ESC/Java will first check that the precondition of m holds. Then,
it will assign new values to any designator expression e occurring
in the modifies list of m for class T where e is accessible
to the caller, and will expand the set of allocated objects and arbitrarily
assign an outcome of the method. Finally, it assumes the postcondition
of m, which relates the new values of the modified variables with
those the values of variables before the invocation. If the outcome of
the method is exceptional, the exception is re-raised.
For an implementation S of m given in a class T,
ESC/Java will first assume that the precondition of m holds. Then
it will check that the postcondition holds upon exit from S. No
modifies list checking is performed unless the user specifies the -modifiesChecking
switch on the ESC/Java command line. In that case, ESC/Java checks that
for any field o.f that S changes, either o.f is in
the modifies list of m for class T, or o is not a
parameter to m, or o was not allocated upon entry to S.
Locking order
TBW.
New adjectives for local variables
defined-if
A local variable x can be declared with the adjective defined-if
E, where E denotes some boolean specification expression.
ESC/Java checks that condition E holds whenever x is read.
uninitialized
A local variable x can be declared with the adjective uninitialized.
This is useful if the Java compiler requires the programmer to give x
an explicitly initial value and the programmer doesn't want to. ESC/Java
will check that any read of x takes place after x has been
assigned to after its initialization.
Specifying methods of an interface
TBW.
Automatic checks
This section describes checks that ESC/Java performs that don't require
special annotations.
Run-time checks
For every field dereference o.f in the body of a method being checked,
ESC/Java will check that o is non-null, unless:
-
the dereference occurs statically in a context where a surrounding try
statement will catch null-dereference errors,
-
the method specification shows a raises clause for null-dereference
errors, or
-
the user has turned off null-dereference checking, for example
by using an appropriate command line switch.
Similar for all other run-time errors.
Use of this in constructors
ESC/Java also imposes a syntactic restriction on all constructor bodies:
The only uses of this allowed within the constructor body are those
of the form this.f for some field f. That is, the reference
this is not allowed to be passed to any method or assigned to any
field.
Candidate additions
The keywords writable-private, writable-package, writable-protected,
and writable-public. To be placed at the declaration of a field.
Allowing extensions to method specifications to allow ensures
clauses.
HP SRC Classic Lab
Mail Stop 1250
1501 Page Mill Road, Palo Alto, CA 94304
Tel: (650) 857-2361 Fax: (650) 852-8186
|
|
Send comments to the owner of this page.
Last modified: Monday, 27-Jan-2003 16:29:40 PST
|
Legal
Statement Privacy Statement