(57)【特許請求の範囲】
【請求項１】
計算機で実行される実行プログラムまたはこの実行プログラムを生成するためのソースプログラムの検証方法であって、前記計算機が、
前記実行プログラムまたはソースプログラムを分岐によって区分されたブロックに分割するステップと、
２以上の前記ブロックを前記分岐の前後で組み合わせて構成した検証ルートを複数抽出するステップと、
前記検証ルートを走査し、資源の獲得と開放または優先度の上昇と低下を含む、対となって構成される第１の処理と第２の処理のうち、第１の処理が実行される検証ルートについて第２の処理が実行されるか否かを判定するステップと、
所定数以上の前記第１の処理が実行される検証ルートにおいて前記第２の処理が実行されるときに、前記第１の処理が実行される検証ルートのうち前記第２の処理が実行されない検証ルートにおいては第２の処理の実行が漏れていると判定する判定ステップと、
前記第１の処理が実行される検証ルートのうち前記第２の処理が実行されない検証ルートをプログラムの欠陥のある可能性のある部分として検出するステップと、を実行する実行プログラムまたはソースプログラムの検証方法。
【請求項２】
前記ブロック、前記検証ルート、前記第１の処理が実行される検証ルート、前記第１の処理が実行される検証ルートのうち前記第２の処理が実行されない検証ルート、第１の処理、または前記第２の処理を表示するステップをさらに実行する請求項１記載の実行プログラムまたはソースプログラムの検証方法。
【請求項３】
前記第１の処理または第２の処理の特定を補助する情報を補助情報として入力させるステップをさらに実行する請求項１または２に記載の実行プログラムまたはソースプログラムの検証方法。
【請求項４】
計算機で実行される実行プログラムまたはこの実行プログラムを生成するためのソースプログラムの検証方法であって、前記計算機が、
前記実行プログラムまたはソースプログラムを分岐によって区分されたブロックに分割するステップと、
２以上の前記ブロックを前記分岐の前後で組み合わせて構成した検証ルートを複数抽出するステップと、
前記実行プログラムまたはソースプログラムで呼び出される関数の１つずつに対してそれぞれ、すべての検証ルートを走査し、その１つの関数の呼び出しがなされる検証ルートを判定し、呼び出される関数ごとにその関数呼び出しがなされる関数呼び出しルートについてその関数呼び出し位置において引数となっている構造体の要素が設定されているか否かを抽出する関数呼び出しルート抽出ステップと、
所定数以上の前記関数呼び出しルートについて前記関数呼び出し位置において引数に含まれる同一の構造体の要素が設定されているときに、前記引数に含まれる前記構造体の要素が前記関数呼び出し位置において設定されるべき要素であると判定する判定ステップと、
前記関数呼び出しルートにおいて前記引数に含まれる前記構造体の要素が前記関数呼び出し位置において設定されないときにその関数呼び出しルートをプログラムの欠陥のある可能性のある部分として検出するステップと、を実行する実行プログラムまたはソースプログラムの検証方法。
【請求項５】
計算機で実行される実行プログラムまたはこの実行プログラムを生成するためのソースプログラムの検証装置であって、
前記実行プログラムまたはソースプログラムを分岐によって区分されたブロックに分割するブロック分割部と、
２以上の前記ブロックを前記分岐の前後で組み合わせて構成した検証ルートを複数抽出する検証ルート抽出部と、
前記検証ルートを走査し、資源の獲得と開放または優先度の上昇と低下を含む、対となって構成される第１の処理と第２の処理のうち、第１の処理が実行される検証ルートについて第２の処理が実行されるか否かを判定する特定ルート判定部と、
所定数以上の前記第１の処理が実行される検証ルートにおいて前記第２の処理が実行されるときに、前記第１の処理が実行される検証ルートのうち前記第２の処理が実行されない検証ルートにおいては第２の処理の実行が漏れていると判定する判定部と、
前記第１の処理が実行される検証ルートのうち前記第２の処理が実行されない前記検証ルートをプログラムの欠陥のある可能性のある部分として検出する欠陥検出部と、を備えた実行プログラムまたはソースプログラムの検証装置。
【請求項６】
前記ブロック、前記検証ルート、前記第１の処理が実行される検証ルート、前記第１の処理が実行される検証ルートのうち前記第２の処理が実行されない検証ルート、第１の処理、または前記第２の処理を表示する表示手段をさらに備えた請求項５記載の実行プログラムまたはソースプログラムの検証装置。
【請求項７】
前記第１の処理または第２の処理の特定を補助する情報を補助情報として入力させる入力手段をさらに備える請求項５または６に記載の実行プログラムまたはソースプログラムの検証装置。
【請求項８】
計算機で実行される実行プログラムまたはこの実行プログラムを生成するためのソースプログラムの検証装置であって、
前記実行プログラムまたはソースプログラムを分岐によって区分されたブロックに分割するブロック分割部と、
２以上の前記ブロックを前記分岐の前後で組み合わせて構成した検証ルートを複数抽出する検証ルート抽出部と、
前記実行プログラムまたはソースプログラムで呼び出される関数の１つずつに対してそれぞれ、すべての検証ルートを走査し、その１つの関数の呼び出しがなされる検証ルートを判定し、呼び出される関数ごとにその関数呼び出しがなされる関数呼び出しルートについてその関数呼び出し位置において引数となっている構造体の要素が設定されているか否かを抽出する関数呼び出しルート抽出部と、
所定数以上の前記関数呼び出しルートについて前記関数呼び出し位置において引数に含まれる同一の構造体の要素が設定されているときに、前記引数に含まれる前記構造体の要素が前記関数呼び出し位置において設定されるべき要素であると判定する判定部と、
前記関数呼び出しルートにおいて前記引数に含まれる前記構造体の要素が前記関数呼び出し位置において設定されないときにその関数呼び出しルートをプログラムの欠陥のある可能性のある部分として検出する欠陥検出部と、を備えた実行プログラムまたはソースプログラムの検証装置。
【請求項９】
計算機で実行される実行プログラムまたはこの実行プログラムを生成するためのソースプログラムを計算機に検証させるプログラムを記録したコンピュータ読み取り可能な記録媒体であって、
前記実行プログラムまたはソースプログラムを分岐によって区分されたブロックに分割するステップと、
２以上の前記ブロックを前記分岐の前後で組み合わせて構成した検証ルートを複数抽出するステップと、
前記検証ルートを走査し、資源の獲得と開放または優先度の上昇と低下を含む、対となって構成される第１の処理と第２の処理のうち、第１の処理が実行される検証ルートについて第２の処理が実行されるか否かを判定するステップと、
所定数以上の前記第１の処理が実行される検証ルートにおいて前記第２の処理が実行されるときに、前記第１の処理が実行される検証ルートのうち前記第２の処理が実行されない検証ルートにおいては第２の処理の実行が漏れていると判定する判定ステップと、
前記第１の処理が実行される検証ルートのうち前記第２の処理が実行されない検証ルートをプログラムの欠陥のある可能性のある部分として検出するステップと、を前記計算機に実行させるプログラムを記録したコンピュータ読み取り可能な記録媒体。
【請求項１０】
前記ブロック、前記検証ルート、前記第１の処理が実行される検証ルート、前記第１の処理が実行される検証ルートのうち前記第２の処理が実行されない検証ルート、第１の処理、または前記第２の処理を表示するステップをさらに実行する請求項９記載のプログラムを記録したコンピュータ読み取り可能な記録媒体。
【請求項１１】
前記第１の処理または第２の処理の特定を補助する情報を補助情報として入力させるステップをさらに実行する請求項９または１０に記載のプログラムを記録したコンピュータ読み取り可能な記録媒体。
【請求項１２】
計算機で実行される実行プログラムまたはこの実行プログラムを生成するためのソースプログラムを計算機に検証させるプログラムを記録したコンピュータ読み取り可能な記録媒体であって、
２以上の前記ブロックを前記分岐の前後で組み合わせて構成した検証ルートを複数抽出するステップと、
前記実行プログラムまたはソースプログラムで呼び出される関数の１つずつに対してそれぞれ、すべての検証ルートを走査し、その１つの関数の呼び出しがなされる検証ルートを判定し、呼び出される関数ごとにその関数呼び出しがなされる関数呼び出しルートについてその関数呼び出し位置において引数となっている構造体の要素が設定されているか否かを抽出する関数呼び出しルート抽出ステップと、
所定数以上の前記関数呼び出しルートについて前記関数呼び出し位置において引数に含まれる同一の構造体の要素が設定されているときに、前記引数に含まれる前記構造体の要素が前記関数呼び出し位置において設定されるべき要素であると判定する判定ステップと、
前記関数呼び出しルートにおいて前記引数に含まれる前記構造体の要素が前記関数呼び出し位置において設定されないときにその関数呼び出しルートをプログラムの欠陥のある可能性のある部分として検出するステップと、を前記計算機に実行させるプログラムを記録したコンピュータ読み取り可能な記録媒体。
【発明の詳細な説明】
【０００１】
【発明の属する技術分野】
本発明は、プログラム開発を支援する技術に係り、特にプログラムの欠陥摘出に好適な検証方法及び検証システムに関するものである。
【０００２】
【従来の技術】
この種のプログラムの動作を検証するシステムの代表的なものとして、次の２つの技術がある。１つは、実際にプログラムを動作させてメモリ領域への不正なアクセス等、障害の要因となるプログラムの動作の有無をチェックすることにより行うものである。
【０００３】
もう一つは、この種の検証をプログラムの実行前に行うもので、例えばUNIXオペレーティングシステムにおけるlintコマンドのように、プログラムの記述が所定のプログラム言語の文法に合致するものであるか否かをチェックするものである。
【０００４】
しかし、上記のような従来技術においては以下のような問題があった。すなわち、実際にプログラムを動作させて検証する方法では、検証対象は、実際に実行されたプログラムのステップのみであり、すべてのステップではない。その上、分岐条件のすべての組み合わせに対してプログラムの検証を行うことは困難であった。また、そのような検証のためのテストデータは通常人手で準備されるため、重要な箇所の検証漏れ等人為ミスも誘発されやすい。
【０００５】
また、プログラムがプログラム言語の文法に合致するか否かの検証では、たとえ検証結果が正常であっても、それは単にソースプログラムが所定の文法に従って記述されていることが検証されたにすぎず、プログラムの動作が正常か否かまでを検証するものではない。
【０００６】
このような状況から、個々のプログラムの要求仕様を計算機に記憶させ、その仕様が正しく反映されているかを自動で検証するシステムが検討されているが、これらの要求仕様は、個々のプログラムが対象とする応用分野と実現すべき機能とに依存しており、プログラムの検証システム（あるいは検証方法）として、汎用的なシステムの開発は、困難と考えられていた。
【０００７】
【発明が解決しようとする課題】
本発明は、上記プログラムの要求仕様を計算機で自動的に検証する方法及び装置に関わるものであり、上記従来技術の問題を解決する汎用的なプログラム検証技術を提供することを目的とする。
【０００８】
すなわち、本発明は個々のプログラムが持つ要求仕様の共通部分を予め検証する仕様として規定し、その検証する仕様に対応した個々のプログラムが持つ具体的仕様（処理仕様）を自動的に抽出することにより、上記問題点の解決を図るものである。
【０００９】
【課題を解決するための手段】
本発明は上記課題を解決するために、以下の手段を採用した。すなわち、本発明は、計算機で実行される実行プログラムまたはこの実行プログラムを生成するためのソースプログラムを検証するものであって、前記実行プログラムまたはソースプログラムを分岐によって区分されたブロックに分割し、２以上の前記ブロックを前記分岐の前後で組み合わせて構成した検証ルートを複数抽出し、前記検証ルートを走査し、資源の獲得と開放または優先度の上昇と低下を含む対となって構成される第１の処理と第２の処理のうち、第１の処理が実行される検証ルートについて第２の処理が実行されるか否かを判定し、所定数以上の前記第１の処理が実行される検証ルートにおいて第２の処理が実行されるときに、前記第１の処理が実行される検証ルートのうち前記第２の処理が実行されない検証ルートにおいては第２の処理の実行が漏れていると判定する判定し、前記第１の処理が実行される検証ルートのうち前記第２の処理が実行されない検証ルートをプログラムの欠陥のある可能性のある部分として検出することにより、プログラムを検証するものである。
【００１０】
このような処理仕様として抽出された処理が実行されない検証ルートをプログラムの欠陥として抽出してもよい。
上記のブロック，検証ルート，処理仕様として抽出された処理，または処理仕様として抽出されなかった処理を表示するようにしてもよい。
【００１１】
このようにして抽出される処理仕様に含まれるべき処理に係る情報を補助情報として入力させるようにしてもよい。
次に、本発明が使用する方式の機能構成を、従来方式との比較から説明する。図１は、従来方式の構成と本発明の方式の構成とを比較するためのイメージ図である。
【００１２】
ここで、検証すべき仕様の例として、以下のＡ，Ｂを、また対応する処理仕様としてａ１，ａ２及びｂ１，ｂ２を挙げる。
Ａ：  一つの関数の中で、特定のプログラム資源を扱う場合、対となる処理が必要である。
ａ１：一つの関数の中でデータバッファに対する処理には、獲得／開放処理に対応する対となる処理がある。
ａ２：一つの関数の中で、実行レベル（プログラムを実行するときの他のプログラムと比較した優先度）を操作する場合、実行レベルを上げる処理と実行レベルを下げる処理とが対となって存在する。
Ｂ：個々の関数は、それが呼び出される場合、設定されなければならない引数の要素は一定である。
ｂ１：関数１が呼び出される場合、引数の要素１，２，３，．．．が設定されていなければならない。
ｂ２：関数２が呼び出される場合、引数の要素ａ，ｂ，ｃ，．．．が設定されていなければならない。
【００１３】
図１から分かるように、従来は個々の処理仕様を入力値として準備すること、または検証システム内部に予めそれらを保持することが必要であった。
これに対し、本発明は、検証すべき仕様として、より汎用的なものを予め準備し、複数の検証ルートでの比較結果から具体的仕様を検証システム自体が自動的に抽出する方法を採用している。したがって、従来技術に比べてより汎用的なシステムの提供が可能となっている。
【００１４】
【発明の実施の形態】
以下、本発明の実施の形態を図２から図１７の図面に基いて説明する。図２は、本実施の形態に係るプログラム検証装置のハードウェアの構成図であり、図３は図２に示すＣＰＵ１において実行されるプログラムの構成図であり、図４〜図８は本実施の形態で取り扱うデータ構造を示す図であり、図９は本実施の形態の動作を例示するための検証対象となるサンプルプログラムの構造を示す図であり、図１０、１１、１２は、図９のサンプルプログラムを検証対象として処理した際の中間結果を示すものであり、図１０はプログラムのブロック構造、図１１はプログラムの検証ルートの抽出例、図１２は検証ルート抽出時に使用するリスト構造を示す構造図である。図１３は図３に示した構成図の検証ルート抽出部１２と処理パターン抽出部１３との関連を示す図であり、図１４及び図１５は本実施の形態の動作を例示するためのサンプルプログラム１を示す図であり、図１６及び図１７は図１４のサンプルプログラム１に対する処理結果を示す図である。
＜構成＞
図２は本発明の実施の形態に係るプログラム検証装置を示すものである。図２に示すように、このプログラム検証装置は、ＣＰＵ１、メモリ２、ハードディスク装置３、表示装置４、キーボード５、及びマウス６を備えている。
【００１５】
図３は本実施の形態に係るプログラム検証装置に備えたＣＰＵ１において実行されるプログラムの構成図である。このプログラムは、検証の対象となるプログラムをブロックに分割するブロック分割部１１と、２以上のブロックを組み合わせて、連続して実行される文（命令）の集合としての検証ルートを抽出する検証ルート抽出部１２と、抽出された検証ルートから特定の処理を実行する文（以下処理パターンという）を抽出する処理パターン抽出部１３と、複数の検証ルートにおいて抽出された処理パターンを比較して本来実行されるべき処理としての処理仕様を抽出する処理仕様抽出部１４と、検証を補助する情報を入力するための補助情報入力部１６（入力手段に相当）とを備えている。
＜ブロック分割部１１の処理＞
ブロック分割部１１は、処理対象のソースプログラムに含まれる分岐文（分岐命令）と関数呼び出し文とからプログラムの階層構造を解析する。分岐文とは、if文、while文、あるいはcase文等のように、指定された条件に従って、あるいは無条件にプログラムの実行順を変更する文をいう。一方、関数呼び出し文とは、プログラムの部品としての関数を呼び出すための文をいう。関数をサブルーチンともいい、関数呼び出し文をサブルーチン呼び出し文ともいう。
【００１６】
本実施の形態のプログラム検証装置では、このような関数または分岐文の定義の中の’｛’及び’｝’または’(’及び’)’で囲まれた範囲には、通常のソースプログラムの文の他、文と文とを組み合わせた複数の文が含まれるので、これをブロックと呼ぶ。
【００１７】
本実施の形態のプログラム検証装置が処理対象とするソースプログラムは、複数の分岐文と関数呼び出し文によって、複数の部分としてのブロックに区分される。このブロックの中には、さらに分岐文や関数呼び出し文が存在する。したがって、処理対象となるプログラムは分岐文や関数呼び出し文が組み合わされて、階層構造をなしている。ブロック分割部１１は、分岐文と関数呼び出し文とによって構成されるこのようなブロック間の組み合わせ、すなわちプログラムの階層構造を解析し、図３に示す検証ルート抽出部１２において処理可能なデータ構造として表現する。
【００１８】
図４〜図８に、ブロック分割部１１が生成するソースプログラムの階層構造（ブロックの組み合わせ）を表現するためのデータ構造を示す。
図４は、関数もしくは、分岐文の構造を示す文構造体である。文構造体は、その文の種類を表す情報と、その種類に依存した情報とを含む。
【００１９】
図５は、関数もしくは、分岐文に含まれる第一階層のブロックの構造を示すブロック構造体である。図５に示すようにこのブロック構造体は、ブロック情報と、そのブロックに直接含まれる分岐文と関数とを示す文構造体へのポインタ配列へのポインタからなっている。
【００２０】
図６は、関数を示す文構造体の例である。この構造体は、図６のように、関数を示す情報、その関数の定義を含むファイルの名称であるファイル名、このファイル内において、その関数が定義されている先頭の行を示す行番号、及びその関数内の第１階層のブロック構造へのポインタを含んでいる。
【００２１】
図７は、if(a)then{b}else{ｃ}という分岐文の文構造体を示したものである。
図７でif文であることを示す情報は、この文構造体で表現した分岐文がif文であることを示している。ブロックaに対するブロック構造体へのポインタとは、if(a)に含まれるブロックaを表現するブロック構造体（図５で示したもの）へのポインタである。また、ブロックbに対するブロック構造体へのポインタとは、if(a)then{b}に含まれるブロックbを表現するブロック構造体へのポインタである。ブロックｃに対するブロック構造体へのポインタも同様である。
【００２２】
したがって、ブロックa、b、あるいはｃに分岐文が含まれている場合には、上述した図４と図５の構造を繰り返すことによって、文の階層構造が表現されることになる。なお、この文構造体は、図６〜図８に例示したものの他、case文、for文等プログラミング言語に現れる他の制御文も同様に表現することができる。
【００２３】
以上の図４〜図８に示す構造により、関数内部の関数呼び出し及び分岐文によって区分されるブロックの組み合わせとしての階層構造が表現されることになる。
【００２４】
図９は、ブロック分割部１１における処理を例示するためのサンプルプログラムであり、図１０は、このサンプルプログラムをブロック分割部１１が処理した結果の例である。
＜検証ルート抽出部の処理＞
検証ルート抽出部１２は、上記ブロック分割部１１によって認識されたプログラムの階層構造（図４〜図８）を利用し、分岐文によって実行を制御されるプログラムの部分（ブロック）の組み合わせとしての検証ルートを生成する。
【００２５】
図９のサンプルプログラムは、３個のif文から構成されており、最初のif(a1)のに含まれるブロックa1が真か偽かによって、ブロックA1またはブロックA2のいずれかが実行される。同様に、次のif(b1)に含まれるb1が真か偽かによって、ブロックB1またはブロックB2のいずれかが実行される。そして、ブロックB1が実行される場合には、さらにif(c1)に含まれるブロックc1が真か偽かによってブロックC1またはブロックC2のいずれかが実行される。
【００２６】
検証ルートとは、このような分岐文によって区分されたプログラムの部分（ブロック）を組み合わせて得られる連続して実行される文の並びをいう。例えば、ブロックa1、b1及びc1のいずれもが真の場合、a1=>A1=>b1=>B1(c1=>C1)のように実行される。このようなブロックの並びが検証ルートである。
【００２７】
検証ルート抽出部１２は、図１０のような関数のブロック（図４から図８に示すブロック分割部１１によって作成された階層構造を表すデータ構造）からプログラムが実行されるすべての検証ルートを作成する。
【００２８】
本実施の形態では、以下に示す走査規則に従って検証ルートが抽出される。この走査規則は、検証する仕様に依存にしない一般的走査規則と検証する仕様に依存して適用される具体的走査規則に区分される。なお、検証ルートの抽出は、指定により、プログラムを構成する個々の関数ごとに、または関数を組み合わせたプログラム全体に対して実行される。
＜一般的走査規則＞
以下に検証する仕様に依存しない走査規則を示す。
（１）１個の分岐文においては、先に現れるブロックが優先して実行される。例えば、if(a)then{b}else{ｃ}なる分岐において、ブロックbとブロックｃとでは、ブロックbが優先されて検証ルートが作成される。
（２）同一階層中にある分岐文は、実行順序が後ろにある分岐文のルートの判定を優先して変化させて検証ルートが網羅される。
（３）複数階層に渡る分岐文の組み合わせにおいては、最も深い階層の分岐文の判定を優先して変化させて検証ルートが網羅される。
【００２９】
以上の規則に従って図９のサンプルプログラムから生成した検証ルートを図１１に示す。まず、最初の検証ルート１）は、上記規則（１）に従って最初に現れるブロックを優先して生成したものである。次の検証ルート２）は、上記規則（２）（３）に従って、実行順序が後ろにあって、かつ、最も深い階層構造のif(c1)then{C1}else{C2}の判定を変更して検証ルートをC1からC2に変更したものである。3)以下は同様の手順で生成したものである。
【００３０】
このようにして生成される検証ルートを表現するためのデータ構造を図１２に示す。図１２はリスト構造と呼ばれるデータ構造により図１１の検証ルート１）を表現したものである。リスト構造とは、複数の要素を矢印で示されるポインタで連結したもので、各要素に値を格納することで、格納された値の順序を保持することができる。図１２では、a1=>A1=>b1=>B1(c1=>C1)に従って値（この場合は、ブロックa1等へのポインタ）が保持されるので、検証ルートとしてのブロックの順序に関する情報が保持される。
＜具体的走査規則＞
上記抽出した検証ルートに沿って、プログラムを走査する場合は、検証する仕様に対応してより詳細な具体的走査規則が必要になる。以下に検証仕様１とそれに対応する具体的走査規則とを示す。
【００３１】
検証仕様１：一つの関数の中で、特定のプログラム資源を扱う場合、対となる処理（例えば資源の獲得／資源の開放）が必要である。
具体的走査規則：
（１）個々の関数内部の先頭から走査を開始し、他の関数呼び出しが存在しても呼び出し先の関数内部までは走査しない。
（２）複数の分岐文が同一レベルで組み合わされている場合、すべての組み合わせを網羅して検証ルートを走査する。例えば、２分岐のif文と４分岐のcase文があった場合、２×４＝８個の検証ルートを走査する。
（３）ループ文（for文、while文）については、そのループ処理部を一度だけ走査する。
（４）ループ内にbreak文を検出した場合、ループ処理部から抜ける。
（５）return文検出時は、その関数から抜けるものとする。
＜処理パターン抽出部及び処理仕様抽出部の処理＞
処理パターン抽出部１３は、上記の検証する仕様に対応する処理パターンが各検証ルートに含まれているか否かを調査し、含まれている処理パターンを各検証ルートごとに処理仕様抽出部１４に報告する。
【００３２】
一方、処理仕様抽出部１４は、処理パターン抽出部１３の報告に基づいて、各検証ルートごとにどの処理パターンが含まれるかを集計し、その結果として上記検証する仕様に対応する処理仕様が成立するか否かを判断する。この処理仕様が一定数以上の検証ルートで成立する場合、これを他の検証ルートでも成立すべき処理仕様として決定する。また、上記決定された処理仕様が成立しない検証ルートについて、プログラム上の欠陥とみなし、当該検証ルートと成立しない処理仕様及び処理仕様が成立しない原因となった処理パターンを提示する。従って、本実施の形態では、処理仕様抽出部１４が、欠陥検出部を兼ねている。
【００３３】
以下に、検証する仕様が上記検証仕様１の場合、処理パターン抽出部の抽出規則における対となるパターンを示す。
−獲得パターン
・関数内で、変数に具体的値が設定されている部分が該当する（関数の引数となる変数は、その関数の先頭で、関数の呼び出し元から値を獲得しているとみなす）。
【００３４】
・変数が、関数の復帰値を値として受け取る部分が該当する。
−開放パターン
・変数が、関数呼び出し時の引数となる部分が該当する。
【００３５】
・変数の値が、制御テーブルに記憶される部分が該当する。
なお、これらのパターン抽出規則を適用した場合、検証仕様１に対応する処理仕様には以下のものがある。
処理仕様１：一つの関数の中でデータバッファに対する処理には、獲得／開放処理に対応する対となる処理がある。
処理仕様２：一つの関数の中で、実行レベル（プログラムを実行するときの他のプログラムと比較した優先度）を操作する場合、実行レベルを上げる処理と実行レベルを下げる処理とが対となって存在する。
処理仕様３：一つの関数の中で資源の排他制御をする場合、リザーブ（資源の占有）とフリー（資源の開放）とが対となって存在する。
＜動作例＞
検証する仕様が上記検証仕様１の場合の検証ルート抽出部１２、処理パターン抽出部１３、及び処理仕様抽出部１４の関係を図１３に詳細に示す。処理パターン抽出部１３は、検証ルート抽出部１２から指示された検証ルート（今このルートをａとする）について、獲得パターンと開放パターンの存在を調査する。処理仕様抽出部は、獲得パターンαと開放パターンβとが存在して、検証仕様１が適用できる場合、検証ルートａの獲得パターンαの処理を共有する他のすべての検証ルート（これを検証ルートａの獲得パターンαを基準にした補ルートという）について、開放パターンが存在するか否かを判定する。
【００３６】
以上の検証ルート抽出部１２、処理パターン抽出部１３、及び処理仕様抽出部１４の動作を図１４に示すサンプルプログラム（プログラム１）を例にして説明する。プログラム１は、通信プロトコルの一階層を実現するための機能を簡易化して記述したものである。このプログラムは、図１５に示すようにプロトコルの下位層から関数として呼び出され、プロトコルの上位層を実現するプログラムに下位層から通知された情報をsndmsg()という関数の呼び出し（実際にはＯＳの機能の実行）によって通知するものである。このプログラム１ではstruct buf及びstruct ctlで定義された構造体変数へのポインタが獲得パターンと開放パターンの調査の対象にあてはまる。なお、プログラム１は、本発明の説明のため、ブロックＡ１とＣ２とで、bufpの開放処理（relbuf(bufp)）漏れが発生するように記述してある。
【００３７】
このプログラム１から検証ルート抽出部１２が抽出した検証ルート及び上記検証仕様１に基づいて抽出した獲得と開放の処理パターンを図１６に示す。また、これらの獲得、開放パターンを抽出する場合の処理の流れを図１７に示す。
【００３８】
図１７では、プログラム１のルート１、すなわち、ａ１＝＞Ａ１から走査が開始される。獲得パターンとして、bufp、ctlp、及びbuf2p=getbuf()が検出され、開放パターンとしてreturn(buf2p)が検出されている。そのため、buf2pの獲得パターンを共有する他の検証ルートに開放パターンが存在するかが検証され、ルート２、３、及び４においてbuf2pの開放パターンが検出され正常と判定されている。
【００３９】
ルート１に続いて、ルート２の走査が行われる。bufp、ctlp及びbuf2pの獲得パターンと開放パターンとが検出されているが、buf2pについては、すでにルート１の走査において検証済みであるので、bufpとctlpとについて他の検証ルートの検証が行われる。その結果、ルート１とルート４とでbufp及びctlpの開放パターンがないことが判明する。以下同様にルート４まで走査がなされ、最終的にルート１とルート４とにおいて、bufpとctlpの開放処理の漏れが検出される。
【００４０】
一方、実際のプログラム１のバグは、上述のように、ルート１（ブロックＡ１）とルート４（ブロックＣ２）とで、bufpの開放処理が漏れていることだけであり、ctlpについては、開放処理は必要ない。この結果は、ctlpが仕様的には、獲得／開放処理の対象にならないが、上記のパターンの抽出規則の条件を満たしたために発生したことである。このような結果は、後から人が確認すれば容易にチェックできることであるが、この例で示したctlpのように、予め特定の資源について開放処理の必要がないことが分かっているような場合には、処理パターン抽出時の補助情報として、事前に判定対象外の資源を指定できるようにしておけば、上記のような無用の情報の検出を防止することができる（第１の処理または第２の処理の特定を補助する情報を補助情報として入力することに相当）。
【００４１】
このように本実施の形態のプログラム検証装置は、種々のプログラムに共通に必要とされる一般的な規則を検証する仕様として規定し、その検証する仕様に対応した検証ルートをプログラムから抽出し、一定数以上の検証ルート（上述では１以上の検証ルート）において成立している、そのプログラムが持つ検証する仕様に対応した具体的な仕様を、そのプログラムの全体で成立する仕様（処理仕様）であると判定するものである。そして、その結果、本来満たすべき処理仕様が成立していない検証ルートをプログラムのバグの可能性がある部分として抽出する機能を提供するものである。
【００４２】
本実施の形態によれば、個々のプログラム独自の要求仕様や複雑な文法規則を用いることなく、プログラム開発上の汎用的な規則としての検証する仕様に基づき、プログラムの正当性を検証することができる。
＜変形例＞
上記実施の形態では、図１４のサンプルプログラムに対して、検証する仕様として検証仕様１を適用した例を示したが、本発明の実施は検証仕様１には限定されない。他の検証する仕様の例として、以下に検証仕様２とこれに対応する具体的走査規則を示す。
検証仕様２：個々の関数はプログラム上のどのルートで呼び出されても、その関数の引数となる要素のうちで、設定が必要なものは一定である。
具体的走査規則：
（１）検証ルートの走査の開始点（具体的には、コマンドの入り口、一次割り込みの入り口となるもの）を外部から指定させる。
（２）複数の分岐文が同一レベルで組み合わされている場合、すべての組み合わせを網羅して検証ルートを走査する。例えば、２分岐のif文と４分岐のcase文があった場合、２×４＝８個の検証ルートが走査される。
（３）ループ文（for文、while文）については、そのループ処理部を一度だけ走査する。
（４）関数内部で他の関数を呼び出す場合、呼び出し先の関数まで検証ルートを走査する。ただし、走査済みの検証ルートですでに走査されている関数を再度走査することはしない。
（５）ループ内にbreak文を検出した場合、ループ処理部から抜ける。
（６）return文検出時は、その関数から抜けるものとする。
【００４３】
以下に、検証する仕様が上記検証仕様２の場合、処理パターン抽出部の抽出規則を示す。
（１）検証対象のプログラムを構成するすべての関数を抽出する。
（２）１つの関数に対して、上記具体的走査規則に従って抽出したすべてのルートにおけるその関数の呼び出し位置に対して、その関数呼び出し時にどれだけの情報（引数となっている構造体の要素）が設定されているかを抽出する。
【００４４】
以上の走査の結果、各関数に対して、呼び出されるときに設定されている要素が、一定以上の検証ルートで同一のとき、その要素がその関数呼び出し時に設定が必要な要素であると判断される。
【００４５】
上記実施の形態では、ソースプログラムを検証対象としたが、本発明はソースプログラムの検証に限るものではない。すなわち、本発明は、検証ルートとその検証ルートに含まれる処理パターンを抽出できるプログラム一般に適用できるので、その処理対象のプログラムの形式がソースプログラムのようにテキスト形式であるか、コンパイルされたバイナリ形式であるかには依存しない。例えば、上述した実施の形態において、文を命令に置き換え、ブロックを命令列に置き換えて、図４の行番号をファイルのアドレスに変更すれば、本発明をバイナリ形式のプログラムにもそのまま適用できる。
【００４６】
【発明の効果】
以上説明したように、本発明によれば、計算機で実行される実行プログラムまたはこの実行プログラムを生成するためのソースプログラムを検証する仕様に対応したプログラムの部分としての１以上の処理からなるブロックに分割し、２以上のブロックの組み合わせを、前記検証する仕様に対応した検証ルートとして複数抽出し、所定数以上の検証ルートにおいて実行される検証する仕様に対応した処理を他の検証ルートにおいても実行されるべき処理としての処理仕様として抽出することによりプログラムを検証するので、個々のプログラムが実現すべき本来の処理仕様を抽出し、その処理仕様に合致しないプログラムの部分を自動的に抽出することができる
【図面の簡単な説明】
【図１】本発明の概念を示す図
【図２】本発明の実施の形態におけるハードウェアの構成図
【図３】本発明の実施の形態におけるプログラムの構成図
【図４】文構造体を示す図
【図５】ブロック構造体を示す図
【図６】文構造体例１
【図７】文構造体例２
【図８】文構造体例３
【図９】サンプルプログラムを示す図
【図１０】文の階層構造を示す図
【図１１】検証ルートの例を示す図
【図１２】検証ルートを表現するためのデータ構造を示す図
【図１３】検証ルート抽出部、処理パターン抽出部及び処理仕様抽出部の関係を示す図
【図１４】サンプルプログラムを示す図
【図１５】サンプルプログラムを示す図
【図１６】検証ルートから獲得パターンと開放パターンを抽出した例を示す図
【図１７】本発明の一実施の形態の処理を示す図
【符号の説明】
１  ＣＰＵ
２  メモリ
１１  ブロック分割部
１２  検証ルート抽出部
１３  処理パターン抽出部
１４  処理仕様抽出部
【図１】
0004098448.tif 000002
【図２】
0004098448.tif 000003
【図３】
0004098448.tif 000004
【図４】
0004098448.tif 000005
【図５】
0004098448.tif 000006
【図６】
0004098448.tif 000007
【図７】
0004098448.tif 000008
【図８】
0004098448.tif 000009
【図９】
0004098448.tif 000010
【図１０】
0004098448.tif 000011
【図１１】
0004098448.tif 000012
【図１２】
0004098448.tif 000013
【図１３】
0004098448.tif 000014
【図１４】
0004098448.tif 000015
【図１５】
0004098448.tif 000016
【図１６】
0004098448.tif 000017
【図１７】
0004098448.tif 000018