目次 | | | 索引 Java言語規定
第2版

16. 確実な代入

個々の局所変数(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 変数を表すものとする。また,abce は式を表し,S と T は文を表すものとする。

16.1 確実な代入及び式

16.1.1 論理定数式

値が true である定数式が false になることはなく,値が false である定数式が true になることはないので,上記の二つの定義は,意味はなさないが論理上形式的に真となる。この二つの定義は,演算子 && (16.1.2)|| (16.1.3)! (16.1.4),及び? : (16.1.5)を含む式の解析において役立つ。

16.1.2 論理演算子 &&

16.1.3 論理演算子 ||

16.1.4 論理演算子 !

16.1.5 論理演算子 ? :

b 及び c を論理値式と仮定する。

16.1.6 条件演算子 ? :

b 及び c を論理値式でない式と仮定する。

16.1.7 代入式

代入式 a = ba += ba -= ba *= ba /= ba %= ba <<= ba >>= ba >>>= ba &= ba |= b又は a ^= b について考える。

a が V であり,V が a &= b などの複合代入の前に確実に代入されていない場合は,コンパイル時エラーとする必要があることに注意のこと。上記の確実な代入についての最初の規則には,V は,コードの以降の時点で確実に代入されることがあることを考慮して,単純な代入に対してだけでなく複合代入式に対しても,分離した"a は, V である"という命題が含まれている。分離した"a は, V である"という命題が含まれていても,プログラムが受け付けられるかコンパイル時エラーとされるかの判定には影響しないが,コードの中の何箇所の場所がエラーと見なされるかに影響するので,実際には,エラー報告の質を上げることができる。上記の確実な未代入についての最初の規則に含意される "a は,V でない" という命題にも,同様のことが適用される。

代入式が論理値をもつ場合,次の規則も適用される。

16.1.8 演算子 ++ 及び --

16.1.9 他の式

式が論理定数式ではなく,かつ前置増分式 ++a,前置減分式 --a,後置増分式 a++,後置減分式 a--,論理補数式 !a,条件AND式 a && b,条件OR式 a || b,条件式 a ? b : c,又は代入式ではない場合は,次の規則が適用される。

変数 V がメソッド呼出しの後で確実に未代入であることが判定可能であるという断定の背後には巧妙な論理がある。文字通りの意味で,かつ限定がなければ,このような断定自体は,呼び出されたメソッドが代入を実行し得るため必ずしも真ではない。しかし,Java プログラム言語の目的上,確実な未代入の概念は,blank final の変数にだけ適用される。V が blank final 局所変数である場合,その宣言が属するメソッドのみが V に対して代入を実行できる。V が blank final フィールドである場合,V についての宣言を含むクラスのコンストラクタ又は初期化子だけが,V に対する代入を実行できる。すなわち,V に対する代入を実行できるメソッドは存在しない。最後に,明示的なコンストラクタ呼出し(8.8.5) は特別に処理される(16.8)。この呼出しは,メソッド呼出しを含む式文と構文が似ているが,式文ではない。したがって,ここで示した規則は,明示的なコンストラクタ呼出しには適用されない。

x のすべての直接部分式 y に対して,V は,次のいずれか一つが成り立つ場合に限り,y の前で[未]代入されている。

16.2 確実な代入及び文

16.2.1 空文

16.2.2 ブロック

16.2.3 局所クラス宣言文

16.2.4 局所変数宣言文

16.2.5 ラベル付き文

16.2.6 式文

16.2.7 if

次の規則が,if (e) S 文に適用される。

次の規則が,if (e) S else T 文に適用される。

16.2.8 switch

switch ブロックに少なくとも一つのブロック文グループが含まれている場合,次の規則も適用される。

16.2.9 while

16.2.10 do

16.2.11 for

16.2.11.1 初期化部

16.2.11.2 増分部

16.2.12 break, continue, return, 及びthrow

16.2.13 synchronized

16.2.14 try

次の規則は,finally ブロックがあるかないかにかかわらず,すべての try 文に適用される。

try 文に finally ブロックがない場合は,次の規則も適用される。

try 文に finally ブロックがある場合は,次の規則も適用される。

16.3 確実な代入及び仮引数

16.4 確実な代入及び配列初期化子

16.5 確実な代入及び匿名クラス

16.6 確実な代入及びメンバの型

C を,V の範囲内で宣言されたクラスとする場合,次のことが成り立つ。

16.7 確実な代入及び静的初期化子

C を,V の範囲内で宣言されたクラスとする場合,次のことが成り立つ。

C をクラスとし,V を C で宣言されている C の blank final 静的メンバフィールドとする場合,次のことが成り立つ。

C をクラスとし,V を C の上位クラスで宣言されている C の blank final 静的メンバフィールドとする場合,次のことが成り立つ。

16.8 確実な代入,コンストラクタ,及びインスタンス初期化子

C を,V の範囲内で宣言されたクラスとする場合,次のことが成り立つ。

C をクラスとし,V を C で宣言されている C の blank final 非静的メンバフィールドとする場合,次のことが成り立つ。

クラス C のコンストラクタ内では,次の規則が適用される。

C をクラスとし,V を C の上位クラスで宣言されている C のblank final メンバフィールドとする場合,次のことが成り立つ。

目次 | | | 索引 Java言語規定
第2版