| Contents | Prev | Next | Index | Java Language Specification Second Edition |
CHAPTER 16
Each local variable (§14.4) and every blank final (§4.5.4) field (§8.3.1.2) must have a definitely assigned value when any access of its value occurs. A Java compiler must carry out a specific conservative flow analysis to make sure that, for every access of a local variable or blank final field f, f is definitely assigned before the access; otherwise a compile-time error must occur.
Similarly, every blank final variable must be assigned at most once; it must be definitely unassigned when an assignment to it occurs. A Java compiler must carry out a specific conservative flow analysis to make sure that, for every assignment to a blank final variable, the variable is definitely unassigned before the assignment; otherwise a compile-time error must occur.
The remainder of this chapter is devoted to a precise explanation of the words "definitely assigned before" and "definitely unassigned before".
The idea behind definite assignment is that an assignment to the local variable or blank final field must occur on every possible execution path to the access. Similarly, the idea behind definite unassignment is that no other assignment to the blank final variable is permitted to occur on any possible execution path to an assignment. The analysis takes into account the structure of statements and expressions; it also provides a special treatment of the expression operators !, &&, ||, and ? :, and of boolean-valued constant expressions.
For example, a Java compiler recognizes that k is definitely assigned before its access (as an argument of a method invocation) in the code:
{
int k;
if (v > 0 && (k = System.in.read()) >= 0)
System.out.println(k);
}
because the access occurs only if the value of the expression:
is true, and the value can bev > 0 && (k = System.in.read()) >= 0
true only if the assignment to k is executed (more properly, evaluated).Similarly, a Java compiler will recognize that in the code:
{
int k;
while (true) {
k = n;
if (k >= 5) break;
n = 6;
}
System.out.println(k);
}
the variable k is definitely assigned by the while statement because the condition expression true never has the value false, so only the break statement can cause the while statement to complete normally, and k is definitely assigned before the break statement.
{
int k;
while (n < 4) {
k = n;
if (k >= 5) break;
n = 6;
}
System.out.println(k); // k is not "definitely assigned" before this
}
must be rejected by a Java compiler, because in this case the while statement is not guaranteed to execute its body as far as the rules of definite assignment are concerned.
Except for the special treatment of the conditional boolean operators &&, ||, and ? : and of boolean-valued constant expressions, the values of expressions are not taken into account in the flow analysis.
For example, a Java compiler must produce a compile-time error for the code:
{
int k;
int n = 5;
if (n > 2)
k = 3;
System.out.println(k); // k is not "definitely assigned" before this
}
even though the value of n is known at compile time, and in principle it can be known at compile time that the assignment to k will always be executed (more properly, evaluated). A Java compiler must operate according to the rules laid out in this section. The rules recognize only constant expressions; in this example, the expression n > 2 is not a constant expression as defined in §15.28. As another example, a Java compiler will accept the code:
void flow(boolean flag) {
int k;
if (flag)
k = 3;
else
k = 4;
System.out.println(k);
}
as far as definite assignment of k is concerned, because the rules outlined in this section allow it to tell that k is assigned no matter whether the flag is true or false. But the rules do not accept the variation:
void flow(boolean flag) {
int k;
if (flag)
k = 3;
if (!flag)
k = 4;
System.out.println(k); // k is not "definitely assigned" before here
}
and so compiling this program must cause a compile-time error to occur.A related example illustrates rules of definite unassignment. A Java compiler will accept the code:
void unflow(boolean flag) {
final int k;
if (flag) {
k = 3;
System.out.println(k);
}
else {
k = 4;
System.out.println(k);
}
}
as far as definite unassignment of k is concerned, because the rules outlined in this section allow it to tell that k is assigned at most once (indeed, exactly once) no matter whether the flag is true or false. But the rules do not accept the variation:
void unflow(boolean flag) {
final int k;
if (flag) {
k = 3;
System.out.println(k);
}
if (!flag) {
k = 4; // k is not "definitely unassigned" before here
System.out.println(k);
}
}
and so compiling this program must cause a compile-time error to occur.In order to precisely specify all the cases of definite assignment, the rules in this section define several technical terms:
For example, the local variable k is definitely assigned a value after evaluation of the expression
when the expression isa && ((k=m) > 5)
true but not when the expression is false (because if a is false, then the assignment to k is not necessarily executed (more properly, evaluated)).
The phrase "V is definitely assigned after X" (where V is a local variable and X is a statement or expression) means "V is definitely assigned after X if X completes normally". If X completes abruptly, the assignment need not have occurred, and the rules stated here take this into account. A peculiar consequence of this definition is that "V is definitely assigned after break;" is always true! Because a break statement never completes normally, it is vacuously true that V has been assigned a value if the break statement completes normally.
Similarly, the statement "V is definitely unassigned after X" (where V is a variable and X is a statement or expression) means "V is definitely unassigned after X if X completes normally". An even more peculiar consequence of this definition is that "V is definitely unassigned after break;" is always true! Because a break statement never completes normally, it is vacuously true that V has not been assigned a value if the break statement completes normally. (For that matter, it is also vacuously true that the moon is made of green cheese if the break statement completes normally.)
In all, there are four possibilities for a variable V after a statement or expression has been executed:
V is [un]assigned after an empty statement iff it is [un]assigned before the empty statement.
should be understood to stand for two rules:
The definite unassignment analysis of loop statements raises a special problem. Consider the statement while (e) S. In order to determine whether V is definitely unassigned within some subexpression of e, we need to determine whether V is definitely unassigned before e. One might argue, by analogy with the rule for definite assignment (§16.2.9), that V is definitely unassigned before e iff it is definitely unassigned before the while statement. However, such a rule is inadequate for our purposes. If e evaluates to true, the statement S will be executed. Later, if V is assigned by S, then in the following iteration(s) V will have already been assigned when e is evaluated. Under the rule suggested above, it would be possible to assign V multiple times, which is exactly what we have sought to avoid by introducing these rules.
A revised rule would be: "V is definitely unassigned before e iff it is definitely unassigned before the while statement and definitely unassigned after S". However, when we formulate the rule for S, we find: "V is definitely unassigned before S iff it is definitely unassigned after e when true". This leads to a circularity. In effect, V is definitely unassigned before the loop condition e only if it is unassigned after the loop as a whole!
We break this vicious circle using a hypothetical analysis of the loop condition and body. For example, if we assume that V is definitely unassigned before e (regardless of whether V really is definitely unassigned before e), and can then prove that V was definitely unassigned after e then we know that e does not assign V. This is stated more formally as:
Assuming V is definitely unassigned before e, V is definitely unassigned after e.
Variations on the above analysis are used to define well founded definite unassignment rules for all loop statements in the language.
Throughout the rest of this chapter, we will, unless explicitly stated otherwise, write V to represent a local variable or a blank final field (for rules of definite assignment) or a blank final variable (for rules of definite unassignment). Likewise, we will use a, b, c, and e to represent expressions, and S and T to represent statements.
true when false.
false when true.
true never has the value false, and a constant expression whose value is false never has the value true, the two preceding rules are vacuously satisfied. They are helpful in analyzing expressions involving the operators && (§16.1.2), || (§16.1.3), ! (§16.1.4), and ? : (§16.1.5).
true when true iff V is [un]assigned before the constant expression.
false when false iff V is [un]assigned before the constant expression.
&& b when true iff V is [un]assigned after b when true.
&& b when false iff V is [un]assigned after a when false and V is [un]assigned after b when false.
&& b.
&& b iff V is [un]assigned after a && b when true and V is [un]assigned after a && b when false.
|| b when true iff V is [un]assigned after a when true and V is [un]assigned after b when true.
|| b when false iff V is [un]assigned after b when false.
|| b.
|| b iff V is [un]assigned after a || b when true and V is [un]assigned after a || b when false.
!a when true iff V is [un]assigned after a when false.
!a when false iff V is [un]assigned after a when true.
!a.
!a iff V is [un]assigned after !a when true and V is [un]assigned after !a when false. (This is equivalent to saying that V is [un]assigned after !a iff V is [un]assigned after a.)
? b : c when true iff V is [un]assigned after b when true and V is [un]assigned after c when true.
? b : c when false iff V is [un]assigned after b when false and V is [un]assigned after c when false.
? b : c.
? b : c iff V is [un]assigned after a ? b : c when true and V is [un]assigned after a ? b : c when false.
? b : c iff V is [un]assigned after b and V is [un]assigned after c.
? b : c.
= b, a += b, a -= b, a *= b, a /= b, a %= b, a <<= b, a >>= b, a >>>= b, a &= b, a |= b, or a ^= b.
&= b, then a compile-time error will necessarily occur. The first rule for definite assignment stated above includes the disjunct "a is V" even for compound assignment expressions, not just simple assignments, so that V will be considered to have been definitely assigned at later points in the code. Including the disjunct "a is V" does not affect the binary decision as to whether a program is acceptable or will result in a compile-time error, but it affects how many different points in the code may be regarded as erroneous, and so in practice it can improve the quality of error reporting. A similar remark applies to the inclusion of the conjunct "a is not V" in the first rule for definite unassignment stated above.
++a, --a, a++, or a-- iff either a is V or V is definitely assigned after the operand expression.
++a, --a, a++, or a-- iff a is not V and V is definitely unassigned after the operand expression.
++a, --a, a++, or a--.
++a, predecrement expression --a, postincrement expression a++, postdecrement expression a--, logical complement expression !a, conditional-and expression a && b, conditional-or expression a || b, conditional expression a ? b : c, or assignment expression, then the following rules apply:
this (both qualified and unqualified), unqualified class instance creation expressions with no arguments, initialized array creation expressions whose initializers contain no expressions, unqualified superclass field access expressions, named method invocations with no arguments, and unqualified superclass method invocations with no arguments.
final variables. If V is a blank final local variable, then only the method to which its declaration belongs can perform assignments to V. If V is a blank final field, then only a constructor or an initializer for the class containing the declaration for V can perform assignments to V; no method can perform assignments to V. Finally, explicit constructor invocations (§8.8.5) are handled specially (§16.8); although they are syntactically similar to expression statements containing method invocations, they are not expression statements and therefore the rules of this section do not apply to explicit constructor invocations.For any immediate subexpression y of an expression x, V is [un]assigned before y iff one of the following situations is true:
:S (where L is a label) iff V is [un]assigned after S and V is [un]assigned before every break statement that may exit the labeled statement L:S.
:S.
; iff it is [un]assigned after e.
;.
if Statementsif (e) S:
if (e) S iff V is [un]assigned after S and V is [un]assigned after e when false.
if (e) S.
if (e) S else T:
if (e) S else T iff V is [un]assigned after S and V is [un]assigned after T.
if (e) S else T.
switch Statementsswitch statement iff all of the following are true:
default label in the switch block or V is [un]assigned after the switch expression.
switch block that do not begin a block-statement-group (that is, there are no switch labels immediately before the "}" that ends the switch block) or V is [un]assigned after the switch expression.
switch block contains no block-statement-groups or V is [un]assigned after the last block-statement of the last block-statement-group.
break statement that may exit the switch statement.
switch statement.
while Statementswhile (e) S iff V is [un]assigned after e when false and V is [un]assigned before every break statement for which the while statement is the break target.
while statement.
while statement.
continue statement for which the while statement is the continue target.
do Statementsdo S while (e); iff V is [un]assigned after e when false and V is [un]assigned before every break statement for which the do statement is the break target.
do statement.
do statement.
continue statement for which the do statement is the continue target.
for Statementsfor statement iff both of the following are true:
break statement for which the for statement is the break target.
for statement iff V is [un]assigned before the for statement.
for statement iff V is definitely assigned after the initialization part of the for statement.
for statement iff all of the following conditions hold:
for statement.
for statement, V is definitely unassigned after the contained statement.
continue statement for which the for statement is the continue target.
for statement.
for statement iff V is [un]assigned after the contained statement and V is [un]assigned before every continue statement for which the for statement is the continue target.
for statement is a local variable declaration statement, the rules of §16.2.4 apply.
for statement is empty, then V is [un]assigned after the incrementation part iff V is [un]assigned before the incrementation part.
break, continue, return, and throw Statementsbreak, continue, return, or throw statement. The notion that a variable is "[un]assigned after" a statement or expression really means "is [un]assigned after the statement or expression completes normally". Because a break, continue, return, or throw statement never completes normally, it vacuously satisfies this notion.
return statement with an expression e or a throw statement with an expression e, V is [un]assigned before e iff V is [un]assigned before the return or throw statement.
synchronized Statementssynchronized (e) S iff V is [un]assigned after S.
synchronized (e) S.
try Statementstry statement, whether or not it has a finally block:
try block iff V is [un]assigned before the try statement.
catch block iff V is definitely assigned before the try block.
catch block iff V is definitely unassigned after the try block and V is definitely unassigned before every return statement that belongs to the try block, every throw statement that belongs to the try block, every break statement that belongs to the try block and whose break target contains (or is) the try statement, and every continue statement that belongs to the try block and whose continue target contains the try statement.
try statement does not have a finally block, then this rule also applies:
try statement iff V is [un]assigned after the try block and V is [un]assigned after every catch block in the try statement.
try statement does have a finally block, then these rules also apply:
try statement iff at least one of the following is true:
catch block in the try statement.
finally block.
try statement iff V is definitely unassigned after the finally block.
finally block iff V is definitely assigned before the try statement.
finally block iff V is definitely unassigned after the try block and V is definitely unassigned before every return statement that belongs to the try block, every throw statement that belongs to the try block, every break statement that belongs to the try block and whose break target contains (or is) the try statement, and every continue statement that belongs to the try block and whose continue target contains the try statement and V is definitely unassigned after every catch block of the try statement.
catch clause is definitely assigned (and moreover is not definitely unassigned) before the body of the catch clause.
final static member field of C, declared in C. Then:
static initializer or static variable initializer of C.
static initializer or static variable initializer of C other than the leftmost iff V is [un]assigned after the preceding static initializer or static variable initializer of C.
final static member field of C, declared in a superclass of C. Then:
final non-static member field of C, declared in C. Then:
final member field of C, declared in a superclass of C. Then:
| Contents | Prev | Next | Index | Java Language Specification Second Edition |