Wikipedia

表明 (プログラミング)

【計算機プログラミング】コード実行時において述語が常に真であるような言明
（表明から転送）
曖昧さ回避 この項目では、プログラミング技法について説明しています。一般的な意味については「wikt:表明」、「アサーション」をご覧ください。

表明（ひょうめい、英: 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][3][4]。表明が失敗した場合、エラーメッセージを標準エラーに表示した後、abort()関数でプログラムを強制終了させることが規定されている。C の標準では cassert というヘッダを必要とするが、ライブラリによってはC言語同様の assert.h が使用可能となっている。

表明はメモリの内容を書き換えてしまったり、スレッドの動作タイミングを変えてしまったり、といった副作用を持つ危険性がある。表明はプログラム本体への副作用を生じないよう注意深く実装する必要がある。

開発サイクル内での表明

編集

開発中、プログラマは表明を入れた状態でプログラムを実行する。表明違反が発生すると、プログラマに即座に問題が通知される。ほとんどの表明の実装ではプログラムの実行も停止する。プログラムがそのまま実行を続けてしまうと問題の原因を究明することが困難となる可能性が高い。表明違反で表示される情報（違反発生箇所やスタックトレース）を使えば、プログラマは容易に問題を解決できる。このようにして表明はデバッグ工程を単純化する。

静的表明

編集

コンパイル時にチェックされる表明は静的表明と呼ばれる。静的表明は言語規格で規定されていない数値型のサイズをコンパイル時にチェックするといった用途のほか、コンパイル時のテンプレートメタプログラミングに特に有効である。D言語は静的表明 static assert をサポートしている[5]。また、C ではC 11規格において static_assert が導入された。C言語でもC11規格で _Static_assert が導入された。

旧規格のC/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言語でよく知られている静的表明の実装として、次の方式がある[6]。 

static char const static_assertion[ (BOOLEAN CONDITION)
                                    ? 1 : -1
                                  ] = {'!'};

(BOOLEAN CONDITION) が偽と評価されると、配列の長さが負になるため、このコードはコンパイルエラーになる。たとえコンパイラが負のサイズの配列を許したとしても、初期値（'!' の部分）を設定しようとした時点で問題に気付くだろう。

これを何度も使用するには、配列名がそれぞれ別々でなければならない。最近[いつ?]のメジャーなコンパイラにはプリプロセッサに __COUNTER__ というマクロ定義があり、出現の度に増加する数を返す[7][8]ので、それを名前に含める方法があるが、移植性はない[9]。

Boost C ライブラリではC 03以前でも利用可能なマクロBOOST_STATIC_ASSERTおよびBOOST_STATIC_ASSERT_MSGが用意されている[10]。

表明の抑止

編集

表明は有効化/無効化を切り替えられるよう多くの言語で実装されている。表明は本来、開発ツールであるため、最終テストおよびリリース時には無効化する。したがって有効化時/無効化時の違いがプログラムの意味的な違いを生じないことが前提にある。換言すれば、表明は副作用を持っていてはならない。

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) をいくつもするべきである」と述べている[11][12]。

脚注

編集
[脚注の使い方]
  1. ^ C.A.R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, 1969.
  2. ^ assert - cppreference.com (C)
  3. ^ assert - cppreference.com (C )
  4. ^ assert - cpprefjp C 日本語リファレンス
  5. ^ Conditional Compilation - D Programming Language, §Static Assert
  6. ^ Jon Jagger, Compile Time Assertions in C, 1999.[リンク切れ]
  7. ^ GCC 4.3 Release Series — Changes, New Features, and Fixes - GNU Project
  8. ^ Predefined Macros | Microsoft Docs (Visual C 2008)
  9. ^ Predefined Macros | Microsoft Docs (Visual C 6.0)
  10. ^ コンパイル時アサート - boostjp
  11. ^ Alan Turing, Checking a Large Routine, 1949
  12. ^ quoted in C.A.R Hoare, "The Emperor's Old Clothes", 1980 Turing Award lecture.

関連項目

編集

外部リンク

編集
「https://ja.wikipedia.org/w/index.php?title=表明_(プログラミング)&oldid=93755780」から取得