(57)【要約】【課題】検査対象プログラムを効率よく検査可能な検査データを得ること。【解決手段】検査データ生成装置は、第一変数と第二変数を含む所定の事前条件１１１ａ，１１２ａに対して所定の事後条件を満たす仕様を複数有する検査対象プログラムの検査データを生成する。検査データ生成装置は、複数の仕様ごとの事前条件を示す条件情報１３１を入力し、入力された条件情報１３１が示す事前条件１１１ａ，１１２ａの第一変数を事前条件ごとに異なる識別変数に変換する。検査データ生成装置は、第一変数を識別変数に変換された事前条件群１３２をすべて満たす識別変数と第二変数との検査データ群１３４を算出し、算出結果を出力する。【選択図】図１−３
2011081653.tif 000002
【特許請求の範囲】
【請求項１】
変数を含む所定の事前条件に対して所定の事後条件を満たす仕様を複数有する検査対象プログラムの検査データを生成する検査データ生成装置において、
前記仕様ごとの前記事前条件を示す条件情報を入力する入力手段と、
前記入力手段によって入力された条件情報が示す各事前条件の前記変数を前記事前条件ごとに異なる識別変数に変換する変換手段と、
前記変換手段によって前記変数が前記識別変数に変換された前記各事前条件を、検査データを算出する算出手段に送信する送信手段と、
前記算出手段による算出結果を受信して出力する出力手段と、
を備えることを特徴とする検査データ生成装置。
【請求項２】
前記変数は、画面上の項目を示す画面項目変数である第一変数、及びデータベースの項目を示すデータベース項目変数である第二変数を含み、
前記変換手段は、
前記条件情報が示す各事前条件の各変数を前記第一変数と前記第二変数に分類する分類手段と、
前記分類手段によって分類された第一変数に対して前記事前条件ごとに異なる識別子を付加して前記識別変数に変換する変数変換手段と、
前記変数変換手段によって変換された前記識別変数によって前記各事前条件の前記第一変数を変換する条件変換手段と、
を備えることを特徴とする請求項１に記載の検査データ生成装置。
【請求項３】
前記算出手段によって算出された前記識別変数の検査データを前記変数に還元する還元手段を備え、
前記出力手段は、前記還元手段によって還元された前記変数の検査データを出力することを特徴とする請求項１または２に記載の検査データ生成装置。
【請求項４】
前記算出手段は、前記各事前条件をすべて満たす前記識別変数と前記第二変数との検査データが存在しない場合は、前記各事前条件のうちの一部の事前条件をすべて満たす前記識別変数と前記第二変数との検査データを算出することを特徴とする請求項２に記載の検査データ生成装置。
【請求項５】
変数を含む所定の事前条件に対して所定の事後条件を満たす仕様を複数有する検査対象プログラムの検査データを生成する検査データ生成方法において、
前記仕様ごとの前記事前条件を示す条件情報を入力する入力工程と、
前記入力工程によって入力された条件情報が示す各事前条件の前記変数を前記事前条件ごとに異なる識別変数に変換する変換工程と、
前記変換工程によって前記変数が前記識別変数に変換された前記各事前条件を、検査データを算出する算出工程に送信する送信工程と、
前記算出工程による算出結果を受信して出力する出力工程と、
を含むことを特徴とする検査データ生成方法。
【請求項６】
変数を含む所定の事前条件に対して所定の事後条件を満たす仕様を複数有する検査対象プログラムの検査データを生成するコンピュータに、
前記仕様ごとの前記事前条件を示す条件情報を入力する入力手段と、
前記入力手段によって入力された条件情報が示す各事前条件の前記変数を前記事前条件ごとに異なる識別変数に変換する変換手段と、
前記変換手段によって前記変数が前記識別変数に変換された前記各事前条件を、検査データを算出する算出手段に送信する送信手段と、
前記算出手段による算出結果を受信して出力する出力手段と、
を実行させることを特徴とする検査データ生成プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、検査データを生成する検査データ生成装置、検査データ生成方法および検査データ生成プログラムに関する。
【背景技術】
【０００２】
近年、ウェブアプリケーションのバグが存在しないことを検証する方法として、プログラムのモデル検査を適用する技術が開発されている（たとえば、下記特許文献１参照。）。ウェブアプリケーションに対するプログラムのモデル検査においては、観測するプログラム状態としてブラウザなどに表示される画面状態とサーバー側のＤＢ（データベース）状態を用いる。モデル検査の処理については、まず、検査対象プログラムに対して画面とＤＢの初期状態を設定し、ドライバを用いてプログラムに対してイベントを駆動する。ここでいうイベントは、たとえば、画面上のボタンを押下するなどのユーザ操作に対応するプログラムイベントである。
【０００３】
そして、イベントを駆動する中で、プログラム状態がプロパティを満たしているかどうかを検査することによって、バグが発生していないことを確認する。ここでいうプロパティは、たとえば、評価対象のイベントおよび評価対象のイベントに関する事前条件と事後条件を含む。検査対象プログラムに含まれる事前条件と事後条件は、たとえば一階述語論理や時相論理などを用いた論理式で記述される。
【０００４】
モデル検査におけるプロパティの検査においては、評価対象イベントについて、イベント駆動前のプログラム状態において事前条件が真であるとき、イベント駆動後のプログラム状態において事後条件が真であることを確認する。したがって、事前条件が真であると評価されなければ事後条件は評価されず、プロパティの検査はされない。
【０００５】
このため、事前条件を真とするようなプログラム状態に確実に遷移するように、ドライバとプログラム初期状態を調整することが求められる。また、プロパティからの検査データ生成において、検査対象のプログラムのすべてのプロパティを検査可能である小規模な検査データを生成することが求められている。
【先行技術文献】
【特許文献】
【０００６】
【特許文献１】特開２００９−８７３５４号公報
【発明の概要】
【発明が解決しようとする課題】
【０００７】
しかしながら、従来技術では、検査対象プログラムの各プロパティを効率よく検査可能な検査データを得ることができないという問題がある。たとえば、画面とＤＢを有するプログラムのモデル検査において、画面データはドライバによって動的に設定される一方、ＤＢデータは初期状態として静的に設定される。したがって、検査対象プログラムのプロパティごとにＤＢデータを用意する場合は、すべてのプロパティを検査するために、プロパティを変更するたびにＤＢデータを設定し直してモデル検査を繰り返すことになる。このため、１回のモデル検査に時間がかかるとともに、モデル検査が繰り返されることによってすべてのプロパティを検査するための時間が膨大になってしまう。
【０００８】
これに対して、検査対象プログラムの複数のプロパティの各事前条件をすべて満たす検査データを生成することで、複数のプロパティを同時に検査可能にすることが考えられる。しかしながら、検査対象プログラムの複数の事前条件を同時に充足不能な場合は、検査データを生成することができないという問題がある。
【０００９】
本開示技術は、上述した従来技術による問題点を解消するため、検査対象プログラムを効率よく検査可能な検査データを得ることを目的とする。
【課題を解決するための手段】
【００１０】
上述した課題を解決し、目的を達成するため、本開示技術は、第一変数と第二変数を含む所定の事前条件に対して所定の事後条件を満たす仕様を複数有する検査対象プログラムの検査データを生成する技術において、前記仕様ごとの前記事前条件を示す条件情報を入力し、入力された条件情報が示す各事前条件の前記第一変数を前記事前条件ごとに異なる識別変数に変換し、前記第一変数が前記識別変数に変換された前記各事前条件をすべて満たす前記識別変数と前記第二変数との検査データを算出し、算出結果を出力することを要件とする。
【発明の効果】
【００１１】
本検査データ生成装置、検査データ生成方法および検査データ生成プログラムによれば、検査対象プログラムを効率よく検査可能な検査データを得ることができるという効果を奏する。
【図面の簡単な説明】
【００１２】
【図１−１】検査対象プログラムの一例を示す図である。
【図１−２】実施の形態１にかかる検査対象プログラム１１０の動作例を示す図である。
【図１−３】実施の形態１にかかる検査データ生成装置による検査データの生成の一例を示す図である。
【図２】実施の形態１にかかる検査データ生成装置のハードウェア構成の一例を示すブロック図である。
【図３】実施の形態１にかかる検査データ生成装置の機能的構成を示すブロック図である。
【図４】実施の形態１にかかる検査対象プログラム１１０の動作の一例を示す図である。
【図５】実施の形態１にかかる検査データ生成装置３００の動作の一例を示すフローチャートである。
【図６】実施の形態１にかかるプロパティ情報１０の一例を示す図である。
【図７】実施の形態１にかかる画面項目情報１１の一例を示す図である。
【図８】実施の形態１にかかるＤＢ項目情報１２の一例を示す図である。
【図９】実施の形態１にかかる共通制約情報１３の一例を示す図である。
【図１０】実施の形態１にかかるイベント前画面情報１４の一例を示す図である。
【図１１】図５のステップＳ５０１の一例を示すフローチャートである。
【図１２】実施の形態１にかかる変数分類情報２０の一例を示す図である。
【図１３】図５のステップＳ５０２の一例を示すフローチャートである。
【図１４】実施の形態１にかかる固有変数情報２１の一例を示す図である。
【図１５】図５のステップＳ５０３の一例を示すフローチャートである。
【図１６】実施の形態１にかかる変換後事前条件情報２２の一例を示す図である。
【図１７】図５のステップＳ５０４の一例を示すフローチャートである。
【図１８】実施の形態１にかかる制約条件式２３の一例を示す図である。
【図１９】図１７のステップＳ１７０４の一例を示すフローチャートである。
【図２０】実施の形態１にかかる制約条件式２３を満たす検査データの算出例を示す図である。
【図２１】実施の形態１にかかるＤＢデータ情報２５の一例を示す図である。
【図２２】図２１に示したＤＢデータ情報２５が表現するテーブルを示す図である。
【図２３】実施の形態１にかかる還元前画面データ情報２４の一例を示す図である。
【図２４】図５のステップＳ５０７の一例を示すフローチャートである。
【図２５】図２４のステップＳ２４０７の一例を示すフローチャートである。
【図２６】実施の形態１にかかるプロパティ対応テーブルの一例を示す図である。
【図２７】実施の形態１にかかる画面データ情報２６の一例を示す図である。
【図２８】実施の形態１にかかる検査データの適用例を示す図である。
【図２９】実施の形態２にかかる検査データ生成装置３００による検査データの生成の一例を示す図である。
【図３０】実施の形態２にかかる検査データ生成装置３００の機能的構成を示すブロック図である。
【図３１】実施の形態２にかかる検査対象プログラム１１０の動作の一例を示す図である。
【図３２】実施の形態２にかかる検査データ生成装置３００の動作の一例を示すフローチャートである。
【図３３】実施の形態２にかかるプロパティ情報１０の一例を示す図である。
【図３４】実施の形態２にかかる画面項目情報１１の一例を示す図である。
【図３５】実施の形態２にかかるＤＢ項目情報１２の一例を示す図である。
【図３６】実施の形態２にかかる共通制約情報１３の一例を示す図である。
【図３７】実施の形態２にかかる変数分類情報２０の一例を示す図である。
【図３８】実施の形態２にかかる固有変数情報２１の一例を示す図である。
【図３９】実施の形態２にかかる変換後事前条件情報２２の一例を示す図である。
【図４０】図３２のステップＳ３２０４の一例を示すフローチャートである。
【図４１】図４０のステップＳ４００３の一例を示すフローチャートである。
【図４２】図４１のステップＳ４１０４の一例を示すフローチャートである。
【図４３】図４０のステップＳ４００６の一例を示すフローチャートである。
【図４４】データ未生成プロパティ情報４０（その１）の一例を示す図である。
【図４５】実施の形態２にかかる制約条件式２３（Ｐ３，Ｐ４，Ｐ５）の一例を示す図である。
【図４６】取得される部分集合の一例を示す図である。
【図４７】実施の形態２にかかる制約条件式２３（Ｐ３，Ｐ５）の一例を示す図である。
【図４８】実施の形態２にかかるデータ未生成プロパティ情報４０（その２）の一例を示す図である。
【図４９】実施の形態２にかかる制約条件式２３（Ｐ４）の一例を示す図である。
【図５０】実施の形態２にかかるデータ未生成プロパティ情報４０（その３）の一例を示す図である。
【図５１】実施の形態２にかかる制約条件式を満たす検査データの算出例を示す図である。
【図５２】実施の形態２にかかるＤＢデータ情報２５の一例を示す図である。
【図５３】図５２に示したＤＢデータ情報２５が表現するテーブル（その１）を示す図である。
【図５４】図５２に示したＤＢデータ情報２５が表現するテーブル（その２）を示す図である。
【図５５】実施の形態２にかかる還元前画面データ情報の一例を示す図である。
【図５６】実施の形態２にかかるプロパティ対応テーブルの一例を示す図である。
【図５７】実施の形態２にかかる画面データ情報２６の一例を示す図である。
【図５８】実施の形態２にかかる検査データの適用例を示す図である。
【発明を実施するための形態】
【００１３】
以下に添付図面を参照して、本発明にかかる検査データ生成装置、検査データ生成方法および検査データ生成プログラムの好適な実施の形態を詳細に説明する。
【００１４】
（実施の形態１）
図１−１は、検査対象プログラムの一例を示す図である。実施の形態１にかかる検査データ生成装置は、たとえば図１−１に示す検査対象プログラム１１０の検査データを生成する。検査対象プログラム１１０に対する複数のプロパティとしてプロパティ１１１（Ｐ１）とプロパティ１１２（Ｐ２）がある。プロパティ１１１は、所定の事前条件１１１ａに対して所定の事後条件１１１ｂを満たすべき旨の仕様である。プロパティ１１２は、所定の事前条件１１２ａに対して所定の事後条件１１２ｂを満たすべき旨の仕様である。
【００１５】
図１−２は、実施の形態１にかかる検査対象プログラム１１０の動作例を示す図である。検査対象プログラム１１０は、たとえば画面とＤＢ（データベース）を有するウェブシステムである。プログラム状態１２１は、所定の状態の画面１２１ａと所定の状態のＤＢ１２１ｂを含んでいる。
【００１６】
画面１２１ａには、たとえば「ユーザ」、「購入点数」および「合計」などの項目が含まれている。また、ＤＢ１２１ｂには、たとえば画面１２１ａの「ユーザ」が示すユーザと対応付けられた「残高」などの項目が対応付けられている。プログラム状態１２１において、画面１２１ａにおけるボタンが押されるなどのイベントが発生すると、プログラム状態１２２に移行する。
【００１７】
プログラム状態１２２は、画面移行時のプログラム状態１２１が図１−１に示した事前条件１１１ａまたは１１２ａを満たしていれば、図１−１に示した対応する事後条件１１１ｂまたは事後条件１１２ｂを満たす。プログラム状態１２２は、所定の状態の画面１２２ａと所定の状態のＤＢ１２２ｂを含んでいる。検査対象プログラム１１０のプロパティ１１１，１１２の事前条件１１１ａ，１１２ａには第一変数と第二変数が含まれている。たとえば、画面１２１ａにおける各項目の値を第一変数（以下、「画面項目変数」と称する。）とし、ＤＢ１２１ｂにおける各項目の値を第二変数（以下、「ＤＢ項目変数」と称する。）とする。
【００１８】
図１−３は、実施の形態１にかかる検査データ生成装置による検査データの生成の一例を示す図である。実施の形態１にかかる検査データ生成装置には、プロパティ１１１，１１２ごとの事前条件を示す条件情報１３１が入力される。条件情報１３１は、事前条件１１１ａおよび事前条件１１２ａを示している。
【００１９】
条件情報１３１において、「画面．ユーザ」は画面１２１ａの「ユーザ」を示している。「画面．購入点数」は画面１２１ａの「購入点数」を示している。「画面．合計」は画面１２１ａの「合計」を示している。また、「ＤＢ［画面．ユーザ］．残高」は、ＤＢ１２１ｂにおいて、画面１２１ａの「ユーザ」と対応付けられた「残高」を示している。
【００２０】
したがって、事前条件１１１ａは、画面１２１ａの「購入点数」が０より大きく、かつ画面１２１ａの「合計」が、画面１２１ａの「ユーザ」とＤＢ１２１ｂにおいて対応付けられた「残高」より大きいことを示している。事前条件１１２ａは、画面１２１ａの「購入点数」が０より大きく、かつ画面１２１ａの「合計」が、画面１２１ａの「ユーザ」とＤＢ１２１ｂにおいて対応付けられた「残高」より小さい状態を示している。
【００２１】
検査データ生成装置は、入力された条件情報１３１が示す事前条件１１１ａ，１１２ａの画面項目変数を事前条件ごとに異なる識別変数に変換する。たとえば、検査データ生成装置は、事前条件１１１ａ，１１２ａに含まれる画面項目変数に、対応するプロパティの名称（Ｐ１またはＰ２）を付加する。事前条件１１１ａ，１１２ａに含まれる画面項目変数は、「画面．ユーザ」、「画面．購入点数」および「画面．合計」がある。
【００２２】
事前条件群１３２は、画面項目変数が識別変数に変換された事前条件１１１ａ，１１２ａを示している。たとえば、事前条件１１１ａの「画面．購入点数」、「画面．合計」および「画面．ユーザ」は、それぞれ対応するプロパティ名「Ｐ１」が付加されて識別変数「画面Ｐ１．購入点数」、「画面Ｐ１．合計」および「画面Ｐ１．ユーザ」となっている。また、事前条件１１２ａの「画面．購入点数」、「画面．合計」および「画面．ユーザ」は、それぞれ対応するプロパティ名「Ｐ２」が付加されて識別変数「画面Ｐ２．購入点数」、「画面Ｐ２．合計」および「画面Ｐ２．ユーザ」となっている。
【００２３】
制約条件式１３３は事前条件群１３２に含まれる事前条件１１１ａ，１１２ａをすべて満たすべき旨の条件を示している。検査データ生成装置は、制約条件式１３３を満たす、識別変数とＤＢ項目変数との検査データを算出する。
【００２４】
検査データ群１３４は、検査データ生成装置によって算出される各検査データを示している。検査データ１３４ａは、識別変数である「画面Ｐ１．購入点数」と「画面Ｐ１．合計」との検査データを示している。検査データ１３４ｂは、識別変数である「画面Ｐ２．購入点数」と「画面Ｐ２．合計」との検査データを示している。検査データ１３４ｃは、各「ユーザ」の「残高」の検査データを示している。たとえば、検査データ生成装置は、検査データ群１３４を出力する。
【００２５】
ユーザは、出力された検査データ群１３４のうちの検査データ１３４ａを画面１２１ａに設定するとともに検査データ１３４ｃをＤＢ１２１ｂに設定してコンピュータに検査対象プログラム１１０を実行させる。そして、検査対象プログラム１１０によってプロパティ１１１の事後条件１１１ｂが得られるか否かによって、検査対象プログラム１１０がプロパティ１１１の通りに動作するか否かを検査することができる。
【００２６】
また、ユーザは、出力された検査データ群１３４のうちの検査データ１３４ｂを画面１２１ａに設定するとともに検査データ１３４ｃをＤＢ１２１ｂに設定してコンピュータに検査対象プログラム１１０を実行させる。そして、検査対象プログラム１１０によってプロパティ１１２の事後条件１１２ｂが得られるか否かによって、検査対象プログラム１１０がプロパティ１１２の通りに動作するか否かを検査することができる。
【００２７】
また、検査データ生成装置は、識別変数の検査データである検査データ１３４ａ，１３４ｂを、画面項目変数の検査データに還元して出力してもよい。これにより、出力された検査データ１３４ａ，１３４ｂを画面１２１ａに設定すべきことをユーザにとってより分かりやすくすることができる。画面項目変数への還元の詳細については後述する。
【００２８】
（検査データ生成装置のハードウェア構成）
図２は、実施の形態１にかかる検査データ生成装置のハードウェア構成の一例を示すブロック図である。図２において、実施の形態１にかかる検査データ生成装置は、ＣＰＵ２０１（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）と、ＲＯＭ２０２（Ｒｅａｄ‐Ｏｎｌｙ  Ｍｅｍｏｒｙ）と、ＲＡＭ２０３（Ｒａｎｄｏｍ  Ａｃｃｅｓｓ  Ｍｅｍｏｒｙ）と、磁気ディスクドライブ２０４と、磁気ディスク２０５と、光ディスクドライブ２０６と、光ディスク２０７と、ディスプレイ２０８と、Ｉ／Ｆ２０９（Ｉｎｔｅｒｆａｃｅ）と、キーボード２１０と、マウス２１１と、スキャナ２１２と、プリンタ２１３と、を備えている。また、各構成部はバス２００によってそれぞれ接続されている。
【００２９】
ここで、ＣＰＵ２０１は、検査データ生成装置の全体の制御を司る。ＲＯＭ２０２は、ブートプログラムなどのプログラムを記憶している。ＲＡＭ２０３は、ＣＰＵ２０１のワークエリアとして使用される。磁気ディスクドライブ２０４は、ＣＰＵ２０１の制御にしたがって磁気ディスク２０５に対するデータのリード／ライトを制御する。磁気ディスク２０５は、磁気ディスクドライブ２０４の制御で書き込まれたデータを記憶する。
【００３０】
光ディスクドライブ２０６は、ＣＰＵ２０１の制御にしたがって光ディスク２０７に対するデータのリード／ライトを制御する。光ディスク２０７は、光ディスクドライブ２０６の制御で書き込まれたデータを記憶したり、光ディスク２０７に記憶されたデータをコンピュータに読み取らせたりする。
【００３１】
ディスプレイ２０８は、カーソル、アイコンあるいはツールボックスをはじめ、文書、画像、機能情報などのデータを表示する。このディスプレイ２０８は、たとえば、ＣＲＴ、ＴＦＴ液晶ディスプレイ、プラズマディスプレイなどを採用することができる。
【００３２】
Ｉ／Ｆ２０９は、通信回線を通じてＬＡＮ（Ｌｏｃａｌ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、ＷＡＮ（Ｗｉｄｅ  Ａｒｅａ  Ｎｅｔｗｏｒｋ）、インターネットなどのネットワーク２１４に接続され、このネットワーク２１４を介して他の装置に接続される。そして、Ｉ／Ｆ２０９は、ネットワーク２１４と内部のインターフェースを司り、外部装置からのデータの入出力を制御する。Ｉ／Ｆ２０９には、たとえばモデムやＬＡＮアダプタなどを採用することができる。
【００３３】
キーボード２１０は、文字、数字、各種指示などの入力のためのキーを備え、データの入力を行う。また、タッチパネル式の入力パッドやテンキーなどであってもよい。マウス２１１は、カーソルの移動や範囲選択、あるいはウィンドウの移動やサイズの変更などを行う。ポインティングデバイスとして同様に機能を備えるものであれば、トラックボールやジョイスティックなどであってもよい。
【００３４】
スキャナ２１２は、画像を光学的に読み取り、検査データ生成装置内に画像データを取り込む。なお、スキャナ２１２は、ＯＣＲ（Ｏｐｔｉｃａｌ  Ｃｈａｒａｃｔｅｒ  Ｒｅａｄｅｒ）機能を持たせてもよい。また、プリンタ２１３は、画像データや文書データを印刷する。プリンタ２１３には、たとえば、レーザプリンタやインクジェットプリンタを採用することができる。
【００３５】
（検査データ生成装置の機能的構成）
図３は、実施の形態１にかかる検査データ生成装置の機能的構成を示すブロック図である。図３に示すように、実施の形態１にかかる検査データ生成装置３００は、入力部３１０と、変換部３２０と、算出部３３０と、還元部３４０と、出力部３５０と、を備えている。入力部３１０は、プロパティごとの事前条件を示す条件情報を入力する。
【００３６】
たとえば、入力部３１０は、複数のプロパティを示すプロパティ情報１０を条件情報として入力する。また、入力部３１０は、画面項目情報１１と、ＤＢ項目情報１２と、共通制約情報１３と、イベント前画面情報１４と、を入力する。入力部３１０が入力する各情報は、たとえば図２に示したＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶領域に記憶される。
【００３７】
ここでは、検査対象プログラム１１０が、図１−２に示したように、画面１２１ａ上の値を示す画面項目変数と、ＤＢ１２１ｂの値を示すＤＢ項目変数と、に基づく処理を行うプログラムであるとする。この場合は、プロパティ情報１０が示す各事前条件は、画面項目変数を第一変数として含み、ＤＢ項目変数を第二変数として含む。
【００３８】
入力部３１０へ入力される画面項目情報１１は、画面１２１ａに含まれる各項目を示す情報である。ＤＢ項目情報１２は、ＤＢ１２１ｂに記憶された各項目を示す情報である。共通制約情報１３は、検査データの生成の制約条件であって、複数のプロパティに共通の共通制約条件を示す情報である。イベント前画面情報１４は、検査対象プログラム１１０の各イベント駆動時の画面を示す情報である。
【００３９】
変換部３２０は、入力部３１０によって入力されたプロパティ情報１０が示す各事前条件の画面項目変数（第一変数）を事前条件ごとに異なる識別変数に変換する。具体的には、変換部３２０は、変数分類部３２１と、変数変換部３２２と、条件変換部３２３と、を備えている。
【００４０】
変数分類部３２１は、入力部３１０によって入力された変数分類情報２０が示す各事前条件の各変数を、画面項目情報１１が示す画面項目変数とＤＢ項目情報１２が示すＤＢ項目変数とに分類する。たとえば、変数分類部３２１は、各プロパティのイベントに対応する画面名をイベント前画面情報１４から取得し、取得した画面名に対応する画面項目リストを取得する。そして、変数分類部３２１は、取得した画面項目リストに含まれる変数を画面項目変数に分類する。変数分類部３２１は、分類結果を示す変数分類情報２０を生成する。変数分類情報２０は、たとえば図２に示したＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶領域に記憶される。
【００４１】
変数変換部３２２は、変数分類部３２１によって生成された変数分類情報２０が示す画面項目変数に対して事前条件ごとに異なる識別子を付加することで、画面項目変数を事前条件ごとに異なる識別変数に変換する。変数変換部３２２は、変換結果を示す固有変数情報２１を生成する。固有変数情報２１は、たとえば図２に示したＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶領域に記憶される。
【００４２】
条件変換部３２３は、変数変換部３２２によって生成された固有変数情報２１が示す識別変数によって、プロパティ情報１０が示す各事前条件の画面項目変数を変換する。条件変換部３２３は、変換した各事前条件を示す変換後事前条件情報２２を生成する。変換後事前条件情報２２は、たとえば図２に示したＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶領域に記憶される。
【００４３】
算出部３３０は、変換部３２０によって画面項目変数が識別変数に変換された各事前条件をすべて満たす、識別変数の検査データとＤＢ項目変数の検査データと算出する。具体的には、算出部３３０は、条件生成部３３１と、データ算出部３３２と、を備えている。
【００４４】
条件生成部３３１は、変換部３２０によって画面項目変数が変換された各事前条件をすべて満たすべき旨の制約条件式を生成する。具体的には、条件生成部３３１は、変換部３２０によって生成された変換後事前条件情報２２が示す各事前条件を論理積で結合した制約条件式２３を生成する。
【００４５】
または、条件生成部３３１は、変換後事前条件情報２２が示す各事前条件と、入力部３１０によって入力された共通制約情報１３が示す共通制約条件と、を論理積で結合した制約条件式２３を生成してもよい。制約条件式２３は、たとえば図２に示したＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶領域に記憶される。
【００４６】
データ算出部３３２は、条件生成部３３１によって生成された制約条件式２３を満たす、識別変数の検査データとＤＢ項目変数との検査データを算出する。データ算出部３３２は、算出した識別変数の検査データを示す還元前画面データ情報２４と、算出したＤＢ項目変数の検査データを示すＤＢデータ情報２５と、を生成する。還元前画面データ情報２４およびＤＢデータ情報２５は、たとえば図２に示したＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶領域に記憶される。
【００４７】
データ算出部３３２にはたとえばＳＡＴ（ＳＡＴｉｓｆｉａｂｉｌｉｔｙ  ｐｒｏｂｌｅｍ）やＳＭＴ（Ｓａｔｉｓｆｉａｂｉｌｉｔｙ  Ｍｏｄｕｌｏ  Ｔｈｅｏｒｉｅｓ）などのソルバを適用することができる。ＳＭＴソルバの適用に関しては、たとえば非特許文献（足立正和，他、「充足可能性判定に基づくリアルタイムシステムのスケジューリング解析」、組込みシステムシンポジウム２００８、平成２０年１０月）などを応用できる。
【００４８】
また、ここでは算出部３３０がデータ算出部３３２を備える構成について説明したが、データ算出部３３２に代えて外部の算出プログラムを利用してもよい。この場合は、算出部３３０は、制約条件式２３を外部の算出プログラムへ送信する送信部と、外部の算出プログラムによる算出結果を受信する受信部と、備える。そして、受信部によって受信された還元前画面データ情報２４およびＤＢデータ情報２５が、たとえば図２に示したＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶領域に記憶される。
【００４９】
還元部３４０は、算出部３３０から出力された識別変数の検査データを変換前の画面データ変数に還元する。具体的には、還元部３４０は、還元前画面データ情報２４が示す識別変数の検査データを、画面項目情報１１が示す変換前の画面データ変数に還元する。還元部３４０は、還元した画面データ変数の検査データを示す画面データ情報２６を生成する。画面データ情報２６は、たとえば図２に示したＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶領域に記憶される。
【００５０】
出力部３５０は、ＤＢデータ情報２５と画面データ情報２６を極小データセット３０として出力する。出力部３５０の出力形式としては、たとえば、ディスプレイ２０８への表示、プリンタ２１３への印刷出力、Ｉ／Ｆ２０９による外部装置への送信がある。また、出力部３５０は、極小データセット３０をＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶領域に記憶することとしてもよい。
【００５１】
検査データ生成装置３００の入力部３１０、変換部３２０、算出部３３０、還元部３４０および出力部３５０は、たとえば、図２に示したＲＯＭ２０２、ＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶装置に記憶されたプログラムをＣＰＵ２０１に実行させることにより、または、Ｉ／Ｆ２０９により、その機能を実現する。
【００５２】
（検査対象プログラムの例）
図４は、実施の形態１にかかる検査対象プログラム１１０の動作の一例を示す図である。ここでは、検査対象プログラム１１０が、業者とユーザがウェブシステム上で商取引を行うための電子商取引システムのプログラムであるとする。図４に示すログイン画面４１０、商品選択画面４２０、支払確認画面４３０および支払結果画面４４０，４５０は、検査対象プログラムによってディスプレイ２０８などの表示デバイスに表示される画面である。ＤＢ４６０は、たとえば検査対象プログラム１１０によって参照可能なデータベースである。ＤＢ４６０は、ユーザとユーザの残高を対応付けたテーブルＴを記憶している。
【００５３】
検査対象プログラム１１０を実行すると、たとえば、まずログイン画面４１０が表示される。ログイン画面４１０には、入力ボックス４１１，４１２と、ログインボタン４１３と、が含まれている。入力ボックス４１１は、ユーザのＩＤを入力するための入力ボックスである。入力ボックス４１２は、パスワードを入力するための入力ボックスである。
【００５４】
ログインボタン４１３が押されると、入力ボックス４１１に入力されたＩＤと入力ボックス４１２に入力されたパスワードの認証が行われ、ＩＤに対して正しいパスワードが入力されていれば商品選択画面４２０が表示される。
【００５５】
商品選択画面４２０には、テーブル４２１と、ログアウトボタン４２２と、支払ボタン４２３と、が含まれている。テーブル４２１は、項目として「商品名」、「価格」および「数量」を含んでいる。「商品名」および「価格」はあらかじめ定められた値が表示され、「数量」はユーザによって入力されるようになっている。
【００５６】
ログアウトボタン４２２が押されると、商品選択画面４２０が非表示となり、ユーザのログアウト処理が行われるとともにログイン画面４１０が表示される。支払ボタン４２３が押されると、テーブル４２１の状態が保持され、支払確認画面４３０が表示される。
【００５７】
支払確認画面４３０には、ログイン画面４１０の入力ボックス４１１に入力されたＩＤ（ｕｓｅｒ１）と、保持されているテーブル４２１に基づいて算出された「購入点数」および「合計」と、が表示される。ここでは、テーブル４２１の「数量」の合計が２＋２＝４であるため「購入点数：４」と表示されるとともに、テーブル４２１の「価格」×「数量」の合計が５００×２＋２５０×２＋２５０×０＝１５００であるため「合計：１５００」と表示される。
【００５８】
また、支払確認画面４３０には、購入ボタン４３１と、戻るボタン４３２と、が含まれている。戻るボタン４３２が押されると、支払確認画面４３０が非表示となるとともに商品選択画面４２０が表示される。購入ボタン４３１が押されると、ＤＢ４６０が参照され、ログイン画面４１０の入力ボックス４１１に入力されたＩＤと対応付けられた残高が取得される。そして、取得された残高と、支払確認画面４３０の「合計」とが比較され、比較結果に応じて支払結果画面４４０，４５０のいずれかが表示される。
【００５９】
取得された残高が「合計」以上である場合は支払結果画面４４０が表示される。支払結果画面４４０には、ＩＤ（ｕｓｅｒ１）と、「支払い金額」、「支払い前残高」および「支払い後残高」が表示される。ここでは、支払確認画面４３０の「合計」に基づいて「支払い金額：１５００」と表示される。また、ここではＤＢ４６０から取得された残高が「２０００」であったとする。この場合は「支払い前残高：２０００」と表示される。また、「支払い前残高」から「支払い金額」を減算した結果として「支払い後残高：５００」と表示される。また、支払結果画面４４０には戻るボタン４４１が含まれている。戻るボタン４４１が押されると、支払結果画面４４０が非表示となるとともに商品選択画面４２０が表示される。
【００６０】
取得された残高が「合計」未満である場合は支払結果画面４５０が表示される。支払結果画面４５０には、ＩＤ（ｕｓｅｒ１）と、「合計」、「残高」および「不足」が表示される。ここでは、支払確認画面４３０の「合計」に基づいて「合計：１５００」と表示される。また、ここではＤＢ４６０から取得された残高が「１０００」であったとする。この場合は「残高：１０００」と表示される。また、「合計」から「残高」を減算した結果として「不足：５００」と表示される。また、支払結果画面４５０には戻るボタン４５１が含まれている。戻るボタン４５１が押されると、支払結果画面４５０が非表示となるとともに商品選択画面４２０が表示される。
【００６１】
実施の形態１にかかる検査データ生成装置は、支払確認画面４３０の状態から支払結果画面４４０，４５０のいずれかの状態へ変化するときの各プロパティを検査するための検査データを生成する。
【００６２】
（検査データ生成装置の動作）
図５は、実施の形態１にかかる検査データ生成装置３００の動作の一例を示すフローチャートである。まず、変数分類部３２１が、プロパティ情報１０が示す各プロパティの事前条件に含まれる各変数を、画面項目変数とＤＢ項目変数に分類する（ステップＳ５０１）。つぎに、変数変換部３２２が、ステップＳ５０１によって分類された画面項目変数を事前条件ごとに異なる識別変数に変換する（ステップＳ５０２）。
【００６３】
つぎに、条件変換部３２３が、各プロパティの事前条件の画面項目変数を、ステップＳ５０２によって変換された識別変数に変換する（ステップＳ５０３）。つぎに、算出部３３０が、ステップＳ５０３によって画面項目変数が識別変数に変換された各事前条件と共通制約条件とをすべて満たすように極小データを生成する（ステップＳ５０４）。
【００６４】
つぎに、ステップＳ５０４による極小データの生成が成功したか否かを判断する（ステップＳ５０５）。極小データの生成が成功していない場合（ステップＳ５０５：Ｎｏ）は、出力部３５０からエラーメッセージを出力し（ステップＳ５０６）、一連の動作を終了する。極小データの生成が成功した場合（ステップＳ５０５：Ｙｅｓ）は、ステップＳ５０４によって生成された極小データに含まれる識別変数の検査データを画面項目変数に還元する（ステップＳ５０７）。
【００６５】
つぎに、ステップＳ５０７によって還元された画面項目変数を示す画面データ情報２６と、ステップＳ５０４によって生成された極小データに含まれるＤＢ項目変数の検査データをＤＢデータ情報２５と、を出力部３５０から出力し（ステップＳ５０８）、一連の動作を終了する。図５に示した各ステップにより、各事前条件に含まれる画面項目変数を事前条件ごとに異なる識別変数に変換し、変換した各事前条件を満たす検査データを算出することができる。
【００６６】
（検査データ生成装置へ入力される各情報の例）
図６は、実施の形態１にかかるプロパティ情報１０の一例を示す図である。検査データ生成装置３００へ入力されるプロパティ情報１０は、「プロパティ名」と、「イベント」と、「事前条件」と、「事後条件」と、を対応付ける情報である。プロパティ情報１０は、「プロパティ名」が「Ｐ１」と「Ｐ２」の２つのプロパティを示している。「イベント」は、検査対象プログラム１１０が画面項目変数とＤＢ項目変数に基づく処理を行う契機を示している。「イベント」の「購入」は、図４の支払確認画面４３０の購入ボタン４３１が押されることを示している。
【００６７】
「事前条件」の「画面．ユーザ」は、支払確認画面４３０の「ユーザ」を示している。「事前条件」の「画面．購入点数」は、支払確認画面４３０の「購入点数」を示している。「事前条件」の「画面．合計」は、支払確認画面４３０の「合計」を示している。「事前条件」の「テーブルＴ［画面．ユーザ］．残高」は、支払確認画面４３０の「ユーザ」に対してＤＢ４６０において対応付けられた残高を示している。
【００６８】
プロパティＰ１の「事前条件」は、「購入点数」が０より大きく、かつ「合計」が「ユーザ」の残高未満であることを示している。プロパティＰ２の「事前条件」は、「購入点数」が０より大きく、かつ「合計」が「ユーザ」の残高より大きいことを示している。
【００６９】
「事後条件」の「画面．支払い後残高」は、支払結果画面４４０の「支払い後残高」を示している。「事後条件」の「画面．不足」は、支払結果画面４５０の「不足」を示している。プロパティＰ１の「事後条件」は、支払結果画面４４０の「支払い後残高」として、「ユーザ」の残高から「合計」を減算した値を表示することを示している。プロパティＰ２の「事後条件」は、支払結果画面４５０の「不足」として、「合計」から「ユーザ」の残高を減算した値を表示することを示している。
【００７０】
したがって、プロパティＰ１は、「購入点数」が０より大きく、かつ「合計」が「ユーザ」の残高未満である状態で購入ボタン４３１が押されると、支払結果画面４４０の「支払い後残高」として、残高から「合計」を減算した値が表示されることを示している。また、プロパティＰ２は、「購入点数」が０より大きく、かつ「合計」が「ユーザ」の残高より大きい状態で購入ボタン４３１が押されると、支払結果画面４５０の「不足」として、「合計」から残高を減算した値が表示されることを示している。
【００７１】
図７は、実施の形態１にかかる画面項目情報１１の一例を示す図である。画面項目情報１１は、「画面名」と「画面項目リスト」とを対応付ける情報である。「画面名」の「ログイン画面」は、図４に示したログイン画面４１０を示している。「ログイン画面」に対応する「画面項目リスト」には、入力ボックス４１１を示す「ＩＤ」と、入力ボックス４１２を示す「パスワード」と、が含まれている。
【００７２】
「画面名」の「商品選択画面」は、図４に示した商品選択画面４２０を示している。「商品選択画面」に対応する「画面項目リスト」には、商品選択画面４２０の「ユーザ」と、テーブル４２１の「商品名」を示す「テーブル１．商品名」と、テーブル４２１の「価格」を示す「テーブル１．価格」と、テーブル４２１の「数量」を示す「テーブル１．数量」と、が含まれている。
【００７３】
「画面名」の「支払確認画面」は、図４に示した支払確認画面４３０を示している。「支払確認画面」に対応する「画面項目リスト」には、支払確認画面４３０の「ユーザ」、「購入点数」および「合計」が含まれている。
【００７４】
「画面名」の「支払結果画面」は、図２に示した支払結果画面４４０，４５０を示している。「支払結果画面」に対応する「画面項目リスト」には、支払結果画面４４０，４５０の「ユーザ」、「支払い金額」、「支払い前残高」「支払い後残高」「合計」、「残高」および「不足」と、が含まれている。
【００７５】
図８は、実施の形態１にかかるＤＢ項目情報１２の一例を示す図である。ＤＢ項目情報１２は、「テーブル名」と「ＤＢ項目リスト」と「レコード数」とを対応付ける情報である。「テーブル名」は、ＤＢ４６０に記憶された「テーブルＴ」を示している。「ＤＢ項目リスト」は、「テーブルＴ」に含まれる各項目である「ユーザ」および「残高」が含まれている。「レコード数」は、「テーブルＴ」のレコード数を示している。ここでは「レコード数」は「３」となっており、「テーブルＴ」には「ユーザ」と「残高」の組からなるレコードが３つ含まれていることを示している。
【００７６】
図９は、実施の形態１にかかる共通制約情報１３の一例を示す図である。共通制約情報１３は、「共通制約条件名」と「条件」とを対応付ける情報である。共通制約情報１３は、「共通制約条件名」が「Ｃ」の共通制約条件を示している。「共通制約条件Ｃ」は、任意のテーブルＴのレコードｒｅｃ１，ｒｅｃ２について、（ｉｎｄｅｘ（ｒｅｃ１）≠ｉｎｄｅｘ（ｒｅｃ２））ならば、（ｒｅｃ１．ユーザ≠ｒｅｃ２．ユーザ）であることを示している。すなわち、「共通制約条件Ｃ」は、ＤＢ４６０の各レコードにおいてユーザが重複しないことを示している。
【００７７】
図１０は、実施の形態１にかかるイベント前画面情報１４の一例を示す図である。イベント前画面情報１４は、「イベント名」と「画面名」とを対応付ける情報である。「イベント名」の「ログイン」は、ログイン画面４１０においてログインボタン４１３が押されることを示している。また、「ログイン」は、ログイン画面４１０を示す「ログイン画面」と対応付けられている。
【００７８】
「イベント名」の「支払い」は、商品選択画面４２０において支払ボタン４２３が押されることを示している。また、「支払い」は、商品選択画面４２０を示す「商品選択画面」と対応付けられている。「イベント名」の「購入」は、支払確認画面４３０において購入ボタン４３１が押されることを示している。また、「購入」は、支払確認画面４３０を示す「支払確認画面」と対応付けられている。
【００７９】
（変数分類動作の例）
図１１は、図５のステップＳ５０１の一例を示すフローチャートである。変数分類部３２１は、まず、プロパティ情報１０が示すすべてのプロパティについて、事前条件に含まれる各変数を分類したか否かを判断する（ステップＳ１１０１）。すべてのプロパティについて各変数を分類していない場合（ステップＳ１１０１：Ｎｏ）は、各変数を分類していないプロパティを選択する（ステップＳ１１０２）。
【００８０】
つぎに、ステップＳ１１０２によって選択されたプロパティのイベントをプロパティ情報１０から取得し、取得したイベントに対応する画面名をイベント前画面情報１４から取得する（ステップＳ１１０３）。つぎに、ステップＳ１１０３によって取得された画面名と対応する画面項目リストを画面項目情報１１から取得する（ステップＳ１１０４）。つぎに、ステップＳ１１０４によって取得された画面項目リストを変数分類情報２０に追加する（ステップＳ１１０５）。
【００８１】
つぎに、ＤＢ項目情報１２からＤＢ項目リストを取得する（ステップＳ１１０６）。つぎに、ステップＳ１１０６によって取得されたＤＢ項目リストを変数分類情報２０に追加し（ステップＳ１１０７）、ステップＳ１１０１へ戻る。ステップＳ１１０３〜Ｓ１１０７によって、ステップＳ１１０２によって選択されたプロパティの事前条件に含まれる各変数を画面項目変数とＤＢ項目変数に分類することができる。
【００８２】
ステップＳ１１０１において、すべてのプロパティについて各変数を分類した場合（ステップＳ１１０１：Ｙｅｓ）は、ステップＳ５０２へ移行する。図１１に示した各ステップにより、各プロパティの事前条件に含まれる各変数を、画面項目変数とＤＢ項目変数に分類し、分類結果を示す変数分類情報２０を得ることができる。
【００８３】
（変数分類情報の例）
図１２は、実施の形態１にかかる変数分類情報２０の一例を示す図である。変数分類情報２０は、「プロパティ名」と「画面項目リスト」と「ＤＢ項目リスト」とを対応付ける情報である。図１１に示したように、変数分類部３２１は、プロパティ情報１０と、画面項目情報１１と、ＤＢ項目情報１２と、イベント前画面情報１４と、に基づいて変数分類情報２０を生成する。
【００８４】
たとえば、変数分類部３２１は、プロパティＰ１の「購入」に対応する「支払確認画面」をイベント前画面情報１４から取得し、取得した「支払確認画面」に対応する「ユーザ：購入点数：合計」を画面項目情報１１から取得する。そして、変数分類部３２１は、取得した「ユーザ：購入点数：合計」に基づく「画面．購入点数：画面．合計：画面．ユーザ」をプロパティＰ１の「画面項目リスト」として変数分類情報２０へ追加する。
【００８５】
また、変数分類部３２１は、プロパティＰ２の「購入」に対応する「支払確認画面」をイベント前画面情報１４から取得し、取得した「支払確認画面」に対応する「ユーザ：購入点数：合計」を画面項目情報１１から取得する。そして、変数分類部３２１は、取得した「ユーザ：購入点数：合計」に基づく「画面．購入点数：画面．合計：画面．ユーザ」をプロパティＰ２の「画面項目リスト」として変数分類情報２０へ追加する。
【００８６】
また、変数分類部３２１は、ＤＢ項目情報１２からＤＢ項目リストを取得する。そして、変数分類部３２１は、取得したＤＢ項目リストのうちのプロパティＰ１，Ｐ２に含まれる「テーブルＴ．残高」をプロパティＰ１，Ｐ２の「ＤＢ項目リスト」として変数分類情報２０に追加する。
【００８７】
（変数変換動作の例）
図１３は、図５のステップＳ５０２の一例を示すフローチャートである。変数変換部３２２は、まず、プロパティ情報１０が示すすべてのプロパティについて、事前条件に含まれる各変数を変換したか否かを判断する（ステップＳ１３０１）。すべてのプロパティについて各変数を変換していない場合（ステップＳ１３０１：Ｎｏ）は、各プロパティのうちの各変数を変換していないプロパティを選択する（ステップＳ１３０２）。
【００８８】
つぎに、ステップＳ１３０２によって選択されたプロパティの事前条件に含まれる画面項目リストの画面項目変数を事前条件ごとに異なる識別変数に変換する（ステップＳ１３０３）。つぎに、ステップＳ１３０３によって変換された識別変数を固有変数情報２１に追加し（ステップＳ１３０４）、ステップＳ１３０１へ戻る。
【００８９】
ステップＳ１３０１において、すべてのプロパティについて各変数を変換した場合（ステップＳ１３０１：Ｙｅｓ）は、ステップＳ５０３へ移行する。図１３に示した各ステップにより、ステップＳ５０１によって分類された画面項目変数を事前条件ごとに異なる変数に変換し、変換結果を示す固有変数情報２１を得ることができる。
【００９０】
（固有変数情報の例）
図１４は、実施の形態１にかかる固有変数情報２１の一例を示す図である。固有変数情報２１は、「プロパティ名」と「変換後画面項目リスト」とを対応付ける情報である。「変換後画面項目リスト」は、変数分類情報２０の「画面項目リスト」に含まれている各画面項目変数をプロパティ名に基づいて変換した各識別変数を示す情報である。
【００９１】
たとえば、変数変換部３２２は、プロパティＰ１に対応付けられた画面項目変数である「画面．購入点数」、「画面．合計」および「画面．ユーザ」を、それぞれ識別変数「画面Ｐ１．購入点数」、「画面Ｐ１．合計」および「画面Ｐ１．ユーザ」に変換する。また、変数変換部３２２は、「プロパティＰ２」に対応付けられた画面項目変数である「画面．購入点数」、「画面．合計」および「画面．ユーザ」を、それぞれ識別変数「画面Ｐ２．購入点数」、「画面Ｐ２．合計」および「画面Ｐ２．ユーザ」に変換する。
【００９２】
そして、変数変換部３２２は、「プロパティ名」と、変換後の識別変数を示す「変換後画面項目リスト」と、を対応付けた固有変数情報２１を生成する。なお、ここでは変数名に「プロパティ名」を付加することで変数を変換する場合について説明したが、変数名の変換方法はこれに限らず、変換後の各識別変数が事前条件ごと（あるいはプロパティごと）に識別可能な変数であればよい。
【００９３】
（条件変換動作の例）
図１５は、図５のステップＳ５０３の一例を示すフローチャートである。条件変換部３２３は、まず、プロパティ情報１０が示すすべてのプロパティについて事前条件を変換したか否かを判断する（ステップＳ１５０１）。すべてのプロパティについて事前条件を変換していない場合（ステップＳ１５０１：Ｎｏ）は、各プロパティのうちの事前条件を変換していないプロパティを選択する（ステップＳ１５０２）。
【００９４】
つぎに、ステップＳ１５０２によって選択されたプロパティの事前条件に含まれる各変数をステップＳ１５０４によりすべて選択したか否かを判断する（ステップＳ１５０３）。各変数をすべて選択していない場合（ステップＳ１５０３：Ｎｏ）は、ステップＳ１５０２によって選択されたプロパティの事前条件に含まれる各変数のうちの未選択の変数を選択する（ステップＳ１５０４）。
【００９５】
つぎに、ステップＳ１５０４によって選択された変数が変数分類情報２０の画面項目リストに含まれているか否かを判断する（ステップＳ１５０５）。変数分類情報２０の画面項目リストに含まれていない場合（ステップＳ１５０５：Ｎｏ）は、ステップＳ１５０３へ戻る。変数分類情報２０の画面項目リストに含まれている場合（ステップＳ１５０５：Ｙｅｓ）は、ステップＳ１５０４によって選択された変数を固有変数情報２１の変換後画面項目リストの識別変数に変換し（ステップＳ１５０６）、ステップＳ１５０３へ戻る。
【００９６】
ステップＳ１５０３において、各変数をすべて選択した場合（ステップＳ１５０３：Ｙｅｓ）は、ステップＳ１５０１へ戻る。ステップＳ１５０１において、すべてのプロパティについて事前条件を変換した場合（ステップＳ１５０１：Ｙｅｓ）は、ステップＳ５０４へ移行する。図１５に示した各ステップにより、各プロパティの事前条件の画面項目変数を識別変数に変換し、画面項目変数を識別変数に変換された各事前条件を示す変換後事前条件情報２２を得ることができる。
【００９７】
（変換後事前条件情報の例）
図１６は、実施の形態１にかかる変換後事前条件情報２２の一例を示す図である。変換後事前条件情報２２は、「プロパティ名」と「変換後事前条件」とを対応付ける情報である。「変換後事前条件」は、プロパティ情報１０の「事前条件」を固有変数情報２１の「変換後画面項目リスト」により変換した情報である。
【００９８】
たとえば、条件変換部３２３は、プロパティＰ１に対応付けられた「事前条件」に含まれる画面項目変数を、固有変数情報２１のプロパティＰ１に対応付けられた「変換後画面項目リスト」により変換する。具体的には、条件変換部３２３は、「画面．購入点数」を識別変数「画面Ｐ１．購入点数」に変換し、「画面．合計」を識別変数「画面Ｐ１．合計」に変換し、「画面．ユーザ」を識別変数「画面Ｐ１．ユーザ」に変換する。
【００９９】
また、条件変換部３２３は、プロパティＰ２に対応付けられた「事前条件」に含まれる画面項目変数を、固有変数情報２１の「プロパティＰ２」に対応付けられた「変換後画面項目リスト」により変換する。具体的には、条件変換部３２３は、「画面．購入点数」を識別変数「画面Ｐ２．購入点数」に変換し、「画面．合計」を識別変数「画面Ｐ２．合計」に変換し、「画面．ユーザ」を識別変数「画面Ｐ２．ユーザ」に変換する。
【０１００】
（極小データ生成動作の例）
図１７は、図５のステップＳ５０４の一例を示すフローチャートである。算出部３３０は、まず、制約条件式２３を恒真式に設定する（ステップＳ１７０１）。つぎに、ステップＳ１７０１によって設定された制約条件式２３に、変換後事前条件情報２２が示す各変換後事前条件を論理積（ａｎｄ）で結合する（ステップＳ１７０２）。つぎに、ステップＳ１７０２によって結合された制約条件式２３に、共通制約情報１３が示す「共通制約条件Ｃ」を論理積で結合する（ステップＳ１７０３）。
【０１０１】
つぎに、ステップＳ１７０３によって結合された制約条件式２３を用いて極小データを生成し（ステップＳ１７０４）、ステップＳ５０５へ移行する。図１７に示す各ステップにより、ステップＳ５０３によって画面項目変数が変換された各事前条件と共通制約条件とをすべて満たすように極小データを生成することができる。
【０１０２】
（制約条件式の例）
図１８は、実施の形態１にかかる制約条件式２３の一例を示す図である。制約条件式２３は、変換後事前条件情報２２が示す「プロパティ名」ごとの各「変換後事前条件」と、共通制約情報１３が示す「共通制約条件Ｃ」と、をすべて満たすべき旨の条件を示している。算出部３３０は、変換後事前条件情報２２および共通制約情報１３に基づいて制約条件式２３を生成する。
【０１０３】
図１９は、図１７のステップＳ１７０４の一例を示すフローチャートである。算出部３３０は、まず、ステップＳ１７０３によって結合された制約条件式２３を満たす、変換後事前条件情報２２の変換後事前条件に含まれる各変数の値を算出する（ステップＳ１９０１）。つぎに、ステップＳ１９０１による算出の結果、制約条件式２３を満たす各変数の値が存在するか否かを判断する（ステップＳ１９０２）。
【０１０４】
ステップＳ１９０２において、制約条件式２３を満たす各変数の値が存在しない場合（ステップＳ１９０２：Ｎｏ）は、一連の動作を終了する。制約条件式２３を満たす各変数の値が存在する場合（ステップＳ１９０２：Ｙｅｓ）は、変換後事前条件情報２２の変換後事前条件に含まれるすべての変数をステップＳ１９０４によって選択したか否かを判断する（ステップＳ１９０３）。
【０１０５】
ステップＳ１９０３において、すべての変数を選択していない場合（ステップＳ１９０３：Ｎｏ）は、変換後事前条件に含まれる各変数のうちの未選択の変数を選択する（ステップＳ１９０４）。つぎに、ステップＳ１９０４によって選択された変数がＤＢ項目変数であるか否かを判断する（ステップＳ１９０５）。選択された変数がＤＢ項目変数である場合（ステップＳ１９０５：Ｙｅｓ）は、選択された変数と、選択された変数についてステップＳ１９０１によって算出された値と、をＤＢデータ情報２５に追加し（ステップＳ１９０６）、ステップＳ１９０３へ戻る。
【０１０６】
ステップＳ１９０５において、選択された変数がＤＢ項目変数でない場合（ステップＳ１９０５：Ｎｏ）は、ステップＳ１９０４によって選択された変数が識別変数であるか否かを判断する（ステップＳ１９０７）。選択された変数が識別変数である場合（ステップＳ１９０７：Ｙｅｓ）は、選択された変数と、選択された変数についてステップＳ１９０１によって算出された値と、を還元前画面データ情報２４に追加し（ステップＳ１９０８）、ステップＳ１９０３へ戻る。
【０１０７】
ステップＳ１９０７において、選択された変数が識別変数でない場合（ステップＳ１９０７：Ｎｏ）は、一連の動作を終了する。ただし、一連の動作を終了せずに、ステップＳ１９０３へ戻ってもよい。ステップＳ１９０３において、すべての変数を選択した場合（ステップＳ１９０３：Ｙｅｓ）は、一連の動作を終了する。図１９に示した各ステップにより、ステップＳ１７０３によって結合された制約条件式２３を用いて極小データを生成することができる。生成される極小データには、ＤＢデータ情報２５と還元前画面データ情報２４が含まれている。
【０１０８】
ステップＳ１９０３においてすべての変数を選択したと判断して動作を終了した場合は、図５に示したステップＳ５０５において極小データの生成が成功したと判断する。また、ステップＳ１９０２において制約条件式２３を満たす各変数の値が存在しないと判断して動作を終了した場合は、図５に示したステップＳ５０５において極小データの生成が成功しなかったと判断する。また、ステップＳ１９０７において選択された変数が識別変数でないと判断して動作を終了した場合は、図５に示したステップＳ５０５において極小データの生成が成功しなかったと判断する。
【０１０９】
（制約条件式を満たす各変数の値の例）
図２０は、実施の形態１にかかる制約条件式２３を満たす検査データの算出例を示す図である。生成データ２０００は、図１９のステップＳ１９０１による各変数の値の算出結果の一例を示している。生成データ２０００に示す各変数のうちの「テーブルＴ［１］．ユーザ」、「テーブルＴ［１］．残高」、「テーブルＴ［２］．ユーザ」、「テーブルＴ［２］．残高」、「テーブルＴ［３］．ユーザ」および「テーブルＴ［３］．残高」はＤＢ項目変数である。また、生成データ２０００に示す各変数のうちの「画面Ｐ１．ユーザ」、「画面Ｐ１．購入点数」、「画面Ｐ１．合計」、「画面Ｐ２．ユーザ」、「画面Ｐ２．購入点数」および「画面Ｐ２．合計」は、画面項目変数を変換した識別変数である。
【０１１０】
（ＤＢデータ情報の例）
図２１は、実施の形態１にかかるＤＢデータ情報２５の一例を示す図である。ＤＢデータ情報２５は、「ＤＢテーブル名」と「ＤＢテーブル値リスト」とを対応付ける情報である。「ＤＢテーブル名」は、ＤＢ４６０に格納されるテーブルＴを示している。「ＤＢテーブル値リスト」は、テーブルＴに格納される「ユーザ」と「残高」の対応情報を示している。データ算出部３３２は、生成データ２０００（図２０参照）が示す各変数のうちのＤＢ項目変数に基づいてＤＢデータ情報２５を生成する。
【０１１１】
図２２は、図２１に示したＤＢデータ情報２５が表現するテーブルを示す図である。ＤＢデータ情報２５（図２１参照）は、テーブル２２００を表現している。テーブル２２００に示すように、「ｕｓｅｒ１」には残高として「２０００」が対応付けられ、「ｕｓｅｒ２」には残高として「１０００」が対応付けられ、「ｕｓｅｒ３」には残高として「２０００」が対応付けられている。
【０１１２】
（還元前画面データ情報の例）
図２３は、実施の形態１にかかる還元前画面データ情報２４の一例を示す図である。還元前画面データ情報２４は、「画面項目名」と「画面項目値」とを対応付ける情報である。「画面項目名」は、変換後事前条件情報２２に含まれる識別変数を示している。「画面項目値」は、「画面項目名」が示す識別変数に代入される値を示している。データ算出部３３２は、生成データ２０００（図２０参照）が示す各変数のうちの識別変数に基づいて還元前画面データ情報２４を生成する。
【０１１３】
（画面項目変数の還元動作の例）
図２４は、図５のステップＳ５０７の一例を示すフローチャートである。還元部３４０は、まず、プロパティ情報１０が示すすべてのプロパティを選択したか否かを判断する（ステップＳ２４０１）。すべてのプロパティを選択していない場合（ステップＳ２４０１：Ｎｏ）は、未選択のプロパティを選択する（ステップＳ２４０２）。
【０１１４】
つぎに、ステップＳ２４０２によって選択されたプロパティに対応する変換後画面項目リストを固有変数情報２１から取得する（ステップＳ２４０３）。つぎに、ステップＳ２４０２によって選択されたプロパティに対応する画面項目リストを変数分類情報２０から取得する（ステップＳ２４０４）。つぎに、画面データ情報２６のエントリを作成する（ステップＳ２４０５）。具体的には、ステップＳ２４０２によって選択されたプロパティに対応付けた画面データ名を画面データ情報２６に追加する。
【０１１５】
つぎに、還元前画面データ情報２４が示すすべての識別変数のうちの、ステップＳ２４０２によって選択されたプロパティに対応するすべての識別変数を画面項目変数に還元したか否かを判断する（ステップＳ２４０６）。すべての識別変数を還元していない場合（ステップＳ２４０６：Ｎｏ）は、還元していない識別変数を画面項目変数に還元し（ステップＳ２４０７）、ステップＳ２４０６へ戻る。すべての識別変数を還元した場合（ステップＳ２４０６：Ｙｅｓ）は、プロパティ名と画面データ名の組をプロパティ対応テーブル（図２６参照）へ追加し（ステップＳ２４０８）、ステップＳ２４０１へ戻る。
【０１１６】
ステップＳ２４０１において、すべてのプロパティを選択した場合（ステップＳ２４０１：Ｙｅｓ）は、ステップＳ５０８へ移行する。図２４に示した各ステップにより、ステップＳ５０４によって生成された極小データに含まれる識別変数の検査データを変換前の画面項目変数の値に還元し、還元結果を示す画面データ情報２６を得ることができる。
【０１１７】
図２５は、図２４のステップＳ２４０７の一例を示すフローチャートである。還元部３４０は、まず、ステップＳ５０４によって得られた還元前画面データ情報２４の各識別変数のうちの未処理の画面項目名を選択する（ステップＳ２５０１）。つぎに、ステップＳ２５０１によって選択された画面項目名が、ステップＳ２４０３によって取得された変換後画面項目リストに含まれているか否かを判断する（ステップＳ２５０２）。
【０１１８】
ステップＳ２５０２において、画面項目名が固有変数情報２１の変換後画面項目リストに含まれていない場合（ステップＳ２５０２：Ｎｏ）は、一連の動作を終了する。画面項目名が固有変数情報２１の変換後画面項目リストに含まれている場合（ステップＳ２５０２：Ｙｅｓ）は、画面項目名に対応する変換前の画面項目変数を、変数分類情報２０の画面項目リストから取得する（ステップＳ２５０３）。変数分類情報２０は、ステップＳ２４０４によって取得された変数分類情報２０である。
【０１１９】
つぎに、画面項目情報１１の所定の画面項目リストに含まれる画面項目名のうちの、ステップＳ２５０３によって取得された変換前の画面項目変数と対応する画面項目名を取得する（ステップＳ２５０４）。所定の画面項目リストは、ステップＳ２４０２によって選択されたプロパティのイベントに対応する画面名をイベント前画面情報１４から取得し、取得した画面名と画面項目情報１１において対応する画面項目リストである。
【０１２０】
つぎに、ステップＳ２５０４によって取得された画面項目名と、ステップＳ２５０１によって選択された画面項目名と対応する画面項目値と、の組を画面データ情報２６に追加し（ステップＳ２５０５）、一連の動作を終了する。画面項目値は、ステップＳ２５０１によって選択された画面項目名と還元前画面データ情報２４において対応する画面項目値である。図２５に示した各ステップにより、還元していない識別変数を画面項目変数に還元し、還元結果を示す画面データ情報２６を得ることができる。
【０１２１】
（プロパティ対応テーブルの例）
図２６は、実施の形態１にかかるプロパティ対応テーブルの一例を示す図である。図２６に示すプロパティ対応テーブル２６００は、「プロパティ名」と「画面データ名」とを対応付ける情報である。算出部３３０は、たとえば「プロパティＰ１」と「画面データＰ１」とを対応付けるとともに、「プロパティＰ２」と「画面データＰ２」とを対応付け、プロパティ対応テーブル２６００を生成する。プロパティ対応テーブル２６００は、図２４のステップＳ２４０８によって生成される。
【０１２２】
（画面データ情報の例）
図２７は、実施の形態１にかかる画面データ情報２６の一例を示す図である。画面データ情報２６は、「画面データ名」と「画面項目値リスト」とを対応付ける情報である。「画面データ名」は、プロパティ対応テーブル２６００の「画面データ名」を示している。「画面項目値リスト」は、図４の支払確認画面４３０の各項目に代入する値を示している。還元部３４０は、変数分類情報２０と、イベント前画面情報１４と、画面項目情報１１とを利用し、還元前画面データ情報２４と固有変数情報２１とに基づいて画面データ情報２６を生成する。
【０１２３】
たとえば、還元部３４０は、還元前画面データ情報２４の「画面項目名」が固有変数情報２１において対応付けられている「プロパティ名」を取得する。そして、還元部３４０は、取得した「プロパティ名」がプロパティ対応テーブル２６００において対応付けられている「画面データ名」を取得する。
【０１２４】
さらに、還元部３４０は、取得した「プロパティ名」に対応する固有変数情報２１の「変換後画面項目リスト」と取得した「プロパティ名」に対応する変数分類情報２０の「画面項目リスト」から、還元前画面データ情報２４の「画面項目名」に対応する変換前の画面項目変数を取得する。さらに、還元部３４０は、プロパティのイベントに対応するイベント前画面情報１４の「画面名」を取得する。そして、還元部３４０は、取得した「画面名」に対応する画面項目情報１１の「画面項目リスト」において、変数分類情報２０から取得した変換前の画面項目変数に対応する画面項目名を取得する。
【０１２５】
そして、還元部３４０は、取得した「画面データ名」と、画面項目情報１１から取得した画面項目名と、還元前画面データ情報２４の「画面項目名」に対応付けられた「画面項目値」と、を対応付けて画面データ情報２６を生成する。
【０１２６】
たとえば、還元部３４０は、還元前画面データ情報２４の「画面Ｐ１．ユーザ」が固有変数情報２１において対応付けられているプロパティＰ１を取得する。そして、還元部３４０は、取得したプロパティＰ１がプロパティ対応テーブル２６００において対応付けられている「画面データＰ１」を取得する。
【０１２７】
さらに、還元部３４０は、取得したプロパティＰ１に対応する固有変数情報２１の「変換後画面項目リスト」と取得したプロパティＰ１に対応する変数分類情報２０の「画面項目リスト」から、還元前画面データ情報２４の「画面Ｐ１．ユーザ」に対応する変換前の画面項目変数「画面．ユーザ」を取得する。さらに、還元部３４０は、プロパティＰ１のイベント「購入」に対応するイベント前画面情報１４の「支払い確認画面」を取得する。
【０１２８】
そして、還元部３４０は、取得した「支払い確認画面」に対応する画面項目情報１１の「画面項目リスト」において、変数分類情報２０から取得した変換前の画面項目変数「画面．ユーザ」に対応する「ユーザ」を取得する。そして、還元部３４０は、取得した「画面データＰ１」と、画面項目情報１１から取得した「ユーザ」と、還元前画面データ情報２４の「画面Ｐ１．ユーザ」に対応付けられた「ｕｓｅｒ１」と、を対応付けて「画面項目値リスト」に追加する。
【０１２９】
また、還元部３４０は、還元前画面データ情報２４の「画面Ｐ１．購入点数」が固有変数情報２１において対応付けられているプロパティＰ１を取得する。そして、還元部３４０は、取得したプロパティＰ１がプロパティ対応テーブル２６００において対応付けられている「画面データＰ１」を取得する。
【０１３０】
さらに、還元部３４０は、取得したプロパティＰ１に対応する固有変数情報２１の「変換後画面項目リスト」と取得したプロパティＰ１に対応する変数分類情報２０の「画面項目リスト」から、還元前画面データ情報２４の「画面Ｐ１．購入点数」に対応する変換前の画面項目変数「画面．購入点数」を取得する。さらに、還元部３４０は、プロパティＰ１のイベント「購入」に対応するイベント前画面情報１４の「支払い確認画面」を取得する。
【０１３１】
そして、還元部３４０は、取得した「支払い確認画面」に対応する画面項目情報１１の「画面項目リスト」において、変数分類情報２０から取得した変換前の画面項目変数「画面．購入点数」に対応する「購入点数」を取得する。そして、還元部３４０は、取得した「画面データＰ１」と、画面項目情報１１から取得した「購入点数」と、還元前画面データ情報２４の「画面Ｐ１．購入点数」に対応付けられた「４」と、を対応付けて「画面項目値リスト」に追加する。
【０１３２】
また、還元部３４０は、還元前画面データ情報２４の「画面Ｐ１．合計」が固有変数情報２１において対応付けられているプロパティＰ１を取得する。そして、還元部３４０は、取得したプロパティＰ１がプロパティ対応テーブル２６００において対応付けられている「画面データＰ１」を取得する。
【０１３３】
さらに、還元部３４０は、取得したプロパティＰ１に対応する固有変数情報２１の「変換後画面項目リスト」と取得したプロパティＰ１に対応する変数分類情報２０の「画面項目リスト」から、還元前画面データ情報２４の「画面Ｐ１．合計」に対応する変換前の画面項目変数「画面．合計」を取得する。さらに、還元部３４０は、プロパティＰ１のイベント「購入」に対応するイベント前画面情報１４の「支払い確認画面」を取得する。
【０１３４】
そして、還元部３４０は、取得した「支払い確認画面」に対応する画面項目情報１１の「画面項目リスト」において、変数分類情報２０から取得した変換前の画面項目変数「画面．合計」に対応する「合計」を取得する。そして、還元部３４０は、取得した「画面データＰ１」と、画面項目情報１１から取得した「合計」と、還元前画面データ情報２４の「画面Ｐ１．合計」に対応付けられた「１５００」と、を対応付けて「画面項目値リスト」に追加する。
【０１３５】
同様に、還元部３４０は、還元前画面データ情報２４の「画面Ｐ２．ユーザ」が固有変数情報２１において対応付けられているプロパティＰ２を取得する。そして、還元部３４０は、取得したプロパティＰ２がプロパティ対応テーブル２６００において対応付けられている「画面データＰ２」を取得する。さらに、還元部３４０は、取得したプロパティＰ２に対応する固有変数情報２１の「変換後画面項目リスト」と取得したプロパティＰ２に対応する変数分類情報２０の「画面項目リスト」から、還元前画面データ情報２４の「画面Ｐ２．ユーザ」に対応する変換前の画面項目変数「画面．ユーザ」を取得する。
【０１３６】
さらに、還元部３４０は、プロパティＰ２のイベント「購入」に対応するイベント前画面情報１４の「支払い確認画面」を取得する。そして、還元部３４０は、取得した「支払い確認画面」に対応する画面項目情報１１の「画面項目リスト」において、変数分類情報２０から取得した変換前の画面項目変数「画面．ユーザ」に対応する「ユーザ」を取得する。そして、還元部３４０は、取得した「画面データＰ２」と、画面項目情報１１から取得した「ユーザ」と、還元前画面データ情報２４の「画面Ｐ２．ユーザ」に対応付けられた「ｕｓｅｒ２」と、を対応付けて「画面項目値リスト」に追加する。
【０１３７】
また、還元部３４０は、還元前画面データ情報２４の「画面Ｐ２．購入点数」が固有変数情報２１において対応付けられているプロパティＰ２を取得する。そして、還元部３４０は、取得したプロパティＰ２がプロパティ対応テーブル２６００において対応付けられている「画面データＰ２」を取得する。
【０１３８】
さらに、還元部３４０は、取得したプロパティＰ２に対応する固有変数情報２１の「変換後画面項目リスト」と取得したプロパティＰ２に対応する変数分類情報２０の「画面項目リスト」から、還元前画面データ情報２４の「画面Ｐ２．購入点数」に対応する変換前の画面項目変数「画面．購入点数」を取得する。さらに、還元部３４０は、プロパティＰ２のイベント「購入」に対応するイベント前画面情報１４の「支払い確認画面」を取得する。
【０１３９】
そして、還元部３４０は、取得した「支払い確認画面」に対応する画面項目情報１１の「画面項目リスト」において、変数分類情報２０から取得した変換前の画面項目変数「画面．購入点数」に対応する「購入点数」を取得する。そして、還元部３４０は、取得した「画面データＰ２」と、画面項目情報１１から取得した「購入点数」と、還元前画面データ情報２４の「画面Ｐ２．購入点数」に対応付けられた「４」と、を対応付けて「画面項目値リスト」に追加する。
【０１４０】
また、還元部３４０は、還元前画面データ情報２４の「画面Ｐ２．合計」が固有変数情報２１において対応付けられているプロパティＰ２を取得する。そして、還元部３４０は、取得したプロパティＰ２がプロパティ対応テーブル２６００において対応付けられている「画面データＰ２」を取得する。
【０１４１】
さらに、還元部３４０は、取得したプロパティＰ２に対応する固有変数情報２１の「変換後画面項目リスト」と取得したプロパティＰ２に対応する変数分類情報２０の「画面項目リスト」から、還元前画面データ情報２４の「画面Ｐ２．合計」に対応する変換前の画面項目変数「画面．合計」を取得する。さらに、還元部３４０は、プロパティＰ２のイベント「購入」に対応するイベント前画面情報１４の「支払い確認画面」を取得する。そして、還元部３４０は、取得した「支払い確認画面」に対応する画面項目情報１１の「画面項目リスト」において、変数分類情報２０から取得した変換前の画面項目変数「画面．合計」に対応する「合計」を取得する。そして、還元部３４０は、取得した「画面データＰ２」と、画面項目情報１１から取得した「合計」と、還元前画面データ情報２４の「画面Ｐ２．合計」に対応付けられた「１５００」と、を対応付けて「画面項目値リスト」に追加する。
【０１４２】
（検査データの適用例）
図２８は、実施の形態１にかかる検査データの適用例を示す図である。図２８に示すように、画面データ情報２６の「画面データＰ１」が設定されると、図４の支払確認画面４３０は符号２８１０のようになる。また、画面データ情報２６の「画面データＰ２」が設定されると、図４の支払確認画面４３０は符号２８２０のようになる。また、符号２８１０と符号２８２０のいずれの場合も、ＤＢ４６０に設定されるテーブルは共通でテーブル２２００（図２２参照）となる。
【０１４３】
このように、実施の形態１にかかる検査データ生成装置３００によれば、事前条件に含まれる画面項目変数（第一変数）を事前条件ごとに異なる識別変数に変換し、変換した各事前条件を満たす検査データを得ることができる。これにより、同時に充足不能な複数の事前条件を有する検査対象プログラム１１０であっても、ＤＢ項目変数（第二変数）を共通化した検査データを得ることができる。ＤＢ項目変数を共通化することで、モデル検査にかかる時間を短縮することができるため、検査対象プログラム１１０を効率よく検査することが可能になる。
【０１４４】
（実施の形態２）
実施の形態２において、実施の形態１と同様の部分については同一の符号を付して説明を省略する。
【０１４５】
図２９は、実施の形態２にかかる検査データ生成装置３００による検査データの生成の一例を示す図である。符号２９１０に示すように、条件生成部３３１によって生成された制約条件式２３が、プロパティＰ３〜Ｐ５の各事前条件と共通制約条件Ｃとをすべて満たすべき旨の制約条件式２９１１であるとする。そして、制約条件式２３を満たす検査データが存在しない（充足不能）とする。この場合に、実施の形態２にかかる算出部３３０は、各事前条件のうちの一部の事前条件をすべて満たす検査データを算出する。
【０１４６】
たとえば、条件生成部３３１は、符号２９２０に示すように、プロパティＰ３，Ｐ５の各事前条件と共通制約条件Ｃをすべて満たすべき旨の制約条件式２９２１を生成する。データ算出部３３２は、制約条件式２９２１を満たす検査データ（データｆｏｒＰ３  ａｎｄ  Ｐ５）を算出する。これにより、検査対象プログラム１１０のプロパティＰ３，Ｐ５を検査する検査データを生成することができる。
【０１４７】
さらに、条件生成部３３１は、符号２９３０に示すように、プロパティＰ３〜Ｐ５の各事前条件からプロパティＰ３，Ｐ５を除いたプロパティＰ４の事前条件と共通制約条件Ｃをすべて満たすべき旨の制約条件式２９３１を構成する。データ算出部３３２は、制約条件式２９３１を満たす検査データ（データｆｏｒＰ４）を算出する。これにより、検査対象プログラム１１０のプロパティＰ４を検査する検査データを生成することができる。
【０１４８】
（検査データ生成装置のハードウェア構成）
実施の形態２にかかる検査データ生成装置３００のハードウェア構成については、図２に示した検査データ生成装置のハードウェア構成と同様であるため説明を省略する。
【０１４９】
（検査データ生成装置の機能的構成）
図３０は、実施の形態２にかかる検査データ生成装置３００の機能的構成を示すブロック図である。図３０に示すように、実施の形態２にかかる検査データ生成装置３００の条件生成部３３１は、プロパティごとに極小データを生成したかを示すデータ未生成プロパティ情報４０を生成する。データ未生成プロパティ情報４０は、たとえば図２に示したＲＡＭ２０３、磁気ディスク２０５、光ディスク２０７などの記憶領域に記憶される。
【０１５０】
（検査対象プログラムの例）
図３１は、実施の形態２にかかる検査対象プログラム１１０の動作の一例を示す図である。図３１において、図４に示した部分と同様の部分については同一の符号を付して説明を省略する。ここでは、ＤＢ４６０においては、各ユーザと残高が対応付けられているとともに、各ユーザが当選者か否かが記憶されている。実施の形態２にかかる検査対象プログラム１１０は、ログインボタン４１３が押され、ＩＤに対して正しいパスワードが入力されていた場合に、ＩＤが示すユーザが当選者か否かをＤＢ４６０に基づいて判断する。
【０１５１】
ユーザが当選者である場合は、検査対象プログラム１１０は、ユーザの残高が１００００以上であれば、ＤＢ４６０におけるユーザの残高に１００００ポイントを加えるとともにポイント追加通知画面３１１０を表示する。ポイント追加通知画面３１１０は、ユーザが当選者であり、残高に１００００ポイントを追加する旨を示す。また、ポイント追加通知画面３１１０には続行ボタン３１１１が含まれており、続行ボタン３１１１が押されると商品選択画面４２０が表示される。
【０１５２】
また、検査対象プログラム１１０は、ユーザが当選者でありユーザの残高が１００００未満であれば、ＤＢ４６０におけるユーザの残高に５０００ポイントを加えるとともにポイント追加通知画面３１２０を表示する。ポイント追加通知画面３１２０は、ユーザが当選者であり、残高に５０００ポイントを追加する旨を示す。また、ポイント追加通知画面３１２０には続行ボタン３１２１が含まれており、続行ボタン３１２１が押されると商品選択画面４２０が表示される。
【０１５３】
ユーザが当選者でない場合は、検査対象プログラム１１０は、図４に示した動作と同様に商品選択画面４２０を表示する。商品選択画面４２０が表示された後の検査対象プログラム１１０については図４に示した通りである。検査データ生成装置３００は、ログイン画面４１０の状態からポイント追加通知画面３１１０，３１２０または商品選択画面４２０の状態へ変化するときのプロパティを検査するための検査データを生成する。
【０１５４】
（検査データ生成装置の動作）
図３２は、実施の形態２にかかる検査データ生成装置３００の動作の一例を示すフローチャートである。図３２に示すステップＳ３２０１〜Ｓ３２０３は、図５に示したステップＳ５０１〜Ｓ５０３と同様であるため説明を省略する。ステップＳ３２０３のつぎに、算出部３３０および還元部３４０が、極小データの生成および識別変数の画面項目変数への還元を行う（ステップＳ３２０４）。
【０１５５】
つぎに、ステップＳ３２０４による極小データの生成が成功したか否かを判断する（ステップＳ３２０５）。ステップＳ３２０４によるデータの生成が成功していない場合（ステップＳ３２０５：Ｎｏ）は、出力部３５０からエラーメッセージを出力し（ステップＳ３２０６）、一連の動作を終了する。
【０１５６】
ステップＳ３２０５において、極小データの生成が成功した場合（ステップＳ３２０５：Ｙｅｓ）は、ステップＳ３２０４によって生成された極小データに含まれる画面データ情報２６とＤＢデータ情報２５を出力部３５０から出力し（ステップＳ３２０７）、一連の動作を終了する。図３２に示した各ステップにより、各事前条件に含まれる画面項目変数を事前条件ごとに異なる識別変数に変換し、変換した各事前条件を満たす検査データを算出することができる。
【０１５７】
（検査データ生成装置へ入力される情報の例）
図３３は、実施の形態２にかかるプロパティ情報１０の一例を示す図である。プロパティ情報１０は、「プロパティ名」が「Ｐ３」、「Ｐ４」および「Ｐ５」の３つのプロパティを示している。「イベント」の「ログイン」は、図３１のログイン画面４１０のログインボタン４１３が押されることを示している。
【０１５８】
「事前条件」の「画面．ＩＤ」は、ログイン画面４１０の入力ボックス４１１の値を示している。「事前条件」の「テーブルＴ［画面．ＩＤ］．当選者」は、ＤＢ４６０の変数であり、入力ボックス４１１の値が示すユーザが当選者か否かを示している。具体的には、「テーブルＴ［画面．ＩＤ］．当選者」は、入力ボックス４１１の値が示すユーザが当選者である場合は値が「ｔｒｕｅ」となり、当選者でない場合は値が「ｆａｌｓｅ」となる。「事前条件」の「テーブルＴ［画面．ＩＤ］．残高」は、入力ボックス４１１の値が示すユーザに対してＤＢ４６０において対応付けられた残高を示している。
【０１５９】
プロパティＰ３の「事前条件」は、「テーブルＴ［画面．ＩＤ］．当選者」が「ｔｒｕｅ」であり、かつ「テーブルＴ［画面．ＩＤ］．残高」が１００００ポイント以上であることを示している。プロパティＰ４の「事前条件」は、「テーブルＴ［画面．ＩＤ］．当選者」が「ｔｒｕｅ」であり、かつ「テーブルＴ［画面．ＩＤ］．残高」が１００００ポイント未満であることを示している。プロパティＰ５の「事前条件」は、「テーブルＴ［画面．ＩＤ］．当選者」が「ｆａｌｓｅ」であることを示している。
【０１６０】
「事後条件」の「画面．ユーザ」は、ポイント追加通知画面３１１０またはポイント追加通知画面３１２０または商品選択画面４２０に表示される「ユーザ」を示している。「事後条件」の「テーブルＴ［画面．ユーザ］．残高」は、ＤＢ４６０の変数であり、ポイント追加通知画面３１１０またはポイント追加通知画面３１２０または商品選択画面４２０に表示される「ユーザ」に対応付けられた残高を示している。「事後条件」の「テーブルＴ＠イベント前［画面．ユーザ］．残高」は、ＤＢ４６０の変数であり、ログインボタン４１３が押される前（イベント前）においてポイント追加通知画面３１１０またはポイント追加通知画面３１２０または商品選択画面４２０に表示される「ユーザ」に対応付けられた残高を示している。
【０１６１】
プロパティＰ３の「事後条件」は、ポイント追加通知画面３１１０に表示される「ユーザ」に対応付けられた残高に１００００ポイントを加算することを示している。プロパティＰ４の「事後条件」は、ポイント追加通知画面３１２０に表示される「ユーザ」に対応付けられた残高に５０００ポイントを加算することを示している。プロパティＰ５の「事後条件」は、商品選択画面４２０の「ユーザ」に対応付けられた残高をそのまま維持することを示している。
【０１６２】
したがって、プロパティＰ３は、入力ボックス４１１の値が示すユーザが当選者であり、ユーザの残高が１００００ポイント以上である状態でログインボタン４１３が押されると、ユーザの残高に１００００ポイントが加算されることを示す。また、プロパティＰ４は、入力ボックス４１１の値が示すユーザが当選者であり、ユーザの残高が１００００ポイント未満である状態でログインボタン４１３が押されると、ユーザの残高に５０００ポイントが加算されることを示す。また、プロパティＰ５は、入力ボックス４１１の値が示すユーザが当選者でない状態でログインボタン４１３が押されると、ユーザの残高がそのまま維持されることを示す。
【０１６３】
図３４は、実施の形態２にかかる画面項目情報１１の一例を示す図である。実施の形態２にかかる画面項目情報１１の「ログイン画面」、「商品選択画面」、「支払確認画面」および「支払結果画面」は、図７に示した画面項目情報１１と同様である。「画面名」の「当選表示画面」は、図３１に示したポイント追加通知画面３１１０，３１２０を示している。「当選表示画面」に対応する「画面項目リスト」には、ポイント追加通知画面３１１０，３１２０に表示される「ユーザ」と「ポイント」が含まれている。
【０１６４】
図３５は、実施の形態２にかかるＤＢ項目情報１２の一例を示す図である。実施の形態２にかかるＤＢ項目情報１２においては、「テーブル名」が「テーブルＴ」の「ＤＢ項目リスト」を示している。「ＤＢ項目リスト」には、「ユーザ」、「残高」および「当選者」が含まれている。また、「レコード数」は「３」となっており、「ユーザ」と「残高」の「ＤＢ項目リスト」に３つ含まれていることを示している。
【０１６５】
実施の形態２にかかるイベント前画面情報１４については、図１０に示したイベント前画面情報１４と同様であるため説明を省略する。
【０１６６】
図３６は、実施の形態２にかかる共通制約情報１３の一例を示す図である。共通制約情報１３は、「共通制約条件名」が「Ｃ１」と「Ｃ２」の２つの共通制約条件を示している。「共通制約条件Ｃ１」は、図９に示した「共通制約条件Ｃ」と同じ共通制約条件であるため説明を省略する。「共通制約条件Ｃ２」は、テーブルＴのレコードｒｅｃについて、ｒｅｃ．当選者＝ｔｒｕｅとなるレコードｒｅｃの数は１であることを示している。すなわち、「共通制約条件Ｃ２」は、ＤＢ４６０の各レコードにおいて当選者であるユーザは一人だけであることを示している。
【０１６７】
（変数分類動作の例）
図３２のステップＳ３２０１（変数分類動作）については、図１１に示した変数分類動作と同様であるため説明を省略する。
【０１６８】
（変数分類情報の例）
図３７は、実施の形態２にかかる変数分類情報２０の一例を示す図である。変数分類部３２１は、プロパティＰ３の「ログイン」に対応する「ログイン画面」をイベント前画面情報１４から取得し、取得した「ログイン画面」に対応する「ＩＤ：パスワード」を画面項目情報１１から取得する。そして、変数分類部３２１は、取得した「ＩＤ：パスワード」に基づく「画面：ＩＤ」をプロパティＰ３の「画面項目リスト」として変数分類情報２０へ追加する。なお、「画面：パスワード」については事前条件に含まれていないため、変数分類情報２０に追加しなくてもよい。
【０１６９】
また、変数分類部３２１は、プロパティＰ４，Ｐ５についても同様に、「ログイン」に対応する「ログイン画面」をイベント前画面情報１４から取得し、取得した「ログイン画面」に対応する「ＩＤ：パスワード」を画面項目情報１１から取得する。そして、変数分類部３２１は、取得した「ＩＤ：パスワード」に基づく「画面：ＩＤ」をプロパティＰ４，Ｐ５の「画面項目リスト」として変数分類情報２０へ追加する。
【０１７０】
また、変数分類部３２１は、ＤＢ項目情報１２からＤＢ項目リストを取得する。そして、変数分類部３２１は、取得したＤＢ項目リストのうちのプロパティＰ３，Ｐ４の「事前条件」に含まれる「テーブルＴ．残高：テーブルＴ．当選者」をプロパティＰ３，Ｐ４の「ＤＢ項目リスト」として変数分類情報２０に追加する。また、変数分類部３２１は、取得したＤＢ項目リストのうちのプロパティＰ５の「事前条件」に含まれる「テーブルＴ．当選者」をプロパティＰ５の「ＤＢ項目リスト」として変数分類情報２０に追加する。
【０１７１】
（変数変換動作の例）
図３２のステップＳ３２０２（変数変換動作）については、図１３に示した変数変換動作と同様であるため説明を省略する。
【０１７２】
（固有変数情報の例）
図３８は、実施の形態２にかかる固有変数情報２１の一例を示す図である。変数変換部３２２は、変数分類情報２０のプロパティＰ３に対応付けられた画面項目変数である「画面．ＩＤ」を識別変数「画面Ｐ３．ＩＤ」に変換する。また、変数変換部３２２は、プロパティＰ４に対応付けられた画面項目変数である「画面．ＩＤ」を識別変数「画面Ｐ４．ＩＤ」に変換する。また、変数変換部３２２は、プロパティＰ５に対応付けられた画面項目変数である「画面．ＩＤ」を識別変数「画面Ｐ５．ＩＤ」に変換する。
【０１７３】
そして、変数変換部３２２は、「プロパティ名」と、識別変数を示す「変換後画面項目リスト」と、を対応付けた固有変数情報２１を生成する。なお、ここでは変数名に「プロパティ名」を付加することで変数を識別変数「画面Ｐ５．ＩＤ」に変換する場合について説明したが、変数名の変換方法はこれに限らず、変換後の各識別変数が事前条件ごと（あるいはプロパティごと）に識別可能な変数であればよい。
【０１７４】
（条件変換動作の例）
図３２のステップＳ３２０３（条件変換動作）については、図１５に示した条件変換動作と同様であるため説明を省略する。
【０１７５】
（変換後事前条件情報の例）
図３９は、実施の形態２にかかる変換後事前条件情報２２の一例を示す図である。条件変換部３２３は、プロパティ情報１０のプロパティＰ３に対応付けられた「事前条件」に含まれる画面項目変数を、固有変数情報２１のプロパティＰ３に対応付けられた「変換後画面項目リスト」が示す識別変数により変換する。具体的には、条件変換部３２３は、プロパティＰ３の事前条件の「画面．ＩＤ」を識別変数「画面Ｐ３．ＩＤ」に変換する。
【０１７６】
同様に、条件変換部３２３は、プロパティ情報１０のプロパティＰ４，Ｐ５に対応付けられた「事前条件」に含まれる画面項目変数を、固有変数情報２１のプロパティＰ４，Ｐ５に対応付けられた「変換後画面項目リスト」が示す識別変数により変換する。具体的には、条件変換部３２３は、プロパティＰ４の事前条件の「画面．ＩＤ」を識別変数「画面Ｐ４．ＩＤ」に変換するとともに、プロパティＰ５の事前条件の「画面．ＩＤ」を識別変数「画面Ｐ５．ＩＤ」に変換する。
【０１７７】
（極小データ生成動作の例）
図４０は、図３２のステップＳ３２０４の一例を示すフローチャートである。算出部３３０は、まず、データ未生成プロパティ情報４０を参照することで、極小データを未生成のプロパティが存在するか否かを判断する（ステップＳ４００１）。極小データを未生成のプロパティが存在する場合（ステップＳ４００１：Ｙｅｓ）は、極小データを未生成のプロパティのうちの未取得のプロパティの部分集合を取得する（ステップＳ４００２）。ステップＳ４００２においては、たとえば、部分集合の要素数（プロパティの数）が最も大きくなるように部分集合を取得する。
【０１７８】
つぎに、ステップＳ４００２によって取得された部分集合の極小データを生成する（ステップＳ４００３）。つぎに、ステップＳ４００３による極小データの生成が成功したか否かを判断する（ステップＳ４００４）。ステップＳ４００３による極小データの生成が成功していない場合（ステップＳ４００４：Ｎｏ）は、ステップＳ４００２によって取得された部分集合の要素数が１か否かを判断する（ステップＳ４００５）。
【０１７９】
ステップＳ４００５において、取得された部分集合の要素数が１でない場合（ステップＳ４００５：Ｎｏ）は、ステップＳ４００２に戻る。取得された部分集合の要素数が１である場合（ステップＳ４００５：Ｙｅｓ）は、一連の動作を終了する。ステップＳ４００４において、極小データの生成が成功した場合（ステップＳ４００４：Ｙｅｓ）は、還元部３４０が、ステップＳ４００３によって生成された極小データに含まれる識別変数を画面項目変数に還元する（ステップＳ４００６）。
【０１８０】
つぎに、算出部３３０が、データ未生成プロパティ情報４０を更新し（ステップＳ４００７）、ステップＳ４００１へ戻る。ステップＳ４００１において、極小データを未生成のプロパティが存在しない場合（ステップＳ４００１：Ｎｏ）は、一連の動作を終了する。図４０に示した各ステップによって、極小データを生成するとともに、生成した極小データに含まれる識別変数を画面項目変数に還元することができる。
【０１８１】
図４１は、図４０のステップＳ４００３の一例を示すフローチャートである。算出部３３０は、まず、制約条件式２３を恒真式に設定する（ステップＳ４１０１）。つぎに、ステップＳ４１０１によって設定された制約条件式２３に、ステップＳ４００２によって取得された部分集合に含まれる各プロパティの各変換後事前条件を論理積（ａｎｄ）で結合する（ステップＳ４１０２）。
【０１８２】
図４１に示すステップＳ４１０３，Ｓ４１０４は、図１７に示したステップＳ１７０３，Ｓ１７０４と同様であるため説明を省略する。図４１に示す各ステップにより、ステップＳ４００２によって取得された部分集合の極小データを生成することができる。
【０１８３】
図４２は、図４１のステップＳ４１０４の一例を示すフローチャートである。図４２に示すステップＳ４２０１〜Ｓ４２０８は、図１９に示したステップＳ１９０１〜Ｓ１９０８と同様であるため説明を省略する。ステップＳ４２０２において制約条件式２３を満たす各変数の値が存在しない場合（ステップＳ４２０２：Ｎｏ）、およびステップＳ４２０７において、選択された変数が識別変数でない場合（ステップＳ４２０７：Ｎｏ）は、ステップＳ４２０９へ移行する。すなわち、ＤＢデータ情報２５のＤＢデータ名に対応するエントリを削除し（ステップＳ４２０９）、一連の動作を終了する。ただし、選択された変数が識別変数でない場合（ステップＳ４２０２：Ｎｏ）、一連の動作を終了せず、Ｓ４２０３へ戻ってもよい。
【０１８４】
図４２に示した各ステップにより、ステップＳ４１０３によって結合された制約条件式２３を用いて極小データを生成することができる。生成される極小データには、ＤＢデータ情報２５と還元前画面データ情報２４が含まれている。
【０１８５】
図４３は、図４０のステップＳ４００６の一例を示すフローチャートである。還元部３４０は、まず、ステップＳ４００２によって取得された部分集合に含まれるすべてのプロパティを選択したか否かを判断する（ステップＳ４３０１）。図４３に示すステップＳ４３０２〜Ｓ４３０７は、図２４に示したステップＳ２４０２〜Ｓ２４０７と同様であるため説明を省略する。
【０１８６】
すべての識別変数を還元した場合（ステップＳ４３０６：Ｙｅｓ）は、プロパティ名と画面データ名とＤＢデータ名の組をプロパティ対応テーブル（図２６参照）へ追加し（ステップＳ４３０８）、ステップＳ４３０１へ戻る。図４３に示した各ステップにより、ステップＳ４００２によって生成された極小データに含まれる識別変数を画面項目変数に還元し、還元結果を示す画面データ情報２６を得ることができる。
【０１８７】
図４４は、データ未生成プロパティ情報４０（その１）の一例を示す図である。算出部３３０は、図４４に示すデータ未生成プロパティ情報４０を管理することでプロパティごとに極小データを生成したか否かの情報を管理する。データ未生成プロパティ情報４０は「プロパティ名」と「データ生成済フラグ」とを対応付ける情報である。
【０１８８】
「データ生成済フラグ」は、対応するプロパティを含む部分集合の極小データを生成したか否かを示す情報である。極小データが生成されていない場合は「データ生成済フラグ」の値は「ｆａｌｓｅ」となる。極小データが生成されている場合は「データ生成済フラグ」の値は「ｔｒｕｅ」となる。初期状態においては、プロパティＰ３〜Ｐ５のすべての「データ生成済フラグ」の値は「ｆａｌｓｅ」になっている。
【０１８９】
（制約条件式の例）
図４５は、実施の形態２にかかる制約条件式２３（Ｐ３，Ｐ４，Ｐ５）の一例を示す図である。図４０のステップＳ４００２の１ループ目においては、すべてのプロパティが部分集合として取得される。したがって、制約条件式２３は、図４５に示すように、変換後事前条件情報２２が示すプロパティＰ３，Ｐ４，Ｐ５の各「変換後事前条件」と、共通制約情報１３が示す共通制約条件Ｃ１，Ｃ２と、をすべて満たすべき旨の条件となる。
【０１９０】
ここで、図４５に示す制約条件式２３を満たす検査データは存在しないとする。この場合は、ステップＳ４００３による極小データの生成が成功せず、ステップＳ４００２の２ループ目においては、プロパティＰ３，Ｐ４，Ｐ５のうちの一部のプロパティを除いた部分集合が取得される。
【０１９１】
図４６は、取得される部分集合の一例を示す図である。図４６に示す部分集合４６０１〜４６０６のそれぞれは、プロパティ情報１０が示すプロパティＰ３，Ｐ４，Ｐ５の部分集合を示している。算出部３３０は、部分集合４６０１〜４６０６のうちの要素数が大きい部分集合を優先的に取得する。たとえば、算出部３３０は、部分集合４６０１，４６０２，４６０３，４６０４，４６０５，４６０６の順に取得する。
【０１９２】
たとえば、ステップＳ４００２の２ループ目において部分集合４６０１が取得される。そして、部分集合４６０１の各「変換後事前条件」と、共通制約情報１３が示す共通制約条件Ｃ１，Ｃ２と、をすべて満たす検査データが存在しなかったとする（充足不能）。この場合は、ステップＳ４００２の３ループ目において部分集合４６０２が取得される。
【０１９３】
図４７は、実施の形態２にかかる制約条件式２３（Ｐ３，Ｐ５）の一例を示す図である。ステップＳ４００２の３ループ目において部分集合４６０２が取得されると、制約条件式２３は、図４７に示すように、プロパティＰ３，Ｐ５の各「変換後事前条件」と、共通制約情報１３が示す共通制約条件Ｃ１，Ｃ２と、をすべて満たすべき旨の条件となる。
【０１９４】
ここで、図４７に示す制約条件式２３を満たす検査データが存在するとする（充足可能）。この場合は、ステップＳ４００３による極小データの生成が成功し、ステップＳ４００６により、部分集合４６０２に含まれるプロパティＰ３，Ｐ５における識別変数が画面項目変数に還元される。
【０１９５】
図４８は、実施の形態２にかかるデータ未生成プロパティ情報４０（その２）の一例を示す図である。ステップＳ４００６により、部分集合４６０２に含まれるプロパティＰ３，Ｐ５における識別変数が画面項目変数に還元されると、ステップＳ４００７により、データ未生成プロパティ情報４０が更新される。具体的には、部分集合４６０２に含まれるプロパティＰ３，Ｐ５の「データ生成済フラグ」の値が「ｔｒｕｅ」になる。
【０１９６】
図４０のステップＳ４００１の２ループ目においては、データ未生成プロパティ情報４０のプロパティＰ４の「データ生成済フラグ」がまだ「ｆａｌｓｅ」であるため、極小データを未生成のプロパティが存在すると判断される。そして、ステップＳ４００２においては、「データ生成済フラグ」の値が「ｆａｌｓｅ」であるプロパティＰ４が部分集合として取得される。すなわち、図４６に示した部分集合４６０５が取得される。
【０１９７】
図４９は、実施の形態２にかかる制約条件式２３（Ｐ４）の一例を示す図である。ステップＳ４００２において部分集合４６０５が取得されると、制約条件式２３は、図４９に示すように、プロパティＰ４の「変換後事前条件」と、共通制約情報１３が示す共通制約条件Ｃ１，Ｃ２と、をすべて満たすべき条件となる。
【０１９８】
ここで、図４９に示す制約条件式２３を満たす検査データが存在したとする。この場合は、ステップＳ４００３による極小データの生成が成功し、ステップＳ４００６においてプロパティＰ４の識別変数が画面項目変数に還元される。
【０１９９】
図５０は、実施の形態２にかかるデータ未生成プロパティ情報４０（その３）の一例を示す図である。ステップＳ４００６により、部分集合４６０５に含まれるプロパティＰ４における識別変数が画面項目変数に還元されると、ステップＳ４００７により、データ未生成プロパティ情報４０が更新される。具体的には、部分集合４６０５に含まれるプロパティＰ４の「データ生成済フラグ」の値が「ｔｒｕｅ」になる。
【０２００】
図４０のステップＳ４００１の３ループ目においては、データ未生成プロパティ情報４０のプロパティＰ３〜Ｐ５の「データ生成済フラグ」がすべて「ｔｒｕｅ」であるため、極小データを未生成のプロパティが存在しないと判断される。
【０２０１】
（制約条件式を満たす各変数の値の例）
図５１は、実施の形態２にかかる制約条件式を満たす検査データの算出例を示す図である。生成データ２０００は、図４２のステップＳ４２０１による各変数の値の算出結果の一例を示している。生成データ２０００に示す各変数のうちの「テーブルＴ［１］．ユーザ」、「テーブルＴ［１］．残高」、「テーブルＴ［１］．当選者」、「テーブルＴ［２］．ユーザ」、「テーブルＴ［２］．残高」、「テーブルＴ［２］．当選者」、「テーブルＴ［３］．ユーザ」、「テーブルＴ［３］．残高」および「テーブルＴ［３］．当選者」はＤＢ項目変数である。また、生成データ２０００に示す各変数のうちの「画面Ｐ３．ＩＤ」および「画面Ｐ５．ＩＤ」は、画面項目変数を変換した識別変数である。
【０２０２】
（ＤＢデータ情報の例）
図５２は、実施の形態２にかかるＤＢデータ情報２５の一例を示す図である。ＤＢデータ情報２５は、「ＤＢデータ名」と「ＤＢテーブル名」と「ＤＢテーブル値リスト」とを対応付ける情報である。「ＤＢデータ名」の「ＤＢデータＰ３Ｐ５」は、プロパティＰ３，Ｐ５を検査するためのＤＢデータを示している。「ＤＢデータ名」の「ＤＢデータＰ４」は、プロパティＰ４を検査するためのＤＢデータを示している。データ算出部３３２は、生成データ２０００（図５１参照）が示す各変数のうちのＤＢ項目変数に基づいてＤＢデータ情報２５を生成する。
【０２０３】
図５３は、図５２に示したＤＢデータ情報２５が表現するテーブル（その１）を示す図である。ＤＢデータ情報２５（図５２参照）の「ＤＢデータＰ３Ｐ５」は、テーブル５５００を表現している。テーブル５５００に示すように、「ｕｓｅｒ１」には残高として「１００００」が対応付けられ、「ｕｓｅｒ２」には残高として「１０００」が対応付けられ、「ｕｓｅｒ３」には残高として「２０００」が対応付けられている。また、当選者は「ｕｓｅｒ１」となっている。
【０２０４】
図５４は、図５２に示したＤＢデータ情報２５が表現するテーブル（その２）を示す図である。ＤＢデータ情報２５（図５２参照）の「ＤＢデータＰ４」は、テーブル５６００を表現している。テーブル５６００に示すように、「ｕｓｅｒ１」には残高として「５０００」が対応付けられ、「ｕｓｅｒ２」には残高として「１０００」が対応付けられ、「ｕｓｅｒ３」には残高として「２０００」が対応付けられている。また、当選者は「ｕｓｅｒ１」となっている。
【０２０５】
（還元前画面データ情報の例）
図５５は、実施の形態２にかかる還元前画面データ情報の一例を示す図である。還元前画面データ情報２４は、「画面項目名」と「画面項目値」とを対応付ける情報である。「画面項目名」は、変換後事前条件情報２２に含まれる識別変数を示している。「画面項目値」は、「画面項目名」が示す識別変数に代入される値を示している。データ算出部３３２は、生成データ２０００（図５１参照）が示す各変数のうちの識別変数に基づいて還元前画面データ情報２４を生成する。
【０２０６】
（プロパティ対応テーブルの例）
図５６は、実施の形態２にかかるプロパティ対応テーブルの一例を示す図である。図５６に示すプロパティ対応テーブル２６００は、「プロパティ名」と「画面データ名」と「ＤＢデータ名」とを対応付ける情報である。算出部３３０は、たとえばプロパティＰ３に対して「画面データＰ３」と「ＤＢデータＰ３Ｐ５」を対応付けるとともに、プロパティＰ５に対して「画面データＰ５」と「ＤＢデータＰ３Ｐ５」を対応付け、プロパティ対応テーブル２６００を生成する。
【０２０７】
（画面データ情報の例）
図５７は、実施の形態２にかかる画面データ情報２６の一例を示す図である。たとえば、還元部３４０は、還元前画面データ情報２４の「画面Ｐ３．ＩＤ」が固有変数情報２１において対応付けられているプロパティＰ３を取得する。そして、還元部３４０は、取得したプロパティＰ３がプロパティ対応テーブル２６００において対応付けられている「画面データＰ３」を取得する。
【０２０８】
さらに、還元部３４０は、取得したプロパティＰ３に対応する固有変数情報２１の「変換後画面項目リスト」と取得したプロパティＰ３に対応する変数分類情報２０の「画面項目リスト」から、還元前画面データ情報２４の「画面Ｐ３．ＩＤ」に対応する変換前の画面項目変数「画面．ＩＤ」を取得する。さらに、還元部３４０は、プロパティＰ３のイベント「ログイン」に対応するイベント前画面情報１４の「ログイン画面」を取得する。
【０２０９】
そして、還元部３４０は、取得した「ログイン画面」に対応する画面項目情報１１の「画面項目リスト」において、変数分類情報２０から取得した変換前の画面項目変数「画面．ＩＤ」に対応する「ＩＤ」を取得する。そして、還元部３４０は、取得した「画面データＰ３」と、画面項目情報１１から取得した「ＩＤ」と、還元前画面データ情報２４の「画面Ｐ３．ＩＤ」に対応付けられた「ｕｓｅｒ１」と、を対応付けて「画面項目値リスト」に追加する。
【０２１０】
同様に、還元部３４０は、還元前画面データ情報２４の「画面Ｐ５．ＩＤ」が固有変数情報２１において対応付けられているプロパティＰ５を取得する。そして、還元部３４０は、取得したプロパティＰ５がプロパティ対応テーブル２６００において対応付けられている「画面データＰ５」を取得する。
【０２１１】
さらに、還元部３４０は、取得したプロパティＰ５に対応する固有変数情報２１の「変換後画面項目リスト」と取得したプロパティＰ５に対応する変数分類情報２０の「画面項目リスト」から、還元前画面データ情報２４の「画面Ｐ５．ＩＤ」に対応する変換前の画面項目変数「画面．ＩＤ」を取得する。さらに、還元部３４０は、プロパティＰ５のイベント「ログイン」に対応するイベント前画面情報１４の「ログイン画面」を取得する。
【０２１２】
そして、還元部３４０は、取得した「ログイン画面」に対応する画面項目情報１１の「画面項目リスト」において、変数分類情報２０から取得した変換前の画面項目変数「画面．ＩＤ」に対応する「ＩＤ」を取得する。そして、還元部３４０は、取得した「画面データＰ５」と、画面項目情報１１から取得した「ＩＤ」と、還元前画面データ情報２４の「画面Ｐ５．ＩＤ」に対応付けられた「ｕｓｅｒ２」と、を対応付けて「画面項目値リスト」に追加する。
【０２１３】
（検査データの適用例）
図５８は、実施の形態２にかかる検査データの適用例を示す図である。図５８に示すように、画面データ情報２６の「画面データＰ３」が設定されると、図４のログイン画面４１０は符号５８１０のようになる。また、画面データ情報２６の「画面データＰ４」が設定されると、図４のログイン画面４１０は符号５８２０のようになる。また、画面データ情報２６の「画面データＰ５」が設定されると、図４のログイン画面４１０は符号５８３０のようになる。また、符号５８１０または符号５８３０の場合は、ＤＢ４６０に設定されるテーブルは共通でテーブル５５００（図５３参照）となる。また、符号５８２０の場合は、ＤＢ４６０に設定されるテーブルはテーブル５６００（図５４参照）となる。
【０２１４】
このように、実施の形態２にかかる検査データ生成装置３００は、画面項目変数（第一変数）を識別変数に変換した各事前条件をすべて満たす検査データが存在しない場合は、各事前条件のうちの一部の事前条件をすべて満たす検査データを算出する。これにより、同時に充足不能な複数の事前条件を有する検査対象プログラム１１０であっても、ＤＢ項目変数（第二変数）の一部を共通化した検査データを得ることができる。ＤＢ項目変数の一部を共通化することで、モデル検査にかかる時間を短縮することができるため、検査対象プログラム１１０を効率よく検査することが可能になる。
【０２１５】
以上説明したように、検査データ生成装置、検査データ生成方法および検査データ生成プログラムによれば、事前条件に含まれる第一変数を事前条件ごとに異なる識別変数に変換し、変換した各事前条件を満たす検査データを得ることができる。これにより、同時に充足不能な複数の事前条件を有する検査対象プログラムであっても、第二変数を共通化した検査データを得ることができるため、検査対象プログラムを効率よく検査できる。
【０２１６】
また、検査対象プログラムは、画面上の項目を示す画面項目変数とデータベースの項目を示すデータベース項目変数とに基づく処理を行うプログラムとすることで、データベース項目変数を共通化した検査データを得ることができる。モデル検査のたびに設定し直されるデータベース変数の検査データを共通化することで、モデル検査にかかる時間をさらに短縮することができる。
【０２１７】
また、条件情報が示す各事前条件の各変数を第一変数と第二変数に分類し、分類された第一変数に対して事前条件ごとに異なる識別子を付加して識別変数に変換し、変換された識別変数によって各事前条件の第一変数を変換するようにしてもよい。これにより、事前条件に含まれる第一変数を事前条件ごとに異なる識別変数に変換することができる。
【０２１８】
また、第一変数が識別変数に変換された各事前条件をすべて満たすべき旨の制約条件式を生成し、生成された制約条件式を満たす識別変数と第二変数との検査データを算出するようにしてもよい。これにより、第一変数が識別変数に変換された各事前条件をすべて満たす検査データを算出することができる。
【０２１９】
また、第一変数が識別変数に変換された各事前条件と、複数の仕様に共通の共通制約条件と、をすべて満たす検査データを算出するようにしてもよい。これにより、共通制約条件も同時に考慮した場合に同時に充足不能な複数の事前条件を有する検査対象プログラムであっても、第二変数を共通化した検査データを得ることができる。また、識別変数の検査データを第一変数に還元して出力することで、出力された各検査データのいずれを第一変数に設定すべきかをユーザにとってより分かりやすくすることができる。
【０２２０】
また、第一変数を識別変数に変換した各事前条件をすべて満たす検査データが存在しない場合は、各事前条件のうちの一部の事前条件をすべて満たす検査データを算出する。これにより、同時に充足不能な複数の事前条件を有する検査対象プログラムであっても、第二変数の一部を共通化した検査データを得ることができる。また、各事前条件から、検査データを算出した一部の事前条件を除いた事前条件をすべて満たす検査データを算出することで、検査対象プログラムのすべての仕様に対応する検査データを得ることができる。
【０２２１】
なお、本実施の形態で説明した検査データ生成方法は、あらかじめ用意されたプログラムをパーソナルコンピュータやワークステーションなどのコンピュータで実行することにより実現することができる。このプログラムに含まれる各モジュールがＣＰＵに読み込まれて実行されることにより、プロセスが生成される。この各プロセスが、変換部、算出部、変数分類部、条件生成部等の手段に相当する。本検査データ生成プログラムは、ハードディスク、フレキシブルディスク、ＣＤ−ＲＯＭ、ＭＯ、ＤＶＤなどのコンピュータで読み取り可能な記録媒体に記録され、コンピュータによって記録媒体から読み出されることによって実行される。また本検査データ生成プログラムは、インターネットなどのネットワークを介して配布してもよい。
【０２２２】
また、本実施の形態で説明した検査データ生成装置３００は、スタンダードセルやストラクチャードＡＳＩＣ（Ａｐｐｌｉｃａｔｉｏｎ  Ｓｐｅｃｉｆｉｃ  Ｉｎｔｅｇｒａｔｅｄ  Ｃｉｒｃｕｉｔ）などの特定用途向けＩＣ（以下、単に「ＡＳＩＣ」と称す。）やＦＰＧＡなどのＰＬＤ（Ｐｒｏｇｒａｍｍａｂｌｅ  Ｌｏｇｉｃ  Ｄｅｖｉｃｅ）によっても実現することができる。具体的には、たとえば、検査データ生成装置３００の機能（入力部３１０、変換部３２０、算出部３３０、還元部３４０および出力部３５０）をＨＤＬ記述によって機能定義し、そのＨＤＬ記述を論理合成してＡＳＩＣやＰＬＤに与えることにより、検査データ生成装置３００を製造することができる。
【０２２３】
上述した実施の形態に関し、さらに以下の付記を開示する。
【０２２４】
（付記１）変数を含む所定の事前条件に対して所定の事後条件を満たす仕様を複数有する検査対象プログラムの検査データを生成する検査データ生成装置において、
前記仕様ごとの前記事前条件を示す条件情報を入力する入力手段と、
前記入力手段によって入力された条件情報が示す各事前条件の前記変数を前記事前条件ごとに異なる識別変数に変換する変換手段と、
前記変換手段によって前記変数が前記識別変数に変換された前記各事前条件を、検査データを算出する算出手段に送信する送信手段と、
前記算出手段による算出結果を受信して出力する出力手段と、
を備えることを特徴とする検査データ生成装置。
【０２２５】
（付記２）前記変数は、画面上の項目を示す画面項目変数である第一変数、及びデータベースの項目を示すデータベース項目変数である第二変数を含み、
前記変換手段は、
前記条件情報が示す各事前条件の各変数を前記第一変数と前記第二変数に分類する分類手段と、
前記分類手段によって分類された第一変数に対して前記事前条件ごとに異なる識別子を付加して前記識別変数に変換する変数変換手段と、
前記変数変換手段によって変換された前記識別変数によって前記各事前条件の前記第一変数を変換する条件変換手段と、
を備えることを特徴とする付記１に記載の検査データ生成装置。
【０２２６】
（付記３）前記算出手段は、
前記変換手段によって前記第一変数が前記識別変数に変換された前記各事前条件をすべて満たすべき旨の制約条件式を生成する条件生成手段と、
前記条件生成手段によって生成された制約条件式を満たす前記識別変数と前記第二変数との検査データを算出するデータ算出手段と、
を備えることを特徴とする付記２に記載の検査データ生成装置。
【０２２７】
（付記４）前記条件生成手段は、前記変換手段によって前記第一変数が前記識別変数に変換された前記各事前条件と、複数の前記仕様に共通の共通制約条件と、をすべて満たす前記識別変数と前記第二変数との検査データを算出することを特徴とする付記３に記載の検査データ生成装置。
【０２２８】
（付記５）前記算出手段によって算出された前記識別変数の検査データを前記変数に還元する還元手段を備え、
前記出力手段は、前記還元手段によって還元された前記変数の検査データを出力することを特徴とする付記１〜４のいずれか一つに記載の検査データ生成装置。
【０２２９】
（付記６）前記算出手段は、前記各事前条件をすべて満たす前記識別変数と前記第二変数との検査データが存在しない場合は、前記各事前条件のうちの一部の事前条件をすべて満たす前記識別変数と前記第二変数との検査データを算出することを特徴とする付記２に記載の検査データ生成装置。
【０２３０】
（付記７）前記算出手段は、前記各事前条件から前記一部の事前条件を除いた事前条件をすべて満たす前記識別変数と前記第二変数との検査データを算出することを特徴とする付記６に記載の検査データ生成装置。
【０２３１】
（付記８）変数を含む所定の事前条件に対して所定の事後条件を満たす仕様を複数有する検査対象プログラムの検査データを生成する検査データ生成方法において、
前記仕様ごとの前記事前条件を示す条件情報を入力する入力工程と、
前記入力工程によって入力された条件情報が示す各事前条件の前記変数を前記事前条件ごとに異なる識別変数に変換する変換工程と、
前記変換工程によって前記変数が前記識別変数に変換された前記各事前条件を、検査データを算出する算出工程に送信する送信工程と、
前記算出工程による算出結果を受信して出力する出力工程と、
を含むことを特徴とする検査データ生成方法。
【０２３２】
（付記９）変数を含む所定の事前条件に対して所定の事後条件を満たす仕様を複数有する検査対象プログラムの検査データを生成するコンピュータに、
前記仕様ごとの前記事前条件を示す条件情報を入力する入力手段と、
前記入力手段によって入力された条件情報が示す各事前条件の前記変数を前記事前条件ごとに異なる識別変数に変換する変換手段と、
前記変換手段によって前記変数が前記識別変数に変換された前記各事前条件を、検査データを算出する算出手段に送信する送信手段と、
前記算出手段による算出結果を受信して出力する出力手段と、
を実行させることを特徴とする検査データ生成プログラム。
【符号の説明】
【０２３３】
１１０  検査対象プログラム
１１１，１１２  プロパティ
１１１ａ，１１２ａ  事前条件
１１１ｂ，１１２ｂ  事後条件
１２１，１２２  プログラム状態
１２１ａ，１２２ａ  画面
１２１ｂ，１２２ｂ，４６０  ＤＢ
１３１  条件情報
１３２  事前条件群
１３４  検査データ群
１３４ａ〜１３４ｃ  検査データ
４１０  ログイン画面
４１１，４１２  入力ボックス
４１３  ログインボタン
４２０  商品選択画面
４２２  ログアウトボタン
４２３  支払ボタン
４３０  支払確認画面
４３１  購入ボタン
４３２，４４１，４５１  戻るボタン
４４０，４５０  支払結果画面
２０００  生成データ
２６００  プロパティ対応テーブル
３１１０，３１２０  ポイント追加通知画面
３１１１，３１２１  続行ボタン
４６０１〜４６０６  部分集合
【図１−１】
2011081653.tif 000003
【図１−２】
2011081653.tif 000004
【図１−３】
2011081653.tif 000005
【図２】
2011081653.tif 000006
【図３】
2011081653.tif 000007
【図４】
2011081653.tif 000008
【図５】
2011081653.tif 000009
【図６】
2011081653.tif 000010
【図７】
2011081653.tif 000011
【図８】
2011081653.tif 000012
【図９】
2011081653.tif 000013
【図１０】
2011081653.tif 000014
【図１１】
2011081653.tif 000015
【図１２】
2011081653.tif 000016
【図１３】
2011081653.tif 000017
【図１４】
2011081653.tif 000018
【図１５】
2011081653.tif 000019
【図１６】
2011081653.tif 000020
【図１７】
2011081653.tif 000021
【図１８】
2011081653.tif 000022
【図１９】
2011081653.tif 000023
【図２０】
2011081653.tif 000024
【図２１】
2011081653.tif 000025
【図２２】
2011081653.tif 000026
【図２３】
2011081653.tif 000027
【図２４】
2011081653.tif 000028
【図２５】
2011081653.tif 000029
【図２６】
2011081653.tif 000030
【図２７】
2011081653.tif 000031
【図２８】
2011081653.tif 000032
【図２９】
2011081653.tif 000033
【図３０】
2011081653.tif 000034
【図３１】
2011081653.tif 000035
【図３２】
2011081653.tif 000036
【図３３】
2011081653.tif 000037
【図３４】
2011081653.tif 000038
【図３５】
2011081653.tif 000039
【図３６】
2011081653.tif 000040
【図３７】
2011081653.tif 000041
【図３８】
2011081653.tif 000042
【図３９】
2011081653.tif 000043
【図４０】
2011081653.tif 000044
【図４１】
2011081653.tif 000045
【図４２】
2011081653.tif 000046
【図４３】
2011081653.tif 000047
【図４４】
2011081653.tif 000048
【図４５】
2011081653.tif 000049
【図４６】
2011081653.tif 000050
【図４７】
2011081653.tif 000051
【図４８】
2011081653.tif 000052
【図４９】
2011081653.tif 000053
【図５０】
2011081653.tif 000054
【図５１】
2011081653.tif 000055
【図５２】
2011081653.tif 000056
【図５３】
2011081653.tif 000057
【図５４】
2011081653.tif 000058
【図５５】
2011081653.tif 000059
【図５６】
2011081653.tif 000060
【図５７】
2011081653.tif 000061
【図５８】
2011081653.tif 000062