目次 | 前 | 次 | 索引 | 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版 |