アサーション(ソフトウェア開発)

ウィキペディアから、無料の百科事典
ナビゲーションにジャンプ 検索にジャンプ

コンピュータープログラミングでは、特に命令型プログラミングパラダイムを使用する場合、アサーションは、プログラム内のポイントに接続された述語状態空間上のブール値関数、通常はプログラムの変数を使用した論理命題として表されます)であり、コード実行のその時点で常にtrueと評価される必要があります。アサーションは、プログラマーがコードを読んだり、コンパイラーがコードをコンパイルしたり、プログラムが自身の欠陥を検出したりするのに役立ちます。

後者の場合、一部のプログラムは、実行時に述語を実際に評価することによってアサーションをチェックします。次に、それが実際には当てはまらない場合(アサーションの失敗)、プログラムはそれ自体が壊れていると見なし、通常は意図的にクラッシュするか、アサーションの失敗の例外をスローします

詳細

次のコードには、2つのアサーションx > 0とが含まれx > 1ています。これらは、実行中の指定されたポイントで実際に当てはまります。

x = 1 ;  
x > 0をアサートします;   
x ++ ;
x > 1をアサートします;   

プログラマーは、アサーションを使用して、プログラムを指定し、プログラムの正当性について推論することができます。たとえば、前提条件(コードのセクションの先頭に配置されるアサーション)は、プログラマーがコードの実行を期待する状態のセットを決定します。事後条件最後に配置)は、実行の最後に予想される状態を示します。例:x > 0 { x++ } x > 1

上記の例では、1969年の記事でCARHoareが使用したアサーションを含めるための表記法を使用しています。[1]この表記は、既存の主流のプログラミング言語では使用できません。ただし、プログラマーは、プログラミング言語のコメント機能を使用して、チェックされていないアサーションを含めることができます。たとえば、Cでは:

x = 5 ;  
x = x + 1 ;    
// {x> 1}

コメントに含まれる中括弧は、コメントのこの使用法を他の使用法と区別するのに役立ちます。

ライブラリは、アサーション機能も提供する場合があります。たとえば、CでC99をサポートするglibcを使用すると、次のようになります。

#include <assert.h> 

int f void  
{{
    int x = 5 ;   
    x = x + 1 ;    
    アサートx > 1 );  
}

いくつかの最新のプログラミング言語には、チェックされたアサーション(実行時に、または場合によっては静的にチェックされるステートメント)が含まれています。実行時にアサーションがfalseと評価されると、アサーションが失敗し、通常は実行が中止されます。これにより、論理的な不整合が検出された場所に注意が向けられ、そうでない場合に発生する動作よりも優先される可能性があります。

アサーションの使用は、プログラマーがプログラムを設計、開発、および推論するのに役立ちます。

使用法

Eiffelなどの言語では、アサーションは設計プロセスの一部を形成します。CJavaなどの他の言語は、実行時に仮定をチェックするためにのみそれらを使用します。どちらの場合も、実行時に有効性をチェックできますが、通常は非表示にすることもできます。

契約による設計の主張

アサーションはドキュメントの形式として機能できます。アサーションは、実行前にコードが検出すると予想される状態(前提条件)と、実行が終了したときにコードがもたらすと予想される状態(事後条件)を記述できます。クラスの不変条件指定することもできますEiffelはそのようなアサーションを言語に統合し、それらを自動的に抽出してクラスを文書化します。これは、契約による設計方法の重要な部分を形成します。

このアプローチは、明示的にサポートされていない言語でも役立ちます。コメントでアサーションではなくアサーションステートメントを使用する利点は、プログラムが実行されるたびにアサーションをチェックできることです。アサーションが保持されなくなった場合は、エラーを報告できます。これにより、コードがアサーションと同期しなくなるのを防ぎます。

実行時チェックのアサーション

アサーションを使用して、プログラムの実装中にプログラマーが行った仮定が、プログラムの実行時に有効なままであることを確認できます。たとえば、次のJavaコード について考えてみます。

 int  total  =  countNumberOfUsers (); 
 if  total   2  ==  0  { 
     //合計は偶数
 }  else  { 
     //合計は奇数で非負の
     assert 合計  2  ==  1 ; 
 }

Javaでは%剰余演算子(モジュロ)であり、Javaでは、最初のオペランドが負の場合、結果も負になる可能性があります(数学で使用されるモジュロとは異なります)。ここで、プログラマーはそれが負ではないと仮定しているtotalため、2での除算の余りは常に0または1になります。アサーションはこの仮定を明示的にcountNumberOfUsersします。負の値を返す場合、プログラムにバグがある可能性があります。

この手法の主な利点は、エラーが発生したときに、後でしばしば不明瞭な影響を介してではなく、すぐに直接検出されることです。アサーションの失敗は通常、コードの場所を報告するため、さらにデバッグしなくてもエラーを特定できることがよくあります。

アサーションは、実行が到達するはずのないポイントに配置されることもあります。たとえば、アサーションは、CC ++Javaなどの言語のステートメントのdefault句に配置できますプログラマーが意図的に処理しない場合は、エラーが発生し、プログラムは誤った状態で黙って続行するのではなく、中止されます。Dでは、ステートメントに句 が含まれていない場合、このようなアサーションが自動的に追加されます。switchswitchdefault

Javaでは、バージョン1.4以降、アサーションは言語の一部になっています。アサーションに失敗するAssertionErrorと、プログラムが適切なフラグを使用して実行されたときにが発生します。これがないと、アサーションステートメントは無視されます。Cでは、これらは、失敗した場合にエラーを通知するマクロとしてassert.h定義されている標準ヘッダーによって追加され、通常はプログラムを終了します。C ++ではヘッダーの両方がマクロを提供します。 assert (assertion) assert.hcassertassert

アサーションの危険性は、メモリデータを変更するか、スレッドのタイミングを変更することによって副作用を引き起こす可能性があることです。アサーションは、プログラムコードに副作用が発生しないように、慎重に実装する必要があります。

言語のアサーション構造により、サードパーティのライブラリを使用せずに テスト駆動開発(TDD)を簡単に実行できます。

開発サイクル中のアサーション

開発サイクル、プログラマーは通常、アサーションを有効にしてプログラムを実行します。アサーションエラーが発生すると、プログラマーはすぐに問題を通知されます。多くのアサーション実装もプログラムの実行を停止します。これは、アサーション違反が発生した後もプログラムが実行を継続すると、その状態が破損し、問題の原因を特定するのがより困難になる可能性があるため、便利です。アサーションの失敗によって提供される情報(失敗の場所やスタックトレースなど、または環境がコアダンプをサポートしている場合、またはプログラムがデバッガーで実行されている場合は、完全なプログラム状態)を使用する)、プログラマーは通常問題を修正できます。したがって、アサーションはデバッグにおいて非常に強力なツールを提供します。

本番環境でのアサーション

プログラムが本番環境にデプロイされると、アサーションは通常、オーバーヘッドや副作用を回避するためにオフになります。マクロを介したC/C ++アサーションなど、デプロイされたコードにアサーションが完全に含まれていない場合があります。Javaなどの他のケースでは、アサーションはデプロイされたコードに存在し、デバッグのためにフィールドでオンにすることができます。[2]

アサーションを使用して、特定のエッジ条件に実際に到達できないことをコンパイラーに約束することもできます。これにより、他の方法では不可能な特定の最適化が可能になります。この場合、アサーションを無効にすると、実際にパフォーマンスが低下する可能性があります。

静的アサーション

コンパイル時にチェックされるアサーションは、静的アサーションと呼ばれます。

静的アサーションは、コンパイル時のテンプレートメタプログラミングで特に役立ちますが、アサーションが失敗した場合にのみ、不正なコードを導入することにより、Cなどの低レベル言語で使用することもできます。C11およびC++11は、を介して直接静的アサーションをサポートしますstatic_assert以前のCバージョンでは、静的アサーションは次のように実装できます。

#define SASSERT(pred)switch(0){case 0:case pred :;}

SASSERT BOOLEAN CONDITION );   

パーツがfalseと評価された場合、コンパイラは同じ定数を持つ2つのケースラベル(BOOLEAN CONDITION)を許可しないため、上記のコードはコンパイルされません。ブール式はコンパイル時定数値である必要があります。たとえば、そのコンテキストでは有効な式になります。この構成はファイルスコープでは機能しないため(つまり、関数内では機能しません)、関数内でラップする必要があります。 (sizeof(int)==4)

Cでアサーションを実装する もう1つの一般的な[3]方法は次のとおりです。

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

パーツがfalseと評価された場合、(BOOLEAN CONDITION)配列の長さが負でない可能性があるため、上記のコードはコンパイルされません。実際にコンパイラーが負の長さを許可している場合、初期化バイト('!'部分)により、そのような過度に寛大なコンパイラーでさえ不平を言うはずです。ブール式はコンパイル時定数値である必要があります。たとえば(sizeof(int) == 4)、そのコンテキストでは有効な式になります。

これらの方法は両方とも、一意の名前を作成する方法を必要とします。最新のコンパイラは__COUNTER__、コンパイル単位ごとに単調に増加する数値を返すことにより、一意の名前の作成を容易にするプリプロセッサ定義をサポートしています。[4]

Dは、を使用して静的アサーションを提供しますstatic assert[5]

アサーションの無効化

ほとんどの言語では、アサーションをグローバルに、場合によっては独立して有効または無効にすることができます。アサーションは、多くの場合、開発中に有効になり、最終テスト中および顧客へのリリース時に無効になります。アサーションをチェックしないことで、アサーションを評価するコストを回避しながら(アサーションに副作用がないと仮定して)、通常の条件下でも同じ結果を生成します。異常な状態では、アサーションチェックを無効にすると、中止されたはずのプログラムが引き続き実行される可能性があります。これが望ましい場合があります。

CC++などの一部の言語では、プリプロセッサを使用してコンパイル時にアサーションを完全に削除できます

同様に、引数として「-O」(「最適化」を表す)を指定してPythonインタープリターを起動すると、Pythonコードジェネレーターはアサート用のバイトコードを発行しません。[6]

Javaでは、アサーションを有効にするために、ランタイムエンジンにオプションを渡す必要があります。オプションがない場合、アサーションはバイパスされますが、実行時にJITコンパイラーによって最適化されるか、コンパイル時if (false)にプログラマーが各アサーションを節 の後ろに手動で配置することによって除外されない限り、アサーションは常にコードに残ります。

プログラマーは、言語の通常のアサーションチェックメカニズムをバイパスまたは操作することにより、常にアクティブなチェックをコードに組み込むことができます。

エラー処理との比較

アサーションは、通常のエラー処理とは異なります。アサーションは論理的に不可能な状況を文書化し、プログラミングエラーを発見します。不可能が発生した場合、プログラムに根本的な問題があることは明らかです。これはエラー処理とは異なります。実際には発生する可能性が非常に低い場合もありますが、ほとんどのエラー状態が発生する可能性があります。汎用のエラー処理メカニズムとしてアサーションを使用することは賢明ではありません。アサーションはエラーからの回復を許可しません。アサーションに失敗すると、通常、プログラムの実行が突然停止します。また、アサーションは本番コードでは無効になっていることがよくあります。アサーションは、ユーザーフレンドリーなエラーメッセージも表示しません。

エラーを処理するためにアサーションを使用する次の例を考えてみましょう。

  int * ptr = malloc sizeof int * 10 );     
  アサートptr );
  //ptrを使用し
ます...  

ここで、プログラマーは、メモリーが割り当てられていない場合にポインターmallocを返すことを認識しています。これは可能です。オペレーティングシステムは、へのすべての呼び出しが成功することを保証しません。メモリ不足エラーが発生した場合、プログラムはすぐに中止されます。アサーションがないと、プログラムは次のようになるまで実行を続けます。NULLmallocptr使用されている特定のハードウェアによっては、逆参照され、場合によってはそれより長くなります。アサーションが無効にされていない限り、即時終了が保証されます。ただし、正常な障害が必要な場合は、プログラムが障害を処理する必要があります。たとえば、サーバーに複数のクライアントがある場合や、クリーンに解放されないリソースを保持している場合、またはデータストアに書き込むためのコミットされていない変更がある場合があります。このような場合、突然中止するよりも、単一のトランザクションを失敗させる方が適切です。

もう1つのエラーは、アサーションの引数として使用される式の副作用に依存することです。アサーションは、常に真であるはずの条件が実際に真であるかどうかを検証することが唯一の目的であるため、アサーションがまったく実行されない可能性があることを常に念頭に置いておく必要があります。したがって、プログラムにエラーがなくリリースされていると見なされた場合、アサーションが無効になり、評価されなくなる可能性があります。

前の例の別のバージョンを考えてみましょう。

  int * ptr ; 
  // malloc()がNULLを返す場合、以下のステートメントは失敗しますが、
// -NDEBUGを使用してコンパイルすると、まったく実行されません。assert ptr = malloc sizeof int * 10 ));  
      
  // ptrを使用します:-NDEBUGを使用してコンパイルすると、ptrは初期化されません!
..。  

mallocこれは、 toの戻り値を割り当てて、それが1つのステップにあるptrかどうかを確認するための賢い方法のように見えるかもしれませんが、呼び出しとtoの割り当ては、条件を形成する式を評価することの副作用ですプログラムがエラーなしで解放されたと見なされる場合のように、パラメーターがコンパイラーに渡されると、ステートメントが削除されるため、呼び出されず、初期化されませんこれにより、プログラム実行のさらに下流でセグメンテーション違反または同様のnullポインタエラーが発生し、散発的に発生する可能性のあるバグが発生する可能性があります。NULLmallocptrassertNDEBUGassert()malloc()ptrおよび/または追跡するのが難しい。プログラマーは、この問題を軽減するために、同様のVERIFY(X)定義を使用することがあります。

最近のコンパイラは、上記のコードに遭遇すると警告を発する場合があります。[7]

歴史

IASマシンの設計に関するフォンノイマンゴールドスタインによる1947年の報告[8]で、彼らはフローチャートの初期バージョンを使用したアルゴリズムを説明しました。フローチャートでは、1つ以上のバインドされた変数は、必ず特定の指定値を所有するか、特定のプロパティを所有するか、または特定のプロパティを相互に満たします。さらに、そのような時点で、これらの制限の有効性を示す場合があります。このため、そのような制限の有効性が主張されている各領域を、主張ボックスと呼ばれる特別なボックスで示します。」

プログラムの正当性を証明するための断定的な方法は、 AlanTuringによって提唱されました1949年6月24日、ケンブリッジでの「大規模なルーチンのチェック」の講演で、チューリングは次のように提案しました。タスクでは、プログラマーは、個別にチェックでき、プログラム全体の正確性を簡単に追跡できる、いくつかの明確なアサーションを作成する必要があります。」[9]

も参照してください

参照

  1. ^ CAR Hoareコンピュータプログラミングの公理的基礎、ACMのコミュニケーション1969年。
  2. ^ アサーションを使用したプログラミング、アサーション有効化と無効化
  3. ^ Jon Jagger、 Cでのコンパイル時アサーション、1999年。
  4. ^ GNU、「GCC 4.3リリースシリーズ—変更、新機能、および修正」
  5. ^ 「静的アサーション」D言語リファレンスD言語財団2022-03-16を取得
  6. ^ 公式Pythonドキュメント、assertステートメント
  7. ^ 「警告オプション(GNUコンパイラコレクション(GCC)を使用)」
  8. ^ ゴールドスタインとフォンノイマン。「電子計算機の問題の計画とコーディング」パートII、ボリュームI、1947年4月1日、p。12.12。
  9. ^ アランチューリング。大規模なルーチンのチェック、1949; CAR Hoare、「皇帝の古着」、1980年チューリング賞講演で引用。

外部リンク