| 目次 | 前 | 次 | 索引 | Java言語規定 第2版 |
個々の局所変数(14.4)及びすべての blank final (4.5.4) フィールド (8.3.1.2) は，その値にアクセスが発生するときには，確実に代入された(definitely assigned) 値をもたなければならない。Javaコンパイラは，すべての局所変数又は blank final フィールド f のアクセスに対して，その f がアクセス前に確実に代入されていることを保証するために，慎重なフロー解析を行わなければならない。確実に代入されていない場合は，コンパイル時エラーとしなければならない。
同様に，blank final 変数はすべて，高々一度しか代入されてはならない。blank final 変数は，代入が実行されるときに確実に未代入(definitely unassigned) でなければならない。Java コンパイラは，blank final 変数へのすべての代入に対して，その変数が代入前で確実に未代入であることを保証するために，慎重なフロー解析を行わなければならない。確実に未代入でない場合は，コンパイル時エラーとしなければならない。
16.では，用語"…前に確実に代入されている"及び"…前で確実に未代入である"について厳密に規定する。
確実な代入とは，その局所変数又は blank final フィールドが，そのアクセスまでに通過し得るすべての実行経路で代入されていなければならないことを示す。同様に確実な未代入とは，blank final 変数が，その代入までに通過し得るすべての実行経路でいかなる代入もされてはならないことを示す。解析では，文及び式の構造を考慮する。さらに，! ，&& ，|| 及び ? : という式演算子並びに論理定数式に対しては，特別な処理を行う。
例えば，次のコードでは，Javaコンパイラは，メソッド呼出しの引数としてk がアクセスされる前に確実に代入されていると判定する。
{
int k;
if (v > 0 && (k = System.in.read()) >= 0)
System.out.println(k);
}
true になるのは， k への代入が実行された(正確には，評価された) 場合だけであることによる。
v > 0 && (k = System.in.read()) >= 0
同様に，次のコードでは，Javaコンパイラは，変数 kが そのwhile 文で確実に代入されていると判定する。
{
int k;
while (true) {
k = n;
if (k >= 5) break;
n = 6;
}
System.out.println(k);
}
while 文の条件式 trueの値が false になることはないので，そのwhile 文は， break文によってだけ終了し，k は， break 文の前に確実に代入されていることによる。逆に，Java コンパイラは，次のコードを，必ずコンパイル時エラーとしなければならない。
{
int k;
while (n < 4) {
k = n;
if (k >= 5) break;
n = 6;
}
System.out.println(k); // k is not "definitely assigned" before this
}
while 文によるその本体の実行が保証されていないことによる。
フロー解析では，条件論理演算子&& ，|| 及び ? : と論理定数式の特別な場合を除いて，式の値は，考慮しない。
例えば，Javaコンパイラは，次のコードを，必ずコンパイル時エラーとしなければならない。
{
int k;
int n = 5;
if (n > 2)
k = 3;
System.out.println(k); // k is not "definitely assigned" before this
}
n の値がコンパイル時に分かり，原理的には，k の代入が常に実行される (正確には，評価される) ことが既知であっても，エラーとしなければならない。 Javaコンパイラは，必ずここで規定する規則に従って動作しなければならない。この規則では，定数式だけを判定する。上記の例では，式 n > 2 は，15.28 の定義による定数式ではない。
次に，別の例を挙げる。Javaコンパイラは，k の確実な代入に関する限り，次のコードを受け付ける。
void flow(boolean flag) {
int k;
if (flag)
k = 3;
else
k = 4;
System.out.println(k);
}
k は，flagが true であるか false であるかによらず必ず代入されていると判断してもよいことを規定していることによる。しかし，この規則は，次のコードは，受け付けない。
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
}
似た例を使って，確実な未代入の規則を示す。Java コンパイラは，k が確実に未代入であることに関する限り，次のコードを受け付ける。
void unflow(boolean flag) {
final int k;
if (flag) {
k = 3;
System.out.println(k);
}
else {
k = 4;
System.out.println(k);
}
}
k は，flagが true であるか false であるかによらず最大で一度 (実際は一度だけ) 代入されてよいことを規定していることによる。しかし，この規則は，次のコードは，受け付けない。
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);
}
}
確実な代入のすべての場合を正確に規定するために，ここで次の幾つかの用語を定義する。
例えば，次のコードでは，局所変数 k は，式がtrueの場合，式の評価の後で値が確実に代入されているが，式がfalseの場合は，代入されていない。
その理由は，a && ((k=m) > 5)
a が 偽の場合には，k への代入が必ずしも実行されない(正確には，評価されない)ことによる。
"局所変数 V が，文又は式 X の後で確実に代入されている"とは，"V は，X が正常完了する場合，X の後で確実に代入されている"ことを意味する。 X が中途完了する場合，代入は行われている必要がなく，ここに述べた規則では，このことを考慮している。この定義では，"V は， break; の後で確実に代入されている"という奇妙な文が常に成立する。その理由は，break 文は，正常完了することがないので，break 文が正常完了する場合に V に値が代入されているという定義は，意味をなさないものとして成立する。
同様に，"変数 V が，文又は式 X の後で確実に未代入である" とは，"V は，X が正常完了する場合，X の後で確実に未代入である" ことを意味する。この定義では，"V は，break; の後で確実に未代入である" というさらに奇妙な文が常に成立する。その理由は，break 文は，正常完了することがないので，break 文が正常完了する場合に V に値が代入されていないという定義は，意味をなさないものとして成立する。(これに関する限り，break 文が正常完了する場合に，月はグリーンチーズでできているという定義も，意味をなさないものとして成立する。)
文又は式が実行された後，変数 V には次の四つの可能性がある。
V は，空文の前で[未]代入されている場合に限り，その空文の後で[未]代入されている。
これは，次の二つの規則を表しているものと解釈する必要がある。
loop 文の確実な未代入についての解析により，特殊な問題が明らかになる。while (e) S 文の例を考える。V が e の副式で確実に未代入であるかどうかを判断するためには，V が e の前で確実に未代入であるかどうかを判断する必要がある。確実な代入の規則(16.2.9)から類推して，V は while 文の前で確実に未代入である場合に限り，e の前で確実に未代入であると考えられる。しかし，ここでの目的には，この規則では不十分である。e が真であると評価されると，文 S が実行される。S によって V が代入されると，以降の繰返しでは，e が評価されるときには V が既に代入されていることになる。前述の規則では，V には複数回の代入が可能である。前述の規則を導入することによって避けようとしたのはこのことである。
改定規則では，"V は，while 文の前で確実に未代入であり，かつ S の後で確実に未代入である場合に限り，e の前で確実に未代入である"となる。ただし，S についての規則を示す場合は，"V は，e が真の場合に e の後で確実に未代入である場合に限り，s の前で確実に未代入である" となる。これによって，循環が生じる。要するに，V は概して，ループの後で未代入である場合に限り，ループ条件 e の前で確実に未代入である。
この悪循環を脱するために，ループの条件と本体に条件を仮定して解析を行う。例えば，V が (実際に e の前で確実に未代入であるかどうかにかかわらず) e の前で確実に未代入であると仮定すると，V が e の後で確実に未代入であることを証明でき，e によって V に代入されないことが分かる。より形式的に述べると，次のようになる。
V が e の前で確実に未代入であると仮定すると，V は e の後で確実に未代入である。
この解析の変形を使って，言語に含まれるすべてのループ文に対して，根拠が十分な，確実な未代入の規則を定義できる。
以下では，特に明示しない限り，V は，確実な代入の規則の場合には局所変数又は blank final フィールドを表し，確実な未代入の規則の場合には blank final 変数を表すものとする。また，a，b，c，e は式を表し，S と T は文を表すものとする。
true である定数式が false になることはなく，値が false である定数式が true になることはないので，上記の二つの定義は，意味はなさないが論理上形式的に真となる。この二つの定義は，演算子 && (16.1.2)，|| (16.1.3)，! (16.1.4)，及び? : (16.1.5)を含む式の解析において役立つ。
true である定数式が真の場合，定数式の前で[未]代入されている場合に限り，定数式の後で[未]代入されている。
false である定数式が偽の場合，定数式の前で[未]代入されている場合に限り，定数式の後で[未]代入されている。
&& b が真の場合の後で[未]代入されている。
&& b が偽の場合の後で[未]代入されている。
&& b の前で[未]代入されている場合に限り，a の前で[未]代入されている。
&& b が真の場合にその後で[未]代入されている，かつa && b が偽の場合にその後で[未]代入されている場合に限り，a && b の後で[未]代入されている。
|| b が真の場合にその後で[未]代入されている。
|| b が偽の場合にその後で[未]代入されている。
|| b の前で[未]代入されている場合に限り，a の前で[未]代入されている。
|| b が真の場合にその後で[未]代入されており，かつa || b が偽の場合にその後で[未]代入されている場合に限り，a || b の後で[未]代入されている。
!a が真の場合にその後で[未]代入されている。
!a が偽の場合にその後で[未]代入されている。
!a の前で[未]代入されている場合に限り，a の前で[未]代入されている。
!a が真の場合にその後で[未]代入されている，かつ !a が偽の場合にその後で[未]代入されている場合に限り，!a の後で[未]代入されている (これは，V は，a の後で[未]代入されている場合に限り，!a の後で[未]代入されているということに等しい)。
? b : c が真の場合にその後で[未]代入されている。
? b : c が偽の場合にその後で[未]代入されている。
? b : c の前で[未]代入されている場合に限り，a の前で[未]代入されている。
? b : c が真の場合にその後で[未]代入されている，かつ a ? b : c が偽の場合にその後で[未]代入されている場合に限り，a ? b : c の後で[未]代入されている。
? b : c の後で[未]代入されている。
? b : c の前で[未]代入されている場合に限り，a の前で[未]代入されている。
= b，a += b，a -= b，a *= b，a /= b，a %= b，a <<= b，a >>= b，a >>>= b，a &= b，a |= b又は a ^= b について考える。
&= b などの複合代入の前に確実に代入されていない場合は，コンパイル時エラーとする必要があることに注意のこと。上記の確実な代入についての最初の規則には，V は，コードの以降の時点で確実に代入されることがあることを考慮して，単純な代入に対してだけでなく複合代入式に対しても，分離した"a は， V である"という命題が含まれている。分離した"a は， V である"という命題が含まれていても，プログラムが受け付けられるかコンパイル時エラーとされるかの判定には影響しないが，コードの中の何箇所の場所がエラーと見なされるかに影響するので，実際には，エラー報告の質を上げることができる。上記の確実な未代入についての最初の規則に含意される "a は，V でない" という命題にも，同様のことが適用される。
++a，--a，a++，又は a-- の後で確実に代入されている。
++a，--a，a++，又は a-- の後で確実に未代入である。
++a，--a，a++，又は a-- の前で[未]代入されている場合に限り，a の前で[未]代入されている。
++a，前置減分式 --a，後置増分式 a++，後置減分式 a--，論理補数式 !a，条件AND式 a && b，条件OR式 a || b，条件式 a ? b : c，又は代入式ではない場合は，次の規則が適用される。
this(限定されている場合及び限定されていない場合)，実引数を取らない非限定クラスインスタンス作成式，初期化子に式が含まれない初期化済み配列生成式，非限定上位クラスフィールドアクセス式，実引数を取らない名前付きメソッド呼出し，実引数を取らない非限定上位クラスメソッド呼出しに適用される。
final の変数にだけ適用される。V が blank final 局所変数である場合，その宣言が属するメソッドのみが V に対して代入を実行できる。V が blank final フィールドである場合，V についての宣言を含むクラスのコンストラクタ又は初期化子だけが，V に対する代入を実行できる。すなわち，V に対する代入を実行できるメソッドは存在しない。最後に，明示的なコンストラクタ呼出し(8.8.5) は特別に処理される(16.8)。この呼出しは，メソッド呼出しを含む式文と構文が似ているが，式文ではない。したがって，ここで示した規則は，明示的なコンストラクタ呼出しには適用されない。式 x のすべての直接部分式 y に対して，V は，次のいずれか一つが成り立つ場合に限り，y の前で[未]代入されている。
:S (ここでLは，ラベルとする) から抜けることのあるすべての break 文の前に[未]代入されている場合に限り，ラベル付き文 L:S の後で[未]代入されている。
:S の前で[未]代入されている場合に限り，S の前で[未]代入されている。
if 文if (e) S 文に適用される。
if (e) S の後で[未]代入されている。
if (e) S の前で[未]代入されている場合に限り，e の前で[未]代入されている。
if (e) S else T 文に適用される。
if (e) S else T の後で[未]代入されている。
if (e) S else T の前で[未]代入されている場合に限り，e の前で[未]代入されている。
switch 文switch 文の後で[未]代入されている。
switch ブロックにデフォルトラベルがあるか，又は V が その switch 式の後で[未]代入されている場合
switch ブロックに，ブロック文グループを開始しない switch ラベルがない (すなわち，switch ブロックを終了させる "}" の直前に switch ラベルがない) か，又は V が その switch 式の後で[未]代入されている場合
switch ブロックにブロック文グループがないか，V が最後のブロック文グループの最後のブロック文の後で[未]代入されている場合
switch 文から抜けることのあるすべての break 文の前で[未]代入されている場合
switch 文の前で[未]代入されている場合に限り，switch 式の前で[未]代入されている。
switch ブロック内の最初のブロック文グループの最初のブロック文の前で[未]代入されている。
while 文while 文が breakターゲット (break target) であるすべての break 文の前で[未]代入されている場合に限り，while (e) S の後で[未]代入されている。
while 文の前に確実に代入されている場合に限り，e の前に確実に代入されている。
while 文の前で確実に未代入である。
while 文が continue ターゲット(continue target) であるすべての continue 文の前で，確実に未代入である。
do 文do 文がbreakターゲットであるすべての break 文の前で[未]代入されている場合に限り，do S while (e); の後で[未]代入されている。
do 文の前に確実に代入されている場合に限り，Sの前に確実に代入されている。
do 文が continue ターゲットであるすべての continue 文の前で[未]代入されている場合に限り，e の前で[未]代入されている。
for 文for 文の後で[未]代入されている。
for 文の初期化部の前では，そのfor 文の前で[未]代入されている場合に限り，[未]代入されている。
for 文の条件部の前では，そのfor 文の初期化部の後で確実に代入されている場合に限り，確実に代入されている。
for 文の条件部の前では，次のすべての条件が満たされる場合に限り，確実に未代入である。
for 文の初期化部の後で確実に未代入である。
for 文の条件部の前で確実に未代入であると仮定すると，含まれる文の後で確実に未代入である。
for 文が continue ターゲットであるすべての continue 文の前で確実に未代入である。
for 文が continue ターゲットであるすべての continue 文の前で[未]代入されている場合に限り，for 文の増分部の前で[未]代入されている。
for 文の初期化部が局所変数宣言文である場合，16.2.4の規則が適用される。
break, continue, return, 及びthrow 文break 文，continue 文，return 文，又は throw 文の後で[未]代入されていると表現する。変数が文又は式の"後で[未]代入されている"とは，"文又は式が正常完了した後で[未]代入されている"ことを意味する。break 文，continue 文，return 文，又は throw 文は正常完了することがないので，これは意味をなさないものとして成立する。
return 文又は式 e 付きの throw 文において，V は，そのreturn 文又は throw 文の前で[未]代入されている場合に限り，e の前で[未]代入されている。
synchronized 文synchronized (e) S の後で[未]代入されている。
synchronized (e) S 文の前で[未]代入されている場合に限り，e の前で[未]代入されている。
try 文finally ブロックがあるかないかにかかわらず，すべての try 文に適用される。
try 文の前で[未]代入されている場合に限り，try ブロックの前で[未]代入されている。
try ブロックの前に確実に代入されている場合に限り，catch ブロックの前に確実に代入されている。
try ブロックの後で確実に未代入であり，かつ try ブロックに属するすべての return 文，try ブロックに属するすべての throw 文，try ブロックに属しその break ターゲットに try 文が含まれる (又は，break ターゲットが try 文である) すべての break 文，及び try ブロックに属しその continue ターゲットに try 文が含まれるすべての continue 文の前で確実に未代入である場合に限り，catch ブロックの前で確実に未代入である。
try 文に finally ブロックがない場合は，次の規則も適用される。
try ブロックの後で[未]代入されている，かつ try 文内のすべての catch ブロックの後で[未]代入されている場合に限り，try 文の後で[未]代入されている。
try 文に finally ブロックがある場合は，次の規則も適用される。
try 文の後に確実に代入されている。
try ブロックの後に確実に代入されており，かつV が try 文のすべての catch ブロックの後に確実に代入されている場合
finally ブロックの後に確実に代入されている。
finally ブロックの後で確実に未代入である場合に限り，try 文の後で確実に未代入である。
try 文の前に確実に代入されている場合に限り，finally ブロックの前に確実に代入されている。
try ブロックの後で確実に未代入であり，かつ try ブロックに属するすべての return 文，try ブロックに属するすべての throw 文，try ブロックに属しその break ターゲットに try 文が含まれる (又は，break ターゲットが try 文である) すべての break 文，及び try ブロックに属しその continue ターゲットに try 文が含まれるすべての continue 文の前で確実に未代入であり，さらに try 文のすべての catch ブロックの後で未代入である場合に限り，finally ブロックの前で確実に未代入である。
catch 節の例外パラメタ V は，そのcatch 節の本体の前に確実に代入されている (かつ，確実に未代入でない)。
final 静的メンバフィールドとする場合，次のことが成り立つ。
final 静的メンバフィールドとする場合，次のことが成り立つ。
final 非静的メンバフィールドとする場合，次のことが成り立つ。
final メンバフィールドとする場合，次のことが成り立つ。
| 目次 | 前 | 次 | 索引 | Java言語規定 第2版 |