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?

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:

• 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:

• 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