"プログラムの仕様条件を変数を用いて表した複数の第1のコードが記憶された記憶部を参照して前記第1のコードを取得し、前記プログラムを入力とするシンボリック実行により抽出された、前記プログラムが実行し得るパス各々に対応する実装条件を変数を用いて表した複数の第2のコードが記憶された記憶部を参照して前記第2のコードを取得し、前記第1のコード各々と前記第2のコード各々と、を組み合わせて、前記仕様条件と前記実装条件との組み合わせ条件を表す複数の第3のコードを生成し、前記各第3のコードに基づき当該第3のコードに含まれる前記変数の充足解を求め、前記充足解を、前記プログラムのテストデータを記憶する記憶部に記憶する、処理をコンピュータに実行させるテストデータ生成プログラム。コンピュータによって実行されるテストデータ生成方法であって、プログラムの仕様条件を変数を用いて表した複数の第1のコードが記憶された記憶部を参照して前記第1のコードを取得し、前記プログラムを入力とするシンボリック実行により抽出された、前記プログラムが実行し得るパス各々に対応する実装条件を変数を用いて表した複数の第2のコードが記憶された記憶部を参照して前記第2のコードを取得し、前記第1のコード各々と前記第2のコード各々と、を組み合わせて、前記仕様条件と前記実装条件との組み合わせ条件を表す複数の第3のコードを生成し、前記各第3のコードに基づき当該第3のコードに含まれる前記変数の充足解を求め、前記充足解を、前記プログラムのテストデータを記憶する記憶部に記憶する、ことを特徴とするテストデータ生成方法。プログラムの仕様条件を変数を用いて表した複数の第1のコードが記憶された記憶部を参照して前記第1のコードを取得し、前記プログラムを入力とするシンボリック実行により抽出された、前記プログラムが実行し得るパス各々に対応する実装条件を変数を用いて表した複数の第2のコードが記憶された記憶部を参照して前記第2のコードを取得し、前記第1のコード各々と前記第2のコード各々と、を組み合わせて、前記仕様条件と前記実装条件との組み合わせ条件を表す複数の第3のコードを生成し、前記第3のコードに含まれる前記変数の充足解を充足値生成部から取得し、前記充足解を、前記プログラムのテストデータを記憶する記憶部に記憶する生成部と、前記各第3のコードに基づき当該第3のコードに含まれる前記変数の充足解を求める前記充足値生成部と、を備えることを特徴とするプログラム検査装置。本発明は、仕様と異なる誤りを有するプログラムを用いて該プログラムのテストを行う場合であっても、必要十分なテストデータを生成するテストデータ生成プログラム、テストデータ生成方法、テストデータ生成装置を提供することを目的とする。実施の態様のひとつであるコンピュータに実行させるテストデータ生成プログラムは、次の処理を実行する。プログラムの仕様条件を変数を用いて表した複数の第1のコードが記憶された記憶部を参照して上記第1のコードを取得する。上記プログラムを入力とするシンボリック実行により抽出された、上記プログラムが実行し得るパス各々に対応する実装条件を変数を用いて表した複数の第2のコードが記憶された記憶部を参照して上記第2のコードを取得する。上記第1のコード各々と上記第2のコード各々と、を組み合わせて、上記仕様条件と上記実装条件との組み合わせ条件を表す複数の第3のコードを生成する。上記各第3のコードに基づき当該第3のコードに含まれる上記変数の充足解を求める。上記充足解を、上記プログラムのテストデータを記憶する記憶部に記憶する。実施の態様によれば、仕様と異なる誤りを有するプログラムを用いて該プログラムのテストを行う場合であっても、必要十分なテストデータを生成できるという効果を奏する。実施の態様に示すテストデータを生成する方法は、プログラムの仕様条件を変数を用いて表した複数の第1のコードが記憶された記憶部を参照して上記第1のコードを取得する。また、プログラムを入力とするシンボリック実行により抽出された、上記プログラムが実行し得るパス各々に対応する実装条件を変数を用いて表した複数の第2のコードが記憶された記憶部を参照して上記第2のコードを取得する。そして、第1のコード各々と第2のコード各々と、を組み合わせて、仕様条件と実装条件との組み合わせ条件を表す複数の第3のコードを生成する。次に、各第3のコードに基づき当該第3のコードに含まれる変数の充足解を求める。例えば、後述するSatisfiabilityModuloTheoriesSMTソルバなどを用いて解を求める。その後、充足解を、プログラムのテストデータを記憶する記憶部に記憶する。その結果、仕様と異なる誤りを有するプログラムを用いて該プログラムのテストを行う場合であっても、必要十分なテストデータを生成することができる。以下図面に基づいて、実施形態について詳細を説明する。テストデータ生成装置1について説明する。図1は、テストデータ生成装置のハードウェアの一実施例を示す図である。テストデータ生成装置1は、制御部2、記憶部3、記録媒体読取装置4、入出力インタフェース5入出力I/F、通信インタフェース6通信I/Fなどを備えている。また、上記各構成部はバス7によってそれぞれ接続されている。制御部2は、後述する抽出部201、生成部202、充足値生成部203などを有している。また、制御部2はCentralProcessingUnitCPU、マルチコアCPU、プログラマブルなデバイスFieldProgrammableGateArrayFPGA、ProgrammableLogicDevicePLDなどを用いることが考えられる。記憶部3は、後述する仕様条件情報、プログラム情報、実装条件情報、組合条件情報、テストデータなどを記憶している。記憶部3は、例えばReadOnlyMemoryROM、RandomAccessMemoryRAMなどのメモリやハードディスクなどが考えられる。なお、記憶部3にはパラメータ値、変数値などのデータを記録してもよいし、実行時のワークエリアとして用いてもよい。上記プログラム情報、実装条件情報、組合条件情報、テストデータなどは、データベースに記録されていてもよい。記録媒体読取装置4は、制御部3の制御に従って記録媒体8に対するデータのリード/ライトを制御する。そして、記録媒体8に記録媒体読取装置4の制御で書き込まれたデータを記録させたり、記録媒体8に記録されたデータを読み取らせたりする。また、着脱可能な記録媒体8は、コンピュータで読み取り可能なnontransitory非一時的な記録媒体として、磁気記録装置、光ディスク、光磁気記録媒体、半導体メモリなどがある。磁気記録装置には、ハードディスク装置HDDなどがある。光ディスクには、DigitalVersatileDiscDVD、DVD-RAM、CompactDiscReadOnlyMemoryCD-ROM、CD-R/RWReWritableなどがある。光磁気記録媒体には、MagnetoOpticaldiskMOなどがある。なお、記憶部3もnontransitory非一時的な記録媒体に含まれる。入出力インタフェース5には、入出力部9が接続され、利用者が入力した情報例えば、プログラムやモデル記述などのデータを受信し、バス7を介して制御部2または記憶部3などに送信する。また、制御部2からの命令に従ってディスプレイの画面上に出力情報プログラムのテスト結果などや操作情報などを表示する。入出力部9の入力装置は、例えば、キーボード、ポインティングデバイスマウスなど、タッチパネルなどが考えられる。なお、入出力部9の出力部であるディスプレイは、例えば、液晶ディスプレイなどが考えられる。また、出力部はCathodeRayTubeCRTディスプレイ、プリンタなどの出力装置であってもよい。通信インタフェース6は、LocalAreaNetworkLAN接続やインターネット接続や無線接続を行うためのインタフェースである。また、通信インタフェース6は必要に応じ、他のコンピュータとの間のLAN接続やインターネット接続や無線接続を行うためのインタフェースである。また、他の装置に接続され、外部装置からのデータの入出力を制御する。このようなハードウェア構成を有するコンピュータを用いることによって、後述する各種処理機能が実現される。その場合システムが有すべき機能の処理内容を記述したプログラムが提供される。そのプログラムをコンピュータで実行することにより、上記処理機能例えば、図3に示すフローがコンピュータ上で実現される。処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体8に記録しておくことができる。プログラムを流通させる場合には、例えば、そのプログラムが記録されたDVD、CD-ROMなどの記録媒体8が販売される。また、プログラムをサーバコンピュータの記憶装置に記録しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。プログラムを実行するコンピュータは、例えば、記録媒体8に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを、自己の記憶部3に記録する。そして、コンピュータは、自己の記憶部3からプログラムを読み取り、プログラムに従った処理を実行する。なお、コンピュータは、記録媒体8から直接プログラムを読み取り、そのプログラムに従った処理を実行することもできる。また、コンピュータは、サーバコンピュータからプログラムが転送されるごとに、逐次、受け取ったプログラムに従った処理を実行することもできる。制御部2いついて説明する。図2は、テストデータ生成装置の制御部の一実施例を示す図である。制御部2は、抽出部201、生成部202、充足値生成部203を有する。抽出部201は、例えば、プログラムを入力としてシンボリック実行を行い、抽出されたパス各々で用いられている変数に対する条件実装条件を抽出する。シンボリック実行では、プログラムを、そのプログラムに含まれる変数に具体的な数値を入力する代わりに、数値を代表するシンボルでプログラムを模擬的に実行し、その結果を評価する。なお、抽出部201は、テストデータ生成装置と別に設けられていてもよい。すなわち、対象のプログラムを入力とし、別のコンピュータによりシンボリック実行を行って実装条件を求めてもよい。生成部202は、仕様に基づいて作成した仕様条件各々と、シンボリック実行を用いて抽出された実装条件各々とを組合条件を生成し、生成部202は充足値生成部203に生成した組合条件テストケース各々を送信する。また、生成部202は、充足値生成部203が求めた組合条件各々を充足する組合条件に含まれる変数の解を取得し、テストデータを生成する。充足値生成部203は、生成した組合条件が成り立つか否かを判定し、成り立つ場合には、組合条件が成り立つ変数の解を求めテストデータとし、組合条件に関連付けてテストデータを記憶部3の後述するテストデータ情報に記憶する。充足値生成部203は、例えば、SMTソルバを用いてテストデータを求めることが考えられる。SMTソルバは、論理式が矛盾していないことを示すために、論理式全体を真とするような各部分論理式の真偽時の組み合わせが存在するか否かを判定する。なお、SMTソルバは、整数、実数、配列などを扱うことができるという利点がある。SMTソルバに関しては、例えば、次の非特許文献を参照されたい。足立正和,他、充足可能性判定に基づくリアルタイムシステムのスケジューリング解析、組込みシステムシンポジウム2008、平成20年10月ArminBiereMarijnHeuleHansVanMaarenTobyWalshHandbookofSatisfiabilityIOSPress2009年2月REBryantDanielKroeningOferStrichmanDecisionProceduresAnAlgorithmicPointofViewSpringer2008年7月7日なお、抽出部201、生成部202、充足値生成部203各々の機能を、それぞれを異なるコンピュータに実装し、コンピュータ各々をネットワークにより接続してテストデータを生成してもよい。テストデータ生成装置の動作について説明する。図3は、テストデータ生成装置の動作の一実施例を示すフロー図である。ステップS1では、生成部202が仕様に基づいてモデル記述した仕様条件を示すコード第1のコードが記憶されている記憶部3の仕様条件情報を参照して、未処理の仕様条件を特定する。仕様条件情報は、例えば、図4に示す仕様条件情報401などが考えられる。図4は、仕様条件情報とプログラム情報と実装条件情報のデータ構造の一実施例を示す図である。仕様条件情報401は、No仕様条件処理済みなどの情報を有する。Noは仕様条件に関連付けられる識別子で、本例では、識別子123などが記憶されている。仕様条件には、仕様条件が識別子123に関連付けて記憶されている。本例では、仕様に1入力データである変数aが0以下ならばエラーを表示すること、2変数aが0より大きく10より小さいとき変数aを10倍して表示すること、3変数aが10以上ならばエラーを表示すること、が記載されている。そして、この記載に対してモデル記述した仕様条件を示すコードが、Noに関連付けられて記憶されている。図4の例では、a<=0は1の仕様に対応する仕様条件であり、0<aa<10は2の仕様に対応する仕様条件であり、a>=10は3の仕様に対応する仕様条件である。処理済みには、現在選択されている仕様条件を示すコードに対して後述する実装条件と組み合わせた例えば、論理積で結合した条件を生成したか否かを示す情報が記憶されている。本例では、210が記載されており、現在選択されている仕様条件に対して全ての実装条件と組合条件に対してステップS3の処理が実施されていれば、識別子2が記憶される。現在選択されている仕様条件に対してまだ組み合わされていない実装条件がまだある場合、識別子1が記憶される。まだ選択されていない仕様条件に対しては識別子0が記憶される。すなわち、ステップS1では仕様条件情報401の処理済みを参照し、処理済みに1または0が記載されている仕様条件を選択する。図4の仕様条件情報401の場合であれば、Noの2に関連する処理済みが1の状態の仕様条件を選択する。ステップS2では、生成部202が現在選択されている仕様条件に対して未処理の実装条件を示すコード第2のコードを特定する。実装条件について説明する。実装条件を示すコードは、例えば、抽出部201が図4のプログラム情報402を記憶部3から取得して、プログラム情報402に対してシンボリック実行を行って得られるコードである。本例では、プログラム情報402に対してシンボリック実行を行って得られる条件として、図4に示す実装条件情報403が得られる。プログラム情報402は、上記仕様1~3に基づいて作成したプログラムであり、2行目と4行目に誤りがある。本来、仕様に基づいてプログラムを作成すると2行目の記載は、if0<aa<4{でなければならない。また、4行目の記載は、}elseif4<=aa<10{でなければならない。実装条件情報403には、プログラム情報402に対してシンボリック実行を行った結果である実装条件が記憶され、No実装条件処理済みなどの情報が記憶されている。Noは実装条件に関連付けられる識別子で、本例では、識別子12345などが記憶されている。実装条件には対象のプログラムに対してシンボリック実行を行った結果である実装条件が、識別子12345に関連付けて記憶されている。本例では、シンボリック実行をした結果としてnot0100anot4anotが記憶されている。例えば、組合条件情報501の識別子1に関連付けられてa0notを生成する場合、ステップS1で仕様条件情報401の最初のNo1に対応する仕様条件a0が選択される。ステップS2で実装条件情報403の最初のNo1に対応する実装条件notが選択され、で結合される。このとき、仕様条件情報401の最初のNo1に対応する処理済みを0から1にし、実装条件情報403の最初のNo1に対応する処理済みは0から1にする。次に、組合条件情報501の識別子2に関連付けられてa00aa4を生成する場合、ステップS1で仕様条件情報401の最初のNo1に対応する仕様条件a0が選択されたまま、ステップS2で実装条件情報403の未処理のNo2に対応する実装条件0aa4が選択され、で結合される。このとき、仕様条件情報401の最初のNo1に対応する処理済みは1のままで、実装条件情報403のNo2に対応する処理済みは0から1になる。続いて、仕様条件a0において、実装条件情報403のNo3~4に関連する実装条件を用いた処理が終了すると、実装条件情報403のNo5に関連する実装条件0anot4anotが選択される。すなわち、ステップS1で仕様条件情報401のNo1に対応する仕様条件a0が選択されたまま、ステップS2で実装条件情報403の最後の未処理のNo5に対応する実装条件が選択され、で結合される。このとき、仕様条件情報401のNo1に対応する処理済みは1から2になり、実装条件情報403のNo5に対応する処理済みは0から1になる。続いて、仕様条件情報401のNo1の処理が終了仕様条件情報401のNo1の処理済みが2し、仕様条件情報401のNo2がステップS1で選択される処理済みが1。このとき、実装条件情報403のNo1~5に対応する処理済みはすべて0にする。続いて、仕様条件情報401のNo2~3に対応する仕様条件各々について、実装条件情報403のNo1~5に関連する実装条件各々と組み合わせて、組合条件情報501に示す組合条件を生成する。仕様条件情報401のNo3が選択され、実装条件情報403のNo5が選択されているとき全て組み合わされたとき、仕様条件情報401の処理済みはすべて2になり、実装条件情報403の処理済みはすべて2にる。なお、本例では組合条件を記憶部3に記憶しているが、組合条件は組合条件情報に記憶しなくてもよい。ステップS4では、充足値生成部203が組合条件を生成部202から取得し、組合条件に対してSMTソルバを用いて条件を同時に充足する解を求め、求めた解を生成部202に送信する。ステップS5では、生成部202が充足値生成部203から求めた解を受信し、解が存在するか否かを判定し、解が存在する場合にはステップS6Yesに移行し、解が存在しない場合にはステップS7Noに移行する。例えば、ステップS4で仕様条件情報401のNo2の仕様条件を示すコードと、実装条件情報403のNo3の仕様条件を示すコードと、をで結合した組合条件を示すコードを用いて、変数aに対して充足する解を求める。その場合、SMTソルバの実行結果としてa=4を得られる。すなわち、変数aが仕様条件情報401のNo2の仕様条件を満たすにも関わらず、実装条件情報403のNo3の実装条件では、エラー表示に到達するパスが存在することになる。つまり、仕様と異なる記載がプログラムにあるような場合でも、誤りを検出することが可能な組合条件テストケースを漏れなく抽出することができる。また、ステップS4で仕様条件情報401のNo3の仕様条件を示すコードと、実装条件情報403のNo1の仕様条件を示すコードと、をで結合した組合条件を示すコードを用いて、変数aに対して充足する解を求める。しかし、SMTソルバの実行結果として解を得ることができない。すなわち、仕様条件情報401のNo3の仕様条件を満たすにも関わらず、実装条件情報403のNo1の仕様条件を満たすようなパスはありえないことがわかる。続いて、ステップS5で判定をした組合条件について、解がある場合にはステップS6で、生成部202は解をテストデータとして記憶部3に記憶する。図6は、組合条件に対してSMTソルバにより求められる解の一実施例を示す図である。組合条件情報501において、解が存在するのはNo12、7~9、15に対応する組合条件である。そして、No1の解は-1、2の解は0、7の解は1、8の解は4、9の解は5、15の解は10であるので、テストデータをa=-1、0、1、4、5、10とする。続いて、生成部202は記憶部3にテストデータをa=-1、0、1、4、5、10を記憶する。ステップS7では、生成部202が現在選択されている仕様条件に対して未処理の実装条件が存在するか否かを判定し、未処理の実装条件が存在する場合にはステップS2Yesに移行し、未処理の実装条件がない場合にはステップS8Noに移行する。本例では、実装条件情報403の処理済みを参照して未処理の実装条件が存在するか否かを判定する。処理済みのいずれかに未処理を示す0が記憶されているときにはステップS2Yesに移行する。処理済みがすべて1である場合には、ステップS8Noに移行する。ステップS8では、生成部202が未処理の仕様条件が存在するか否かを判定し、未処理の仕様条件が存在する場合にはステップS1Yesに移行し、未処理の仕様条件がない場合には処理を終了Noする。本例では、仕様条件情報401の処理済みを参報して未処理の実装条件が存在するか否かを判定する。処理済みのいずれかに未処理を示す0または処理中であることを示す1が記憶されているときにはステップS1Yesに移行する。すべての処理済みが、処理が終了したことを示す2である場合には、ステップS8Noに移行する。図7は、仕様条件と実装条件とテストデータの関係を示す図である。仕様条件1仕様条件情報401のNo1に対応と実装条件1実装条件情報403のNo1に対応とは同時に満たされる範囲があり、その範囲のテストデータとして-1が求められている。次に、仕様条件1と実装条件2実装条件情報403のNo2に対応とは同時に満たされる範囲があり、その範囲のテストデータとして0が求められている。次に、仕様条件2仕様条件情報401のNo2に対応と実装条件2とは同時に満たされる範囲があり、その範囲のテストデータとして1が求められている。次に、仕様条件2と実装条件3実装条件情報403のNo3に対応とは同時に満たされる範囲があり、その範囲のテストデータとして4が求められている。次に、仕様条件2と実装条件4実装条件情報403のNo4に対応とは同時に満たされる範囲があり、その範囲のテストデータとして5が求められている。次に、仕様条件3仕様条件情報401のNo3に対応と実装条件5実装条件情報403のNo5に対応とは同時に満たされる範囲があり、その範囲のテストデータとして10が求められている。本実施の形態によれば、仕様と異なる誤りを有するプログラムを用いて該プログラムのテストを行う場合であっても、必要十分なテストデータを生成できる。なお、本実施の態様では、変数が1つの場合について説明したが、変数が複数ある場合でも必要十分なテストデータを生成できる。変数が複数の場合でも、仕様条件を示すコード各々と実装条件を示すコード各々とを組み合わせて組合条件を示すコードを作成する。その後、該組合条件を示すコード各々に対して、SMTソルバを用いて複数の変数を充足させる解を求め、求めた解を用いて必要十分なテストデータを生成できる。また、プログラムに誤りがあっても、仕様と異なる分岐条件if分などがある部分を検出できるテストケースが生成でき、その結果プログラムの分岐条件の確認に必要十分なテストデータが生成できる。また、仕様条件と実装条件とが同時に満たされるテストケースを求めているため、冗長なテストデータが生成されない。なお、実施の形態で説明したテスト対象のプログラムは、例えば、業務アプリケーションなどに用いられるプログラムなどが考えられる。また、本発明は、上記実施の形態に限定されるものでなく、本発明の要旨を逸脱しない範囲内で種々の改良、変更が可能である。"