「表明 (プログラミング)」の版間の差分
編集の要約なし |
|||
7行目: | 7行目: | ||
例えば、次の疑似コードには2つの表明が含まれている。 |
例えば、次の疑似コードには2つの表明が含まれている。 |
||
< |
<syntaxhighlight lang="pascal"> |
||
x := 5 |
x := 5 |
||
{x > 0} |
{x > 0} |
||
x := x + 1 |
x := x + 1 |
||
{x > 1} |
{x > 1} |
||
</syntaxhighlight> |
|||
</source> |
|||
<code>x > 0</code> と <code>x > 1</code> が表明であり、実行時のその時点でいずれも真である。 |
<code>x > 0</code> と <code>x > 1</code> が表明であり、実行時のその時点でいずれも真である。 |
||
18行目: | 18行目: | ||
この例では、[[アントニー・ホーア]]が1969年の論文で採用した表明の記法を使っている<ref>[[アントニー・ホーア|C.A.R. Hoare]], [http://lambda-the-ultimate.org/node/1912 An axiomatic basis for computer programming], ''Communications of the ACM'', 1969.</ref>。この記法は主なプログラミング言語では採用されていない。しかし、実行時にチェックされない表明として[[コメント (コンピュータ)|コメント]]にこの記法で書いておくことはできる。例えば[[C言語|C]]/[[C++]]では次のようになる。 |
この例では、[[アントニー・ホーア]]が1969年の論文で採用した表明の記法を使っている<ref>[[アントニー・ホーア|C.A.R. Hoare]], [http://lambda-the-ultimate.org/node/1912 An axiomatic basis for computer programming], ''Communications of the ACM'', 1969.</ref>。この記法は主なプログラミング言語では採用されていない。しかし、実行時にチェックされない表明として[[コメント (コンピュータ)|コメント]]にこの記法で書いておくことはできる。例えば[[C言語|C]]/[[C++]]では次のようになる。 |
||
< |
<syntaxhighlight lang="C"> |
||
x = 5; |
x = 5; |
||
x = x + 1; |
x = x + 1; |
||
/* {x > 1} */ |
/* {x > 1} */ |
||
</ |
</syntaxhighlight><!-- "//" によるコメントが標準化されたのはC99以降。余計な前提条件を記述しないで済むよう、/**/ を使う。 --> |
||
コメント内の表明を括弧で囲んでおくことで、他の通常のコメントと区別しやすくなる。 |
コメント内の表明を括弧で囲んでおくことで、他の通常のコメントと区別しやすくなる。 |
||
36行目: | 36行目: | ||
=== 実行時チェックとしての表明 === |
=== 実行時チェックとしての表明 === |
||
表明はプログラマが前提条件としていたことがプログラム実装中にも保持され、プログラム実行時でも正しいことを保証するのに使われる。例えば、以下の[[Java]]コードを見てみよう: |
表明はプログラマが前提条件としていたことがプログラム実装中にも保持され、プログラム実行時でも正しいことを保証するのに使われる。例えば、以下の[[Java]]コードを見てみよう: |
||
< |
<syntaxhighlight lang="java"> |
||
int total = countNumberOfUsers(); |
int total = countNumberOfUsers(); |
||
assert(total >= 0); // total must be non-negative |
assert(total >= 0); // total must be non-negative |
||
45行目: | 45行目: | ||
assert(total % 2 == 1); |
assert(total % 2 == 1); |
||
} |
} |
||
</syntaxhighlight> |
|||
</source> |
|||
Javaでは <code>%</code> は剰余演算子である。その第一オペランドが負であった場合、演算結果も負となる。ここでプログラマは <code>total</code> が負でないという前提でコーディングしており、2 で割った剰余は常に 0 か 1 だと考えている。表明(assert)は、その前提条件を明確に示している。<code>countNumberOfUsers</code> が負数を返す可能性があるなら、これはプログラムのバグとなる可能性がある。 |
Javaでは <code>%</code> は剰余演算子である。その第一オペランドが負であった場合、演算結果も負となる。ここでプログラマは <code>total</code> が負でないという前提でコーディングしており、2 で割った剰余は常に 0 か 1 だと考えている。表明(assert)は、その前提条件を明確に示している。<code>countNumberOfUsers</code> が負数を返す可能性があるなら、これはプログラムのバグとなる可能性がある。 |
||
63行目: | 63行目: | ||
コンパイル時にチェックされる表明は静的表明と呼ばれる。静的表明はコンパイル時の[[テンプレートメタプログラミング]]に特に有効だが、C言語でも表明違反となったときのみ不正なコード(コンパイルエラーとなるコード)が導入されるようにして静的表明を実装可能である。例えば、C言語では次のように静的表明を実装できる。 |
コンパイル時にチェックされる表明は静的表明と呼ばれる。静的表明はコンパイル時の[[テンプレートメタプログラミング]]に特に有効だが、C言語でも表明違反となったときのみ不正なコード(コンパイルエラーとなるコード)が導入されるようにして静的表明を実装可能である。例えば、C言語では次のように静的表明を実装できる。 |
||
< |
<syntaxhighlight lang="c"> |
||
#define COMPILE_TIME_ASSERT(pred) switch(0){case 0:case pred:;} |
#define COMPILE_TIME_ASSERT(pred) switch(0){case 0:case pred:;} |
||
COMPILE_TIME_ASSERT( BOOLEAN CONDITION ); |
COMPILE_TIME_ASSERT( BOOLEAN CONDITION ); |
||
</syntaxhighlight> |
|||
</source> |
|||
<code>(BOOLEAN CONDITION)</code> が偽と評価されると、[[switch文]]の2つ目のラベルの値はゼロとなるため、コンパイラは2つのcaseラベルが同じ値だとしてエラーを検出する。なお、指定する式はコンパイル時に値が定まるものでなければならない。例えば <code>(sizeof(int)==4)</code> といった式である。また、関数定義内でないとswitch文が出現しただけでコンパイルエラーになるので、関数内でしか使えない。 |
<code>(BOOLEAN CONDITION)</code> が偽と評価されると、[[switch文]]の2つ目のラベルの値はゼロとなるため、コンパイラは2つのcaseラベルが同じ値だとしてエラーを検出する。なお、指定する式はコンパイル時に値が定まるものでなければならない。例えば <code>(sizeof(int)==4)</code> といった式である。また、関数定義内でないとswitch文が出現しただけでコンパイルエラーになるので、関数内でしか使えない。 |
||
73行目: | 73行目: | ||
もう1つのC言語でよく知られている静的表明の実装として、次の方式がある<ref>Jon Jagger, ''[http://www.jaggersoft.com/pubs/CVu11_3.html Compile Time Assertions in C]'', 1999.</ref>。 |
もう1つのC言語でよく知られている静的表明の実装として、次の方式がある<ref>Jon Jagger, ''[http://www.jaggersoft.com/pubs/CVu11_3.html Compile Time Assertions in C]'', 1999.</ref>。 |
||
< |
<syntaxhighlight lang="c"> |
||
static char const static_assertion[ (BOOLEAN CONDITION) |
static char const static_assertion[ (BOOLEAN CONDITION) |
||
? 1 : -1 |
? 1 : -1 |
||
] = {'!'}; |
] = {'!'}; |
||
</syntaxhighlight> |
|||
</source> |
|||
<code>(BOOLEAN CONDITION)</code> が偽と評価されると、配列の長さが負になるため、このコードはコンパイルされなくなる。たとえコンパイラが負のサイズの配列を許したとしても、初期値(<code>'!'</code> の部分)を設定しようとした時点で問題に気付くだろう。 |
<code>(BOOLEAN CONDITION)</code> が偽と評価されると、配列の長さが負になるため、このコードはコンパイルされなくなる。たとえコンパイラが負のサイズの配列を許したとしても、初期値(<code>'!'</code> の部分)を設定しようとした時点で問題に気付くだろう。 |
||
104行目: | 104行目: | ||
例えば、次のようなC言語のプログラムがあるとする。 |
例えば、次のようなC言語のプログラムがあるとする。 |
||
< |
<syntaxhighlight lang="c"> |
||
int *ptr; |
int *ptr; |
||
assert(ptr = malloc(sizeof(int) * 10)); /* malloc() が失敗すると NULL を返す。しかし、この文は NDEBUG シンボルを定義してコンパイルすると実行されなくなる。 */ |
assert(ptr = malloc(sizeof(int) * 10)); /* malloc() が失敗すると NULL を返す。しかし、この文は NDEBUG シンボルを定義してコンパイルすると実行されなくなる。 */ |
||
111行目: | 111行目: | ||
/* ptr を使用する。 */ |
/* ptr を使用する。 */ |
||
... |
... |
||
</syntaxhighlight> |
|||
</source> |
|||
一見すると、<code>malloc</code> の値を <code>ptr</code> に代入して、同時に <code>NULL</code> かどうかをチェックするという賢いコーディングに見えるかもしれない。しかし、<code>malloc</code> 呼び出しと <code>ptr</code> への代入は副作用を伴い、その副作用はプログラム本体で必須なものである。コンパイル時に <code>NDEBUG</code> というシンボルを定義すると <code>assert()</code> は除去されるので、<code>malloc()</code> が呼び出されなくなり、<code>ptr</code> が初期化されずに使われることになる。結果として未定義動作を引き起こす。 |
一見すると、<code>malloc</code> の値を <code>ptr</code> に代入して、同時に <code>NULL</code> かどうかをチェックするという賢いコーディングに見えるかもしれない。しかし、<code>malloc</code> 呼び出しと <code>ptr</code> への代入は副作用を伴い、その副作用はプログラム本体で必須なものである。コンパイル時に <code>NDEBUG</code> というシンボルを定義すると <code>assert()</code> は除去されるので、<code>malloc()</code> が呼び出されなくなり、<code>ptr</code> が初期化されずに使われることになる。結果として未定義動作を引き起こす。 |
||
2020年7月5日 (日) 22:49時点における版
表明(ひょうめい、assertion)とは、プログラミングにおける概念のひとつであり、そのプログラムの前提条件を示すのに使われる。アサーションとも呼ばれる。表明は、プログラムのその箇所で必ず真であるべき式の形式をとる。多くの言語ではそのような前提条件のチェックに表明を使用するが、設計上の判断を文書化するのに使う場合もある。表明が偽となった場合、プログラムにバグが潜在していることを示している。これを「表明違反; assertion failure」と呼ぶ。表明を言語構文や標準ライブラリとしてサポートするプログラミング言語も存在する。
プログラマは、開発過程でソースコードに表明を追加する。デバッグを単純化し、問題を早期に検出するためである。表明違反はバグを示していることが多いため、表明の実装では問題の元を示すために追加情報を表示するようになっていることが多い(ソースコードのファイル名と行番号、スタックトレースなど)。ほとんどの実装では、そのプログラムの実行が即座に停止する。
例
例えば、次の疑似コードには2つの表明が含まれている。
x := 5
{x > 0}
x := x + 1
{x > 1}
x > 0
と x > 1
が表明であり、実行時のその時点でいずれも真である。
この例では、アントニー・ホーアが1969年の論文で採用した表明の記法を使っている[1]。この記法は主なプログラミング言語では採用されていない。しかし、実行時にチェックされない表明としてコメントにこの記法で書いておくことはできる。例えばC/C++では次のようになる。
x = 5;
x = x + 1;
/* {x > 1} */
コメント内の表明を括弧で囲んでおくことで、他の通常のコメントと区別しやすくなる。
使用法
Eiffelのような言語では、表明は設計工程の一部である。CやJavaでは実行時に前提条件をチェックするだけである。いずれの場合も実行時に正当性をチェックすることができるが、最終的には抑止されることが多い。
契約による設計としての表明
表明を仕様書の一種と見ることもできる。コードの部分が動作する前に期待される状態(事前条件)を記述し、そのコードを実行した後に期待される状態(事後条件)を記述する。また、クラスの不変条件を記述することもできる。Eiffelではそのような表明は言語に組み込まれており、そのクラスの仕様書の自動生成に使用される。これは契約プログラミングの重要な部分でもある。
この手法は、契約プログラミングを明確にはサポートしていない言語でも利用価値がある。コメントではなく表明を使用する利点は、表明がプログラムの実行毎にチェックされる点である。表明が真でなくなると、エラーが表示される。これによりコードの実装が表明とずれてしまった場合を早期に検出する。これはつまり、コメントとコードの内容の不一致の問題と同じである。
実行時チェックとしての表明
表明はプログラマが前提条件としていたことがプログラム実装中にも保持され、プログラム実行時でも正しいことを保証するのに使われる。例えば、以下のJavaコードを見てみよう:
int total = countNumberOfUsers();
assert(total >= 0); // total must be non-negative
if (total % 2 == 0) {
// total is even
} else {
// total must be odd and non-negative
assert(total % 2 == 1);
}
Javaでは %
は剰余演算子である。その第一オペランドが負であった場合、演算結果も負となる。ここでプログラマは total
が負でないという前提でコーディングしており、2 で割った剰余は常に 0 か 1 だと考えている。表明(assert)は、その前提条件を明確に示している。countNumberOfUsers
が負数を返す可能性があるなら、これはプログラムのバグとなる可能性がある。
この技法の主な利点は、問題が発生したときにそれを即時かつ直接的に検出できる点であり、後から検出しても様々な副作用によって真の原因がなかなかつかめないことがある。表明違反はコード上の位置を表示することが多いので、煩雑なデバッグ作業なしで問題点を即座に発見することができる。
表明は決して実行されないと見なされている箇所に置かれることもある。例えば、C、C++、Javaのような言語で、switch
文の default
節に表明を置くことがある。プログラマが予期しない状態が発生した場合、実行をそのまま続けるのではなく、エラーを発生させてプログラムを停止させるのである。
Javaでは、表明はassert
文としてバージョン 1.4 から言語の一部となった。表明違反は AssertionError
を発生させる。Cでは標準ヘッダファイル assert.h
で assert(expression)
マクロが定義されており、NDEBUG
シンボルが定義されていない場合に有効になる[2]。表明が失敗した場合、エラーメッセージを表示してプログラムを停止させるようになっているのが一般的である。C++の標準では cassert
というヘッダを必要とするが、ライブラリによってはC言語同様の assert.h
が使用可能となっている。
表明はメモリの内容を書き換えてしまったり、スレッドの動作タイミングを変えてしまうなどの副作用を持つ危険性がある。表明はプログラム本体への副作用を生じないよう注意深く実装する必要がある。
開発サイクル内での表明
開発中、プログラマは表明を入れた状態でプログラムを実行する。表明違反が発生すると、プログラマに即座に問題が通知される。ほとんどの表明の実装ではプログラムの実行も停止する。プログラムがそのまま実行を続けてしまうと問題の原因を究明することが困難となる可能性が高い。表明違反で表示される情報(違反発生箇所やスタックトレース)を使えば、プログラマは容易に問題を解決できる。このようにして表明はデバッグ工程を単純化する。
静的表明
コンパイル時にチェックされる表明は静的表明と呼ばれる。静的表明はコンパイル時のテンプレートメタプログラミングに特に有効だが、C言語でも表明違反となったときのみ不正なコード(コンパイルエラーとなるコード)が導入されるようにして静的表明を実装可能である。例えば、C言語では次のように静的表明を実装できる。
#define COMPILE_TIME_ASSERT(pred) switch(0){case 0:case pred:;}
COMPILE_TIME_ASSERT( BOOLEAN CONDITION );
(BOOLEAN CONDITION)
が偽と評価されると、switch文の2つ目のラベルの値はゼロとなるため、コンパイラは2つのcaseラベルが同じ値だとしてエラーを検出する。なお、指定する式はコンパイル時に値が定まるものでなければならない。例えば (sizeof(int)==4)
といった式である。また、関数定義内でないとswitch文が出現しただけでコンパイルエラーになるので、関数内でしか使えない。
もう1つのC言語でよく知られている静的表明の実装として、次の方式がある[3]。
static char const static_assertion[ (BOOLEAN CONDITION)
? 1 : -1
] = {'!'};
(BOOLEAN CONDITION)
が偽と評価されると、配列の長さが負になるため、このコードはコンパイルされなくなる。たとえコンパイラが負のサイズの配列を許したとしても、初期値('!'
の部分)を設定しようとした時点で問題に気付くだろう。
これを何度も使用するには、配列名がそれぞれ別々でなければならない。最近[いつ?]のコンパイラにはプリプロセッサに __COUNTER__ というマクロ定義があり、出現の度に増加する数を返すので、それを名前に含めればよい[4]。
D言語は静的表明 static assert
をサポートしている[5]。また、C++ではC++11において static_assert
が導入された。C言語でもC11規格で _Static_assert
が導入された。
表明の抑止
表明は有効化/無効化を切り替えられるよう多くの言語で実装されている。表明は本来、開発ツールであるため、最終テストおよびリリース時には無効化する。したがって有効化時/無効化時の違いがプログラムの意味的な違いを生じないことが前提にある。換言すれば、表明は副作用を持っていてはならない。
CやC++を含む多くの言語では、表明は、リリースコンパイル時にプリプロセッサによって完全に除去される。Javaでは、表明を有効化する場合、実行時にオプションの指定を必要とする。オプションの指定がない場合、表明は無視される。
エラー処理との比較
表明とエラー処理ルーチンを区別することには意味がある。表明は論理的にありえない状況をチェックするのに使うべきである。もし、「ありえない」ことが起きたとしたら、根本的に何かが間違っていたということである。エラー処理は通常発生しうるエラーを処理する(もちろん、一部の状況はほとんど「ありえない」かもしれない)。表明をあらゆるエラー処理に使用するのは賢明ではない。表明ではエラーからの復旧が考慮されておらず、表明違反は無条件でプログラムを停止させてしまう場合がほとんどである。表明はユーザー向けのエラーメッセージも表示しない。
エラー処理に表明を使っているC言語の例を以下に示す。
int *ptr = malloc(sizeof(int) * 10);
assert(ptr != NULL);
/* ptr を使用する。 */
ここで、プログラマは malloc
が NULL
を返す場合があることに気づいている(メモリを確保できなかった場合)。オペレーティングシステムは malloc
が常に成功することは保証していない。したがってプログラムはメモリ確保失敗に対処すべきである。この例では表明は最良の選択ではないだろう。というのも、malloc の失敗は論理的にありえないことではないからである。実際には滅多に発生しないが、設計上考慮すべき可能性である。しかし、このような表明にも利点がある。つまり、プログラマが自分の意思で malloc のエラーに対処するコードを書かない選択をしたことを他の人々に知らしめているのである。
表明の引数である式の副作用に依存するという間違いをすることもある。表明は条件の評価(バグがないことの確認)に使われるものであって、全く実行されないこともあることを常に念頭に置いておく必要がある。最終的にプログラムに問題がないと判断すれば表明を抑止する可能性がある。
例えば、次のようなC言語のプログラムがあるとする。
int *ptr;
assert(ptr = malloc(sizeof(int) * 10)); /* malloc() が失敗すると NULL を返す。しかし、この文は NDEBUG シンボルを定義してコンパイルすると実行されなくなる。 */
/* NDEBUG を定義してコンパイルすると、この時点で ptr は設定されていないことになる(未初期化)。 */
/* ptr を使用する。 */
...
一見すると、malloc
の値を ptr
に代入して、同時に NULL
かどうかをチェックするという賢いコーディングに見えるかもしれない。しかし、malloc
呼び出しと ptr
への代入は副作用を伴い、その副作用はプログラム本体で必須なものである。コンパイル時に NDEBUG
というシンボルを定義すると assert()
は除去されるので、malloc()
が呼び出されなくなり、ptr
が初期化されずに使われることになる。結果として未定義動作を引き起こす。
歴史
プログラムの正しさを証明する手段として表明の概念を最初に提案したのはアラン・チューリングである。1949年6月24日、ケンブリッジ大学で行った "Checking a Large Routine" と題した講演で「大きなルーチンが正しく動作していると確認するにはどうしたらよいだろうか? 確認する人物に多大な負担をかけないようにするには、プログラムの全体としての正しさを容易に確認できるようプログラマが個別に確認可能な明確な「表明」(assertions) をいくつもするべきである」と述べている[6][7]。
脚注
- ^ C.A.R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, 1969.
- ^ assert - cpprefjp C++日本語リファレンス
- ^ Jon Jagger, Compile Time Assertions in C, 1999.
- ^ GNU, "GCC 4.3 Release Series — Changes, New Features, and Fixes"
- ^ Static assertions in Dhttp://dlang.org/version.html#StaticAssert
- ^ Alan Turing, Checking a Large Routine, 1949
- ^ quoted in C.A.R Hoare, "The Emperor's Old Clothes", 1980 Turing Award lecture.
関連項目
外部リンク
- The benefits of programming with assertions by Philip Guo (Stanford University), 2008.
- Java: