Java Reference
In-Depth Information
within some subexpression of
e
, we need to determine whether
V
is definitely unas-
signed before
e
. One might argue, by analogy with the rule for definite assignment
fore the
while
statement. However, such a rule is inadequate for our purposes. If
e
eval-
uates 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 unas-
signed 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 def-
initely unassigned after
e
when true”. This leads to a circularity. In effect,
V
is defin-
itely 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 unassign-
ment rules for all loop statements in the Java programming language.
16.1. Definite Assignment and Expressions
16.1.1. Boolean Constant Expressions
false.
•
V
is [un]assigned after any constant expression whose value is
false
when true.
•
V
is [un]assigned after any constant expression whose value is
true
when true iff
V
is [un]assigned before the constant expression.
•
V
is [un]assigned after any constant expression whose value is
false
when false iff
V
is [un]assigned before the constant expression.
•
V
is [un]assigned after a boolean-valued constant expression
e
iff
V
is [un]assigned
after
e
when true and
V
is [un]assigned after
e
when false.
