ESCJ 17a:  ESC/Java Annotation Reference Manual

DIGITAL Confidential.  By Rustan and Jim, 5 February 1998.  Supersedes ESCJ 7.  Revised on 22 May 1998 (ESCJ 17)  and on 21 Dec 1998 (ESCJ 17a).

To do:

0  Checks

ESC/Java can produce the following error messages: Given an annotated Java program, ESC/Java first parses and type checks the program.  It then produces any warnings for the methods to be checked.  Finally, ESC/Java attempts to prove the absence of uncaught exceptions and of ESC/Java violations in the methods to be checked.  Once ESC/Java has reported an uncaught exception or an ESC/Java violation for a given method, it will stop searching for further errors in that method and will instead go on to the next method.

1  Specification expressions, predicates, and designators

The ESC/Java annotations may contain specification expressions, predicates, and specification designators.  To a first approximation, a specification expression is similar to a Java expression, and a specification designator is similar to a Java LeftHandSide [JLS, 19.12].  A predicate is a specification expression of type boolean.  While we have attempted to avoid gratuitous differences between these specification constructs and the corresponding Java constructs, some differences, for example allowing quantifiers and forbidding side effects, are inevitable.

This section describes the syntax and type checking rules for specification expressions and specification designators.  It also describes some additional syntactic restrictions that go beyond type checking.

1.0  Specification expressions

1.0.0  Syntax of specification expressions

The grammar for specification expressions allows a superset of Java expressions: where Unlike the [JLS, 19.11] grammar, the SpecExpr grammar above does not encode operator binding precedence, so here it is:  The binary operator ==> binds less strongly than && and ||, but more strongly than the ternary conditional operator ? :.  The operator <: has the same precedence as the relational operators <, <=, >=, and >.

The labeled expressions (LBLPOS and LBLNEG) are advanced features of the specification language.  A labeled expression is logically equivalent to the contained SpecExpr.  The Identifier (called the label of the expression) is passed through to the theorem prover (which has built-in support for labeled formulas) and is used partly to generate tracing information and partly to identify a part of a counterexample context.

1.0.1  Name resolution in specification expressions

Name resolution for specification expressions differs in several ways from that for Java expressions.

First, the space of declared names is extended to include the special variables LS and RES (as defined in the Java to Guarded Command Translation), the function symbols typeof, elemtype, and max (as defined in the Logic of ESC/Java), the function symbols elemsnonnull, fresh, and PRE (explained below).

The special variables LS and RES hide any local variable, parameter, or unqualified field of the same name.  This hiding applies even in specification expressions where use of LS or RES is disallowed (see section 1.0.4 and section 2.2).

Applications of the function symbols typeof, elemtype, max, elemsnonnull, fresh, and PRE are parsed like method invocations and must always appear unqualified.  Since ordinary method invocations are not allowed in specification expressions (see section 1.0.4), any name conflict between an ESC/Java function symbol and a method is resolved in favor of the function symbol.

Second, bound variables are scoped like Java local variables.  For example, in a quantified expression (forall int k;  a[k] == 0), the declaration int k; introduces the bound variable k, whose scope is the SpecExpr a[k] == 0.  Furthermore, just as Java forbids declaration of an identifier as a local variable within the scope of a parameter or local variable of the same name [JLS, 14.3.2], so ESC/Java forbids declaration of an identifier as a bound variable within the scope of a parameter, local variable, or bound variable of the same name.  Consequently, the quantified expression (forall int k;  a[k] == 0) cannot occur in a scope where there is already a parameter, local variable, or bound variable named k.  ESC/Java also forbids declaration of LS or RES as a bound variable.

Third, the scoping rules of parameters, this, and super are slightly different from those in Java.  In particular:

Finally, the label Identifier in a LBLPOS or LBLNEG expression is part of a separate name space.  The label does not become available for use inside the SpecExpr.  A label is permitted to have the same name as an identifier already in scope or as a label in an enclosing labeled expression.  If a label has the same name as an identifier already in scope, it does not hide that identifier.

1.0.2  Types of specification expressions

Like expressions in Java, every specification expression has a statically determined type [JLS, 15.3].  This type can either be a Java type, the special type TYPE, or the special type LockSet.  The type of a specification expression is determined in the same way as that of a Java expression, with the following additions:

1.0.3  Type correctness of specification expressions

Just as Java requires expressions to be type correct, so ESC/Java requires specification expressions to be type correct.  The type-correctness rules are the same as in Java, with the following exceptions and additions (where e, e0, and e1 are well-typed):

1.0.4  Further restrictions on specification expressions

In addition to the requirement of type correctness, there are some further restrictions on specification expressions.

First, specification expressions must be free of subexpressions that, in general, may have side effects.  In particular, specification expressions may not contain any:

Note that in spite of this rule, specification expressions may have subexpressions that are parsed as if they were method invocations, namely applications of typeof, elemtype, max, elemsnonnull, fresh, and PRE.  Since method invocations are not allowed specification expressions, no ambiguity arises if one of these names is used as a method.  Similarly, there is no danger that type(...) could be confused with a method application.

Second, applications of fresh and PRE are allowed only in postconditions (ensures, also_ensures, exsures, and also_exsures annotations) and loop_invariant annotations.  Furthermore, applications of fresh and PRE are forbidden in the argument to PRE.
Revisit this if we ever add POST to the specification language.

Third, the special variable RES is allowed only in normal postconditions (ensures and also_ensures annotations) and modifies lists (modifies and also_modifies annotations).  (Note that although RES is allowed in modifies lists, it is not a designator, see section 1.1.)

Finally, there are restrictions on the use of quantified expressions and labeled expressions.  A SpecExpr having a quantified expression or labeled expression as a (not necessarily proper) sub-expression may occur only in one of the following contexts:

As a consequence of this restriction, all legal specification expressions containing quantified or labeled subexpressions are of type boolean.  In particular, a quantified or labeled expression may not occur in an argument to the ternary conditional operator ? : (and this restriction cannot be evaded by use of the (boolean) cast operator).
We have considered a -wizard mode that allows applications of arbitrary functions whose names simply get passed to the prover.  Such functions might take boolean arguments, but even in -wizard mode, these arguments must not contain quantifiers or labels.  That is, the limitations just listed apply even in -wizard mode.

Any further restrictions are explained in the descriptions of the particular annotations where they apply.

1.1  Specification designators

1.1.0  Syntax of specification designators

The grammar for SpecDesignator is an extension of the grammar for a Java LeftHandSide [JLS, 19.12]: where the grammars for ExtendedFieldAccess and ExtendedPrimaryNoNewArray are the same as for the Java non-terminals FieldAccess and PrimaryNoNewArray [JLS, 19.12] but with every right-hand side occurrence of Expression replaced by SpecExpr.

1.1.1  Name resolution in specification designators

Names in a SpecDesignator are resolved as in a SpecExpr.

1.1.2  Type correctness of specification designators

The type-correctness rules for a specification designator are as follows:

1.1.3  Further restrictions on specification designators

The following restrictions apply to specification designators:

2  Annotations

ESC/Java annotations are supplied in special Java comments.  When the very first character after the /* or // that begins a Java comment is @, ESC/Java parses the body of the comment as a sequence of zero or more ESC/Java annotations.  Such a comment is called a pragma.

Many annotations end with an optional semi-colon.  If such an annotation is followed by another annotation in the same pragma, then this semi-colon is required.

Annotations fall into four categories:

All annotations occurring within the same pragma must be of the same category, and the pragma is said to be of the same category as the annotations it contains.  An empty pragma is a lexical pragma.

A lexical pragma can occur anywhere a comment can occur.

A statement pragma can occur only where a BlockStatement [JLS, 19.11] can occur.

A declaration pragma can occur only where a ClassMemberDeclaration [JLS, 19.8.1] or an InterfaceMemberDeclaration [JLS, 19.9.1] can occur.

A modifier pragma can occur only

Particular annotations may have further restrictions on where they may occur.  These restrictions will be described in the sections describing the respective annotations.

The following is a complete list of the annotations supported by ESC/Java:

Consider adding the following modifier annotations:  writeable_private, writeable_package, writeable_protected, unused.  Consider leaving out writeable_deferred and still_deferred.

2.0  nowarn (lexical annotation)

2.1  assume (statement annotation)

The SpecExpr must be a predicate, that is, it must be of type boolean.

2.2  axiom (declaration annotation)

The SpecExpr must be a predicate, and is not allowed to mention this, LS, or RES.

2.3  assert (statement annotation)

The SpecExpr must be a predicate.

2.4  unreachable (statement annotation)

2.5  loop_invariant (statement annotation)

The SpecExpr must be a predicate.

A loop_invariant annotation may occur only within a Block [JLS, 19.1.1] that is the body of a Java for, while, or do statement, and it must occur before any Java BlockStatement of that Block.

Any occurrence of a variable (other than a variable introduced in the ForInit if the loop is a for loop), field, or array access within the argument of any PRE in the SpecExpr refers to the value of that variable, field, or array access as of just before the start of the execution of the loop.  Specification expressions such as PRE(x).f and PRE(a)[i] that mix PRE with . or [] are legal and meaningful, but their meanings may be surprising to the naive user.  Consider adding a section with some examples of such mixed expressions and what they mean.  If the loop is a for loop, any variable introduced in the ForInit and occurring within the argument to PRE in the SpecExpr refers to the current value of that variable at the time the loop invariant is asserted or assumed.

Any occurrence of fresh(e) in the SpecExpr evaluates to true if the object denoted by e was not allocated before the start of the execution of the loop, and to false otherwise.

2.6  uninitialized (modifier annotation)

An uninitialized annotation can occur only as a modifier of a local variable declaration that has an initializer.  For example, the first of the following declarations is allowed: whereas the others are not, because they contain variable declarations with no initializing expressions.

Recall that ESC/Java allows local variable declarations to have modifier annotations, even though Java doesn't allow them to have modifiers.

2.7  non_null (modifiers annotation)

The non_null pragma may be used as a modifier to a formal parameter, a local variable, a static field, or an instance variable.

If applied to x, the type of x must be a reference type.
 
If applied to a static field x, the declaration of x must have an initializer (which in a future version of ESC/Java will be checked to result in a non-null value).
 
If a local variable x is declared with both non_null and uninitialized and has an initializing expression E, then the check that E results in a non-null value is suppressed.

2.8  defined_if (modifier annotation)

The SpecExpr must be a predicate.  It is allowed to mention this if the pragma modifies an instance field, or if the pragma modifies a local variable inside a instance method or constructor.

A defined_if annotation can occur only as a modifier of a field declaration or local variable declaration.

If the modifier annotation is applied to a field, the free variables of SpecExpr must be as accessible as the field.

Note:  The current implementation does not allow a local variable to be mentioned in its own defined_if pragma.  This is probably not a feature.

2.9  monitored_by (modifier annotation)

Each SpecExpr must be of a reference type.  If the modifier pragma is applied to an instance variable, each SpecExpr is allowed to mention this.  The free variables of each SpecExpr must be as accessible as the field to which the modifier applies.  For example, is allowed, but is not.

A monitored_by annotation may occur only as a modifier of a field declaration.

2.10  monitored (modifier annotation)

A monitored annotation may occur only as a modifier of an instance variable declaration.

2.11  requires (modifier annotation)

The SpecExpr must be a predicate, which can mention this if the pragma modifies an instance method (not a static method or constructor).

A requires annotation can occur as a modifier only of a method or constructor declaration, and only when the method declaration does not override [JLS, 4.8.6, "Inheritance, overriding, and hiding"] a method declared in a proper superclass.

Each field mentioned in the SpecExpr must be as accessible as the method or constructor.

2.12  ensures (modifier annotation)

The SpecExpr must be a predicate.  It can mention RES if the pragma modifies a non-void instance method (not a static method or constructor).  It can mention this if the pragma modifies an instance method or constructor (not a static method).  It can always mention PRE and fresh.

An ensures annotation can occur as a modifier only of a method or constructor declaration, and only when the method declaration does not override [JLS, 4.8.6, "Inheritance, overriding, and hiding"] a method declared in a proper superclass.

If the pragma modifies a non-final non-private instance method, then every field mentioned in the SpecExpr must be non-private or spec_public.

2.13  also_ensures (modifier annotation)

The SpecExpr must be a predicate.  It can mention this, RES (if the method has a non-void result type), PRE, and fresh.

An also_ensures annotation can occur as a modifier only of a method declaration, and only when the method declaration overrides [JLS, 4.8.6, "Inheritance, overriding, and hiding"] a method declared in a proper superclass.

If the pragma modifies a non-final non-private instance method, then every field mentioned in the SpecExpr must be non-private or spec_public.

2.14  exsures (modifier annotation)

The SpecExpr must be a predicate.  It can mention the Identifier, PRE, and fresh (but not RES).  It can mention this if the method is an instance method (not a static method or a constructor).

An exsures annotation can occur as a modifier only of a method or constructor declaration, and only when the method declaration does not override [JLS, 4.8.6, "Inheritance, overriding, and hiding"] a method declared in a proper superclass.

The Type must be a reference type that is a subtype of some type mentioned in the method's or constructor's throws set.  The name of the Identifier follows the same rules as would a bound variable in a quantified expression surrounding the SpecExpr.

If the pragma modifies a non-final non-private instance method, then every field mentioned in the SpecExpr must be non-private or spec_public.

2.15  also_exsures (modifier annotation)

The SpecExpr must be a predicate.  It can mention this, the Identifier, PRE, and fresh (but not RES).

An also_exsures annotation can occur as a modifier only of a method declaration, and only when the method declaration overrides [JLS, 4.8.6, "Inheritance, overriding, and hiding"] a method declared in a proper superclass.

The Type must be a reference type that is a subtype of some type mentioned in the method's throws set.  The name of the Identifier follows the same rules as would a bound variable in a quantified expression surrounding the SpecExpr.

If the pragma modifies a non-final non-private instance method, then every field mentioned in the SpecExpr must be non-private or spec_public.

2.16  modifies (modifier annotation)

A modifies annotation can occur as a modifier only of a method or constructor declaration, and only when the method declaration does not override [JLS, 4.8.6, "Inheritance, overriding, and hiding"] a method declared in a proper superclass.

2.17  also_modifies (modifier annotation)

An also_modifies annotation can occur as a modifier only of a method declaration, and only when the method declaration overrides [JLS, 4.8.6, "Inheritance, overriding, and hiding"] a method declared in a proper superclass.

2.18  invariant (declaration annotation)

The SpecExpr must be a predicate, but is not allowed to mention LS.

2.19  spec_public (modifier annotation)

A spec_public annotation may occur only as a modifier of a non-public field declaration.

2.20  ghost (declaration annotation)

The public modifier must be given, but can be given either before or after the optional static modifier.

The Type may make use of the special type TYPE.

The VariableDeclarator declares one identifier and must not give an initial value.

2.21  set (statement annotation)

The PrimarySpecExpr must denote a ghost variable.  Both the PrimarySpecExpr and SpecExpr denote terms, that is, they may not contain quantifiers or labeled expressions.

2.22  writeable_deferred (modifier annotation)

Not supported in ESC/Java 1.0. A writeable_deferred modifier annotation can occur only as a modifier of an instance variable declaration V.  The annotation declares each of the instance variables declared in V to be writeable deferred in the current class.

2.23  still_deferred (declaration annotation)

Not supported in ESC/Java 1.0. A still_deferred declaration annotation can be placed only in a class.  The VariableDeclarators must not contain any initializers.  Each identifier in VariableDeclarators must have been declared as writeable deferred in the direct superclass of the current class.

The still_deferred annotation declares each of the instance variables named in the VariableDeclarators to be writeable deferred in the current class.

Legal Statement Privacy Statement