(57)【要約】【課題】プログラムについて、構造の観点からのカバレッジ基準をみたすパス情報を効果的に生成すること。【解決手段】検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入手段と、前記トラップ挿入手段によってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査手段と、前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成手段と、を備えたことを特徴とする。【選択図】  図１
2012181665.tif 000002
【特許請求の範囲】
【請求項１】
検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入手段と、
前記トラップ挿入手段によってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査手段と、
前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成手段と、
を備えたことを特徴とする情報処理装置。
【請求項２】
前記トラップ挿入手段は、プログラムの構造上のカバレッジ基準として、命令カバレッジ、分岐カバレッジ、MC/DC(Modified condition decision coverage)の少なくともいずれか１つのカバレッジに対応して、検証対象プログラムを整形しトラップを挿入することを特徴とする請求項１に記載の情報処理装置。
【請求項３】
前記トラップ挿入手段は、プログラムの構造上のカバレッジ基準として、命令カバレッジ、分岐カバレッジ、MC/DC(Modified condition decision coverage)の全てのカバレッジに対応すべく検証対象プログラムを整形し、トラップを挿入することを特徴とする請求項１に記載の情報処理装置。
【請求項４】
前記事前条件を整形して、テスト入力を生成するテスト入力生成手段をさらに備えたことを特徴とする請求項１乃至３のいずれか１項に記載の情報処理装置。
【請求項５】
前記事前条件生成手段は、前記トラップ挿入手段が１つのトラップを挿入する度に全パス情報を確認して事前条件を生成することを特徴とする請求項１乃至４のいずれか１項に記載の情報処理装置。
【請求項６】
前記事前条件生成手段は、前記トラップ挿入手段が全てのトラップを挿入した後に全パス情報を確認して事前条件を生成することを特徴とする請求項１乃至４のいずれか１項に記載の情報処理装置。
【請求項７】
前記検証対象プログラムがＣ言語で記述されている場合、
前記トラップ挿入手段は、挿入するトラップとして、Ｃ言語のassertマクロを用いたassertを挿入することを特徴することを特徴とする請求項１乃至６のいずれか１項に記載の情報処理装置。
【請求項８】
前記ソフトウェアモデル検査手段は、前記assertに設定された表明式が満たされるか否かを調べ、表明式が偽になることがあれば、反例のパス情報を出力することを特徴とする請求項７に記載の情報処理装置。
【請求項９】
検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入ステップと、
前記トラップ挿入ステップによってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査ステップと、
前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成ステップと、
を備えたことを特徴とする情報処理方法。
【請求項１０】
検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入ステップと、
前記トラップ挿入ステップによってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査ステップと、
前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成ステップと、
をコンピュータに実行させることを特徴とする情報処理プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、プログラムを静的に解析してプログラムの事前条件を生成するための技術、及び生成された事前条件を用いて動的なテストを行うための技術に関する。
【背景技術】
【０００２】
プログラムが検証したい性質（プロパティ property）を満たすか否かをモデル検査法(model checking)により静的に調べて、不具合を検出する方法がある。この方法は、ソフトウェアモデル検査(software model checking)あるいはモダンモデル検査(modern model checking)と呼ばれている。モデル検査法とは、システムやソフトウェアの振舞いを表した、有限個の状態(state)及び状態間の遷移(transition)からなる有限状態空間(finite state space)において、空間内を網羅探索することにより、検証したい性質が成立するか否かを調べる手法である。
【０００３】
とくに、探索の深さを限定した有界モデル検査法(bounded model checking)は、不具合の検出に有効であるとされている。有界モデル検査法を用いたソフトウェアモデル検査においては、検証対象プログラムに出現する全ての変数に関して、変数値の組合せの一つ一つが状態である。
【０００４】
非特許文献１は、有界モデル検査法をプログラムの検証へ適用した一例である。この例では、プログラムに表れる各変数の値の遷移を制約式Ｃとして表現し、検証したい性質を論理式Ｐとして表現し、Ｃ∧¬Ｐ（∧は論理和、¬は否定）を満たす変数値の推移（パス情報）を網羅探索により検出することを試みる。非特許文献１では、Ｃ言語のプログラムにassertマクロを用いて、検査したい性質を表明式として記述することにより、表明違反を検出できることが示されている。元のプログラムには存在しないが、検査の都合により、人手で、あるいはツールが自動で挿入する表明式及び表明式で用いられる変数をトラップと呼ぶことがある。
【０００５】
検査したい性質Ｐを満たさないようなパス情報はＰへの反例(counter-example)と呼ばれており、反例として示されたパス情報に沿ってプログラムが実行されると、検証したい性質を満たさないような不具合が発生するといえる。パス情報の先頭に出現する変数はプログラムの入力変数であり、パス情報上での入力変数の値を１つのテスト入力の一部として利用できることは、広く知られている。パス情報に含まれない入力変数について固定値やランダムに生成した値などを割り当てることにより、１つのテスト入力の全体を得ることができる。
【０００６】
一方、特許文献１にも、モデル検査の反例からテスト生成を行うことが記されている。プログラムのテストは、所与のテスト入力に関して、プログラムを実際に動かして、プログラムの振舞いや出力が適切であることを確認する。１組のテスト入力により、ある１つの実行パスのみを確認することができる。別の実行パスを確認する場合には、異なるテスト入力を与える必要がある。ゆえに、テストの良否はテスト入力の良否で決まり、テスト入力の良否はカバレッジで判断される。プログラムの内部構造を意識したテストをホワイトボックステストと呼び、プログラムの内部構造のうち特定の構造を検査した比率をカバレッジとする。プログラムの内部構造に着目したカバレッジ基準は、特定の種類の構造として何を選ぶか（何を基準にするか）を示すものである。たとえば、命令カバレッジ(statement coverage)、判定カバレッジ(decision coverage)、及びＭＣ／ＤＣカバレッジ(modified condition decision coverage)が広く使われている。
【０００７】
命令カバレッジ(statement coverage)は、各文(statement)を一度は検査したことを示す。判定カバレッジ(decision coverage)は、各ループや分岐の判定(decision)が真となる場合と偽となる場合を一度は検査したことを示す。ＭＣ／ＤＣカバレッジ(modified decision condition coverage)は、各ループや分岐の判定を構成する条件(condition)が、他の条件の値を固定した場合に、ある条件の真偽によって判定の真偽が決まるような条件の組合せを一度は検査したことを示す。命令カバレッジ基準の場合、プログラム中の文の件数を母数として、検査した文の件数を割った値がカバレッジとなる。
【０００８】
プログラムの内部構造を意識しないテストをブラックボックステストと呼び、入出力データに着目して、どのようなデータを用いて検査したかでカバレッジを決める。入出力データの場合分けの考え方として、入力変数のとり得る値の範囲を同様の出力結果が得られるクラスに分ける同値分割法が知られている。この方法では、クラスの件数を母数として検査したクラスの件数を割った値がカバレッジとなる。何らかのカバレッジ基準のもとで、プログラムを検査した際のカバレッジが高いほど、テスト入力のセットは良いといえる。
【先行技術文献】
【特許文献】
【０００９】
【特許文献１】特開2009-87354号公報
【非特許文献】
【００１０】
【非特許文献１】E. Clarke, D. Kroening, and F. Lerda.A Tool for Checking ANSI-C Programs.Proceedings of TACAS' 04, pages 168-176, 2004（assertを用いた検査の例は頁169-170の節2.1 Generating the Formulaを参照）
【発明の概要】
【発明が解決しようとする課題】
【００１１】
しかしながら、上記従来技術では、プログラムのテストにおいて、１組のテスト入力によって検査できるのは１実行パスのみである。カバレッジを上げるためには、別のテスト入力を与える必要があるが、場合によってはカバレッジが増えないことがある。
【００１２】
たとえば、入力変数 x に関して、「if ( 0 ＜= x ) 文Ａ else 文Ｂ」はxが0以上の場合に文Ａを実行し、0未満の場合に文Ｂを実行することを表す。命令カバレッジ基準では、テスト入力のセット全体に対して、if文と文Ａと文Ｂが実行されれば、カバレッジは100%である。ここで、xが0というテスト入力を与えると文Ａが実行されるが、文Ｂは実行されない。さらに、xが1というテスト入力を与えても、やはり文Ｂは実行されず、カバレッジは増えない。文Ｂを実行するにはxが-1といった0未満のテスト入力を与える必要がある。
【００１３】
構造の観点からのカバレッジを向上させるには、プログラムの構造を反映したテスト入力を与える必要がある。一方、データの観点からカバレッジを考えるためには、出力データのとり得る値の範囲と、それに対応した入力変数がとり得る値の範囲とを知る必要がある。たとえば、「if ( 0 ＜=  x ) { r = x + 1; } else { r = x - 1; }」というコード断片では、出力変数 r が-1未満となるような入力変数xは0未満であり、出力変数 r が1以上となるような入力変数xは0以上である。しかし、設計においてプログラムの入力についての仕様が予め与えられている場合を除き、入力変数のとり得る値の範囲は自明ではない。特許文献１では、モデル検査の反例からテスト生成を行うことが記されているが、反例から得られるテスト入力は、ある１つのパスを実行するためのピンポイントの値の組であり、そこから入力変数の値の範囲を知ることはできない。
【００１４】
本発明の目的は、上述の課題を解決する技術を提供することにある。
【課題を解決するための手段】
【００１５】
上記目的を達成するため、本発明に係る装置は、
検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入手段と、
前記トラップ挿入手段によってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査手段と、
前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成手段と、
を備えたことを特徴とする。
【００１６】
上記目的を達成するため、本発明に係る方法は、
検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入ステップと、
前記トラップ挿入ステップによってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査ステップと、
前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成ステップと、
を備えたことを特徴とする。
【００１７】
上記目的を達成するため、本発明に係るプログラムは、
検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入ステップと、
前記トラップ挿入ステップによってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査ステップと、
前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成ステップと、
をコンピュータに実行させることを特徴とする。
【発明の効果】
【００１８】
本発明によれば、プログラムについて、構造の観点からのカバレッジ基準をみたすパス情報を効果的に生成することができる。
【図面の簡単な説明】
【００１９】
【図１】本発明の第１実施形態に係る情報処理装置の構成を示すブロック図である。
【図２】本発明の第２実施形態としてのシステムの全体構成を示す概略図である。
【図３】本発明の第２実施形態としてのシステムの全体的な処理の流れを示す図である。
【図４】本発明の第２実施形態及び第３実施形態としてのシステムにおいて、パス情報から事前条件を生成する処理の流れを示す図である。
【図５】本発明の第２実施形態及び第３実施形態としてのシステムにおいて、命令カバレッジ基準用にプログラムを整形してトラップを挿入する具体例を示す図である。
【図６】本発明の第２実施形態及び第３実施形態としてのシステムにおいて、分岐カバレッジ基準用にプログラムを整形してトラップを挿入する具体例を示す図である。
【図７】本発明の第２実施形態及び第３実施形態としてのシステムにおいて、MC/DC (Modified condition / decision coverage)基準用にプログラムを整形してトラップを挿入する具体例を示す図である。
【図８】本発明の第２実施形態及び第３実施形態としてのシステムにおいて、二分岐以外の構造についてプログラムを整形する例を示す図である。
【図９】本発明の第２実施形態及び第３実施形態としてのシステムにおいて、パス情報から事前条件を生成する具体例を示す図である。
【図１０】本発明の第３実施形態としてのシステムの全体構成を示す概略図である。
【図１１】本発明の第３実施形態としてのシステムにおいて、事前条件からテスト入力を生成する処理の流れを示す図である。
【図１２】本発明の第３実施形態としてのシステムにおいて、事前条件からテスト入力を生成する具体例を示す図である。
【図１３】本発明の他の実施形態としてのシステムの概要を説明するための図である。
【発明を実施するための形態】
【００２０】
以下に、図面を参照して、本発明の実施の形態について例示的に詳しく説明する。ただし、以下の実施の形態に記載されている構成要素はあくまで例示であり、本発明の技術範囲をそれらのみに限定する趣旨のものではない。
【００２１】
（第１実施形態）
本発明の第１実施形態としての情報処理装置１００について、図１を用いて説明する。情報処理装置１００は、プログラムを静的に解析してプログラムの事前条件を生成する装置である。
【００２２】
図１に示すように、情報処理装置１００は、トラップ挿入部１０１とソフトウェアモデル検査部１０２と事前条件生成部１０３とを含む。トラップ挿入部１０１は、検証対象プログラムをカバレッジ基準に応じて整形してトラップを挿入する。ソフトウェアモデル検査部１０２は、トラップ挿入部１０１によってトラップを挿入されたトラップ入りプログラムに関してソフトウェアモデル検査を行い、カバレッジを満たすパス情報を出力する。さらに、事前条件生成部１０３は、パス情報からカバレッジを満たす事前条件を生成する。
【００２３】
検証対象プログラムについて、構造の観点からのカバレッジ基準をみたすパス情報を効果的に生成することができる。
【００２４】
（第２実施形態）
次に本発明の第２実施形態に係るプログラム検証用事前条件生成装置２００について、図２乃至図９を用いて説明する。
【００２５】
《装置構成》
図２は、本実施形態としてのプログラム検証用事前条件生成装置２００の概略構成を示す図である。プログラム検証用事前条件生成装置２００は、情報処理部２０１とファイル格納部２０２とを含む。情報処理部２０１は、トラップ挿入モジュール２１１とソフトウェアモデル検査モジュール２１３と事前条件生成モジュール２１５とを含む。ここで、検証対象プログラムはＣ言語で記述されているものとする。トラップ挿入モジュール２１１は、ファイル格納部から検証対象プログラムを読み込み、構造上のカバレッジ基準に対応して、トラップの挿入箇所が実行（カバー）されたか否かを調べるためのトラップを挿入し、トラップ入りプログラムを作成する。ここで、本実施形態に係るトラップは、プログラムを静的に解析するソフトウェアモデル検査モジュール２１３に、特定のカバレッジを持つパス情報を算出するようにヒントを与えるものであり、プログラムのテスト実行とは関係がない。トラップを用いて得られたパス情報からはテスト入力や事前条件を生成することができる。
【００２６】
一方、ソフトウェアモデル検査モジュール２１３は、「トラップ挿入箇所が実行されない」ことを調べたい性質として、トラップ入りプログラムを静的に検査し、トラップ挿入箇所が実行されることを示す反例のパス情報を出力する。事前条件生成モジュール２１５は、パス情報をトラップ挿入箇所からプログラムの開始箇所へと逆向きにたどり、プログラムの開始箇所が満たす事前条件、すなわちトラップ挿入箇所を実行するような事前条件を生成して、出力する。このソフトウェアモデル検査は、個々のモジュール内に含まれる命令や条件分岐等の通過率を計測するようなテストカバレッジで十分性を判断する、ソフトウェア単体テストといった下位レベルのテストに関する。
【００２７】
《全体の処理の流れ》
次に、図３のフローチャートを参照してプログラム検証用事前条件生成装置２００が行なう動作全体について詳細に説明する。情報処理部２０１は、利用者から検証対象プログラムの指定を受け付け、他のモジュールに図３で示す一連の処理を実行させる。まず、トラップ挿入モジュール２１１は、ファイル格納部２０２から検証対象プログラムを読み込み、構造の観点でのカバレッジ基準に応じて、プログラム中の分岐文や繰り返し文をある定まった形式に整形する（Ｓ３０１）。
【００２８】
さらに、トラップ挿入モジュール２１１は、整形されたプログラムにおいて、まだトラップを挿入されていないトラップ挿入対象箇所があるか否かを調べる（Ｓ３０２）。トラップ挿入対象箇所がある場合には、トラップ挿入対象箇所を１つ選び、挿入箇所が実行されたことを示すトラップを挿入して、トラップ入りプログラムを作成する（Ｓ３０３）。トラップ挿入対象箇所がなくなった場合には、ステップＳ３０４に進む。
【００２９】
ステップＳ３０４において、ソフトウェアモデル検査モジュール２１３は、「トラップ挿入箇所が実行されない」ことを調べたい性質として、トラップ入りプログラムを静的に検査し、トラップ挿入箇所が実行されることを示す反例のパス情報を出力する。
【００３０】
ステップＳ３０５で、事前条件生成モジュール２１５は、まだ事前条件を生成していないパス情報があるか否かを調べる。まだ事前条件を生成していないパス情報がある場合には、ステップＳ３０６に進み、パス情報を１つ選び、トラップ挿入箇所からプログラムの開始ステップへと逆向きにたどる。そして、プログラムの開始ステップが満たす事前条件、すなわちトラップ挿入箇所を実行するような事前条件を生成して、出力する。事前条件を生成していないパス情報が無くなれば、処理を終了する。
【００３１】
なお、上記フローチャートでは、全てのトラップを挿入してから事前条件を生成している。しかし本発明はこれに限定されるものではなく、１つのトラップを挿入する度に全パス情報を確認して事前条件を生成してもよい。つまり、ステップＳ３０３からステップＳ３０４に進んで、トラップ挿入箇所が無くなるまでステップＳ３０２〜Ｓ３０６の処理を繰り返しても良い。
【００３２】
図４を用いて、事前条件を算出する処理（Ｓ３０６）を詳しく説明する。まず、パス情報においてトラップ挿入箇所を処理対象のステップとし、事前条件を真とする（Ｓ４０１）。処理対象を１つ前のステップに変更し（Ｓ４０２）、処理対象のステップがプログラム開始ステップか否かを調べる（Ｓ４０３）。プログラム開始ステップであれば事前条件生成の処理を終了する。開始ステップでなければ、処理対象ステップが分岐の条件であるか、代入であるかを調べる（Ｓ４０４）。処理対象ステップが分岐の条件であれば、事前条件と処理対象ステップの条件との論理積を新たな事前条件とし（Ｓ４０５）、ステップＳ４０２へ戻る。一方、ステップＳ４０４で、処理対象ステップが代入を行なうステップと判断すれば、事前条件に代入の左辺と同じ変数があれば代入の右辺と置換して新たな事前条件とし（Ｓ４０６）、ステップＳ４０２へ戻る。
【００３３】
《トラップ挿入例》
図５〜図８を用いて、トラップ挿入の具体例について説明する。図５は、命令カバレッジ基準に関するトラップを挿入する例であり、検証対象プログラム５０１における条件文（行１）を整形して、条件式を一時変数 d_ に代入する文（行1a）と一時変数を用いた条件文（行1b）とを有する整形プログラム５０２を生成する。命令カバレッジは、各命令が少なくとも１回実行されたことを確認すればよいので、各代入文（行1a、行2）の直後をトラップ挿入対象箇所として、トラップ入りプログラム５０３、５０４を作成する。図５の例では、挿入トラップとして、Ｃ言語のassertマクロを用いたassert(0); を挿入している。assertマクロを検査できるソフトウェアモデル検査手段は、assertに設定された表明式が満たされるか否かを調べ、表明式が偽になることがあれば、反例のパス情報を出力する。図５の例では、表明式として0すなわちＣ言語における恒偽を設定しているため、このトラップに到達し得るパスが存在すれば、ソフトウェアモデル検査モジュール２１３は反例のパス情報を出力する。
【００３４】
図６は、分岐カバレッジ基準に関するトラップを挿入する具体例を示す図である。検証対象プログラム６０１を整形して整形プログラム６０２を生成し、さらにそこからトラップ入りプログラム６０３、６０４を生成する。
【００３５】
検証対象プログラム６０１における条件文（行1）を、条件全体が真であれば（行1a）一時変数 d_ に真(1)を代入する文(行1b)と、条件全体が偽であれば（行1c）一時変数 d_ に偽(0)を代入する文(行1d)と、一時変数 d_ を用いた条件文（行1f）とに整形する。
【００３６】
分岐カバレッジは、各条件文において、条件全体が真をとる場合と偽をとる場合とが少なくとも１回実行されたことを確認すればよいので、一時変数 d_ への代入（行1b,1c）の直後をトラップ挿入箇所として、トラップ入りプログラム６０３、６０４を作成する。
【００３７】
図７は、MC/DC（Modified condition / decision coverage）基準に関するトラップを挿入する具体例であり、検証対象プログラム７０１を整形して整形プログラム７０２を生成し、さらにそこからトラップ入りプログラム７０３〜７０５を生成する。
【００３８】
ここでは検証対象プログラム７０１の条件文（行1）における条件全体 0＜x && 0＜y を論理演算子を含まない基本条件 0＜x と 0＜y とに分けて考える。検証対象プログラム７０１における条件文（行1）を整形して、0＜xが真（行1a）かつ 0＜y が真（行1b）であれば一時変数 d_ に真(1)を代入する（行1c）文とする。また、条件文（行1）を整形して、0＜xが真（行1a）かつ 0＜y が偽（行1d）であれば一時変数 d_ に偽(0)を代入し（行1e）、0＜xが偽（行1g）であれば一時変数 d_ に偽(0)を代入（行1h）する文を生成する。MC/DC分岐カバレッジでは、他の基本条件を真か偽に固定した場合に、ある基本条件が条件全体の真偽を決定するような基本条件の組合せについて、組合せの数が最小になり、かつ各組合せが少なくとも１回実行されたことを確認する。そのため、一時変数 d_ への代入（行1c,1e,1h）の直後をトラップ挿入箇所として、トラップ入りプログラム７０３〜７０５を作成する。プログラムには二分岐以外の構造もあるが、これらは、二分岐を用いた入力・出力・副作用に影響を与えない等価な構造に整形することにより、図５〜７で例示したトラップ挿入を行うことができる。
【００３９】
図８は、Ｃ言語において、繰返し構造を表すforブロック８０１、whileブロック８０２、doブロック８０３、及び多分岐構造を表すswitchブロック８０４を、while文による繰返しとif文による二分岐からなる等価な構造８０５〜８０８に整形する例を示す。
【００４０】
《事前条件生成例》
図９は、事前条件の生成処理の具体例を説明するための図である。図９の例では、トラップ入りプログラム９０１の13ｘ行にトラップassert(0); が挿入されている。ソフトウェアモデル検査モジュール２１３が出力したパス情報９０２には、変数の値の遷移が記録されている。変数{値}は、変数がカッコ内の値を持つことを示す。条件式と代入式の左辺の値は式の評価後の値であり、代入式の右辺の値は式の評価前の値である。
【００４１】
パス情報９０２として、プログラムの開始箇所（1行目）で、入力変数xとyにそれぞれ0と-1が与えられる。すると二分岐（2行目）の条件 x ＜ 0が成り立たたずに、elseブロック（9行目）では条件 0 ＜= x が成り立つ。次の代入（10行目）で、x から 10が減算され、二分岐（11行目）の条件 x ＜ y − 10 が成り立たたずに、elseブロック（13行目）では条件 y − 10 ＜= x が成り立ち、終了箇所であるトラップ挿入箇所（13x行目）に達する。
【００４２】
事前条件９０３は、パス情報を終了箇所から開始箇所へと逆に辿って計算する。終了箇所での事前条件を真として、１つ前のステップ(13行)を処理対象とし対象ステップの条件式 y − 10 ＜= x と事前条件{真}との論理積{y − 10 ＜= x}を新たな事前条件とする。
【００４３】
次に、１つ前のステップ(10行)を処理対象として、対象ステップの代入式 x =  x − 10に基づき、事前条件の x を x -10 に置き換えた条件{y ＜= x}を新たな事前条件とする。さらに１つ前のステップ(9行)を処理対象として、対象ステップの条件式 0 ＜= x と事前条件{y ＜= x}との論理積{0 ＜= x && y ＜= x }を新たな事前条件とする。１つ前のステップ(1行)を処理対象として、対象ステップがプログラムの開始箇所なので計算を終える。これにより、トラップ（13x行）に達するためのプログラムの事前条件は0 ＜= x && y ＜= x となる。
【００４４】
なお、図５〜８にはプログラムのソースコードを整形する例を示したが、プログラムの制御フロー (Control flow) を整形してもよい。
【００４５】
本実施形態では、パス情報から入力変数のとり得る値の範囲を示す事前条件を生成する。事前条件を満たす入力変数の値を用いることにより、データの観点からのカバレッジを増やすようなテスト入力を人手で作ることができ、また自動生成することもできる。特にソフトウェアモデル検査モジュールによって生成されたパス情報から、入力変数が満たすべき条件（事前条件）を自動で生成する。
【００４６】
（第３実施形態）
次に本発明の第３実施形態に係るプログラム検証用テスト入力生成装置について、図１０及び図１１を用いて説明する。図１０は、本実施形態としてのプログラム検証用テスト入力生成装置１０００の概略構成を示す図である。図２のプログラム検証用事前条件生成装置２００と比べると、テスト入力生成モジュール１０１７が追加されている点が異なる。その他の構成及び動作は、第２実施形態と同様であるため、同じ構成及び動作については同じ符号を付してその詳しい説明を省略する。
【００４７】
図１１は、入力変数のとり得る値の範囲の境界をテストする場合に、テスト入力生成モジュール１０１７が行う処理の流れを示すフローチャートである。まず、テスト入力生成モジュール１０１７は、事前条件生成モジュール２１５が生成した事前条件について、テスト入力をまだ生成していない事前条件があるか否かを調べ（Ｓ１１０１）、なければ処理の流れ全体を終了する。あれば、「以下」「以上」の比較演算子を用いた条件式を「未満」「等号」「超過」の比較演算子を用いた条件式の論理和に変換する（Ｓ１１０２）。次に、テスト入力生成モジュール１０１７は論理和で区切られた各条件式について、テスト入力をまだ生成していない事前条件があるか否かを調べ（Ｓ１１０３）、なければステップＳ１１０１に戻る。あれば、制約充足アルゴリズムなどを用いて条件式を満たすような入力変数への値の割当を計算する（Ｓ１１０４）。
【００４８】
図１２は、テスト入力の生成例を示す図である。図１２では、事前条件１２０１「0＜=x&& y＜=x」を「0==x && y==x || 0==x && y＜x || 0＜x && y==x || 0＜x && y＜x」に変換する。条件式１２０２に含まれる「0==x && y==x」と「0==x && y＜x」と「0＜x && y==x」と「0＜x && y＜x」の各々について、入力変数x, yの組(0,0)、(0,-1)、(1,1)、(1,0)を見つける。これらがテスト入力１２０３の一部となる。事前条件に含まれない入力変数について固定値やランダムに生成した値などを割り当てることにより、１つのテスト入力の全体を得ることができる。
【００４９】
本実施形態によれば、プログラムの単体テストに関して、プログラムを静的かつ網羅的に調べるソフトウェアモデル検査技術を用いて、プログラム構造の観点からのカバレッジ基準を満たすようなパス情報を得る。さらにパス情報からカバレッジ基準を満たすような事前条件を生成することにより、人手でのテスト入力の作成を容易にする、あるいはテスト入力の自動生成を行うことができる。
【００５０】
（他の実施形態）
以上、本発明の実施形態について詳述したが、それぞれの実施形態に含まれる別々の特徴を如何様に組み合わせたシステム又は装置も、本発明の範疇に含まれる。
【００５１】
また、本発明は、複数の機器から構成されるシステムに適用されても良いし、単体の装置に適用されても良い。さらに、本発明は、実施形態の機能を実現する情報処理プログラムが、システムあるいは装置に直接あるいは遠隔から供給される場合にも適用可能である。したがって、本発明の機能をコンピュータで実現するために、コンピュータにインストールされるプログラム、あるいはそのプログラムを格納した媒体、そのプログラムをダウンロードさせるＷＷＷ(World Wide Web)サーバも、本発明の範疇に含まれる。
【００５２】
本発明に係る情報処理プログラムを実行するコンピュータの構成例を図１３に示す。コンピュータ１３００は、ＣＰＵ(Central Processing Unit)１３０１、ＲＯＭ(Read Only Memory)１３０２、通信制御部１３０３、ＲＡＭ(Randam Access Memory)１３０４、及びストレージ１３０５を備えている。ＣＰＵ１３０１は中央処理部であって、様々なプログラムを実行することによりコンピュータ１３００全体を制御する。ＲＯＭ１３０２は、不揮発メモリであり、ＣＰＵ１３０１が最初に実行すべきブートプログラムの他、各種のパラメータ等を記憶している。また、ＲＡＭ１３０４は、ランダムアクセスメモリであり、トラップ挿入モジュール２１１等のアプリケーションの実行領域１３４１及びアプリケーションが扱うデータ（例えば、対象プログラム、スタブプログラム、テスト用プログラム、ドライバプログラム、パス情報など）の記憶領域１３４２を有している。一方、ストレージ１３０５は、各種モジュール１３５１と、各種ファイル（対象プログラムなど）を保存する装置である。また、通信制御部１３０３は、他の端末とのネットワークを介した通信を制御する。
【００５３】
［実施形態の他の表現］
上記の実施形態の一部又は全部は、以下の付記のようにも記載されうるが、以下には限られない。
【００５４】
（付記１）
検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入手段と、
前記トラップ挿入手段によってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査手段と、
前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成手段と、
を備えたことを特徴とする情報処理装置。
（付記２）
前記トラップ挿入手段は、プログラムの構造上のカバレッジ基準として、命令カバレッジ、分岐カバレッジ、MC/DC(Modified condition decision coverage)の少なくともいずれか１つのカバレッジに対応して、検証対象プログラムを整形しトラップを挿入することを特徴とする付記１に記載の情報処理装置。
（付記３）
前記トラップ挿入手段は、プログラムの構造上のカバレッジ基準として、命令カバレッジ、分岐カバレッジ、MC/DC(Modified condition decision coverage)の全てのカバレッジに対応すべく検証対象プログラムを整形し、トラップを挿入することを特徴とする付記１に記載の情報処理装置。
（付記４）
前記事前条件を整形して、テスト入力を生成するテスト入力生成手段をさらに備えたことを特徴とする付記１乃至３のいずれか１項に記載の情報処理装置。
（付記５）
前記事前条件生成手段は、前記トラップ挿入手段が１つのトラップを挿入する度に全パス情報を確認して事前条件を生成することを特徴とする付記１乃至４のいずれか１項に記載の情報処理装置。
（付記６）
前記事前条件生成手段は、前記トラップ挿入手段が全てのトラップを挿入した後に全パス情報を確認して事前条件を生成することを特徴とする付記１乃至４のいずれか１項に記載の情報処理装置。
（付記７）
前記検証対象プログラムがＣ言語で記述されている場合、
前記トラップ挿入手段は、挿入するトラップとして、Ｃ言語のassertマクロを用いたassertを挿入することを特徴することを特徴とする付記１乃至６のいずれか１項に記載の情報処理装置。
（付記８）
前記ソフトウェアモデル検査手段は、前記assertに設定された表明式が満たされるか否かを調べ、表明式が偽になることがあれば、反例のパス情報を出力することを特徴とする付記７に記載の情報処理装置。
（付記９）
検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入ステップと、
前記トラップ挿入ステップによってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査ステップと、
前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成ステップと、
を備えたことを特徴とする情報処理方法。
（付記１０）
検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入ステップと、
前記トラップ挿入ステップによってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査ステップと、
前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成ステップと、
をコンピュータに実行させることを特徴とする情報処理プログラム。
【図１】
2012181665.tif 000003
【図２】
2012181665.tif 000004
【図３】
2012181665.tif 000005
【図４】
2012181665.tif 000006
【図５】
2012181665.tif 000007
【図６】
2012181665.tif 000008
【図７】
2012181665.tif 000009
【図８】
2012181665.tif 000010
【図９】
2012181665.tif 000011
【図１０】
2012181665.tif 000012
【図１１】
2012181665.tif 000013
【図１２】
2012181665.tif 000014
【図１３】
2012181665.tif 000015