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:
-
write a introduction (big picture overview of the system)
-
semantics of all checks
-
In Java-to-Guarded Command translation document: which line
number is associated with a check (to determine whether or check is suppressed
by a nowarn)
-
command line switches
-
function DTTFSA (nee WIZARD, see src.sparta post)
-
Explain what [JLS, 19.4] means, and use it throughout.
-
In Logic document, change elemType to elemtype.
-
Clarify treatment of exceptions vs. runtime errors.
-
Define "current method" and "current class".
-
Clean up "method (or constructor)" language.
-
Add section describing sources of unsoundness and incompleteness.
-
Shorten check names, and make sure they match our implementation.
-
Add Raymie's suggestion for an additional syntactic form of quantifers,
useful when specifying properties of arrays (which is when we expect quantifiers
to be used anyway).
0 Checks
ESC/Java can produce the following error messages:
-
Uncaught exceptions. ESC/Java includes checks to detect the possibility
of the following Java exceptions being raised and not caught:
-
NullPointerException -- an attempt to access a field or call a
method of null or to access an array element of null.
-
IndexOutOfBoundsException -- an attempt to access an array outside
its bounds.
-
ClassCastException -- an attempt to narrow the type of an object
to something it is not.
-
ArrayStoreException -- an attempt to store an object into an array
whose dynamic element type is not a supertype of the object's type.
-
ArithmeticException -- an attempt to divide by the integer 0.
-
NegativeArraySizeException -- an attempt to create an array of
negative length.
If ESC/Java produces one of the error messages above, it doesn't necessarily
mean that the indicated uncaught exception will occur in any execution
of the code being checked; it merely means that ESC/Java is unable to prove
that the exception will never occur, given the annotations that the user
has supplied.
-
ESC/Java violations. ESC/Java allows a user to supply annotations
that record design decisions. It includes checks to detect the following
possible violations of these design decisions:
-
AssertViolation -- An assert statement might not hold.
-
PreconditionViolation -- A precondition of a method call might
not hold.
-
PostconditionViolation -- The current method might not establish
its postcondition.
-
ModifiesViolation -- The current method might modify a variable
not mentioned in its modifies clause.
-
ObjectInvariantViolation -- The current method might fail to preserve
or establish a declared object invariant.
-
InitialLoopInvariantViolation -- A declared loop invariant might
not hold on entry to a loop.
-
IterativeLoopInvariantViolation -- A loop invariant might not
be preserved by the body of a loop.
-
SharingViolation -- A shared variable might be accessed while
the locks declared to protect it are not held.
-
LockingOrderViolation -- A lock might be acquired out of the declared
lock ordering.
-
InitializationViolation -- A local variable might be read before
being given a meaningful value.
-
DefinednessViolation -- A variable might be read while the condition
declaring when it is meaningful does not hold.
-
CodeReachabilityViolation -- A piece of code declared as unreachable
might be reached.
We will define these violations more precisely when we describe the annotations
below.
Again, if ESC/Java produces one of the error messages above, it doesn't
necessarily indicate the presence of an error; it merely means that ESC/Java
is unable to prove that the error will never occur, given the annotations
that the user has supplied.
-
ESC/Java warnings. ESC/Java produces warnings in some situations
when either Java code or annotations use variables in ways that might be
regarded as poor programming style and that may diminish the checker's
effectiveness in detecting errors. These warnings are:
-
ConstructorLeakWarning -- A constructor contains a statement that
uses this as if it were completely constructed before it is.
-
InitializerLeakWarning -- An initializer expression uses this
as if it were completely constructed before it is.
-
WriteableDeferredWarning -- A variable declared as writeable_deferred
is used as an assignment target.
-
UnenforcableObjectInvariantWarning -- An object invariant mentions
a variable that is writeable outside the current scope.
-
ModifiesExtensionWarning -- An also_modifies clause lists
a field of this that neither is declared by the current class
nor is a writeable_deferred field of the direct superclass.
-
IgnoringUninitializedPragmaWarning -- A local variable without
an initializing expression is declared with the uninitialized
pragma, which will be ignored.
ESC/Java produces these warnings based on a purely syntactic inspection
of the program, to be described below. No theorem proving is involved.
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:
SpecExpr ::=
ExtendedExpr
| SpecExpr ==> SpecExpr
| SpecExpr <: SpecExpr
| type ( Type )
| classlock ( Type )
| ( forall BoundVariableDeclarationStatement+
SpecExpr )
| ( exists BoundVariableDeclarationStatement+
SpecExpr )
| ( LBLPOS Identifier SpecExpr )
| ( LBLNEG Identifier SpecExpr )
where
-
the grammar for ExtendedExpr is the same as for a Java Expression
[JLS, 19.12] but with every right-hand side occurrence of Expression
replaced by SpecExpr,
-
the grammar for Type is the same as in Java [JLS, 19.4],
but with the addition of the special type TYPE (described below),
and
-
the grammar for BoundVariableDeclarationStatement is the same as
for a Java LocalVariableDeclarationStatement [JLS, 19.11],
except that initializers are forbidden.
Java 1.1 apparently allows modifiers in local variable
declarations. As far as we can tell, there is no reason to allow
them in bound variable declarations.
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.
Implementation note: If the parser sees
Identifier ( , it compares the Identifier
with "type" and with "classlock". If it matches,
the parser continues to match a Type followed by )
. If it does not match, the parser continues as if the Identifier
were a method name. Since actual method calls are disallowed in specification
expressions (see section 1.0.4),
the only legal Identifier in the latter case would be one of the
ESC/Java special function symbols typeof, elemtype, max,
fresh, or PRE, as explained in section
1.0.1.
Implementation note: If the parser sees (
Identifier , it compares the Identifier with
the strings "forall", "exists", "LBLPOS", and
"LBLNEG". If the Identifier is forall or
exists, and the next token is either a PrimitiveType or
an Identifier, then the parser parses the quantified expression.
If the Identifier is LBLPOS or LBLNEG, and the
next token is an Identifier, then the parser parses the labeled
expression. Otherwise, the parser continues as if the (
Identifier were the beginning of a CastExpression
[JLS, 19.12] or parenthesized expression. No place in the
Java grammar allows an Identifier immediately followed by another
Identifier or PrimitiveType; hence, there is no danger that
the parser will parse an expression as a quantified or labeled expression
when there is some other legitimate way to parse the expression.
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:
-
When a SpecExpr occurs in a modifier annotation (see section
2) applied to a field, names in the SpecExpr are resolved as
if the SpecExpr were part of the initializer of the field.
Consequently, if the field is an instance variable, then this
and super can be mentioned and any unqualified field name f
is a synonym for this.f.
-
When a SpecExpr occurs in a modifier annotation of a method declaration,
names in the SpecExpr are resolved as if the SpecExpr were
placed at the beginning of the method body. Consequently, the names
of the method's parameters are in scope. Furthermore, if the method
is an instance method, then this and super can be mentioned
and any unqualified field name f is a synonym for this.f.
-
When a SpecExpr occurs in a modifier annotation of an abstract method
declaration, names in the SpecExpr are resolved as if the method
could have a body and the SpecExpr were placed there. That
is, the names of the method's parameters are in scope, this can
be mentioned, any unqualified field name f is a synonym for this.f,
and if the abstract method declaration occurs in a class (rather than in
an interface) then super can be mentioned.
-
In any other SpecExpr, the same parameters, local variables, and
fields are in scope as in the Java context where the annotation containing
the SpecExpr occurs; this can be mentioned (and any unqualified
field name f is a synonym for this.f) if the SpecExpr
occurs in a Java context where this can be mentioned; and super
can be mentioned if the SpecExpr occurs in a Java context where
super can be mentioned. Moreover, in a SpecExpr that
occurs in a declaration annotation (see section
2) in a class, this and super can be mentioned and
any unqualified field name f is a synonym for this.f.
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:
-
The type of e0 ==> e1 is boolean.
-
The type of e0 <: e1 is boolean.
-
The type of type(T) is TYPE.
-
The type of classlock(T) is Object.
-
The type of (forall ...) is boolean.
-
The type of (exists ...) is boolean.
-
The type of (LBLPOS n e) is the same as the type of e.
-
The type of (LBLNEG n e) is the same as the type of e.
-
The type of a bound variable is determined by its declaration in the same
way that the type of a local variable is determined.
-
The type of an application of a Logic of ESC/Java function is as follows:
-
The type of typeof(e) is TYPE.
-
The type of elemtype(e) is TYPE.
-
The type of max(e) is Object.
-
The type of elemsnonnull(e) is boolean.
-
The type of fresh(e) is boolean.
-
The type of PRE(e) is the type of e.
-
The type of a special variable is as as follows:
-
The type of LS is LockSet.
-
The type of RES is the same as the result type of the current
method (here, we regard a constructor as a method whose result type is
the class containing the constructor).
-
The type of e0[e1], where e0 is of type LockSet
and e1 is of type Object, is boolean.
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):
-
The expression e0 ==> e1 is well-typed if both e0 and
e1 are of type boolean.
-
The expression e0 <: e1 is well-typed if both e0 and
e1 are of type TYPE.
-
The expression type(T) is well-typed if T is a reference
type.
-
The expression classlock(T) is well-typed if T is a class
type.
-
The expression (forall ...; e) is well-typed if e is
of type boolean.
-
The expression (exists ...; e) is well-typed if e is
of type boolean.
-
The expression (LBLPOS n e) is well-typed (recall the assumption
that e is well-typed).
-
The expression (LBLNEG n e) is well-typed.
-
A bound variable is well-typed.
-
The expression typeof(e) is well-typed if e is of a reference
type.
-
The expression elemtype(e) is well-typed if e is of type
TYPE.
-
The expression max(e) is well-typed if e is of type LockSet.
-
The expression elemsnonnull(e) is well-typed if e is
of an array type.
-
The expression fresh(e) is well-typed if e is of a reference
type.
-
The expression PRE(e) is well-typed.
-
RES is well-typed if the current method is declared with a non-void
result type (RES is not allowed in the specification of constructors).
-
LS is well-typed.
-
The expressions e0 == e1 and e0 != e1 are well-typed
if
-
both operands e0 and e1 are of type boolean,
-
both operands are of numeric types,
-
each operand is either of a reference type or of the null type, or
-
both operands are of type TYPE.
Note that the first three of these cases are exactly the cases in which
an application of == or != is well-typed in Java [JLS,
15.20].
-
The expressions e0 <= e1 and e0 < e1 are well-typed
if
-
both operands are of numeric types, or
-
both operands are of reference types (in this case, the objects are compared
using the locking order mutex$atmost introduced in the Logic
of ESC/Java).
Note that the first case is exactly the case in which an application of
<= or < is well-typed in Java [JLS, 15.19.1].
-
The expression e0[e1] is well-typed if
-
the type of e0 is an array type T[] and the type of e1
(after numeric promotion) is int, or
-
the type of e0 is LockSet and the type of e1
is a reference type.
Note that the first case is exactly the case in which an application of
[] is well-typed in Java [JLS, 15.12].
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:
-
assignment (=, +=, etc.),
-
pre-increment, pre-decrement, post-increment, post-decrement (++
or --),
-
array or object creation (new), or
-
method invocation.
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 an argument to one of the following operators:
-
as the body E of
-
a parenthesized expression (E),
-
a quantified expression (forall ...; E) or (exists
...; E), or
-
a labeled expression (LBLPOS n E) or (LBLNEG n E).
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]:
SpecDesignator ::=
Name
| ExtendedFieldAccess
| ExtendedArrayAccess
ExtendedArrayAccess ::=
Name [ SpecExpr ]
| Name [ * ]
| ExtendedPrimaryNoNewArray [ SpecExpr
]
| ExtendedPrimaryNoNewArray [ * ]
In the future, we may want to allow multiple *-ed
dimensions.
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:
-
A name n is well-typed if it denotes a field.
-
An ExtendedFieldAccess is well-typed if it is well-typed as a SpecExpr.
-
A specification designator e0[e1] is well-typed if it is well-typed
as a SpecExpr and e0 is of an array type (that is, e0
must not be LS).
-
A specification designator e[*] is well-typed if e is
of an array type.
1.1.3 Further restrictions on specification designators
The following restrictions apply to specification designators:
-
A specification designator n, where n is a Name,
must denote a non-final field.
-
The field f in a specification designator e.f must not
be final.
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:
-
lexical annotations
-
statement annotations
-
declaration annotations
-
modifier annotations
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
-
where a Modifier [JLS, 19.7] can occur,
-
between the VariableDeclarators and the ; in
a FieldDeclaration [JLS, 19.8.2],
-
between the MethodHeader and the MethodBody in a MethodDeclaration
[JLS, 19.8.3],
-
before the Type or after the VariableDeclaratorId in a FormalParameter
[JLS, 19.8.3],
We currently don't have any annotations that go in this
position, but unused is an example of one that would.
-
between the Throws (or the ConstructorDeclarator if there
is no Throws) and the ConstructorBody in a ConstructorDeclaration
[JLS, 19.8.5],
-
between the MethodHeader and the ; in an AbstractMethodDeclaration
[JLS, 19.9.1], or
-
before the LocalVariableDeclaration or between the LocalVariableDeclaration
and the ; in a LocalVariableDeclarationStatement
[JLS, 19.11].
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:
LexicalAnnotation ::=
NowarnAnnotation
Consider adding EnableWarnAnnotation and DisableWarnAnnotation.
StatementAnnotation ::=
AssumeAnnotation
| AssertAnnotation
| UnreachableAnnotation
| LoopInvariantAnnotation
| SetStatementAnnotation
DeclarationAnnotation ::=
AxiomAnnotation
| ObjectInvariantAnnotation
| GhostDeclarationAnnotation
| WriteableDeferredDeclarationAnnotation
ModifierAnnotation ::=
UninitializedAnnotation
| NonNullAnnotation
| DefinedIfAnnotation
| MonitoredByAnnotation
| MonitoredAnnotation
| SpecPublicAnnotation
| RequiresAnnotation
| EnsuresAnnotation
| AlsoEnsuresAnnotation
| ExsuresAnnotation
| AlsoExsuresAnnotation
| ModifiesAnnotation
| AlsoModifiesAnnotation
| WriteableDeferredModifierAnnotation
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)
NowarnAnnotation ::=
nowarn Check* [;]
Check ::=
NullPointerException
| IndexOutOfBoundsException
| ClassCastException
| ArrayStoreException
| ArithmeticException
| NegativeArraySizeException
| AssertViolation
| PreconditionViolation
| PostconditionViolation
| ModifiesViolation
| ObjectInvariantViolation
| InitialLoopInvariantViolation
| IterativeLoopInvariantViolation
| SharingViolation
| LockingOrderViolation
| InitializationViolation
| DefinednessViolation
| CodeReachabilityViolation
| ConstructorLeakWarning
| InitializerLeakWarning
| WriteableDeferredWarning
| UnenforcableObjectInvariantWarning
| ModifiesExtensionWarning
2.1 assume (statement annotation)
AssumeAnnotation ::=
assume SpecExpr [;]
The SpecExpr must be a predicate, that is, it must be of type boolean.
2.2 axiom (declaration annotation)
AxiomAnnotation ::=
axiom SpecExpr [;]
The SpecExpr must be a predicate, and is not allowed to mention
this, LS, or RES.
2.3 assert (statement annotation)
AssertAnnotation ::=
assert SpecExpr [;]
The SpecExpr must be a predicate.
2.4 unreachable (statement annotation)
UnreachableAnnotation ::=
unreachable [;]
2.5 loop_invariant (statement annotation)
LoopInvariantAnnotation ::=
loop_invariant SpecExpr [;]
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.
The current implementation does not support PRE
and fresh in invariants.
2.6 uninitialized (modifier annotation)
UninitializedAnnotation ::=
uninitialized
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:
/*@ uninitialized */ T x = null, y = new(T) ;
/*@ uninitialized */ T w, z = null ;
/*@ uninitialized */ T v ;
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)
NonNullAnnotation ::=
non_null
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)
DefinedIfAnnotation ::=
defined_if SpecExpr [;]
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)
MonitoredByAnnotation ::=
monitored_by SpecExpr ( , SpecExpr
)* [;]
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,
public Object mu ;
private int x /*@ monitored_by mu */ ;
is allowed, but
private Object mu ;
public int x /*@ monitored_by mu */ ;
is not.
A monitored_by annotation may occur only as a modifier of a
field declaration.
2.10 monitored (modifier annotation)
MonitoredAnnotation ::=
monitored
A monitored annotation may occur only as a modifier of an instance
variable declaration.
2.11 requires (modifier annotation)
RequiresAnnotation ::=
requires SpecExpr [;]
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)
EnsuresAnnotation ::=
ensures SpecExpr [;]
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)
AlsoEnsuresAnnotation ::=
also_ensures SpecExpr [;]
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)
ExsuresAnnotation ::=
exsures ( Type Identifier
) SpecExpr [;]
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)
AlsoExsuresAnnotation ::=
also_exsures ( Type Identifier
) SpecExpr [;]
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)
ModifiesAnnotation ::=
modifies [ SpecDesignator ( ,
SpecDesignator )* ] [;]
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)
AlsoModifiesAnnotation ::=
also_modifies [ SpecDesignator (
, SpecDesignator )* ] [;]
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)
ObjectInvariantAnnotation ::=
invariant SpecExpr [;]
The SpecExpr must be a predicate, but is not allowed to mention
LS.
2.19 spec_public (modifier annotation)
SpecPublicAnnotation ::=
spec_public
A spec_public annotation may occur only as a modifier of a non-public
field declaration.
2.20 ghost (declaration annotation)
GhostDeclarationAnnotation ::=
ghost [ public ] [ static
] Type VariableDeclarator [;]
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)
SetStatementAnnotation ::=
set PrimarySpecExpr = SpecExpr
[;]
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.
WriteableDeferredModifierAnnotation ::=
writeable_deferred
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.
StillWriteableDeferredDeclarationAnnotation ::=
still_deferred VariableDeclarators
[;]
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