Software Engineering Lecture s11

デバッグ・テスト・検証

人間が書く以上、ソフトウェアにはバグが付物である。バグとは何か?

     ソフトウェアが、期待された動きと別な動きをすること

つまり、「期待された動き」が規定されていない限り、バグを定義することはできない。通常は、それは、仕様と呼ばれ、この授業の最初で議論したように、自然言語または論理で記述されるのが普通である。自明なバグとしては、プログラムの実行が期待されるところまで、続けられなくなる場合がある。これらは、普通は「エラー」と呼ばれる。

また、バグがあることを示すためには、実際に「別な動きをすること」を示す必要がある。これは、「テスト」と呼ばれる実行を行い、実際に、バグまたは、エラーを起こすことで示すことが出来る。

しかし、「ある動作を、たくさん行って、バグがないこと」をいくら繰り返しても、「そのプログラムにバグがないこと」を示すことはできない。示すべきことは、「すべての可能な実行に対して、バグがない」ことである。これを示すためには、要求された仕様に対して、プログラムがバグがないことを証明するしかない。これは、一般的には、困難であるとされている。(が、不可能ではない)

仕様がプログラムに対して示されることは希ではある。しかし、仕様が与えられていれば、

    与えられたプログラムが、その仕様に反する実行があるかどうか

を示すアルゴリズムがある場合がある。これは、「プログラムの可能な実行すべて」(プログラムのモデル)をデータ構造として構築し、そのデータ構造に対して、仕様を検証することによって実現される。(モデル検証) プログラムが、有限状態、あるいは、抽象された有限状態を持つならば、非常に有効であることが示されている。 SPIN などのモデル検証プログラムが知られている。

仕様記述

仕様記述は実装記述と異なり、非決定的に起こること、起こり得るすべてのことを考慮した記述である。仕様記述には論理式を使った記述と代数を使った記述とが使われる。

時相論理を使った仕様記述

仕様記述には論理式を使うことが多い。特に、時間関係を記述するためには、時間の入った論理式を使うことがある。Linear Time Temporal Logic や Branching Time Temporal Logic あるいは、CTL などが知られている。Interval Teporal Logic なども使われることがある。

プロセス代数を使った仕様記述

また、並行に動作する複数のプロセスの動作を代数的にとらえる手法もある。代数的とは、プログラムの動作を記号的にとらえ、抽象的な記述(実装記述よりも簡素であることが期待される)を可能にすることである。記号は具体的な動作に対応することもあれば、動作の無限の集合に対応することもある。プロセス代数記述としては、LOTOSや、π-Calculus、CSP などが使われている。

プロセス代数では、二つのプロセスの同等性を定義して、判定することにより検証を行なう。一般的には難しい操作となるが、プロセスが有限状態ならば、それを判定するアルゴリズムがある。

コンピュータを使った定理証明

ITLはタブロー法などにより直接証明できる。一般的には、証明はValidity を要求するので難しい。計算量的には変数の数に対してco-NP、量化記号がある場合はP Space と言われている。

しかし、Statisfiability の方が若干やさしい。計算量的には NP である。与えられた実装記述が仕様を満たすことは Satisfiablitity を調べることになる。これは、モデル検証と言われている。SPIN などが実用的なツールとして知られている。

デバッグ

既に、バグがあることが分かっていて、その原因を見つけることは、バグを生じさせることが確実に出来れば、簡単である。

[二分法] プログラムの初期実行をα= s0とし、バグが起きた時点の実行ステートメント数を β= sn とする。バグは、プログラムの状態 (大域変数と局所変数の値) から判断できるとする。n' = n/2 とし、sn' の状態にバグがあるかどうかを調べる。バグがあるかないかによって、α=sn' または、β=sn' とする。これを、繰り返すことにより、α+1=β となり、バグが起きた時点の実行ステートメントとプログラムの状態を得ることが出来る。

これを行うためには、デバッガまたは、printf が有効である。

デバッガ

デバッガには、通常以下のような機能がある。

     ブレークポイント break point (プログラムを指定された部分で止める)
     プリント print (プログラムの状態を調べる)

さらに、

     プログラムの表示
     関数呼び出しによって隠された状態(stack frame)の表示 (where, up, down)
     トレース  trace (指定された部分で、なんらかの表示を行う)
     条件付ブレーク

などの機能がある場合がある。条件付ブレークは、極めて遅い(千分の1 程度のスピード)場合があるので注意しよう。

統合型ツール

デバッガとエディタなどを組み合わせて、統合型のツールを提供している場合もある。機能的には、デバッガとprintf と変わらない。

良くあるバグ

コンパイラが出すエラーメッセージ (ウォーニングを含む)

     type mismatch
     used uninitialized value

などは、すべてバグである。gcc ならば、-Wall などを付けることにより、より厳格なチェックを行うことができる。コンパイラのエラーメッセージを無視してはならない。行番号が指定されるので、これらを修正することは容易である。

Segmentation Falut、Bus Error などは、ポインタ関連、配列関連のエラーである。これは、致命的であり、この手のバグを残してはならない。

コンパイルエラーを取るには、error コマンド、あるいは、Emacs のM-X compile が便利である。

メモリ管理

malloc / free

     char * p = (char *) malloc(1000);
     char * q = (char *) malloc(1000);

ここで、malloc で獲得した以上のメモリ領域を使用したらどうなるか?

     p[1002] = 0;
     free(p);
     free(q);

何が起きるか調べてみよう。

man malloc して、MALLOC_CHECK_ の役割を調べよう。

malloc は、メモリ上にmallocの管理データをおいている。それを破壊してしまうと、予測の出来ないエラーが malloc / free 時に起きる。(malloc にバグ無し)

malloc した領域が適切な大きさか常にチェックしよう。配列の大きさを越えてアクセスしていないか?

ポインタ管理

一旦、free した領域を、誰かが使用していたらどうなるだろうか? そのようなことが起きないように、free したポインタ変数を 0 で初期化する。

address 0 をアクセスするとどうなるか? address 0 をアクセスすると必ず SEGV が起きる時の利点について考察せよ。

局所変数へのポインタ

      h() {
	  int i,j;
	  f(&i,&j);
      }
      f(int *i,int *j) {
          *i = 5;
          *i = 6;
      }

は、C で複数の値を返す関数を作る際に良く使われる。

      int i,j;
      return(&i);

は、間違いである。(何故か?) このような間違いをした時に、起きる可能性のあるエラーメッセージについて考察せよ。

メモリリーク

free し忘れると、ゴミがたまっていく。(memory leak) このバグの悪い点は何か? メモリリークを防ぐ方法。

    メモリプールを使う
    fork し、別プロセスとする

エラー処理のし忘れ

    FILE *fp = fopen(filename,"r");
    fgets(fp,buf,sizeof(buf));

は、間違い。何故か? この時に、起きるエラーには、どのようなものがあるか?

core dump

    gdb a.out core

deamon のデバッグを行う

    gdb は、既に立ち上がっているプロセスに接続することができる

編集時、コンパイル時にバグを見つける

ソースがない場合

ktrace, ptrace, truss

どのファイルをアクセスしているのかに着目する。

初期化ファイルのどれを参照しているかを見つける。

バグが「ときどき」起きる場合

再現する状況を構築する。

log を使用する。

core を積極的に生成する。