ESCJ 30: ESC/Java Refcard
Compiled by Silvija Seres, June 1999.
This document is intended to be a non-detailed, trimmed-down version of the
ESC/Java user manual (ESCJ 27),
for people who would like to get an overview of the expressive power of the
ESC/Java annotation language without getting immersed in all its technical intricacies.
It can be a useful reading aid for examples of ESC/Java annotated programs.
For more detailed information, please refer to the ESC/Java user manual (ESCJ 27).
For information about the invocation of the ESC/Java checker, please see the
escjava(1) man page (ESCJ 26).
What does ESC/Java do anyway?
Type annotation and
static type checking of programs have proved to be one of
biggest engineering successes of computer science. Typing
provides a coarse semantics for programs, since it pays no
attention to the semantics of any language constructs that
are not related to types. Nevertheless, the automatic type
checking of programs weeds out already at compile time many
of the most common programming errors, thus making them less
costly for the developers. Also, typing forces a certain
discipline upon the programmer, which results in better
programs.
The ESC/Java language is pushing the idea behind
type checkers a few steps further. The class of errors that
it looks for is much larger and more varied: it addresses,
among others, the potential run-time errors that arise from
illegal array operations, null-pointer dereferencing,
deadlocks and race conditions of threads. Given a Java
program, it automatically infers and checks a set of
verification conditions that correspond to the described
classes of errors. Furthermore, it also allows the
programmer to record design decisions, and to influence the
choice of verification conditions by annotating the program
with a set of pragmas. These can be used to specify
the pre- and post-conditions of routines, modifications of
global variables, properties of abstract-data types,
invariants of loops, and much more.
The errors that ESC/Java looks for are chosen on a
pragmatic basis; they are the errors that, according to the
engineering experience, occur often and are relatively cheap
to find, but the ESC/Java system is flexible and can be
extended to allow for checking of other types of
errors. Presently, ESC/Java is checking Java 1.0 code and
only a subset of the new Java 1.1 features, and the
upgrading is a subject of current work.
In terms of program verification, ESC/Java is unsound, because it can miss
real programming errors (from the specified class), and it is incomplete,
because it can give some spurious warnings. Some unsoundness will always occur
in automated tools like ESC/Java as a result of a tradeoff between the efficiency
of the tool and its semantical completeness. Even so, ESC/Java shows an unprecedented
level of semantical accuracy combined with automation. The user has some control
over ESC/Java's incompleteness thanks to pragmas. These pragmas not only enable
modular program verification, but are also a convenient formalism for recording
programmers' design decisions and program specifications.
The remainder of this page describes the pragmas available in the current ESC/Java
checker and the other concepts used in the pragma annotations.
There are four syntactic categories of ECS/Java pragmas:
A pragma is enlosed in a Java comment whose first character is an @.
For example, /*@ non_null */ is a ESC/Java pragma.
- lexical pragmas may occur in the same places as Java comments,
- statement pragmas may occur in the same places as Java statements,
- declaration pragmas may occur in the same places as Java declarations
of class and interface members,
- modifier pragmas may occur in certain places within Java declarations
of variables or routines.
The list of ECS/Java pragmas with their (syntactic,
semantic) contexts:
The semicolon is a pragma separator, not a terminator.
- nowarn L; (lexical, general):
L denotes a possibly empty comma-separated list of warning types; ECS/Java will suppress any warning messages
of the types in L (or of all types, if L is empty) at the
line where the pragma appears.
- assert E; (statement, general):
E denotes a boolean specification expression; ECS/Java will issue a warning
if it cannot establish that E is true whenever control reaches the
pragma.
- assume E; (statement, general):
E denotes a boolean specification expression; ESC/Java will assume that E
is true whenever control reaches the pragma and ignores the remainder of all
execution paths in which E is false.
- unreachable; (statement,general): semantically equivalent
to assert false;
- requires E; (modifier, routine):
E denotes a boolean specification expression that is a precondition of the routine
the pragma modifies; ESC/Java will assume that E holds initially
when checking the implementation of the routine, and issue a warning if it
cannot establish that E holds at a call site.
- modifies S; (modifier, non-overriding routine):
S denotes a nonempty comma-separated list of modification
targets; ESC/Java will assume that the routine call modifies only the
modification targets in S and the freshly allocated state components,
but will not check the routine implementation correspondingly (that is, ESC/Java
does not warn about implementations that modify more targets than S
allows).
- ensures E; (modifier, non-overriding routine):
E denotes a boolean specification expression that is a normal (i.e. non-exceptional)
postcondition of the routine the pragma modifies; ESC/Java will assume that
E holds just after each call site the routine, and will issue a warning
if it cannot prove from the routine implementation that E holds whenever
the routine terminates normally.
- exsures (T t) E; (modifier, non-overriding routine):
T is a subtype of java.lang.Throwable, and E denotes
a boolean specification expression that is an exceptional postcondition
of the routine the pragma modifies, i.e. E holds whenever the routine
completes abruptly by throwing an exception t whose type is a subtype
of T.
- also_ensures E; (modifier, overriding routine):
This pragma may modify only method declarations that override other method
declaration; otherwise, it has the same denotation as ensures E;
- also_exsures (T t) E; (modifier, overriding routine):
This pragma may modify only method declarations that override other method
declaration; otherwise, it has the same denotation as exsures E;
- also_modifies S; (modifier, overriding routine):
This pragma may modify only method declarations that override other method
declaration; otherwise, it has the same denotation as modifies S;
- non_null (modifier, data invariant):
Modifies the declaration of a variable of a reference type, where the variable
may be a static field, instance variable, local variable, or parameter; ESC/Java
will check at each assignment to the variable that the value assigned is not
null, and assume at each use that the value is not null.
- invariant E; (declaration, data invariant):
E denotes a boolean specification expression that is an object invariant of
the class within whose declaration the pragma occurs. If E does not
mention this, the invariant is called a static invariant, and is
assumed on entry to implementations, check at call sites, assumed upon call
returns, and checked on exit from an implementation. If E mentions
this, the invariant is called an instance invariant. An instance
invariant is assumed to hold for all objects of the class on entry to an implementation
and is checked to hold for all objects of the class on exit from an implementation.
At a call site, a call is an instance invariant is checked only for those
objects passed in the parameters of the call and in static fields. A call
is assumed not to falsify the invariant for any object.
- axiom E; (declaration, data invariant):
ESC/Java assumes that E is true at the start of every routine body
- loop_invariant E; (statement, data invariant):
This pragma may appear only within the body of a Java for, while,
or do statement. ESC/Java will check that E holds at the
start of each iteration of the loop.
- spec_public (modifier, variable referencing):
This pragma may modify only non-public field declarations, and it will cause
the fields in the declaration to be as accessible in pragmas as they would
have been if the declaration had been public.
- defined_if E; (modifier, variable referencing):
This pragma may modify only field declarations or local variable declarations;
E denotes a boolean specification expression
that has to be true before any read access to any of the fields or variables
in the declaration.
- uninitialized (modifier, variable referencing):
This pragma may modify only a local variable declaration that has an initializer;
ESC/Java will check that no execution path accesses the variable without first
performing an assignment (other than the initializer) to the variable.
- ghost M S VD; (declaration, ghost variables):
S is a specification type, VD is an identifier, and M
is a sequence of modifiers including public; this pragma is like
an ordinary Java variable declaration M S VD; except that it makes
the declaration visible only to ESC/Java, and not to the compiler; such variables
are called ghost variables.
- set D = E; (statement, ghost variables):
D refers to a ghost field of some object or class and E
is a specification expression containing no quantifiers
or labels; this pragma has the same meaning as the Java assignment statement
D = E
- monitored_by SL; (modifier, synchronization):
The modified field is a shared variable monitored by the locks in SL,
which is a nonempty, comma-separated list of specification expressions. ESC/Java checks that the field
is never read except by a thread holding at least one non-null lock in SL
and that the field is never written except by a thread holding all non-null
locks in SL.
- monitored (modifier, synchronization):
This pragma may modify only an instance variable declaration, and is the same
as monitored_by this;
The ESC/Java specification expressions:
A specification type is either a Java type or one of the special types TYPE
or LockSet (or an array of special types, for example TYPE[][]).
The specification type LockSet cannot be mentioned in annotations.
Specification expressions must be free of subexpressions that may potentially
have side effects, so they may not contain any assignment (=, +=,
etc.), pre/post-increment/decrement (++ or --), array or object
creation (new), or method invocation.
The additional constructs that are allowed in specification expressions beyond
those allowed in Java expressions are:
-
type(T): TYPE
denotes the
specification type T,
-
typeof(E): TYPE
denotes the
dynamic type of the value of specification expression
E which has reference type,
-
elemtype(E): TYPE
denotes the
specification type T if E denotes an array
type T[], unspecified otherwise,
-
S <: T: boolean
denotes that
S is a subtype of T, where S and
T are specification expressions of type
TYPE,
-
LS: LockSet
denotes the set of
locks held by the current thread
-
S[L]: boolean
denotes that
L is a member of S, where S is a
specification expression of type LockSet and
L is a specification expression of a reference type
-
max(S): Object
denotes the
maximum element of S in the locking order, where
S is a specification expression of type
LockSet
-
classlock(E): Object
denotes
the lock that is acquired by static synchronized methods of
the type denoted by E, where E is a
specification expression of type TYPE
- E ==> F: boolean
denotes the
condition that E implies F, where
E and F are specification expression of
type boolean
-
(forall T V; E): boolean
denotes that E is true for all substitutions of values of type T
for the bound variables V, where T is a specification type,
V is a nonempty comma-separated list of identifiers and E
is a specification expression of type boolean
-
(exists T V; E): boolean
denotes that E is true for some substitution of values of type T
for the bound variables V, where E, T and V
are as above
-
elemsnonnull(A): boolean
denotes that A and all its elements are nonnull, where A
is a specification expression of a reference array type
-
fresh(E): boolean
used in postconditions, denotes that E is non-null and was not allocated
in the pre-state of the routine call, where E is a specification
expression of a reference type
- RES
is a specification expression
whose type is the return type of the non-void method in
whose normal postcondition or modification target it
appears, denoting the value returned by the method
-
PRE(E)
is a specification expression of the same type as the specification expression
E and is used in a postcondition to denote the same thing as E
except that (1) any occurrences in E of a target fields of the routine
are interpreted according to the pre-state value of the field, and (2) if
any modification target of a the routine has the form X[i] or X[*],
then all array accesses within E are interpreted according to the
pre-state contents of arrays
The ESC/Java warning types:
ESC/Java issues warnings for conditions that it regards as
run-time errors, and that, so far is it can tell, might
actually occur at run-time.
- ArrayStore warns that the control may
reach an assignment A[I] = E when the value of
E is not assignment compatible with the actual
element type of A
- Assert warns that control may reach a pragma assert E
when the value of E is false
-
Cast warns that control may reach a cast
(T)E when the value of E cannot be cast to
the type E
- Deadlock warns that control may reach a synchronized
statement or a call to a synchronized method that would acquire a lock in
violation of the locking order
- Exception warns that a routine may terminate abruptly by
throwing an exception that is not an instance of any type listed explicitly
in the routine's throws clause
-
IndexNegative warns that control may reach
an array access A[I] when the value of the index
I is negative
- IndexTooBig warns that control may reach an array access
A[I] when A.length <= I
-
Invariant warns that some object invariant
may not hold when control reaches a routine call, or that
some object invariant may not hold on exit from the current
body
-
LoopInvInit warns that some loop invariant
may not hold at the start of the first iteration of a loop
-
LoopInvIter warns that some loop invariant
may not hold after an iteration of a loop
-
NegSize warns of a possible attempt to
allocate an array of negative length
- NonNull warns of a possible attempt to assign the value
null to a variable whose declaration is modified by a non_null pragma,
or to call a routine with an actual parameter value of null when the declaration
of the corresponding formal parameter is modified by (or inherits) a non_null
pragma
- NonNullInit warns that a constructor may fail to establish
a non-null value for an instance field of the constructed object when the
declaration of that instance field is modified by a non_null pragma
- Null warns of a possible attempt to dereference null, for
example, by field access O.f, an array access O[i], a method
call O.m(...), a synchronized statement synchronized (O) ...,
or a throw statement throw O, where O evaluates to null
-
Post warns that a routine body may fail to
establish some normal postcondition (on terminating
normally) or some exceptional postcondition (when
terminating by throwing an exception of a relevant type)
-
Pre warns that control may reach a routine
call when some precondition of the routine does not hold
-
Race warns of a possible attempt to access a
monitored field while not holding the requisite lock(s)
-
Reachable warns that control may reach an
unreachable pragma
- Undef warns that control may reach a read access to a variable
when the expression in a defined_if pragma modifying the variable's
declaration is false
-
Uninit warns that control may reach a read
access to a local variable before execution of any
assignment to the variable other than an initializer in a
declaration modified by an uninitialized pragma
-
ZeroDiv warns of a possible attempt to apply
the integer division (/) or remainder (%)
operator with zero as the divisor
The ESC/Java modification targets (or
specification designators):
-
a simple name denoting a non-final field,
-
a field access O.f, where O is a
specification expression of a reference type T and
f denotes one of the fields (possibly a ghost field) of
T,
-
an array access of the form A[I], where
A is a specification expression of an array type, and
I is a specification expression of an integral type
other than long,
-
an array range of the form A[*], where
A is a specification expression of an array type.
Legal
Statement Privacy Statement