検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入手段と、前記トラップ挿入手段によってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査手段と、前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成手段と、を備えたことを特徴とする情報処理装置。前記トラップ挿入手段は、プログラムの構造上のカバレッジ基準として、命令カバレッジ、分岐カバレッジ、MCDCの少なくともいずれか1つのカバレッジに対応して、検証対象プログラムを整形しトラップを挿入することを特徴とする請求項1に記載の情報処理装置。前記トラップ挿入手段は、プログラムの構造上のカバレッジ基準として、命令カバレッジ、分岐カバレッジ、MCDCの全てのカバレッジに対応すべく検証対象プログラムを整形し、トラップを挿入することを特徴とする請求項1に記載の情報処理装置。前記事前条件を整形して、テスト入力を生成するテスト入力生成手段をさらに備えたことを特徴とする請求項1乃至3のいずれか1項に記載の情報処理装置。前記事前条件生成手段は、前記トラップ挿入手段が1つのトラップを挿入する度に全パス情報を確認して事前条件を生成することを特徴とする請求項1乃至4のいずれか1項に記載の情報処理装置。前記事前条件生成手段は、前記トラップ挿入手段が全てのトラップを挿入した後に全パス情報を確認して事前条件を生成することを特徴とする請求項1乃至4のいずれか1項に記載の情報処理装置。前記検証対象プログラムがC言語で記述されている場合、前記トラップ挿入手段は、挿入するトラップとして、C言語のassertマクロを用いたassertを挿入することを特徴することを特徴とする請求項1乃至6のいずれか1項に記載の情報処理装置。前記ソフトウェアモデル検査手段は、前記assertに設定された表明式が満たされるか否かを調べ、表明式が偽になることがあれば、反例のパス情報を出力することを特徴とする請求項7に記載の情報処理装置。検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入ステップと、前記トラップ挿入ステップによってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査ステップと、前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成ステップと、を備えたことを特徴とする情報処理方法。検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入ステップと、前記トラップ挿入ステップによってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査ステップと、前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成ステップと、をコンピュータに実行させることを特徴とする情報処理プログラム。しかしながら、上記従来技術では、プログラムのテストにおいて、1組のテスト入力によって検査できるのは1実行パスのみである。カバレッジを上げるためには、別のテスト入力を与える必要があるが、場合によってはカバレッジが増えないことがある。たとえば、入力変数xに関して、if文Aelse文Bはxが0以上の場合に文Aを実行し、0未満の場合に文Bを実行することを表す。命令カバレッジ基準では、テスト入力のセット全体に対して、if文と文Aと文Bが実行されれば、カバレッジは100である。ここで、xが0というテスト入力を与えると文Aが実行されるが、文Bは実行されない。さらに、xが1というテスト入力を与えても、やはり文Bは実行されず、カバレッジは増えない。文Bを実行するにはxが1といった0未満のテスト入力を与える必要がある。構造の観点からのカバレッジを向上させるには、プログラムの構造を反映したテスト入力を与える必要がある。一方、データの観点からカバレッジを考えるためには、出力データのとり得る値の範囲と、それに対応した入力変数がとり得る値の範囲とを知る必要がある。たとえば、ifrx1elserx1というコード断片では、出力変数rが1未満となるような入力変数xは0未満であり、出力変数rが1以上となるような入力変数xは0以上である。しかし、設計においてプログラムの入力についての仕様が予め与えられている場合を除き、入力変数のとり得る値の範囲は自明ではない。特許文献1では、モデル検査の反例からテスト生成を行うことが記されているが、反例から得られるテスト入力は、ある1つのパスを実行するためのピンポイントの値の組であり、そこから入力変数の値の範囲を知ることはできない。本発明の目的は、上述の課題を解決する技術を提供することにある。上記目的を達成するため、本発明に係る装置は、検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入手段と、前記トラップ挿入手段によってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査手段と、前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成手段と、を備えたことを特徴とする。上記目的を達成するため、本発明に係る方法は、検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入ステップと、前記トラップ挿入ステップによってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査ステップと、前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成ステップと、を備えたことを特徴とする。上記目的を達成するため、本発明に係るプログラムは、検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入ステップと、前記トラップ挿入ステップによってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査ステップと、前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成ステップと、をコンピュータに実行させることを特徴とする。本発明によれば、プログラムについて、構造の観点からのカバレッジ基準をみたすパス情報を効果的に生成することができる。以下に、図面を参照して、本発明の実施の形態について例示的に詳しく説明する。ただし、以下の実施の形態に記載されている構成要素はあくまで例示であり、本発明の技術範囲をそれらのみに限定する趣旨のものではない。第1実施形態本発明の第1実施形態としての情報処理装置100について、図1を用いて説明する。情報処理装置100は、プログラムを静的に解析してプログラムの事前条件を生成する装置である。図1に示すように、情報処理装置100は、トラップ挿入部101とソフトウェアモデル検査部102と事前条件生成部103とを含む。トラップ挿入部101は、検証対象プログラムをカバレッジ基準に応じて整形してトラップを挿入する。ソフトウェアモデル検査部102は、トラップ挿入部101によってトラップを挿入されたトラップ入りプログラムに関してソフトウェアモデル検査を行い、カバレッジを満たすパス情報を出力する。さらに、事前条件生成部103は、パス情報からカバレッジを満たす事前条件を生成する。検証対象プログラムについて、構造の観点からのカバレッジ基準をみたすパス情報を効果的に生成することができる。第2実施形態次に本発明の第2実施形態に係るプログラム検証用事前条件生成装置200について、図2乃至図9を用いて説明する。《装置構成》図2は、本実施形態としてのプログラム検証用事前条件生成装置200の概略構成を示す図である。プログラム検証用事前条件生成装置200は、情報処理部201とファイル格納部202とを含む。情報処理部201は、トラップ挿入モジュール211とソフトウェアモデル検査モジュール213と事前条件生成モジュール215とを含む。ここで、検証対象プログラムはC言語で記述されているものとする。トラップ挿入モジュール211は、ファイル格納部から検証対象プログラムを読み込み、構造上のカバレッジ基準に対応して、トラップの挿入箇所が実行カバーされたか否かを調べるためのトラップを挿入し、トラップ入りプログラムを作成する。ここで、本実施形態に係るトラップは、プログラムを静的に解析するソフトウェアモデル検査モジュール213に、特定のカバレッジを持つパス情報を算出するようにヒントを与えるものであり、プログラムのテスト実行とは関係がない。トラップを用いて得られたパス情報からはテスト入力や事前条件を生成することができる。一方、ソフトウェアモデル検査モジュール213は、トラップ挿入箇所が実行されないことを調べたい性質として、トラップ入りプログラムを静的に検査し、トラップ挿入箇所が実行されることを示す反例のパス情報を出力する。事前条件生成モジュール215は、パス情報をトラップ挿入箇所からプログラムの開始箇所へと逆向きにたどり、プログラムの開始箇所が満たす事前条件、すなわちトラップ挿入箇所を実行するような事前条件を生成して、出力する。このソフトウェアモデル検査は、個々のモジュール内に含まれる命令や条件分岐等の通過率を計測するようなテストカバレッジで十分性を判断する、ソフトウェア単体テストといった下位レベルのテストに関する。《全体の処理の流れ》次に、図3のフローチャートを参照してプログラム検証用事前条件生成装置200が行なう動作全体について詳細に説明する。情報処理部201は、利用者から検証対象プログラムの指定を受け付け、他のモジュールに図3で示す一連の処理を実行させる。まず、トラップ挿入モジュール211は、ファイル格納部202から検証対象プログラムを読み込み、構造の観点でのカバレッジ基準に応じて、プログラム中の分岐文や繰り返し文をある定まった形式に整形するS301。さらに、トラップ挿入モジュール211は、整形されたプログラムにおいて、まだトラップを挿入されていないトラップ挿入対象箇所があるか否かを調べるS302。トラップ挿入対象箇所がある場合には、トラップ挿入対象箇所を1つ選び、挿入箇所が実行されたことを示すトラップを挿入して、トラップ入りプログラムを作成するS303。トラップ挿入対象箇所がなくなった場合には、ステップS304に進む。ステップS304において、ソフトウェアモデル検査モジュール213は、トラップ挿入箇所が実行されないことを調べたい性質として、トラップ入りプログラムを静的に検査し、トラップ挿入箇所が実行されることを示す反例のパス情報を出力する。ステップS305で、事前条件生成モジュール215は、まだ事前条件を生成していないパス情報があるか否かを調べる。まだ事前条件を生成していないパス情報がある場合には、ステップS306に進み、パス情報を1つ選び、トラップ挿入箇所からプログラムの開始ステップへと逆向きにたどる。そして、プログラムの開始ステップが満たす事前条件、すなわちトラップ挿入箇所を実行するような事前条件を生成して、出力する。事前条件を生成していないパス情報が無くなれば、処理を終了する。なお、上記フローチャートでは、全てのトラップを挿入してから事前条件を生成している。しかし本発明はこれに限定されるものではなく、1つのトラップを挿入する度に全パス情報を確認して事前条件を生成してもよい。つまり、ステップS303からステップS304に進んで、トラップ挿入箇所が無くなるまでステップS302~S306の処理を繰り返しても良い。図4を用いて、事前条件を算出する処理S306を詳しく説明する。まず、パス情報においてトラップ挿入箇所を処理対象のステップとし、事前条件を真とするS401。処理対象を1つ前のステップに変更しS402、処理対象のステップがプログラム開始ステップか否かを調べるS403。プログラム開始ステップであれば事前条件生成の処理を終了する。開始ステップでなければ、処理対象ステップが分岐の条件であるか、代入であるかを調べるS404。処理対象ステップが分岐の条件であれば、事前条件と処理対象ステップの条件との論理積を新たな事前条件としS405、ステップS402へ戻る。一方、ステップS404で、処理対象ステップが代入を行なうステップと判断すれば、事前条件に代入の左辺と同じ変数があれば代入の右辺と置換して新たな事前条件としS406、ステップS402へ戻る。《トラップ挿入例》図5~図8を用いて、トラップ挿入の具体例について説明する。図5は、命令カバレッジ基準に関するトラップを挿入する例であり、検証対象プログラム501における条件文行1を整形して、条件式を一時変数dに代入する文行1aと一時変数を用いた条件文行1bとを有する整形プログラム502を生成する。命令カバレッジは、各命令が少なくとも1回実行されたことを確認すればよいので、各代入文行1a、行2の直後をトラップ挿入対象箇所として、トラップ入りプログラム503、504を作成する。図5の例では、挿入トラップとして、C言語のassertマクロを用いたassertを挿入している。assertマクロを検査できるソフトウェアモデル検査手段は、assertに設定された表明式が満たされるか否かを調べ、表明式が偽になることがあれば、反例のパス情報を出力する。図5の例では、表明式として0すなわちC言語における恒偽を設定しているため、このトラップに到達し得るパスが存在すれば、ソフトウェアモデル検査モジュール213は反例のパス情報を出力する。図6は、分岐カバレッジ基準に関するトラップを挿入する具体例を示す図である。検証対象プログラム601を整形して整形プログラム602を生成し、さらにそこからトラップ入りプログラム603、604を生成する。検証対象プログラム601における条件文行1を、条件全体が真であれば行1a一時変数dに真を代入する文と、条件全体が偽であれば行1c一時変数dに偽を代入する文と、一時変数dを用いた条件文行1fとに整形する。分岐カバレッジは、各条件文において、条件全体が真をとる場合と偽をとる場合とが少なくとも1回実行されたことを確認すればよいので、一時変数dへの代入行1b1cの直後をトラップ挿入箇所として、トラップ入りプログラム603、604を作成する。図7は、MCDCModifiedconditiondecisioncoverage基準に関するトラップを挿入する具体例であり、検証対象プログラム701を整形して整形プログラム702を生成し、さらにそこからトラップ入りプログラム703~705を生成する。ここでは検証対象プログラム701の条件文行1における条件全体0<x0<yを論理演算子を含まない基本条件0<xと0<yとに分けて考える。検証対象プログラム701における条件文行1を整形して、0<xが真行1aかつ0<yが真行1bであれば一時変数dに真を代入する行1c文とする。また、条件文行1を整形して、0<xが真行1aかつ0<yが偽行1dであれば一時変数dに偽を代入し行1e、0<xが偽行1gであれば一時変数dに偽を代入行1hする文を生成する。MCDC分岐カバレッジでは、他の基本条件を真か偽に固定した場合に、ある基本条件が条件全体の真偽を決定するような基本条件の組合せについて、組合せの数が最小になり、かつ各組合せが少なくとも1回実行されたことを確認する。そのため、一時変数dへの代入行1c1e1hの直後をトラップ挿入箇所として、トラップ入りプログラム703~705を作成する。プログラムには二分岐以外の構造もあるが、これらは、二分岐を用いた入力出力副作用に影響を与えない等価な構造に整形することにより、図5~7で例示したトラップ挿入を行うことができる。図8は、C言語において、繰返し構造を表すforブロック801、whileブロック802、doブロック803、及び多分岐構造を表すswitchブロック804を、while文による繰返しとif文による二分岐からなる等価な構造805~808に整形する例を示す。《事前条件生成例》図9は、事前条件の生成処理の具体例を説明するための図である。図9の例では、トラップ入りプログラム901の13x行にトラップassertが挿入されている。ソフトウェアモデル検査モジュール213が出力したパス情報902には、変数の値の遷移が記録されている。変数値は、変数がカッコ内の値を持つことを示す。条件式と代入式の左辺の値は式の評価後の値であり、代入式の右辺の値は式の評価前の値である。パス情報902として、プログラムの開始箇所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行目に達する。事前条件903は、パス情報を終了箇所から開始箇所へと逆に辿って計算する。終了箇所での事前条件を真として、1つ前のステップを処理対象とし対象ステップの条件式y-10<xと事前条件真との論理積y-10<xを新たな事前条件とする。次に、1つ前のステップを処理対象として、対象ステップの代入式xx-10に基づき、事前条件のxをx10に置き換えた条件y<xを新たな事前条件とする。さらに1つ前のステップを処理対象として、対象ステップの条件式0<xと事前条件y<xとの論理積0<xy<xを新たな事前条件とする。1つ前のステップを処理対象として、対象ステップがプログラムの開始箇所なので計算を終える。これにより、トラップ13x行に達するためのプログラムの事前条件は0<xy<xとなる。なお、図5~8にはプログラムのソースコードを整形する例を示したが、プログラムの制御フローを整形してもよい。本実施形態では、パス情報から入力変数のとり得る値の範囲を示す事前条件を生成する。事前条件を満たす入力変数の値を用いることにより、データの観点からのカバレッジを増やすようなテスト入力を人手で作ることができ、また自動生成することもできる。特にソフトウェアモデル検査モジュールによって生成されたパス情報から、入力変数が満たすべき条件事前条件を自動で生成する。第3実施形態次に本発明の第3実施形態に係るプログラム検証用テスト入力生成装置について、図10及び図11を用いて説明する。図10は、本実施形態としてのプログラム検証用テスト入力生成装置1000の概略構成を示す図である。図2のプログラム検証用事前条件生成装置200と比べると、テスト入力生成モジュール1017が追加されている点が異なる。その他の構成及び動作は、第2実施形態と同様であるため、同じ構成及び動作については同じ符号を付してその詳しい説明を省略する。図11は、入力変数のとり得る値の範囲の境界をテストする場合に、テスト入力生成モジュール1017が行う処理の流れを示すフローチャートである。まず、テスト入力生成モジュール1017は、事前条件生成モジュール215が生成した事前条件について、テスト入力をまだ生成していない事前条件があるか否かを調べS1101、なければ処理の流れ全体を終了する。あれば、以下以上の比較演算子を用いた条件式を未満等号超過の比較演算子を用いた条件式の論理和に変換するS1102。次に、テスト入力生成モジュール1017は論理和で区切られた各条件式について、テスト入力をまだ生成していない事前条件があるか否かを調べS1103、なければステップS1101に戻る。あれば、制約充足アルゴリズムなどを用いて条件式を満たすような入力変数への値の割当を計算するS1104。図12は、テスト入力の生成例を示す図である。図12では、事前条件12010<xy<xを0xyx0xy<x0<xyx0<xy<xに変換する。条件式1202に含まれる0xyxと0xy<xと0<xyxと0<xy<xの各々について、入力変数xyの組、、、を見つける。これらがテスト入力1203の一部となる。事前条件に含まれない入力変数について固定値やランダムに生成した値などを割り当てることにより、1つのテスト入力の全体を得ることができる。本実施形態によれば、プログラムの単体テストに関して、プログラムを静的かつ網羅的に調べるソフトウェアモデル検査技術を用いて、プログラム構造の観点からのカバレッジ基準を満たすようなパス情報を得る。さらにパス情報からカバレッジ基準を満たすような事前条件を生成することにより、人手でのテスト入力の作成を容易にする、あるいはテスト入力の自動生成を行うことができる。他の実施形態以上、本発明の実施形態について詳述したが、それぞれの実施形態に含まれる別々の特徴を如何様に組み合わせたシステム又は装置も、本発明の範疇に含まれる。また、本発明は、複数の機器から構成されるシステムに適用されても良いし、単体の装置に適用されても良い。さらに、本発明は、実施形態の機能を実現する情報処理プログラムが、システムあるいは装置に直接あるいは遠隔から供給される場合にも適用可能である。したがって、本発明の機能をコンピュータで実現するために、コンピュータにインストールされるプログラム、あるいはそのプログラムを格納した媒体、そのプログラムをダウンロードさせるWWWサーバも、本発明の範疇に含まれる。本発明に係る情報処理プログラムを実行するコンピュータの構成例を図13に示す。コンピュータ1300は、CPU1301、ROM1302、通信制御部1303、RAM1304、及びストレージ1305を備えている。CPU1301は中央処理部であって、様々なプログラムを実行することによりコンピュータ1300全体を制御する。ROM1302は、不揮発メモリであり、CPU1301が最初に実行すべきブートプログラムの他、各種のパラメータ等を記憶している。また、RAM1304は、ランダムアクセスメモリであり、トラップ挿入モジュール211等のアプリケーションの実行領域1341及びアプリケーションが扱うデータ例えば、対象プログラム、スタブプログラム、テスト用プログラム、ドライバプログラム、パス情報などの記憶領域1342を有している。一方、ストレージ1305は、各種モジュール1351と、各種ファイル対象プログラムなどを保存する装置である。また、通信制御部1303は、他の端末とのネットワークを介した通信を制御する。[実施形態の他の表現]上記の実施形態の一部又は全部は、以下の付記のようにも記載されうるが、以下には限られない。付記1検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入手段と、前記トラップ挿入手段によってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査手段と、前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成手段と、を備えたことを特徴とする情報処理装置。付記2前記トラップ挿入手段は、プログラムの構造上のカバレッジ基準として、命令カバレッジ、分岐カバレッジ、MCDCの少なくともいずれか1つのカバレッジに対応して、検証対象プログラムを整形しトラップを挿入することを特徴とする付記1に記載の情報処理装置。付記3前記トラップ挿入手段は、プログラムの構造上のカバレッジ基準として、命令カバレッジ、分岐カバレッジ、MCDCの全てのカバレッジに対応すべく検証対象プログラムを整形し、トラップを挿入することを特徴とする付記1に記載の情報処理装置。付記4前記事前条件を整形して、テスト入力を生成するテスト入力生成手段をさらに備えたことを特徴とする付記1乃至3のいずれか1項に記載の情報処理装置。付記5前記事前条件生成手段は、前記トラップ挿入手段が1つのトラップを挿入する度に全パス情報を確認して事前条件を生成することを特徴とする付記1乃至4のいずれか1項に記載の情報処理装置。付記6前記事前条件生成手段は、前記トラップ挿入手段が全てのトラップを挿入した後に全パス情報を確認して事前条件を生成することを特徴とする付記1乃至4のいずれか1項に記載の情報処理装置。付記7前記検証対象プログラムがC言語で記述されている場合、前記トラップ挿入手段は、挿入するトラップとして、C言語のassertマクロを用いたassertを挿入することを特徴することを特徴とする付記1乃至6のいずれか1項に記載の情報処理装置。付記8前記ソフトウェアモデル検査手段は、前記assertに設定された表明式が満たされるか否かを調べ、表明式が偽になることがあれば、反例のパス情報を出力することを特徴とする付記7に記載の情報処理装置。付記9検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入ステップと、前記トラップ挿入ステップによってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査ステップと、前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成ステップと、を備えたことを特徴とする情報処理方法。付記10検証対象プログラムをカバレッジ基準に応じて整形しトラップを挿入するトラップ挿入ステップと、前記トラップ挿入ステップによってトラップを挿入されたトラップ入りプログラムについてソフトウェアモデル検査を行い、前記カバレッジ基準を満たすパス情報を出力するソフトウェアモデル検査ステップと、前記パス情報から前記カバレッジ基準を満たす事前条件を生成する事前条件生成ステップと、をコンピュータに実行させることを特徴とする情報処理プログラム。