(57)【特許請求の範囲】
【請求項１】
プログラムの仕様条件を変数を用いて表した複数の第１のコードが記憶された記憶部を参照して前記第１のコードを取得し、
前記プログラムを入力とするシンボリック実行により抽出された、前記プログラムが実行し得るパス各々に対応する実装条件を変数を用いて表した複数の第２のコードが記憶された記憶部を参照して前記第２のコードを取得し、
前記第１のコード各々と前記第２のコード各々と、を組み合わせて、前記仕様条件と前記実装条件との組み合わせ条件を表す複数の第３のコードを生成し、
前記各第３のコードに基づき当該第３のコードに含まれる前記変数の充足解を求め、
前記充足解を、前記プログラムのテストデータを記憶する記憶部に記憶する、
処理をコンピュータに実行させるテストデータ生成プログラム。
【請求項２】
コンピュータによって実行されるテストデータ生成方法であって、
プログラムの仕様条件を変数を用いて表した複数の第１のコードが記憶された記憶部を参照して前記第１のコードを取得し、
前記プログラムを入力とするシンボリック実行により抽出された、前記プログラムが実行し得るパス各々に対応する実装条件を変数を用いて表した複数の第２のコードが記憶された記憶部を参照して前記第２のコードを取得し、
前記第１のコード各々と前記第２のコード各々と、を組み合わせて、前記仕様条件と前記実装条件との組み合わせ条件を表す複数の第３のコードを生成し、
前記各第３のコードに基づき当該第３のコードに含まれる前記変数の充足解を求め、
前記充足解を、前記プログラムのテストデータを記憶する記憶部に記憶する、
ことを特徴とするテストデータ生成方法。
【請求項３】
プログラムの仕様条件を変数を用いて表した複数の第１のコードが記憶された記憶部を参照して前記第１のコードを取得し、前記プログラムを入力とするシンボリック実行により抽出された、前記プログラムが実行し得るパス各々に対応する実装条件を変数を用いて表した複数の第２のコードが記憶された記憶部を参照して前記第２のコードを取得し、前記第１のコード各々と前記第２のコード各々と、を組み合わせて、前記仕様条件と前記実装条件との組み合わせ条件を表す複数の第３のコードを生成し、前記第３のコードに含まれる前記変数の充足解を充足値生成部から取得し、前記充足解を、前記プログラムのテストデータを記憶する記憶部に記憶する生成部と、
前記各第３のコードに基づき当該第３のコードに含まれる前記変数の充足解を求める前記充足値生成部と、
を備えることを特徴とするプログラム検査装置。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、プログラムのテストに用いるデータを生成するテストデータプログラム、テストデータ生成方法、テストデータ生成装置に関する。
【背景技術】
【０００２】
従来、プログラムのテストを網羅的に行う方法として、仕様に基づいて作成したテストデータを用いてプログラムのテストを行う方法が知られている。例えば、１）〜３）に示す条件を有する仕様に基づいて、従来のテストで用いるテストデータの求め方について説明する。
【０００３】
仕様例
１）入力データａが０以下ならばエラーを表示
２）入力データａが０より大きく１０より小さいとき入力データａを１０倍して表示
３）入力データａが１０以上ならばエラーを表示
１）〜３）を有する仕様を用いて作成されたプログラム例とモデル記述（論理式で記述）した仕様例を示す。
【０００４】
プログラム例
1      public void method(int a){
2            if (0<=a && a<4){
3                  System.out.println(a*10);
4            } else if (4<a && a<10) {
5                  System.out.println(a*10);
6            } else {
7                  System.err.println(“error!”);
8            }
9      }
【０００５】
モデル記述した仕様例
1      a<=0 → error
2      0<a<10 → a*10
3      a>=10 → error
【０００６】
上記プログラム例はＪＡＶＡ（登録商標）などのプログラミング言語で記載されたプログラムの一部分のコードを示している。また、上記プログラム例のコード各々の先頭に示されている１〜９の数字は行数を表している。また、上記プログラムは誤って記載されている。本来、仕様に沿って作成した場合には２行目のｉｆ文に、入力データａが０より大きい場合（０＜ａ）が記載されるべきであるが、入力データａが０以下である場合（０＜＝ａ）について誤って記載されている。また、４行目のｉｆ文には、入力データａが４以上である場合（０＜ａ）が記載されるべきであるが、入力データａが４より小さい場合（４＜ａ）について誤って記載されている。
【０００７】
上記仕様例はモデル記述言語などで記載されたコードで、各行の先頭に示されている１〜３の数字は行数を示している。なお、仕様例のコード中の「→」は左辺の条件を満たしたならば右辺に示す処理を実行することを示している。「error」は出力装置にエラーであることを表示することを示す。「a*10」は出力装置に入力データａを１０倍した値を表示することを示している。
【０００８】
次に、本例では記述されたコードから境界値、値域の中間値や最小値または最大値を抽出する。１行目の条件には入力データａが０以下である場合（０＜＝ａ）、エラーを表示することが示されており、２行目の条件には入力データａが０より大きく１０より小さいとき入力データａを１０倍して表示することが示されている。また、３行目の条件には入力データａが１０以上ならばエラーを表示することが示されている。３つの条件によれば、０以下の値域、１〜９の値域、１０以上の値域が存在し、境界値として０、１、９、１０が存在する。また、０以下の値域では、最小値と中間値が定まらないが例えば−１００を最小値と中間値として用いることが考えられる。１〜９の値域では中間値として５が存在する。１０以上の値域では、中間値と最大値が定まらないが例えば１００を中間値と最大値として用いることが考えられる。次に、上記説明した境界値と、値域の中間値や最小値または最大値とを用いて、テストデータを生成する。
【０００９】
テストデータ例
a=-100, 0, 1, 5, 9, 10, 100
【００１０】
ところが、上記テストデータを用いて、プログラム例についてテストを実施すると、プログラムの誤りを検出することができない。上記説明したプログラム例の４行目の誤りを検出するためにはテストデータに４がなければならない。従って、仕様に基づいて求めた境界値と値域の中間値や最小値または最大値をテストデータとして用いたプログラムでは、仕様どおりにプログラムが作成されているか否かの判定をすることができないことがある。
【００１１】
一方、プログラムからプログラムが実行しうるパスを網羅的に抽出して、そのパスを実行するための条件からテストデータを生成する方法が知られている。例えば、シンボリック実行などの技術を用いて、プログラムを実行した場合に実行される全てのパスを抽出し、パス各々に関連する条件を満たすための変数の条件を抽出する方法が知られている。
【００１２】
なお、シンボリック実行については、基礎的な事項が、例えば、玉井哲雄、福永光一、「記号実行システム」、情報処理、pp18-28、１９８２年１月１５日などに詳しく述べられているので、そちらを参照されたい。
【００１３】
上記プログラム例に対してシンボリック実行を行う場合について説明する。シンボリック実行を行うと、条件を抽出するために、上記プログラム例の２行目と４行目に記載されているｉｆ文などの分岐条件を検出する。本例の場合であれば、検出したｉｆ文に含まれる変数ａの取り得る範囲を場合分けし、条件を示す式を求める。
【００１４】
条件例
1      not(0<=a)
2      0<=a & a<4
3      0<=a & not(a<4) & not(4<a)
4      0<=a & not(a<4) & 4<a & a<10
5      0<=a & not(a<4) & 4<a & not(a<10)
【００１５】
続いて、上記条件例を満たすテストデータを生成する。
条件を満たすテストデータ例
a=-1, 3, 4, 5, 10
【００１６】
条件例の１〜５行目の条件各々からは、テストデータとして１行目に対応するテストデータ−１、２行目に対応するテストデータ３、３行目に対応するテストデータ４、４行目に対応するテストデータ５、５行目に対応するテストデータ１０が生成されたとする。ところが、２行目に対応する条件からはテストデータとして０〜３の値のうち何れか１つが求められればよいため、本例では３がテストデータとして求められている。そのため、条件を満たすテストデータとして上記テストデータ例を用いてテストを行うと、プログラム例の２行目の誤りを検出できないことになる。プログラム例の２行目の誤りを検出するには、条件例の２行目から求めるテストデータとして０が求められなければならない。
【００１７】
さらに、シンボリック実行を用いてテストデータを抽出する場合、テスト対象のプログラムに仕様に対応する記載がない場合には、条件を抽出することすらできない。
また、仕様に基づいて作成したテストデータとシンボリック実行により抽出したテストデータを用いる方法がある。上記プログラム例の場合、テストデータ例と条件を満たすテストデータ例を合わせると、冗長なテストデータとなってしまうことがある。
【００１８】
冗長なテストデータ例
a=-100, -1, 0, 1, 3, 4, 5, 9, 10, 100
【００１９】
例えば、−１００と−１を用いるということは、同じパスを２回通ることとなり、冗長なテストデータが存在することになり、余計なテストをしていることになる。また、１と３、５と９についてもどちらか１つの値があればよいので、冗長なテストデータが存在していることになる。
【００２０】
なお、関連する技術として、自然言語の仕様とＣ言語のプログラムとGraphical User Interface（ＧＵＩ）ベースの制御ロジックとのクロス検証を行うことができ、結果的に当該開発の効率を高めることができるクロス検証が開示されている。このクロス検証によれば、動作仕様、エンジン制御用のＣコードおよびエンジン制御用のＧＵＩロジックを作成する。そして、作成した動作仕様、ＣコードおよびＧＵＩロジックに基づいてアサーションを生成し、生成したアサーションを当該Ｃコードおよび当該ＧＵＩロジックに挿入する。その後、生成したアサーション、アサーションが挿入された後のＣコードおよびアサーションが挿入された後のＧＵＩロジックをConjnctive Normal Form（ＣＮＦ）へ変換する。そして、作成した動作仕様に基づいて、変換した後のＣコードおよびＧＵＩロジックのクロス検証を行い、その検証結果を表示する。
【００２１】
また、関連する技術として、ウェブアプリケーションを検証するためのシンボリック実行につて開示がされている。
また、関連する技術として、現実のシステムを反映する複雑な動作仕様や多様な事象を取り扱いつつ、規模を抑えたシステム状態遷移系ならびにテストケースを生成する技術が開示されている。この技術によれば、システム動作仕様記述に基づいて遷移事象を順次生起させてシステム状態遷移系を生成する。その際に、遷移事象の順序制約を表現するシナリオ状態遷移系も同時に遷移させ、順次生起させる遷移事象を、当該シナリオ状態遷移系で遷移可能なものに制限する。
【００２２】
また、関連する技術として、計算機プログラムのソースコードが意味するプログラムの振る舞いに関する性質を検査するソースコード検査方法が開示されている。このソースコード検査方法では、計算機プログラムのソースコードにより記述されたプログラムを模擬的に実行して実際に実行される命令列を抽出し、抽出した命令列に基づいてソースコードの検査内容を決定する。
【先行技術文献】
【特許文献】
【００２３】
【特許文献１】特開２００８−２７６５５６号公報
【特許文献２】特開２００９−８７３５５号公報
【特許文献３】特開２０１０−２１１４８１号公報
【特許文献４】国際公開第２００６／０３８３９４号
【発明の概要】
【発明が解決しようとする課題】
【００２４】
本発明は、仕様と異なる誤りを有するプログラムを用いて該プログラムのテストを行う場合であっても、必要十分なテストデータを生成するテストデータ生成プログラム、テストデータ生成方法、テストデータ生成装置を提供することを目的とする。
【課題を解決するための手段】
【００２５】
実施の態様のひとつであるコンピュータに実行させるテストデータ生成プログラムは、次の処理を実行する。
プログラムの仕様条件を変数を用いて表した複数の第１のコードが記憶された記憶部を参照して上記第１のコードを取得する。
【００２６】
上記プログラムを入力とするシンボリック実行により抽出された、上記プログラムが実行し得るパス各々に対応する実装条件を変数を用いて表した複数の第２のコードが記憶された記憶部を参照して上記第２のコードを取得する。
【００２７】
上記第１のコード各々と上記第２のコード各々と、を組み合わせて、上記仕様条件と上記実装条件との組み合わせ条件を表す複数の第３のコードを生成する。
上記各第３のコードに基づき当該第３のコードに含まれる上記変数の充足解を求める。
上記充足解を、上記プログラムのテストデータを記憶する記憶部に記憶する。
【発明の効果】
【００２８】
実施の態様によれば、仕様と異なる誤りを有するプログラムを用いて該プログラムのテストを行う場合であっても、必要十分なテストデータを生成できるという効果を奏する。
【図面の簡単な説明】
【００２９】
【図１】テストデータ生成装置のハードウェアの一実施例を示す図である。
【図２】テストデータ生成装置の制御部の一実施例を示す図である。
【図３】テストデータ生成装置の動作の一実施例を示すフロー図である。
【図４】仕様条件情報とプログラム情報と実装条件情報の一実施例を示す図である。
【図５】組合条件情報のデータ構造の一実施例を示す図である。
【図６】組合条件に対してＳＭＴソルバにより求められる解の一実施例を示す図である。
【図７】仕様条件と実装条件とテストデータの関係を示す図である。
【発明を実施するための形態】
【００３０】
実施の態様に示すテストデータを生成する方法は、プログラムの仕様条件を変数を用いて表した複数の第１のコードが記憶された記憶部を参照して上記第１のコードを取得する。また、プログラムを入力とするシンボリック実行により抽出された、上記プログラムが実行し得るパス各々に対応する実装条件を変数を用いて表した複数の第２のコードが記憶された記憶部を参照して上記第２のコードを取得する。
【００３１】
そして、第１のコード各々と第２のコード各々と、を組み合わせて、仕様条件と実装条件との組み合わせ条件を表す複数の第３のコードを生成する。
【００３２】
次に、各第３のコードに基づき当該第３のコードに含まれる変数の充足解を求める。例えば、後述するSatisfiability Modulo Theories（ＳＭＴ）ソルバなどを用いて解を求める。その後、充足解を、プログラムのテストデータを記憶する記憶部に記憶する。
その結果、仕様と異なる誤りを有するプログラムを用いて該プログラムのテストを行う場合であっても、必要十分なテストデータを生成することができる。
【００３３】
以下図面に基づいて、実施形態について詳細を説明する。
テストデータ生成装置１について説明する。
図１は、テストデータ生成装置のハードウェアの一実施例を示す図である。テストデータ生成装置１は、制御部２、記憶部３、記録媒体読取装置４、入出力インタフェース５（入出力Ｉ／Ｆ）、通信インタフェース６（通信Ｉ／Ｆ）などを備えている。また、上記各構成部はバス７によってそれぞれ接続されている。
【００３４】
制御部２は、後述する抽出部２０１、生成部２０２、充足値生成部２０３などを有している。また、制御部２はCentral Processing Unit（ＣＰＵ）、マルチコアＣＰＵ、プログラマブルなデバイス（Field Programmable Gate Array（ＦＰＧＡ）、Programmable Logic Device（ＰＬＤ）など）を用いることが考えられる。
【００３５】
記憶部３は、後述する仕様条件情報、プログラム情報、実装条件情報、組合条件情報、テストデータなどを記憶している。記憶部３は、例えばRead Only Memory（ＲＯＭ）、Random Access Memory（ＲＡＭ）などのメモリやハードディスクなどが考えられる。なお、記憶部３にはパラメータ値、変数値などのデータを記録してもよいし、実行時のワークエリアとして用いてもよい。上記プログラム情報、実装条件情報、組合条件情報、テストデータなどは、データベースに記録されていてもよい。
【００３６】
記録媒体読取装置４は、制御部３の制御に従って記録媒体８に対するデータのリード／ライトを制御する。そして、記録媒体８に記録媒体読取装置４の制御で書き込まれたデータを記録させたり、記録媒体８に記録されたデータを読み取らせたりする。また、着脱可能な記録媒体８は、コンピュータで読み取り可能なnon-transitory（非一時的）な記録媒体として、磁気記録装置、光ディスク、光磁気記録媒体、半導体メモリなどがある。磁気記録装置には、ハードディスク装置（ＨＤＤ）などがある。光ディスクには、Digital Versatile Disc（ＤＶＤ）、ＤＶＤ−ＲＡＭ、Compact Disc Read Only Memory（ＣＤ−ＲＯＭ）、ＣＤ−Ｒ(Recordable)／ＲＷ（ReWritable）などがある。光磁気記録媒体には、Magneto-Optical disk（ＭＯ）などがある。なお、記憶部３もnon-transitory（非一時的）な記録媒体に含まれる。
【００３７】
入出力インタフェース５には、入出力部９が接続され、利用者が入力した情報（例えば、プログラムやモデル記述などのデータ）を受信し、バス７を介して制御部２または記憶部３などに送信する。また、制御部２からの命令に従ってディスプレイの画面上に出力情報（プログラムのテスト結果など）や操作情報などを表示する。入出力部９の入力装置は、例えば、キーボード、ポインティングデバイス（マウスなど）、タッチパネルなどが考えられる。なお、入出力部９の出力部であるディスプレイは、例えば、液晶ディスプレイなどが考えられる。また、出力部はCathode Ray Tube（ＣＲＴ）ディスプレイ、プリンタなどの出力装置であってもよい。
【００３８】
通信インタフェース６は、Local Area Network（ＬＡＮ）接続やインターネット接続や無線接続を行うためのインタフェースである。また、通信インタフェース６は必要に応じ、他のコンピュータとの間のＬＡＮ接続やインターネット接続や無線接続を行うためのインタフェースである。また、他の装置に接続され、外部装置からのデータの入出力を制御する。
【００３９】
このようなハードウェア構成を有するコンピュータを用いることによって、後述する各種処理機能が実現される。その場合システムが有すべき機能の処理内容を記述したプログラムが提供される。そのプログラムをコンピュータで実行することにより、上記処理機能（例えば、図３に示すフロー）がコンピュータ上で実現される。処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体８に記録しておくことができる。
【００４０】
プログラムを流通させる場合には、例えば、そのプログラムが記録されたＤＶＤ、ＣＤ−ＲＯＭなどの記録媒体８が販売される。また、プログラムをサーバコンピュータの記憶装置に記録しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。
【００４１】
プログラムを実行するコンピュータは、例えば、記録媒体８に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを、自己の記憶部３に記録する。そして、コンピュータは、自己の記憶部３からプログラムを読み取り、プログラムに従った処理を実行する。なお、コンピュータは、記録媒体８から直接プログラムを読み取り、そのプログラムに従った処理を実行することもできる。また、コンピュータは、サーバコンピュータからプログラムが転送されるごとに、逐次、受け取ったプログラムに従った処理を実行することもできる。
【００４２】
制御部２いついて説明する。
図２は、テストデータ生成装置の制御部の一実施例を示す図である。制御部２は、抽出部２０１、生成部２０２、充足値生成部２０３を有する。
【００４３】
抽出部２０１は、例えば、プログラムを入力としてシンボリック実行を行い、抽出されたパス各々で用いられている変数に対する条件（実装条件）を抽出する。シンボリック実行では、プログラムを、そのプログラムに含まれる変数に具体的な数値を入力する代わりに、数値を代表するシンボルでプログラムを模擬的に実行し、その結果を評価する。なお、抽出部２０１は、テストデータ生成装置と別に設けられていてもよい。すなわち、対象のプログラムを入力とし、別のコンピュータによりシンボリック実行を行って実装条件を求めてもよい。
【００４４】
生成部２０２は、仕様に基づいて作成した仕様条件各々と、シンボリック実行を用いて抽出された実装条件各々とを組合条件を生成し、生成部２０２は充足値生成部２０３に生成した組合条件（テストケース）各々を送信する。また、生成部２０２は、充足値生成部２０３が求めた組合条件各々を充足する組合条件に含まれる変数の解を取得し、テストデータを生成する。
【００４５】
充足値生成部２０３は、生成した組合条件が成り立つか否かを判定し、成り立つ場合には、組合条件が成り立つ変数の解を求めテストデータとし、組合条件に関連付けてテストデータを記憶部３の後述するテストデータ情報に記憶する。充足値生成部２０３は、例えば、ＳＭＴソルバを用いてテストデータを求めることが考えられる。
【００４６】
ＳＭＴソルバは、論理式が矛盾していないことを示すために、論理式全体を真とするような各部分論理式の真偽時の組み合わせが存在するか否かを判定する。なお、ＳＭＴソルバは、整数、実数、配列などを扱うことができるという利点がある。ＳＭＴソルバに関しては、例えば、次の非特許文献を参照されたい。
・足立正和，他、「充足可能性判定に基づくリアルタイムシステムのスケジューリング解析」、組込みシステムシンポジウム２００８、平成２０年１０月
・Armin Biere, Marijn Heule, Hans Van Maaren, Toby Walsh, "Handbook of Satisfiability(Frontiers in Artificial Intelligence and Applications)",IOS Press, ２００９年２月
・R.E. Bryant, Daniel Kroening, Ofer Strichman, "Decision Procedures: An Algorithmic Point of View (Texts in Theoretical Computer Science. An EATCS Series)", Springer, ２００８年７月７日
【００４７】
なお、抽出部２０１、生成部２０２、充足値生成部２０３各々の機能を、それぞれを異なるコンピュータに実装し、コンピュータ各々をネットワークにより接続してテストデータを生成してもよい。
【００４８】
テストデータ生成装置の動作について説明する。
図３は、テストデータ生成装置の動作の一実施例を示すフロー図である。ステップＳ１では、生成部２０２が仕様に基づいてモデル記述した仕様条件を示すコード（第１のコード）が記憶されている記憶部３の仕様条件情報を参照して、未処理の仕様条件を特定する。仕様条件情報は、例えば、図４に示す仕様条件情報４０１などが考えられる。図４は、仕様条件情報とプログラム情報と実装条件情報のデータ構造の一実施例を示す図である。仕様条件情報４０１は、「Ｎｏ」「仕様条件」「処理済み」などの情報を有する。「Ｎｏ」は仕様条件に関連付けられる識別子で、本例では、識別子「１」「２」「３」などが記憶されている。「仕様条件」には、仕様条件が識別子「１」「２」「３」に関連付けて記憶されている。本例では、仕様に１）入力データである変数ａが０以下ならばエラーを表示すること、２）変数ａが０より大きく１０より小さいとき変数ａを１０倍して表示すること、３）変数ａが１０以上ならばエラーを表示すること、が記載されている。そして、この記載に対してモデル記述した仕様条件を示すコードが、「Ｎｏ」に関連付けられて記憶されている。図４の例では、「ａ＜＝０」は１）の仕様に対応する仕様条件であり、「０＜ａ＆ａ＜１０」は２）の仕様に対応する仕様条件であり、「ａ＞＝１０」は３）の仕様に対応する仕様条件である。「処理済み」には、現在選択されている仕様条件を示すコードに対して後述する実装条件と組み合わせた（例えば、論理積＆で結合した）条件を生成したか否かを示す情報が記憶されている。本例では、「２」「１」「０」が記載されており、現在選択されている仕様条件に対して全ての実装条件と組合条件に対してステップＳ３の処理が実施されていれば、識別子「２」が記憶される。現在選択されている仕様条件に対してまだ組み合わされていない実装条件がまだある場合、識別子「１」が記憶される。まだ選択されていない仕様条件に対しては識別子「０」が記憶される。
【００４９】
すなわち、ステップＳ１では仕様条件情報４０１の「処理済み」を参照し、「処理済み」に「１」または「０」が記載されている仕様条件を選択する。図４の仕様条件情報４０１の場合であれば、「Ｎｏ」の「２」に関連する「処理済み」が「１」の状態の仕様条件を選択する。
【００５０】
ステップＳ２では、生成部２０２が現在選択されている仕様条件に対して未処理の実装条件を示すコード（第２のコード）を特定する。
実装条件について説明する。実装条件を示すコードは、例えば、抽出部２０１が図４のプログラム情報４０２を記憶部３から取得して、プログラム情報４０２に対してシンボリック実行を行って得られるコードである。本例では、プログラム情報４０２に対してシンボリック実行を行って得られる条件として、図４に示す実装条件情報４０３が得られる。プログラム情報４０２は、上記仕様１）〜３）に基づいて作成したプログラムであり、２行目と４行目に誤りがある。本来、仕様に基づいてプログラムを作成すると２行目の記載は、「if （０＜ａ＆＆ａ＜４）｛ 」でなければならない。また、４行目の記載は、「 ｝ ｅｌｓｅ ｉｆ （４＜＝ａ＆＆ａ＜１０）｛ 」でなければならない。
【００５１】
実装条件情報４０３には、プログラム情報４０２に対してシンボリック実行を行った結果である実装条件が記憶され、「Ｎｏ」「実装条件」「処理済み」などの情報が記憶されている。「Ｎｏ」は実装条件に関連付けられる識別子で、本例では、識別子「１」「２」「３」「４」「５」などが記憶されている。「実装条件」には対象のプログラムに対してシンボリック実行を行った結果である実装条件が、識別子「１」「２」「３」「４」「５」に関連付けて記憶されている。本例では、シンボリック実行をした結果として「not (0 <= a)」「0 <= a & a < 4」「0 <= a & not (a < 4) & not (4 < a)」「0 <= a & not (a < 4) & 4 < a & a < 10」「0 <= a & not (a < 4) & 4 < a & not (a < 10)」が記憶されている。「処理済み」には現在選択されている仕様条件と実装条件とを組み合わせた組合条件が生成されたか否かを示す情報が記憶される。本例では、「１」「０」が記載されており、現在選択されている仕様条件と実装条件とが組合条件に対してステップＳ３の処理が実施されていれば、識別子「１」が記憶される。現在選択されている仕様条件に対してまだ組み合わされていない実装条件には識別子「０」が記憶される。また、「処理済み」には１つの仕様条件を示すコードに対して全ての実装条件を示すコードを組み合わせて生成された組合条件を示すコード（第３のコード）に全てに対してステップＳ３の処理が実施されると、全ての「処理済み」に「０」が記憶される。
なお、ステップＳ１の処理とステップＳ２の処理の順番はどちらが先でもよい。
【００５２】
ステップＳ３では、仕様条件と実装条件とを＆で結合して組合条件を生成して、充足値生成部２０３に送信する。このとき、記憶部３に組合条件を記憶してもよい。なお、＆は上述した＆と同じように論理積を示す記号である。図５は、組合条件情報のデータ構造の一実施例を示す図である。図５の組合条件情報５０１は、「Ｎｏ」「組合条件」などの情報を有している。「Ｎｏ」は実装条件に関連付けられる識別子で、本例では、識別子「１」〜「１５」が記憶されている。「組合条件」には、仕様条件を示すコード（第１のコード）と実装条件を示すコード（第２のコード）とを＆で結合したコード（第３のコード）が、識別子「Ｎｏ」に関連付けて記憶されている。本例では、組合条件情報５０１の識別子「１」〜「１５」に関連付けられて、「a <= 0 & not (0 <= a)」〜「a >= 10 & 0 <= a & not (a < 4) & 4 < a & not (a < 10)」が記憶されている。
【００５３】
例えば、組合条件情報５０１の識別子「１」に関連付けられて「a <= 0 & not (0 <= a)」を生成する場合、ステップＳ１で仕様条件情報４０１の最初のＮｏ「１」に対応する仕様条件「a <= 0」が選択される。ステップＳ２で実装条件情報４０３の最初のＮｏ「１」に対応する実装条件「not (0 <= a)」が選択され、＆で結合される。このとき、仕様条件情報４０１の最初のＮｏ「１」に対応する「処理済み」を「０」から「１」にし、実装条件情報４０３の最初のＮｏ「１」に対応する「処理済み」は「０」から「１」にする。
【００５４】
次に、組合条件情報５０１の識別子「２」に関連付けられて「a <= 0 & 0 <= a & a < 4」を生成する場合、ステップＳ１で仕様条件情報４０１の最初のＮｏ「１」に対応する仕様条件「a <= 0」が選択されたまま、ステップＳ２で実装条件情報４０３の未処理のＮｏ「２」に対応する実装条件「0 <= a & a < 4」が選択され、＆で結合される。このとき、仕様条件情報４０１の最初のＮｏ「１」に対応する「処理済み」は「１」のままで、実装条件情報４０３のＮｏ「２」に対応する「処理済み」は「０」から「１」になる。
【００５５】
続いて、仕様条件「a <= 0」において、実装条件情報４０３のＮｏ「３」〜「４」に関連する実装条件を用いた処理が終了すると、実装条件情報４０３のＮｏ「５」に関連する実装条件「0 <= a & not (a < 4) & 4 < a & not (a < 10)」が選択される。すなわち、ステップＳ１で仕様条件情報４０１のＮｏ「１」に対応する仕様条件「a <= 0」が選択されたまま、ステップＳ２で実装条件情報４０３の最後の未処理のＮｏ「５」に対応する実装条件が選択され、＆で結合される。このとき、仕様条件情報４０１のＮｏ「１」に対応する「処理済み」は「１」から「２」になり、実装条件情報４０３のＮｏ「５」に対応する「処理済み」は「０」から「１」になる。
【００５６】
続いて、仕様条件情報４０１のＮｏ「１」の処理が終了（仕様条件情報４０１のＮｏ「１」の「処理済み」が「２」）し、仕様条件情報４０１のＮｏ「２」がステップＳ１で選択される（「処理済み」が「１」）。このとき、実装条件情報４０３のＮｏ「１」〜「５」に対応する「処理済み」はすべて「０」にする。
【００５７】
続いて、仕様条件情報４０１のＮｏ「２」〜「３」に対応する仕様条件各々について、実装条件情報４０３のＮｏ「１」〜「５」に関連する実装条件各々と組み合わせて、組合条件情報５０１に示す組合条件を生成する。仕様条件情報４０１のＮｏ「３」が選択され、実装条件情報４０３のＮｏ「５」が選択されているとき（全て組み合わされたとき）、仕様条件情報４０１の「処理済み」はすべて「２」になり、実装条件情報４０３の「処理済み」はすべて「２」にる。
なお、本例では組合条件を記憶部３に記憶しているが、組合条件は組合条件情報に記憶しなくてもよい。
【００５８】
ステップＳ４では、充足値生成部２０３が組合条件を生成部２０２から取得し、組合条件に対してＳＭＴソルバを用いて条件を同時に充足する解を求め、求めた解を生成部２０２に送信する。
【００５９】
ステップＳ５では、生成部２０２が充足値生成部２０３から求めた解を受信し、解が存在するか否かを判定し、解が存在する場合にはステップＳ６（Ｙｅｓ）に移行し、解が存在しない場合にはステップＳ７（Ｎｏ）に移行する。
【００６０】
例えば、ステップＳ４で仕様条件情報４０１のＮｏ「２」の仕様条件を示すコードと、実装条件情報４０３のＮｏ「３」の仕様条件を示すコードと、を＆で結合した組合条件を示すコードを用いて、変数ａに対して充足する解を求める。その場合、ＳＭＴソルバの実行結果としてａ＝４を得られる。すなわち、変数ａが仕様条件情報４０１のＮｏ「２」の仕様条件を満たすにも関わらず、実装条件情報４０３のＮｏ「３」の実装条件では、エラー表示に到達するパスが存在することになる。つまり、仕様と異なる記載がプログラムにあるような場合でも、誤りを検出することが可能な組合条件（テストケース）を漏れなく抽出することができる。
【００６１】
また、ステップＳ４で仕様条件情報４０１のＮｏ「３」の仕様条件を示すコードと、実装条件情報４０３のＮｏ「１」の仕様条件を示すコードと、を＆で結合した組合条件を示すコードを用いて、変数ａに対して充足する解を求める。しかし、ＳＭＴソルバの実行結果として解を得ることができない。すなわち、仕様条件情報４０１のＮｏ「３」の仕様条件を満たすにも関わらず、実装条件情報４０３のＮｏ「１」の仕様条件を満たすようなパスはありえないことがわかる。
【００６２】
続いて、ステップＳ５で判定をした組合条件について、解がある場合にはステップＳ６で、生成部２０２は解をテストデータとして記憶部３に記憶する。図６は、組合条件に対してＳＭＴソルバにより求められる解の一実施例を示す図である。組合条件情報５０１において、解が存在するのはＮｏ「１」「２」、「７」〜「９」、「１５」に対応する組合条件である。そして、Ｎｏ「１」の解は−１、「２」の解は０、「７」の解は１、「８」の解は４、「９」の解は５、「１５」の解は１０であるので、テストデータをａ＝−１、０、１、４、５、１０とする。続いて、生成部２０２は記憶部３にテストデータをａ＝−１、０、１、４、５、１０を記憶する。
【００６３】
ステップＳ７では、生成部２０２が現在選択されている仕様条件に対して未処理の実装条件が存在するか否かを判定し、未処理の実装条件が存在する場合にはステップＳ２（Ｙｅｓ）に移行し、未処理の実装条件がない場合にはステップＳ８（Ｎｏ）に移行する。本例では、実装条件情報４０３の「処理済み」を参照して未処理の実装条件が存在するか否かを判定する。「処理済み」のいずれかに未処理を示す「０」が記憶されているときにはステップＳ２（Ｙｅｓ）に移行する。「処理済み」がすべて「１」である場合には、ステップＳ８（Ｎｏ）に移行する。
【００６４】
ステップＳ８では、生成部２０２が未処理の仕様条件が存在するか否かを判定し、未処理の仕様条件が存在する場合にはステップＳ１（Ｙｅｓ）に移行し、未処理の仕様条件がない場合には処理を終了（Ｎｏ）する。本例では、仕様条件情報４０１の「処理済み」を参報して未処理の実装条件が存在するか否かを判定する。「処理済み」のいずれかに未処理を示す「０」または処理中であることを示す「１」が記憶されているときにはステップＳ１（Ｙｅｓ）に移行する。すべての「処理済み」が、処理が終了したことを示す「２」である場合には、ステップＳ８（Ｎｏ）に移行する。
【００６５】
図７は、仕様条件と実装条件とテストデータの関係を示す図である。仕様条件１（仕様条件情報４０１のＮｏ「１」に対応）と実装条件１（実装条件情報４０３のＮｏ「１」に対応）とは同時に満たされる範囲があり、その範囲のテストデータとして−１が求められている。次に、仕様条件１と実装条件２（実装条件情報４０３のＮｏ「２」に対応）とは同時に満たされる範囲があり、その範囲のテストデータとして０が求められている。次に、仕様条件２（仕様条件情報４０１のＮｏ「２」に対応）と実装条件２とは同時に満たされる範囲があり、その範囲のテストデータとして１が求められている。次に、仕様条件２と実装条件３（実装条件情報４０３のＮｏ「３」に対応）とは同時に満たされる範囲があり、その範囲のテストデータとして４が求められている。次に、仕様条件２と実装条件４（実装条件情報４０３のＮｏ「４」に対応）とは同時に満たされる範囲があり、その範囲のテストデータとして５が求められている。次に、仕様条件３（仕様条件情報４０１のＮｏ「３」に対応）と実装条件５（実装条件情報４０３のＮｏ「５」に対応）とは同時に満たされる範囲があり、その範囲のテストデータとして１０が求められている。
【００６６】
本実施の形態によれば、仕様と異なる誤りを有するプログラムを用いて該プログラムのテストを行う場合であっても、必要十分なテストデータを生成できる。
なお、本実施の態様では、変数が１つの場合について説明したが、変数が複数ある場合でも必要十分なテストデータを生成できる。変数が複数の場合でも、仕様条件を示すコード各々と実装条件を示すコード各々とを組み合わせて組合条件を示すコードを作成する。その後、該組合条件を示すコード各々に対して、ＳＭＴソルバを用いて複数の変数を充足させる解を求め、求めた解を用いて必要十分なテストデータを生成できる。
【００６７】
また、プログラムに誤りがあっても、仕様と異なる分岐条件（ｉｆ分など）がある部分を検出できるテストケースが生成でき、その結果プログラムの分岐条件の確認に必要十分なテストデータが生成できる。
【００６８】
また、仕様条件と実装条件とが同時に満たされるテストケースを求めているため、冗長なテストデータが生成されない。
なお、実施の形態で説明したテスト対象のプログラムは、例えば、業務アプリケーションなどに用いられるプログラムなどが考えられる。
【００６９】
また、本発明は、上記実施の形態に限定されるものでなく、本発明の要旨を逸脱しない範囲内で種々の改良、変更が可能である。
【符号の説明】
【００７０】
１  テストデータ生成装置
２  制御部
３  記憶部
４  記録媒体読取装置
５  入出力インタフェース
６  通信インタフェース
７  バス
８  記録媒体
９  入出力部
２０１  抽出部
２０２  生成部
２０３  充足値生成部
４０１  仕様条件情報
４０２  プログラム情報
４０３  実装条件情報
５０１  組合条件情報
【図１】
0005672165.tif 000002
【図２】
0005672165.tif 000003
【図３】
0005672165.tif 000004
【図４】
0005672165.tif 000005
【図５】
0005672165.tif 000006
【図６】
0005672165.tif 000007
【図７】
0005672165.tif 000008