Java Reference
In-Depth Information
In all, there are four possibilities for a variable
V
after a statement or expression has been
executed:
•
V
is definitely assigned and is not definitely unassigned.
(The flow analysis rules prove that an assignment to
V
has occurred.)
•
V
is definitely unassigned and is not definitely assigned.
(The flow analysis rules prove that an assignment to
V
has not occurred.)
•
V
is not definitely assigned and is not definitely unassigned.
(The rules cannot prove whether or not an assignment to
V
has occurred.)
•
V
is definitely assigned and is definitely unassigned.
(It is impossible for the statement or expression to complete normally.)
To shorten the rules, the customary abbreviation “iff” is used to mean “if and only if”.
We also use an abbreviation convention: if a rule contains one or more occurrences of
“[un]assigned” then it stands for two rules, one with every occurrence of “[un]assigned” re-
placed by “definitely assigned” and one with every occurrence of “[un]assigned” replaced
by “definitely unassigned”.
For example:
•
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:
•
V
is definitely assigned after an empty statement iff it is definitely assigned
before the empty statement.
•
V
is definitely unassigned after an empty statement iff it is definitely unas-
signed before the empty statement.
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. We will use the phrase “
a
is
V
”
to mean that
a
is either the simple name of the variable
V
, or
V
's simple name qualified by
this
(ignoring parentheses). We will use the phrase “
a
is not
V
” to mean the negation of “
a
is
V
”.
The definite unassignment analysis of loop statements raises a special problem. Con-
sider the statement
while (
e
)
S
. In order to determine whether
V
is definitely unassigned
