"コンピュータが、テスト対象のプログラムの入力データに関する事前条件を表した論理式が記憶された記憶部を参照して、前記論理式に存在記号が含まれているか否かを判定し、前記判定において含まれると判定した場合、前記論理式から前記存在記号と当該存在記号の要素を含む入力データを識別する入力データ識別情報とを含む部分述語論理式を抽出し、前記入力データ識別情報で識別されるテーブル毎に該テーブルの行数が記憶された記憶部を参照して、前記部分述語論理式に含まれる入力データ識別情報に対応するテーブルの行数を取得し、前記行数を表す変数の値を、前記取得した行数の最小値、最大値、及び、前記最小値より大きく前記最大値より小さい範囲とする論理式をそれぞれ生成し、前記生成した論理式を論理和で結んだ制約式を生成し、前記記憶部に記憶された前記論理式に含まれる前記部分述語論理式を前記生成した制約式との論理積に変換する、処理を実行することを特徴とする論理式変換プログラム。前記論理式に否定が係る論理積が含まれるか否かを判定し、前記判定において前記否定が係る論理積が含まれると判定した場合に、前記記憶部に記された前記否定が係る論理積で示される論理式のデータを、前記論理積の左辺及び右辺の論理式に各々否定が係る論理式及び該否定が係る論理式のうちの一方を左辺、他方を右辺とする論理和で示される論理式のデータに変換する、処理を前記コンピュータに実行させることを特徴とする請求項1に記載の論理式変換プログラム。前記論理式に否定が係る論理和が含まれるか否かを判定し、前記判定において前記否定が係る論理和が含まれると判定した場合に、前記記憶部に記憶された前記否定が係る論理和で示される論理式のデータを、前記論理和演算子の左辺及び右辺の論理式の各々に否定が係り、該否定が係る論理式のうちの一方を左辺、他方を右辺とする論理積で示される論理式のデータに変換する、処理を前記コンピュータに実行させることを特徴とする請求項1または2に記載の論理式変換プログラム。前記論理式に含意が含まれるか否かを判定し、前記判定において前記含意が含まれると判定した場合に、前記記憶部に記憶された前記含意で示される論理式のデータを、前記含意の左辺の論理式に否定が付いた第1の論理式と、前記第1の論理式と、前記含意の右辺のうち、一方を左辺、他方を右辺とする論理積で示される論理式とに変換する、処理を前記コンピュータに実行させることを特徴とする請求項1から3のいずれかに記載の論理式変換プログラム。前記論理式に論理積が係る論理和が含まれるか否かを判定し、前記判定において前記論理積が係る論理和が含まれると判定した場合に、前記記憶部に記憶された前記論理積が係る論理和で示される論理式のデータを、前記論理積の左辺を第1の辺とし前記論理和の前記論理積が係らない辺である他方の辺を第2の辺とする第1の論理和と、前記論理積の右辺を第1の辺とし前記他方の辺を第2の辺とする第2の論理和と、前記第1の論理和を第1の辺とし前記第2の論理和を第2の辺とする論理積とで示される論理式のデータに変換する、処理を前記コンピュータに実行させることを特徴とする請求項1から4のいずれかに記載の論理式変換プログラム。前記判定において、前記論理積が係る論理和が含まれないと判定した場合に、前記記憶部に記憶された前記論理式のデータを、論理和を含まず、かつ、論理積で結合された論理式の部分論理式毎に分割し、前記分割した各々の部分論理式のデータを、充足可能性の判定対象の論理式のデータを記憶する記憶部に記憶する、処理を前記コンピュータに実行させることを特徴とする請求項5に記載の論理式変換プログラム。コンピュータによって実行されるテストデータ生成方法であって、テスト対象のプログラムの入力データに関する事前条件を表した論理式が記憶された記憶部を参照して、前記論理式に存在記号が含まれているか否かを判定し、前記判定において含まれると判定した場合、前記論理式から前記存在記号と当該存在記号の要素を含む入力データを識別する入力データ識別情報とを含む部分述語論理式を抽出し、前記入力データ識別情報で識別されるテーブル毎に該テーブルの行数が記憶された記憶部を参照して、前記部分述語論理式に含まれる入力データ識別情報に対応するテーブルの行数を取得し、前記行数を表す変数の値を、前記取得した行数の最小値、最大値、及び、前記最小値より大きく前記最大値より小さい範囲とする論理式をそれぞれ生成し、前記生成した論理式を論理和で結んだ制約式を生成し、前記記憶部に記憶された前記論理式に含まれる前記部分述語論理式を前記生成した制約式との論理積に変換する、ことを特徴とするテストデータ生成方法。テスト対象のプログラムの入力データに関する事前条件を表した論理式が記憶された記憶部を参照して、前記論理式に存在記号が含まれているか否かを判定し、前記判定において含まれると判定した場合、前記論理式から前記存在記号と当該存在記号の要素を含む入力データを識別する入力データ識別情報とを含む部分述語論理式を抽出する抽出部と、前記入力データ識別情報で識別されるテーブル毎に該テーブルの行数が記憶された記憶部を参照して、前記部分述語論理式に含まれる入力データ識別情報に対応するテーブルの行数を取得し、前記行数を表す変数の値を、前記取得した行数の最小値、最大値、及び、前記最小値より大きく前記最大値より小さい範囲とする論理式をそれぞれ生成し、前記生成した論理式を論理和で結んだ制約式を生成し、前記記憶部に記憶された前記論理式に含まれる前記部分述語論理式を前記生成した制約式との論理積に変換する変換部と、前記変換後の論理式に論理積が係る論理和が含まれるか否かを判定し、前記判定において前記論理積が係る論理和が含まれると判定した場合に、前記記憶部に記憶された前記論理積が係る論理和で示される論理式のデータを、前記論理積の左辺を第1の辺とし前記論理和の前記論理積が係らない辺である他方の辺を第2の辺とする第1の論理和と、前記論理積の右辺を第1の辺とし前記他方の辺を第2の辺とする第2の論理和と、前記第1の論理和を第1の辺とし前記第2の論理和を第2の辺とする論理積とで示される論理式のデータに変換し、前記判定において、前記論理積が係る論理和が含まれないと判定した場合に、前記記憶部に記憶された前記論理式のデータを、論理和を含まず、かつ、論理積で結合された論理式の部分論理式毎に分割した部分論理式各々を生成する生成部と、前記部分論理式各々を入力としてSMTソルバを実行し、当該部分論理式を充足する解を求める充足値生成部と、を備えることを特徴とするテストデータ生成装置。本発明は、事前条件を表す論理式に全称記号や存在記号が含まれる場合でも、境界値制約を用いて、組み合わせ爆発を抑えたテストデータを生成するテストデータ生成プログラム、テストデータ生成方法、テストデータ生成装置を提供することを目的とする。本実施の態様のひとつであるテストデータ生成プログラムは、テスト対象のプログラムの入力データに関する事前条件を表した論理式が記憶された記憶部を参照して、上記論理式に存在記号が含まれているか否かを判定する。続いて、上記判定において含まれると判定した場合、上記論理式から上記存在記号と当該存在記号の要素を含む入力データを識別する入力データ識別情報とを含む部分述語論理式を抽出する。続いて、上記入力データ識別情報で識別されるテーブル毎に該テーブルの行数が記憶された記憶部を参照して、上記部分述語論理式に含まれる入力データ識別情報に対応するテーブルの行数を取得する。続いて、上記行数を表す変数の値を、上記取得した行数の最小値、最大値、及び、上記最小値より大きく上記最大値より小さい範囲とする論理式をそれぞれ生成する。続いて、上記生成した論理式を論理和で結んだ制約式を生成する。続いて、上記記憶部に記憶された上記論理式に含まれる上記部分述語論理式を上記生成した制約式との論理積に変換する。本実施の態様によれば、事前条件を表す論理式に全称記号や存在記号が含まれる場合でも、境界値制約を用いて、組み合わせ爆発を抑えたテストデータを生成することができるという効果を奏する。実施の態様に示すテストデータの生成は、プログラムをテストする際に用いるプロパティに含まれる事前条件を表した論理式に全称記号または存在記号が含まれている場合、該論理式を否定標準形に変換して、全称記号を含まない論理式を生成する。次に、生成した論理式から存在記号を含む部分述語論理式を抽出する。続いて、部分述語論理式により特定されるテーブルの行数を表す変数に代入される数値を用いて、最小値と、最大値と、最小値より大きく最大値より小さい範囲を決定する。そして、変数と最小値と最大値とその範囲とを用いて表される論理式各々を論理和で結び、制約式を生成する。また、部分述語論理式の存在記号を論理積に変換する。その後、部分述語論理式に関連して変数を用いて表される論理式と制約式とを変換した論理積で結ぶ。続いて、事前条件の部分述語論理式を、論理積で結んで生成した論理式に変更し、変更した事前条件を論理和標準形に変換し、論理和ごとに変更した該事前条件を分割した部分論理式各々を生成する。その後、事前条件に示されている入力変数に入力するデータと部分論理式各々とを組み合わせて入力として、SMTソルバを実行し、事前条件を充足する解を、部分論理式各々に対して求める。その結果、事前条件を表す論理式に全称記号や存在記号が含まれる場合でも、境界値制約を用いて、組み合わせ爆発を抑えたテストデータを生成することができる。以下図面に基づいて、実施形態について詳細を説明する。テストデータ生成装置1について説明する。図1は、テストデータ生成装置のハードウェアの一実施例を示す図である。テストデータ生成装置1は、制御部2、記憶部3、記録媒体読取装置4、入出力インタフェース5入出力I/F、通信インタフェース6通信I/Fなどを備えている。また、上記各構成部はバス7によってそれぞれ接続されている。制御部2は、後述する抽出部201、変換部202、生成部203、充足値生成部204などを有している。また、制御部2はCentralProcessingUnitCPU、マルチコアCPU、プログラマブルなデバイスFieldProgrammableGateArrayFPGA、ProgrammableLogicDevicePLDなどを用いることが考えられる。記憶部3は、後述するプロパティ情報、論理式情報、変換情報、テストデータ生成情報、データセット情報などを記憶している。記憶部3は、例えばReadOnlyMemoryROM、RandomAccessMemoryRAMなどのメモリやハードディスクなどが考えられる。なお、記憶部3にはパラメータ値、変数値などのデータを記録してもよいし、実行時のワークエリアとして用いてもよい。上記プロパティ情報、論理式情報、変換情報、テストデータ生成情報、データセット情報などは、データベースに記録されていてもよい。記録媒体読取装置4は、制御部2の制御に従って記録媒体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、12に示すフローが実現される。その場合システムが有すべき機能の処理内容を記述したプログラムが提供される。そのプログラムをコンピュータで実行することにより、上記処理機能がコンピュータ上で実現される。処理内容を記述したプログラムは、コンピュータで読み取り可能な記録媒体8に記録しておくことができる。プログラムを流通させる場合には、例えば、そのプログラムが記録されたDVD、CD-ROMなどの記録媒体8が販売される。また、プログラムをサーバコンピュータの記憶装置に記録しておき、ネットワークを介して、サーバコンピュータから他のコンピュータにそのプログラムを転送することもできる。プログラムを実行するコンピュータは、例えば、記録媒体8に記録されたプログラムもしくはサーバコンピュータから転送されたプログラムを、自己の記憶部3に記録する。そして、コンピュータは、自己の記憶部3からプログラムを読み取り、プログラムに従った処理を実行する。なお、コンピュータは、記録媒体8から直接プログラムを読み取り、そのプログラムに従った処理を実行することもできる。また、コンピュータは、サーバコンピュータからプログラムが転送されるごとに、逐次、受け取ったプログラムに従った処理を実行することもできる。図2は、テストデータ生成装置の一実施例を示す図である。抽出部201は、否定標準形変換部206、木構造生成部205、存在記号付論理式抽出部207を有している。否定標準形変換部206は、記憶部3の後述するプロパティ情報からプロパティに含まれる事前条件を表す論理式を取得する。また、否定標準形変換部206は、事前条件を表す論理式に限量子を示す記号全称記号または存在記号がある場合に、該論理式を否定標準形に変換する。否定標準形への変換は、例えば、後述する含意記号除去処理と二重否定除去処理とドモルガンの法則を行う処理と限量子変換処理とを用いて行う。木構造生成部205は、否定標準形へ変換された論理式を木構造で表して後述する論理式情報に記憶する。存在記号付論理式抽出部207は、論理式情報に存在記号の存在する部分述語論理式があるか否かを判定し、存在記号の存在する論理式が場合に、論理式と論理式に関連付けられている情報を変換情報に記憶する。変換部202は、同値クラス算出部208、存在記号なし論理式変換部209を有している。同値クラス算出部208は、変換情報から存在記号を有する論理式を選択し、存在記号を有する論理式により特定されるテーブルを参照して、設定された該テーブルの行数を取得する。また、同値クラス算出部208は、取得した行数を用いて同値クラスを求め、制約式を生成する。また、同値クラス算出部208が制約式を木構造で表し、変換情報に追加する。存在記号なし論理式変換部209は、選択した存在記号を有する論理式を論理積に変換する。また、存在記号なし論理式変換部209は、選択されている変換した論理式と、追加された制約式を関連付ける。その後、存在記号なし論理式変換部209は、変換情報を論理式情報に反映させ、反映させた論理式情報を用いて、論理和標準形に変換し、論理和ごとに分割して部分論理式を生成して記憶部3に記憶する。生成部203は、分割した論理式各々部分論理式と標準値情報を取得する。標準値情報は、アプリケーションが動作した際に必要な入力情報である。生成部203は、部分論理式各々と標準値情報を組み合わせてテストデータ生成情報を生成する。充足値生成部204は、充足値生成部204がテストデータ生成情報を入力として、SMTソルバなどを用いて、テストデータ生成情報の論理式各々を充足する解充足値を求める。そして、生成部203は、テストデータ生成情報各々に対応する充足値であるテストデータ後述するデータセット情報を記憶部3に記憶する。なお、充足値生成部204はテストデータ生成装置1以外のコンピュータに設けてもよい。テストデータ生成装置の制御部の動作について説明する。抽出部201の動作について説明する。図3は、制御部2の抽出部201の動作の一実施例を示す図である。ステップS1では、抽出部201の否定標準形変換部206が記憶部3のプロパティ情報からプロパティに含まれる事前条件を示す論理式を取得する。プロパティ情報は、例えば、仕様に基づいて作成されたプロパティが記憶されている。また、プロパティは事前条件が成立するならば事後条件となるのような形式で記載された情報である。一例として、図4に示す商品購入アプリケーションをテストする仕様のひとつのプロパティについて説明する。図4は、商品購入アプリケーションの商品購入画面の一実施例を示す図である。図4の商品購入画面401は、入出力部9の出力部であるディスプレイに表示される。会員ID入力ボックス402には会員IDが入力される。注文明細表入力ボックス403には品名と購入数が入力される。本例の商品購入アプリケーションでは、5個の商品を購入することが可能で、注文明細表入力ボックス403には品名と購入数を入力するレコードが5行用意されている。メッセージ出力ボックス404には、品名または購入数の入力された状態に応じたメッセージが出力される。商品購入アプリケーションを実行されると、会員ID入力ボックス402に会員IDが入力されると、注文明細表入力ボックス403に品名と購入数を入力することができるようになる。すなわち、会員ID入力ボックス402に会員IDが入力されると、記憶部3に記憶されている複数の会員IDを参照して、入力された会員IDと一致するか否かを判定する。一致する会員IDが存在する場合には、注文明細表入力ボックス403に品名と購入数を入力することができるようにする。続いて、注文明細表入力ボックス403の品名とその購入数が入力されると、記憶部3に記憶されている複数の品名を参照して、入力された品名と一致する品名を検索する。一致する品名が存在する場合には、品名に関連付けられて記憶部3に記憶されている商品ID単価を取得する。そして、注文明細表入力ボックス403には商品ID、品名、単価、購入数がすべて表示される。なお、備考欄に表示する項目があれば表示する。また、注文明細表入力ボックス403のいずれかの行に、品名または購入数が入力されないときには、メッセージ出力ボックス404に品名または購入数が入力されていない主の内容を出力する。上記で説明した商品購入アプリケーションをテストする仕様のひとつのプロパティとして、事前条件会員IDが入力されていて、注文明細表の品名か購入数が空の行があるならば、事後条件メッセージに品名または購入数が入力されていないことを表示するのようなプロパティが考えられる。ステップS1では、論理式で表わされた上記事前条件を否定標準形変換部206が取得する。事前条件を論理式で表した例notand∈注文明細r購入数orr品名なお、本例の論理式おいて、notは、事前条件の会員IDが入力されていてに相当し、∈注文明細r購入数orr品名は、事前条件の注文明細表の購入数か品名が空の行があるに相当する。なお、本例ではnotは否定を示し、はデータが入力されていないことを示し、andは論理積を示している。また、∃は存在記号を示し、∃r∈注文明細部分述語論理式は、注文明細という名称の記憶部に記憶されているテーブルには少なくともi行のレコードが存在することを示している。r購入数orr品名は、i行のレコード各々に含まれている商品の購入数を示すセルに入力がないこと、または、i行のレコード各々に含まれている品名を示すセルに入力がないことを示している。orは論理和を示している。なお、プロパティのならばは例えば→と表す。また、事後条件もメッセージに品名または購入数が入力されていない表示するは、例えば、メッセージ品名または購入数が入力されていないと表す。ステップS2では、木構造生成部205が論理式を木構造で表して論理式情報に記憶する。図5は、論理式を木構造で表した一実施例を示す図である。図6は、論理式情報のデータ構造の一実施例を示す図である。木構造の生成について説明する。図5は、上記事前条件を論理式notand∈注文明細r購入数orr品名を木構造で表した例である。論理式で使用されている演算子notandorを抽出し、notandor各々に直接関係する要素を検出する。論理式のnotに関連する要素はである。論理式のandに関連する要素はnotと∈注文明細r購入数orr品名である。論理式のorに関連する要素は∃r∈注文明細r購入数と∃r∈注文明細r品名である。上記検出の結果、andに関連する要素は、notに関連する要素とorに関連する要素をすべて含んでいるので、and∧を木の頂点のノード0とする。次に、andの左側のnotと∈注文明細r購入数orr品名をノードに分ける。not¬をノード1とし、会員IDをノード5とし、==をノード3とし、をノード6とする。∈注文明細はひとつの要素として扱いノード2とする。r購入数をノード9とし、==をノード7とし、をノード10とし、or∨をノード4とし、r品名をノード11とし、==をノード8とし、をノード12とする。本例では、上記のように木構造を生成したが限定されるものではない。論理式情報について説明する。図6は、論理式情報のデータ構造の一実施例を示す図である。図6の論理式情報601は、図5に示した木構造を記憶部3に記憶した例である。論理式情報601は、ノード番号の情報を記憶するNo、変数名、数値、文字列などが記憶される値、演算子や存在記号を含む論理式の情報を記憶する演算子、限量子を有する。また、演算子、限量子に関連するノードの情報を記憶する左ノード右ノードを有する。左ノードには演算子や存在記号を含む論理式の左側に存在するノード番号が記憶され、右ノードには演算子や存在記号を含む論理式の右側に存在するノード番号が記憶される。本例では、Noにはノード01212が記憶されている。値には、No5に関連付けられて文字列会員IDが、No6に関連付けられて空文字列に含まれるが記憶されている。また、No9に関連付けられて数値r購入数が、No6に関連付けられて空文字列に含まれるが記憶されている。また、No11に関連付けられて数値r品名が、No12に関連付けられて空文字列に含まれるが記憶されている。演算子、限量子には、No0に関連付けられて論理積記号∧が記憶され、No1に関連付けられて否定記号¬が記憶され、No2に関連付けられて存在記号を含む論理式の情報∃r∈注文明細が記憶されている。No3に関連付けられて等号記号==が記憶され、No4に関連付けられて論理積記号∨が記憶されている。左ノードには、値または演算子、限量子に記憶されている情報に関連付けられてNoを示す13457911が記憶されている。右ノードには、値または演算子、限量子に記憶されている情報に関連付けられてNoを示す2681012が記憶されている。ステップS3では、否定標準形変換部206が論理式を否定標準形に変換する。否定標準形への変換は、例えば、含意演算子除去、二重否定演算子除去、ドモルガンの法則、限量子変換を用いて行う。事前条件を示す論理式を否定標準形に変換する方法として、論理式に含意記号がある場合にはまず含意記号をとる含意除去処理を行う。次に、ドモルガンの法則を用いた処理を行い、否定記号を内側に押し込む操作を繰り返すことによって、論理的に等価な否定標準形に置き換える。その結果、変形した論理式に二重否定¬¬:否定記号が連続しているが表れたときは二重否定を除去する処理を行う。そして、上記限量子変換の例の変換前に示した¬∀xS1に当てはまる箇所がある場合には、∃x¬S1の形に変形する。上記に示した処理を繰り返し、全称記号がない否定標準形に変換された論理式が求まると処理を終了する。含意演算子除去の処理について説明する。含意演算子除去の例S1→S2変換前¬S1∨S2変換後S1とS2は要素または論理式などを示し、→は含意演算子を示し、¬は否定演算子を示し、∨は論理和記号を示す記号である。図7は、含意演算子除去処理の動作の一実施例を示すフロー図である。図8は、含意演算子を含む論理式を木構造で表した一実施例を示す図である。図9は、図8に対応する論理式情報のデータ構造の一実施例を示す図である。ステップS201では、否定標準形変換部206が含意演算子を含む論理式情報の最初の行図8の論理式の木構造の最上位のノードから順に、含意演算子を検索する。例えば、図9の左ノードおよび右ノードに記憶された情報ポインタを辿りながら、演算子、限量子に含意→があるノードを検索する。図8に示す木構造は、含意演算子除去の例のS1→S2変換前を示す木構造と、含意演算子除去の例の¬S1∨S2変換後を示す木構造を示している。図9に示す論理式情報91は、含意演算子除去の例のS1→S2変換前を示す情報で、論理式情報92は、含意演算子除去の例の¬S1∨S2変換後を示す情報である。論理式情報91、92は、No値演算子、限量子左ノード右ノードに記憶される情報を有している。論理式情報91、92のNoには、例えば、ノードを示す情報が記憶されている。本例では、ノードを示す情報として連番012が記憶されている。値には、Noに関連付けられた要素が記憶されている。論理式情報91では、No1に関連付けられて要素S1が記憶されている。また、No2に関連付けられて要素S2が記憶されている。本例では、要素S1、S2は木構造の末端のノードであると考えて値が記憶されているが、要素S1、S2が論理式である場合末端のノードでない場合には、要素S1、S2は記憶されない。また、末端のノードでない場合には、後述する演算子、限量子左ノード右ノードに、ノードに関連付けられている論理式に対応付けられる情報各々が記憶される。その場合、Noのノード2以降にも論理式を表現するためのノードを示す情報と、該Noに関連する値演算子、限量子左ノード右ノードが追加される。演算子、限量子には、演算子や限量子を有する情報が記憶されている。論理式情報91では、No0に関連付けられて含意演算子→が記憶され、論理式情報92では、No0に関連付けられて論理和∨が記憶され、No3に関連付けられて否定演算子¬が記憶されている。左ノードには、値または演算子、限量子に記憶されている情報に関連付けられているノードを示す情報が記憶されている。本例では、No0に関連付けられて1が記憶されている。右ノードには、値または演算子、限量子に記憶されている情報に関連付けられているノードを示す情報が記憶されている。本例では、No0に関連付けられて2が記憶されている。ステップS201では、否定標準形変換部206が図8に示す含意演算子を含む論理式の木構造の最上位のノード0、つまり図9に示すNo0のノードから順に左ノードおよび右ノードに記憶された情報ポインタを辿りながら、演算子、限量子に含意→があるノードを検索する。ステップS202では、否定標準形変換部206が論理式情報を検索して含意演算子→が検出できたか否かを判定し、含意演算子→がある場合、ステップS203Yesに移行し、含意演算子→がない場合にはこの処理を終了する。本例では、論理式情報91の演算子、限量子に含意演算子→があるのでステップS203Yesに移行する。ステップS203では、否定標準形変換部206が論理式情報91に示す左ノードの項目の値を記憶部3の図示しない左ノードに記憶されている情報を退避領域に記憶する。本例では、論理式情報91の左ノードのs1が退避領域に記憶される。ステップS204では、否定標準形変換部206が記憶部3に記憶された、ノードの演算子、限量子の項目値を、含意演算子→から論理和∨に更新する。本例では、図4の論理式情報91のNo0の行の演算子、限量子の→が論理和∨に更新され、図4の論理式情報92のNo0に対応する行の演算子、限量子のように論理和∨となる。ステップS205では、否定標準形変換部206が更新した論理和∨に対応する行の左ノードの情報を、新しい番号に更新する。例えば、新しい番号として左ノードの情報を、Noに記憶されている情報としてまだ使用されていない情報にする。本例では、論理式情報91のNoで使用している最大値2に1を加算して3を求め、論理式情報91の左ノードの2を3に更新し、論理式情報92のNo0の行のようになる。ステップS206では、否定標準形変換部206が新しい行を追加する。例えば、新しい行のNoには、ステップS205の処理で作成した新しい番号が記憶され、演算子、限量子に否定演算子¬が記憶される。また、左ノードには、ステップS203で退避領域に記憶した情報を記憶する。それぞれ格納した新しいノードのデータを生成し、記憶部3に追加格納する。本例では、新しい行のNoに3が記憶され、演算子、限量子に否定演算子¬が記憶され、左ノードに1が記憶される。二重否定演算子除去の処理について説明する。二重否定演算子除去の例¬¬S1変換前S1変換後図10は、二重否定演算子除去処理の動作の一実施例を示すフロー図である。図11は、二重否定演算子を含む論理式を木構造で表した一実施例を示す図である。図12は、図11に対応する論理式情報のデータ構造の一実施例を示す図である。ステップS301では、否定標準形変換部206が二重否定演算子を含む論理式情報の最初の行図11の論理式の木構造の最上位のノードから順に、二重否定演算子を検索する。例えば、図12の左ノードおよび右ノードに記憶された情報ポインタを辿りながら、演算子、限量子に二重否定¬¬がある部分木を検索する。図11に示す木構造は、二重否定演算子除去の例の¬¬S1変換前を示す木構造と、二重否定演算子除去の例のS1変換後を示す木構造を示している。図12に示す論理式情報121は、二重否定演算子除去の例の¬¬S1変換前を示す情報で、論理式情報92は、二重否定演算子除去の例のS1変換後を示す情報である。論理式情報121、122は、No値演算子、限量子左ノード右ノードに記憶される情報を有している。論理式情報121、122のNoには、例えば、ノードを示す情報が記憶されている。本例では、ノードを示す情報として連番012が記憶されている。値には、Noに関連付けられた要素が記憶されている。論理式情報121では、No1に関連付けられて要素S1が記憶されている。本例では、要素S1は木構造の末端のノードであると考えて値が記憶されているが、要素S1が論理式である場合末端のノードでない場合には、要素S1は記憶されない。また、末端のノードでない場合には、後述する演算子、限量子左ノード右ノードに、ノードに関連付けられている論理式に対応付けられる情報各々が記憶される。その場合、Noのノード2以降にも論理式を表現するためのノードを示す情報と、該Noに関連する値演算子、限量子左ノード右ノードが追加される。演算子、限量子には、演算子や限量子を有する情報が記憶されている。論理式情報121では、No0に関連付けられて否定演算子¬が記憶されている。左ノードには、値または演算子、限量子に記憶されている情報に関連付けられているノードを示す情報が記憶されている。本例では、No0に関連付けられて1が記憶され、No1に関連付けられて2が記憶され。右ノードには、値または演算子、限量子に記憶されている情報に関連付けられているノードを示す情報が記憶されている。ステップS301では、否定標準形変換部206が図11に示す二重否定演算子を含む論理式の木構造の最上位のノード0、つまり図12に示すNo0のノードから順に左ノードおよび右ノードに記憶された情報ポインタを辿りながら、演算子、限量子に否定¬が2つ連続する二重否定を検索する。ステップS302では、否定標準形変換部206が論理式情報を検索して二重否定演算子¬¬が検出できたか否かを判定し、二重否定演算子¬¬がある場合、ステップS303Yesに移行し、二重否定演算子¬¬がない場合にはこの処理を終了する。本例では、論理式情報121の演算子、限量子に二重否定演算子¬¬があるのでステップS303Yesに移行する。ステップS303では、否定標準形変換部206が検出された部分木¬¬の、下位のノードの下位にあるノードのNo以外値演算子、限量子左ノード右ノードの情報を取得する。本例では、図11の二重否定演算子のノード1に対応する論理式情報121のNo1の下位にあるNo2に対応する値演算子、限量子左ノード右ノードの情報を取得する。論理式情報121の場合、演算子、限量子のS1を取得する。ステップS304では、否定標準形変換部206が検出された部分木の上位のノードに、ステップS303で取得した情報を記憶し、更新する。本例では、論理式情報122のNo0に、取得した情報演算子、限量子のS1を記憶する。また、ステップS304では、上記更新が終了した後、否定標準形変換部206が検出された部分木の上位のノード以外の情報を削除する。本例では、論理式情報122のNo12に対応する行それぞれを削除する。ドモルガンの処理について説明する。ドモルガンの処理の例¬S1∧S2変換前¬S1∨¬S2変換後または、¬S1∨S2変換前¬S1∧¬S2変換後図13は、ドモルガンの処理の動作の一実施例を示すフロー図である。図14は、ドモルガンの処理を含む論理式を木構造で表した一実施例を示す図である。図15は、図14に対応する論理式情報のデータ構造の一実施例を示す図である。ステップS401では、否定標準形変換部206が否定¬と論理演算子論理和∨又は論理積∧とが連続する論理式情報の最初の行から順に検索をする。例えば、図14に示す¬S1∧S2や¬S1∨S2の論理式の木構造の最上位のノード0から検索をする。また、図15の左ノードおよび右ノードに記憶された情報ポインタを辿りながら、演算子、限量子に否定¬と論理演算子論理和∨又は論理積∧とが連続する部分木を検索する。図14に示す木構造は、ドモルガンの処理の例の¬S1∧S2変換前を示す木構造と、ドモルガンの処理の例の¬S1∨¬S2変換後を示す木構造を示している。または、ドモルガンの処理の例の¬S1∨S2変換前を示す木構造と、ドモルガンの処理の例の¬S1∧¬S2変換後を示す木構造を示している。図15に示す論理式情報151は、ドモルガンの処理の例の¬S1∧S2変換前を示す情報で、論理式情報152は、ドモルガンの処理の例の¬S1∨¬S2変換後を示す情報である。図15に示す論理式情報153は、ドモルガンの処理の例の¬S1∨S2変換前を示す情報で、論理式情報154は、ドモルガンの処理の例の¬S1∧¬S2変換後を示す情報である。論理式情報151~154は、No値演算子、限量子左ノード右ノードに記憶される情報を有している。論理式情報151~154のNoには、例えば、ノードを示す情報が記憶されている。本例では、ノードを示す情報として連番012が記憶されている。値には、Noに関連付けられた要素が記憶されている。論理式情報151~154では、No23に関連付けられて要素S1S2が記憶されている。本例では、要素S1、S2は木構造の末端のノードであると考えて値が記憶されているが、要素S1、S2が論理式である場合末端のノードでない場合には、要素S1、S2は記憶されない。また、末端のノードでない場合には、後述する演算子、限量子左ノード右ノードに、ノードに関連付けられている論理式に対応付けられる情報各々が記憶される。その場合、Noのノード2以降にも論理式を表現するためのノードを示す情報と、該Noに関連する値演算子、限量子左ノード右ノードが追加される。演算子、限量子には、演算子や限量子を有する情報が記憶されている。論理式情報151では、No0に関連付けられて否定演算子¬が記憶され、No1に関連付けられて論理積∧が記憶されている。論理式情報152では、No0に関連付けられて論理和∨が記憶され、No45に関連付けられて否定演算子¬がそれぞれ記憶されている。論理式情報153では、No0に関連付けられて否定演算子¬が記憶され、No1に関連付けられて論理和∨が記憶されている。論理式情報154では、No0に関連付けられて論理積∧が記憶され、No45に関連付けられて否定演算子¬がそれぞれ記憶されている。左ノードには、値または演算子、限量子に記憶されている情報に関連付けられているノードを示す情報が記憶されている。本例では、論理式情報151ではNo0に関連付けられて1が記憶され、No1に関連付けられて2が記憶されている。論理式情報152ではNo0に関連付けられて4が記憶され、No4に関連付けられて2が記憶され、No5に関連付けられて3が記憶されている。論理式情報153ではNo0に関連付けられて1が記憶され、No1に関連付けられて2が記憶されている。論理式情報154ではNo0に関連付けられて4が記憶され、No4に関連付けられて2が記憶され、No5に関連付けられて3が記憶されている。右ノードには、値または演算子、限量子に記憶されている情報に関連付けられているノードを示す情報が記憶されている。本例では、論理式情報151ではNo1に関連付けられて3が記憶されている。論理式情報152ではNo0に関連付けられて5が記憶されている。本例では、論理式情報153ではNo1に関連付けられて3が記憶されている。論理式情報154ではNo0に関連付けられて5が記憶されている。ステップS401では、否定標準形変換部206が図14に示す否定演算子を含む論理式の木構造の最上位のノード0、つまり図15に示すNo0のノードから順に左ノードおよび右ノードに記憶された情報ポインタを辿りながら、演算子、限量子に否定¬と論理演算子論理和∨又は論理積∧とが連続する部分木を検索する。ステップS402では、否定標準形変換部206が演算子、限量子に否定¬と論理演算子論理和∨又は論理積∧とが連続する部分木が検出できたか否かを判定する。検出できた場合、ステップS403Yesに移行し、検出できない場合、この処理を終了する。ステップS403では、否定標準形変換部206が否定¬の下位の論理演算子が論理和∨か否かを判定し、論理和∨である場合にはステップS404Yesに移行し、論理積∧である場合にはステップS405Noに移行する。ステップS404では、否定標準形変換部206が検出された部分木の上位のノードである否定演算子¬を論理和∨に更新する。一方、ステップS405では、否定標準形変換部206が検出された部分木の上位のノードである否定演算子¬を論理積∧に更新する。ステップS406では、否定標準形変換部206が検出された部分木の下位ノード、つまり論理演算子論理和∨又は論理積∧の左ノードおよび右ノードの情報を取得する。図15に示す論理式情報151では、左ノードの2、右ノードの3を取得する。また、図15に示す論理式情報153では、左ノードの2、右ノードの3を取得する。ステップS407では、否定標準形変換部206がステップS404又はステップS405で処理した上位ノードの左ノード及び右ノードの情報をそれぞれ新しい番号に更新する。例えば、図15に示す論理式情報152および154では左ノードの新しい番号として、Noの情報の最大値に1加算した値4、右ノードの新しい番号として、左ノードの新しい番号に更に1加算した値5を記憶することが考えられる。ステップS408では、否定標準形変換部206がステップS407で追加した上位の左ノードに記憶した新しい番号をNoに追加する。例えば、図15に示す論理式情報151、153のNoに新しい番号4を追加する。新しい番号を追加したNoに対応する演算子、限量子には否定¬を記憶する。また、左ノードにはステップS406で取得した左ノードの情報を記憶する。例えば、図15に示す論理式情報152、154に示すように、No4に対応する左ノードにステップS406で取得した2を追加する。ステップS409では、否定標準形変換部206がステップS407で追加した上位の右ノードに記憶した新しい番号をNoに追加する。例えば、図15に示す論理式情報151、153のNoに新しい番号5を追加する。新しい番号を追加したNoに対応する演算子、限量子には否定¬を記憶する。また、左ノードにはステップS406で取得した右ノードの情報を記憶する。例えば、図15に示す論理式情報152、154に示すように、No5に対応する右ノードにステップS406で取得した3を追加する。このように、否定標準形変換部206は、処理対象の木構造の論理式データについて、演算子、限量子の情報が否定¬と論理演算子論理和∨又は論理積∧が連続する部分木が検出できなくなるまで、ドモルガンの法則に基づく論理式の否定標準形への変換の処理を繰り返し実行する。限量子変換の処理について説明する。限量子変換の例¬∀xS1変換前∃x¬S1変換後または、¬∃xS1変換前∀x¬S1変換後∀xは全称記号を示し、∃xは存在記号を示している。図16は、限量子変換処理の動作の一実施例を示すフロー図である。図17は、限量子を含む論理式を木構造で表した一実施例を示す図である。図18は、図17に対応する論理式情報のデータ構造の一実施例を示す図である。ステップS501では、否定標準形変換部206が否定演算子¬つき限量子を含む論理式情報の最初の行図17の論理式の木構造の最上位のノードから順に、否定演算子¬つき限量子を検索する。例えば、図18の左ノードおよび右ノードに記憶された情報ポインタを辿りながら、演算子、限量子に否定演算子¬つき限量子があるノードを検索する。図17に示す木構造は、限量子変換の例の¬∀xS1変換前を示す木構造と、限量子変換の例の∃x¬S1変換後を示す木構造を示している。また、限量子変換の例の¬∃xS1変換前を示す木構造と、限量子変換の例の∀x¬S1変換後を示す木構造を示している。図18に示す論理式情報181は、限量子変換の例の¬∀xS1変換前を示す情報で、論理式情報182は、限量子変換の例の∃x¬S1変換後を示す情報である。また、図18に示す論理式情報183は、限量子変換の例の¬∃xS1変換前を示す情報で、論理式情報184は、限量子変換の例の∀x¬S1変換後を示す木構造を示す情報である。論理式情報181~184は、No値演算子、限量子左ノード右ノードに記憶される情報を有している。論理式情報181~184のNoには、例えば、ノードを示す情報が記憶されている。本例では、ノードを示す情報として連番012が記憶されている。値には、Noに関連付けられた要素が記憶されている。論理式情報181~184では、No2に関連付けられて要素S1が記憶されている。本例では、要素S1は木構造の末端のノードであると考えて値が記憶されているが、要素S1が論理式である場合末端のノードでない場合には、要素S1は記憶されない。また、末端のノードでない場合には、後述する演算子、限量子左ノード右ノードに、ノードに関連付けられている論理式に対応付けられる情報各々が記憶される。その場合、Noのノード2以降にも論理式を表現するためのノードを示す情報と、該Noに関連する値演算子、限量子左ノード右ノードが追加される。演算子、限量子には、演算子や限量子を有する情報が記憶されている。論理式情報181では、No0に関連付けられて否定演算子¬が記憶され、No1に関連付けられて全称記号∀xが記憶されている。論理式情報182では、No0に関連付けられて存在記号∃xが記憶され、No1に関連付けられて否定演算子¬が記憶されている。論理式情報183では、No0に関連付けられて否定演算子¬が記憶され、No1に関連付けられて存在記号∃xが記憶されている。論理式情報184では、No0に関連付けられて全称記号∀xが記憶され、No1に関連付けられて否定演算子¬が記憶されている。左ノードには、値または演算子、限量子に記憶されている情報に関連付けられているノードを示す情報が記憶されている。論理式情報181~184では、No0に関連付けられて1が記憶され、No1に関連付けられて2が記憶されている。ステップS501では、否定標準形変換部206が図17に示す否定演算子¬つき限量子を含む論理式の木構造の最上位のノード0、つまり図18に示すNo0のノードから順に左ノードおよび右ノードに記憶された情報ポインタを辿りながら、否定演算子¬つき限量子があるノードを検索する。ステップS502では、否定標準形変換部206が論理式情報を検索して否定演算子¬つき限量子が検出されたか否かを判定し、否定演算子¬つき限量子を含む論理式がある場合、ステップS503Yesに移行する。否定演算子¬つき限量子を含む論理式がない場合にはこの処理を終了する。本例では、論理式情報181、183の演算子、限量子に否定演算子¬つき限量子があるのでステップS503Yesに移行する。ステップS503では、否定標準形変換部206が否定演算子¬つき限量子を、否定演算子¬なし限量子に変更する。論理式情報181の場合、No0に対応する否定演算子¬を存在記号∃xに変更する。No1に対応する全称記号∀xを否定演算子¬に変換して、論理式情報182のようにする。論理式情報183の場合、No0に対応する否定演算子¬を全称記号∀xに変更する。No1に対応する存在記号∃xを否定演算子¬に変換して、論理式情報184のようにする。∀xS1が存在する場合について説明する。S1が{s1,s2,s3}などの要素を有している場合、∀xS1を検出した場合にはs1∧s2∧s3に変換する。この変換は既知の技術である。論理式1を否定標準形に変換する例について説明する。なお、Pxは限量子内論理式とする。∀xPx→a∨¬b→c論理式1上記論理式1に対して含意除去処理を行い論理式2に変形する。¬∀xPx→a∨¬b∨c論理式2上記論理式2に対して含意除去処理を行い論理式3に変形する。¬∀x¬Px∨a∨¬b∨c論理式3上記論理式3に対してドモルガンの法則を用いた処理を行い論理式4に変形する。∨c論理式4上記論理式4に対して二重否定除去の処理を行い論理式5に変形する。¬∀x¬Px∨a∧b∨c論理式5上記論理式4に対して全称子記号を存在子記号に変換する処理を行い論理式5に変形する。∃x¬¬Px∨a∧b∨c論理式6上記論理式6に対してドモルガンの法則を用いた処理を行い論理式7に変形する。∃x¬¬Px∧¬a∧b∨c論理式7上記論理式7に対して二重否定除去の処理を行い論理式8に変形する。∃xPx∧¬a∧b∨c論理式8ステップS4では、存在記号付論理式抽出部207が論理式情報の1行目を選択する。本例では、No0の行を選択する。ステップS5では、存在記号付論理式抽出部207が現在選択されている行の論理式の演算子、限量子を参照し、論理式に存在記号があるか否かを判定し、ある場合にはステップS6Yesに移行し、ない場合にはステップS8Noに移行する。本例では、No2の行が選択された場合に∃r∈注文明細があるので、存在記号があると判定してステップS6Yesに移行する。ステップS6では、存在記号付論理式抽出部207が存在記号の存在する行を変換情報に記憶する。本例では、No2の行を変換情報に記憶する。図19は、変換情報のデータ構造の一実施例を示す図である。変換情報701は、ノード番号の情報を記憶するNo、変数名、数値、文字列などが記憶される値、演算子や存在記号を含む論理式の情報を記憶する演算子、限量子を有する。また、演算子、限量子に関連するノードの情報を記憶する左ノード右ノードを有する。左ノードには演算子や存在記号を含む論理式の左側に存在するノード番号が記憶され、右ノードには演算子や存在記号を含む論理式の右側に存在するノード番号が記憶される。ステップS7では、存在記号付論理式抽出部207が論理式情報に未選択の行があるか否かを判定し、未選択の行がある場合にはステップS8Yesに移行し、未選択の行がない場合には抽出処理を終了Noする。ステップS8では、存在記号付論理式抽出部207が論理式情報の現在選択されている行の次の行を選択する。なお、本例では1行目から順に存在記号を有する論理式を参照しているが、限定されるものではない。変換部202の動作について説明する。図20は、制御部2の変換部202の動作の一実施例を示す図である。ステップS9では、同値クラス算出部208が変換情報から存在記号を有する論理式を選択する。ステップS10では、選択した存在記号を有する論理式により特定されるテーブルに対し、設定された該テーブルの行数を取得する。例えば、∃r∈注文明細の場合、注文明細に関連付けられて、記憶部3に記憶されているテーブルを特定するとともに、該テーブルの行数に関連付けられて記憶部3に記憶されているiを特定する。iには、例えば、記憶部3に記憶されている注文明細のレコード長を決定する5が関連付けられているとする。ただし、注文明細のレコード長は5に限定されるものではない。ステップS11では、同値クラス算出部208が取得した行数を用いて同値クラスを求め、制約式を生成する。例えば、同値クラスは注文明細のテーブルの行数iのとり得る範囲の最小値と最大値と中間値を求める。注文明細のレコード長として現在i=5が記憶されているとすれば、同値クラスは最小値i=0、最大値i=4、中間値のとり得る範囲=0<i<4となる。そして、求めた最大値と最小値と中間値とを論理和で結び、制約式を生成し変形する。制約式の例oror制約式ororandステップS12では、同値クラス算出部208が制約式を木構造で表し、変換情報に追加する。制約式を木構造で表す方法について説明する。図21は、制約式を木構造で表した一実施例を示す図である。図21は、上記制約式ororandを木構造で表した例である。制約式で使用されている演算子orandを抽出し、orand各々に直接関係する要素を検出する。制約式の左から1番目のorに関連する要素はとで、左から2番目のorに関連する要素はorとandである。andに関連する要素はとである。上記検出の結果、左から2番目のorに関連する要素はすべての要素を含んでいるので、左から2番目のor∨を木の頂点のノードY00とする。次に、制約式の左から1番目のor∨をノードY01とし、and∧をノードY02する。制約式の左から1番目のorに関連するを分けて、iと==と0にし、iをノードY07、をノードY03、0をノードY08とする。また、を分けて、iと==と4にし、iをノードY09、をノードY04、4をノードY10とする。次に、制約式のandに関連するを分けて、iと>と0にし、iをノードY11、をノードY05、0をノードY12とする。また、を分けて、iと<と4にし、iをノードY13、をノードY06、4をノードY14とする。本例では、上記のように木構造を生成したが限定されるものではない。変換情報への追加について説明する。図22は、変換情報のデータ構造の一実施例を示す図である。図22の変換情報101は、図19に示した情報に、図21に示した木構造を追加した例である。変換情報101は、本例では、Noにはノード2Y00Y01Y02Y12が記憶されている。値には、NoY07に関連付けられてiが、NoY08に関連付けられて0が記憶されている。また、NoY09に関連付けられてiが、NoY10に関連付けられて4が記憶されている。また、NoY11に関連付けられてiが、NoY12に関連付けられて0が記憶されている。NoY13に関連付けられてiが、NoY14に関連付けられて4が記憶されている。演算子、限量子には、No2に関連付けられて存在記号を含む論理式の情報∃r∈注文明細が記憶されている。NoY00に関連付けられて論理和記号∨が記憶されている。NoY01に関連付けられて論理和記号∨が記憶されている。NoY02に関連付けられて論理積記号∧が記憶されている。NoY03、NoY04に関連付けられて等号記号==がそれぞれ記憶されている。また、NoY05に関連付けられて不等号>が記憶され、NoY06に関連付けられて不等号<が記憶されている。左ノードには、値または演算子、限量子に記憶されている情報に関連付けられてY01Y03Y05Y07Y09Y011が記憶されている。右ノードには、値または演算子、限量子に記憶されている情報に関連付けられてY02Y04Y06Y08Y10Y12Y14が記憶されている。ステップS13では、存在記号なし論理式変換部209が選択した存在記号を有する論理式を論理積に変換する。本例では、演算子、限量子のNo2に関連付けられて存在記号を含む論理式の情報∃r∈注文明細を論理積∧に変換する。例えば、図22の行102を参照。ステップS14では、存在記号なし論理式変換部209が選択されている変換した論理式と、追加された制約式を関連付ける。本例では、No2に関連付けられている右ノードに制約式に関係付けるためのY00を記憶する。すなわち、生成した木構造は、論理式購入数orr品名andororandを示している。ステップS15では、存在記号なし論理式変換部209が変換情報を論理式情報に反映させ、反映させた論理式情報を用いて、論理和標準形に変換する。図23は、変換情報を論理式情報に反映させた一実施例を示す図である。例えば、図23に示すは変換情報を反映させた論理式情報111が示す論理式はnotand購入数orr品名andororandと表すことができる。そして、上記論理式を論理和標準形に変換すると、論理和標準形の例のような式を求めることができる。論理和標準形の例and購入数andorand購入数andorand購入数andandorand品名andorand品名andorand品名andandorなお、論理和標準形へ変換する技術は限定されるものではなく、論理和標準形へ変換できればよい。論理式情報の論理和標準形への変換について説明する。図24は、論理式情報の論理和標準形への変換の一実施例を示す図である。ステップS701では、存在記号なし論理式変換部209が論理式情報の最上位ノードからポインタを辿り論理積と論理和が連続する部分木を検索する。例えば図23の変換情報を反映させた論理式情報111に示す最上位のノード、つまりNoの情報が0の行から順に左ノードおよび右ノードに格納された情報ポインタを辿りながら、演算子、限量子の情報が論理積∧であるノードと、演算子、限量子の情報が論理和∨であるノードが連続する部分木を検索する。ステップS702では、存在記号なし論理式変換部209がステップS701での検索した結果を用いて、演算子、限量子の項目値が論理積∧であるノードと、演算子、限量子の項目値が論理和∨であるノードが連続する部分木を検索し、部分木が検出できたか否かを判定する。検出できた場合にはステップS703Yesに移行し、検出できない場合にはこの処理を終了Noする。ステップS703では、存在記号なし論理式変換部209が検出された部分木の上位のノードつまり演算子、限量子の情報が論理積∧であるノードの、演算子、限量子の情報を、論理積∧から論理和∨に更新する。ステップS704では、存在記号なし論理式変換部209が検出された部分木の上位のノードの左ノードおよび右ノードの情報を、記憶部3の図示しない左ノードと右ノードの情報を退避される領域に記憶する。ステップS705では、存在記号なし論理式変換部209が検出された部分木の上位のノードの左ノードおよび右ノードの情報を、それぞれ新しい番号に更新する。例えば、左ノードの新しい番号として、まだ論理式情報111のNoで使用されていない情報を用いる。また、右ノードの新しい番号として、該左ノードの新しい番号を含めて、まだ論理式情報111のNoで使用されていない情報を用いる。ステップS706では、存在記号なし論理式変換部209が検出された部分木の下位のノード、つまり、演算子、限量子の情報が論理和のノードの左ノードおよび右ノードの情報を取得する。ステップS707では、存在記号なし論理式変換部209が検出された部分木の下位ノードのNoの情報は左ノードの退避領域の情報と一致するか否かを判定する。一致する場合にはステップS708Yesに移行し、一致しない場合にはステップS710Noに移行する。ステップS708では、存在記号なし論理式変換部209が論理式情報111のNoにはステップS705で上位ノードの左ノードに記憶した新しい番号を、演算子、限量子には論理積∧を記憶する。また、左ノードにはステップS706で取得した下位ノードの左ノードの情報を、右ノードには左ノードの退避領域の情報を、それぞれ記憶した新しいノードのデータを生成し、論理式情報111に追加する。ステップS709では、存在記号なし論理式変換部209が論理式情報111のNoにはステップS705で上位ノードの右ノードに記憶した新しい番号を、演算子、限量子には論理積∧を記憶する。また、左ノードにはステップS706で取得した下位ノードの右ノードの情報を、右ノードには左ノードの退避領域の情報を、それぞれ記憶した新しいノードのデータを生成し、論理式情報111に追加する。その後、ステップS701に移行する。ステップS710では、存在記号なし論理式変換部209が論理式情報111のNoにはステップS705で上位ノードの左ノードに記憶した新しい番号を、演算子、限量子には論理積∧を記憶する。また、左ノードには左ノードの退避領域の情報を、右ノードにはステップS706で取得した下位ノードの左ノードの情報を、それぞれ記憶した新しいノードのデータを生成し、論理式情報111に追加する。ステップS710では、存在記号なし論理式変換部209が論理式情報111のNoにはステップS705で上位ノードの右ノードに記憶した新しい番号を、演算子、限量子には論理積∧を記憶する。また、左ノードには左ノードの退避領域の情報を、右ノードにはステップS706で取得した下位ノードの右ノードの情報を、それぞれ記憶した新しいノードのデータを生成し、論理式情報111に追加する。その後、ステップS701に移行する。上記処理によって、木構造形式の論理式情報が表す否定標準形の論理式が、論理和標準形の論理式に変換される。図20のステップS16では、存在記号なし論理式変換部209が論理和標準形へ変換した論理式を、論理和ごとに分割して部分論理式を生成して記憶部3に記憶する。部分論理式の例and購入数and式1and購入数and式2and購入数andand式3and品名and式4and品名and式5and品名andand式6ステップS17では、存在記号なし論理式変換部209が論理式情報に存在記号がある未選択の論理式があるか否かを判定し、未選択の論理式がある場合にはステップS9Yesに移行する。また、未選択の論理式がない場合には変換部の処理を終了Noする。生成部203、充足値生成部204の動作について説明する。図25は、制御部2の生成部203、充足値生成部204の動作の一実施例を示す図である。ステップS18では、生成部203が記憶部3からステップS16で分割した論理式部分論理式各々を取得する。また、生成部203が記憶部3から標準値情報を取得する。標準値情報は、アプリケーションが動作した際に必要な入力情報である。本例では、商品購入アプリケーションが実行された際に入力する情報は、会員ID購入数品名である。標準値情報の例会員ID:X1000文字列購入数:5数値品名:ハ ゚ソコン文字列また、ステップS18では、生成部203が部分論理式各々と標準値情報とを組み合わせて生成されたテストデータ生成情報を生成する。上記部分論理式の例で示した部分論理式各々と、上記標準値情報の例で示した標準値情報と組み合わせて生成したテストデータ生成情報を入力として、SMTソルバを用いて充足する解充足値を求める。すなわち、式1に示す部分論理式と標準値情報の組み合わせ、式2に示す部分論理式と標準値情報の組み合わせ、式3に示す部分論理式と標準値情報の組み合わせ、各々をテストデータ生成情報とする。また、式4に示す部分論理式と標準値情報の組み合わせ、式5に示す部分論理式と標準値情報の組み合わせ、式6に示す部分論理式と標準値情報の組み合わせ、各々をテストデータ生成情報とする。ステップS19では、充足値生成部204が部分論理式各々と標準値情報とを組み合わせて生成されたテストデータ生成情報が示す論理式を充足する解充足値を求める。充足値生成部204は、SMTソルバなどが考えられる。例えば、上記部分論理式の例で示した部分論理式各々と、上記標準値情報の例で示した標準値情報と組み合わせて生成したテストデータ生成情報を入力として、SMTソルバを用いて充足する解充足値を求める。すなわち、上記6つのテストデータ生成情報を入力として、SMTソルバを用いて充足する解充足値であるデータセット情報を求める。図26は、データセット情報のデータ構造の一実施例を示す図である。図26のデータセット情報131~136は、No品名購入数に記憶される情報を有している。データセット1は、式1に示す部分論理式と標準値情報の組み合わせに対する充足値を示している。すなわち、i=0は注文明細のテーブルの1行目の購入数が空であることを示している。データセット2は、式2に示す部分論理式と標準値情報の組み合わせに対する充足値を示している。すなわち、i=4は注文明細のテーブルの5行目の購入数が空であることを示している。データセット3は、式3に示す部分論理式と標準値情報の組み合わせに対する充足値を示している。すなわち、0<i<4は注文明細のテーブルの3行目の購入数が空であることを示している。つまり、0と4の中間値である2に相当する3行目を空にしている。データセット4は、式4に示す部分論理式と標準値情報の組み合わせに対する充足値を示している。すなわち、i=0は注文明細のテーブルの1行目の品名が空であることを示している。データセット5は、式5に示す部分論理式と標準値情報の組み合わせに対する充足値を示している。すなわち、i=4は注文明細のテーブルの5行目の品名が空であることを示している。データセット6は、式6に示す部分論理式と標準値情報の組み合わせに対する充足値を示している。すなわち、0<i<4は注文明細のテーブルの3行目の品名が空であることを示している。つまり、0と4の中間値である2に相当する3行目を空にしている。ステップS20では、生成部203が生成されたテストデータ生成情報各々に対応するテストデータデータセット情報を記憶部3に記憶する。本実施の態様によれば、事前条件を表す論理式に全称記号や存在記号が含まれる場合でも、境界値制約を用いて、組み合わせ爆発を抑えたテストデータを生成することができる。従来の組み合わせ数=i存在記号により特定されるテーブルの行数×m存在記号に関連する論理式内の組合せであったが、本実施の態様を適応した組み合わせ数=L同値クラス数×m存在記号に関連する論理式内の組合せとなる。すなわち、i>Lとなる可能性が大きいため、組み合わせを削減する効果がある。また、テーブルの行数iが大きくなればなるほど効果が高くなる。また、本発明は、上記実施の形態に限定されるものでなく、本発明の要旨を逸脱しない範囲内で種々の改良、変更が可能である。"