"コンピュータに、検査対象のソフトウェアの入力値に関する制約条件を示す論理式のデータが記憶された記憶部を参照して、前記論理式のデータに、等号付き不等号が含まれるか否かを判定し、前記判定において含まれると判定した場合に、前記記憶部に記憶された前記等号付き不等号を等号に変換する処理を実行させることを特徴とする論理式変換プログラム。前記コンピュータに前記判定において含まれると判定した場合に、前記記憶部に記憶された前記等号付き不等号で示される論理式を、前記等号付き不等号を等号に変換した論理式と、前記等号付き不等号を不等号に変換した論理式との論理和で示される論理式のデータに変換する処理を実行させることを特徴とする請求項1記載の論理式変換プログラム。前記論理式に否定が係る不等号が含まれるか否かを更に判定し、前記判定において前記否定が係る不等号が含まれると判定した場合に、前記記憶部に記憶された前記否定が係る不等号で示される論理式を、前記不等号と背反となる不等号で示される論理式のデータに変換する処理を前記コンピュータに実行させることを特徴とする請求項1又は2記載の論理式変換プログラム。前記論理式に否定が係る論理積が含まれるか否かを判定し、前記判定において前記否定が係る論理積が含まれると判定した場合に、前記記憶部に記憶された前記否定が係る論理積で示される論理式のデータを、前記論理積の左辺及び右辺の論理式に各々否定が係る論理式及び該否定が係る論理式のうちの一方を左辺、他方を右辺とする論理和で示される論理式のデータに変換する処理を前記コンピュータに実行させることを特徴とする請求項1から3のいずれかに記載の論理式変換プログラム。前記論理式に否定が係る論理和が含まれるか否かを判定し、前記判定において前記否定が係る論理和が含まれると判定した場合に、前記記憶部に記憶された前記否定が係る論理和で示される論理式のデータを、前記論理和演算子の左辺及び右辺の論理式の各々に否定が係り、該否定が係る論理式のうちの一方を左辺、他方を右辺とする論理積で示される論理式のデータに変換する処理を前記コンピュータに実行させることを特徴とする請求項1から4のいずれかに記載の論理式変換プログラム。前記論理式に含意が含まれるか否かを判定し、前記判定において前記含意が含まれると判定した場合に、前記記憶部に記憶された前記含意で示される論理式のデータを、前記含意の左辺の論理式に否定が付いた第1の論理式と、前記第1の論理式と、前記含意の右辺のうち、一方を左辺、他方を右辺とする論理積で示される論理式とに変換する処理を前記コンピュータに実行させることを特徴とする請求項1から5のいずれかに記載の論理式変換プログラム。前記論理式に論理積が係る論理和が含まれるか否かを判定し、前記判定において前記論理積が係る論理和が含まれると判定した場合に、前記記憶部に記憶された前記論理積が係る論理和で示される論理式のデータを、前記論理積の左辺を第1の辺とし前記論理和の前記論理積が係らない辺である他方の辺を第2の辺とする第1の論理和と、前記論理積の右辺を第1の辺とし前記他方の辺を第2の辺とする第2の論理和と、前記第1の論理和を第1の辺とし前記第2の論理和を第2の辺とする論理積とで示される論理式のデータに変換する処理を前記コンピュータに実行させることを特徴とする請求項1から6のいずれかに記載の論理式変換プログラム。前記判定において、前記論理積が係る論理和が含まれないと判定した場合に、前記記憶部に記憶された前記論理式のデータを、論理和を含まず、かつ、論理積で結合された論理式の部分論理式毎に分割し、前記分割した各々の部分論理式のデータを、充足可能性の判定対象の論理式のデータとして前記記憶部に記憶する処理を前記コンピュータに実行させることを特徴とする請求項7に記載の論理式変換プログラム。検査対象のソフトウェアの入力値に関する制約条件を示す論理式のデータを記憶する記憶部と、前記記憶部に記憶された論理式に、等号付き不等号が含まれるか否かを判定する判定部と、前記判定部が含まれると判定した場合に、前記記憶部に記憶された前記等号付き不等号を等号に変換する論理式変換部と、を備える論理式変換装置。コンピュータが、検査対象のソフトウェアの入力値に関する制約条件を示す論理式データが記憶された記憶部を参照して、前記論理式に、等号付き不等号が含まれるか否かを判定し、前記判定において含まれると判定した場合に、前記記憶部に記憶された前記等号付き不等号を等号に変換する処理を実行することを特徴とする論理式変換方法。業務システムのソフトウェアをテストするにあたり、プログラムのエラーはデータの境界で起こりやすいという経験則に鑑みたテストデータを用意する必要がある。この経験則に鑑みたテストを境界値テストと呼ぶ。境界値テストとは、入力を、有効なデータの範囲と無効なデータの範囲に分け、その境界となる値、即ち境界値を用いて行うテストである。この境界値は、上述の制約式の充足値の範囲に含まれる値であり、完全に同一となる値ではない。例えば、項目Aのデータの値の範囲を表わす制約式として、5≦Aという制約式が与えられたとする。上記のSMTソルバは、この制約式について、5以上のいかなる値も充足値として出力し得る。一方、境界値テストとして有意な値は5である。このように、テストしたい状況として、項目や変数の値の範囲が論理式で表わされた制約式を、SMTソルバを用いて解いても、上記境界値テストの条件を満足する充足解、つまり、境界値となるテストデータが得られる保証はなかった。開示する技術が解決しようとする課題は、論理式に境界値に係る制約が含まれる場合に、この論理式を、SMTソルバが境界値を確実に出力可能な論理式に変換することにある。開示する技術は、検査対象のソフトウェアの入力値に関する制約条件を示す論理式のデータが記憶された記憶部を参照して、前記論理式のデータに、等号付き不等号が含まれるか否かを判定する。開示する技術は、前記判定において含まれると判定した場合に、前記記憶部に記憶された前記等号付き不等号を等号に変換する。開示する技術によれば、論理式に境界値に係る制約が含まれる場合に、この論理式を、SMTソルバが境界値を確実に出力可能な論理式に変換することが出来る、という効果が得られる。以下、実施形態について詳細に説明する。図1に示すように、情報処理装置10は、CPU12、ROM14、RAM16、HDD18、通信インタフェース20、及びこれらを相互に接続するためのバス22を備えている。CPU12は、各種プログラムを実行する。ROM14には、各種プログラムやパラメータ等が記憶されている。RAM16は、CPU12による各種プログラムの実行時におけるワークエリア等として用いられる。記録媒体としてのHDD18には、後述するテストデータ生成処理ルーチンを実行するためのプログラム及び充足可能性を判定する処理を行うプログラムを含む各種プログラムや各種データが記憶されている。情報処理装置10を、テストデータ生成処理ルーチンを実行するためのプログラム及び充足可能性を判定する処理を行うプログラムに沿って、機能ブロックで表わすと、図2に示すようになる。情報処理装置10は、プロパティ記憶部30、論理式木構造生成部32、否定標準形変換部34、否定付き不等号除去変換部36、及び境界値制約生成部38を備えている。情報処理装置10は、更に、テストデータ生成部40、データ生成用プロパティ記憶部41、及び充足可能性判定部42、及びテストデータ記憶部44を備えている。なお、境界値制約生成部38は、等号付き不等号変換部及び選言標準形変換部の一例である。プロパティ記憶部30には、情報処理装置10に入力された、検査対象のソフトウェアの論理的仕様を定める情報であるプロパティが記憶されている。検査対象のソフトウェアは、例えば画面とDBデータベースを有するウェブシステムのためのソフトウェアであり、当該画面には、例えばユーザ、住所、購入個数及び合計などの項目が含まれている。また、本実施形態において、プロパティには、例えば、合計が5000円以上かつ購入個数が5個以内で、住所が東京又は神奈川で会った場合、郵送料が無料となるという業務仕様が設定されている。また、上記の業務仕様における事前条件として、検証対象のソフトウェアの入力値に関する制約条件を示す論理式データが、プロパティ記憶部30に記憶されている。例えば、以下に示す論理式データが記憶されている。事前条件:合計≧5000∧購入個数≧1∧購入個数≦5∧住所=東京∨住所=神奈川上記のように、論理式データは、文字列、数値、論理演算子含意→、論理和∨、論理積∧、否定¬、関係演算子等号=、不等号>、<、≧、≦、、及び括弧を用いて記述されている。論理式木構造生成部32は、プロパティ記憶部30から、事前条件を示す論理式データを読み込み、読み込んだ論理式データの論理構造を解析して、図3及び図4に示すような木構造形式のデータを生成して、RAM16に格納する。図3は、木構造形式のデータの模式図である。また、図4は、RAM16に格納された木構造形式のデータの一例を示す図である。論理式木構造生成部32は、図3に円形又は矩形で示す木構造データのノード毎に、図4に示すNo、値、演算子、左ノード、右ノードの各項目値を含むレコードをRAM16に格納する。図3の最上位のノードは、図4のNoが0の行に相当する。否定標準形変換部34は、木構造形式の論理式データを参照し、入力された論理式を否定標準形に変換する処理を行う。否定標準形とは、部分論理式を持たない論理式である原子論理式にのみ否定が係り、他には論理和と論理積のみが論理演算子として用いられる形の論理式である。入力された論理式に境界値に係る制約を示す等号付き不等号が含まれない場合でも、この処理を行うことにより、原子論理式にのみ否定が係るように変形出来、境界値に係る制約を示す等号付き不等号部分を見出せるようになる。従って、入力された論理式が否定標準形である場合には、否定標準形変換部34によるこの処理は不要である。否定標準形変換部34は、木構造形式の論理式データに対し、以下に示すような変換法則1を適用し、含意演算子→を含む部分木を、含意演算子を含まない含意演算子が除去された部分木に変換する図5、図6を参照。具体的には、否定標準形変換部34は、含意演算子を含む論理式を、含意演算子の前左辺に記述されている論理式の否定と、含意演算子の後右辺に記述されている論理式との論理和に変換する処理を行う。なお、入力された論理式に含意演算子が含まれない場合には、この変換法則1の適用処理は不要である。変換法則1:s1→s2を¬s1∨s2に変換なお、ここで、s1、s2は部分論理式又は原子論理式を示す。否定標準形変換部34は、木構造形式の論理式データから、含意演算子がなくなるまで、論理式データに対して上記の変換法則1を適用する処理を繰り返すことで、論理式データから含意演算子を除去し、論理式データ内の論理演算子を論理積、論理和、否定の3種類のみとすることが出来る。また、否定標準形変換部34は、木構造形式の論理式データに対し、以下に示すような変換法則2を適用し、二重否定を含む部分木を、二重否定を含まない二重否定が除去された部分木に変換する図7,図8を参照。なお、図7及び図8は、ぞれぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図である。この処理は、入力された論理式に含意演算子が含まれ、上述の変換法則1の適用含意演算子の除去処理により否定¬が生じ、この否定が、入力された論理式に元から存在した否定¬に係るようになった場合又は含意演算子が含まれていなくても二重否定が含まれている場合に必要となる処理である。従って、入力された論理式データに、含意演算子と否定を含む部分木、又は、二重否定を含む部分木のいずれも含まれない場合は、この変換法則2の適用処理は不要である。変換法則2:¬¬s1をs1に変換なお、ここでs1は部分論理式又は原子論理式を示す。否定標準形変換部34は、木構造形式の論理式データから、二重否定がなくなるまで、論理式データに対して上記の変換法則2を適用する処理を繰り返すことで、論理式データから二重否定冗長な否定の部分木を除去することが出来る。また、否定標準形変換部34は、木構造形式の論理式データに対し、以下に示すようなドモルガンの法則として知られている変換法則3、4を適用する。これによって、否定標準形変換部34は、論理積の否定及び論理和の否定を含む部分木を、論理積の否定及び論理和の否定を含まない論理積の否定及び論理和の否定が除去された部分木に変換する図9、図10、図11、図12を参照。なお、図9及び図11、図10及び図12は、ぞれぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図である。具体的には、否定標準形変換部34は、論理積の否定を、論理積の前左辺に記述されている論理式の否定と、論理積の後右辺に記述されている論理式の否定との論理和に、また、論理和の否定を、論理和の前左辺に記述されている論理式の否定と、論理和の後右辺に記述されている論理式の否定との論理積に変換する処理を行う。なお、入力された論理式が否定標準形である場合には、この変換法則3、4の適用処理は不要である。変換法則3:¬s1∧s2を¬s1∨¬s2に変換変換法則4:¬s1∨s2を¬s1∧¬s2に変換なお、ここで、s1、s2は部分論理式又は原子論理式を示す。否定標準形変換部34は、例えば、以下に示すように、ドモルガンの法則に基づく変換法則を適用可能な部分木が表わす論理積の否定図13、図15参照。なお、図13及び図15は、それぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図であるを、部分木が表わす2つの論理式の各々の否定の論理和図14、図16参照。なお、図14及び図16はそれぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図であるに変換する。¬購入個数>5∧購入個数<10⇒¬購入個数>5∨¬購入個数<10否定標準形変換部34は、木構造形式の論理式データが、否定が原始論理式のみに係る木構造形式の論理式データに変換されるまで、論理式データに対して上記の変換法則3、4を適用する処理を繰り返すことで、論理積、論理和、否定を含む論理式を否定標準形に変換することが出来る。このように、否定標準形変換部34は、木構造形式の論理式データに対し、含意演算子→を除去するための変換法則1、二重否定を除去するための変換法則2、及びドモルガンの法則に基づく変換法則3、4を適用する。これによって、否定標準形変換部34は、事前条件を示す木構造形式の論理式データを、否定が原子論理式のみに係り、かつ、論理和又は論理積で結合された形式である否定標準形で表わされる木構造形式の論理式データに変換する。また、否定付き不等号除去変換部36は、否定標準形の論理式データに変換された木構造形式の論理式データに対し、以下に示すような変換法則5~8を適用し、不等号に係る否定の部分木を、不等号に係る否定を含まない不等号に係る否定が除去された部分木に変換する図17~図24を参照。なお図17及び図21、図118及び図22、図19及び図23、図20及び図24は、それぞれ、ぞれぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図である。具体的には、否定付き不等号除去変換部36は、各々、不等号に否定が係っている論理式を、当該不等号と背反の不等号を用いた論理式に変換する。なお、入力された論理式が、連言標準形又は選言標準形であって、且つ、否定を含まない場合には、この変換法則5~8の適用処理は不要である。変換法則5:¬a1<a2をa1≧a2に変換変換法則6:¬a1≦a2をa1>a2に変換変換法則7:¬a1>a2をa1≦a2に変換変換法則8:¬a1≧a2をa1<a2に変換なお、ここで、a1、a2は部分論理式又は原子論理式を示す。否定付き不等号除去変換部36は、図25、図27に示すような不等号に係る否定を除去するための変換法則を適用可能な部分木¬購入個数>5、¬購入個数<10を、図26、図28に示すような部分木購入個数≦5、購入個数≧10に変換する。否定付き不等号除去変換部36は、この処理を実行することにより、入力された論理式を、否定付きの不等号で示される無効な範囲を示す論理式から、否定のない不等号で示される有効な範囲を示す論理式に変換することが出来る。境界値制約生成部38は、不等号に係る否定が除去された木構造形式の論理式データに対し、以下に示すような変換法則9、10を適用する。これによって、境界値制約生成部38は、等号付き不等号演算子を用いた論理式を、等号を用いた論理式と等号なし不等号演算子を用いた論理式との論理和を示す論理式に変換する図29、図30、図31、図32を参照。なお、図29及び図31、図30及び図32は、それぞれ、ぞれぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図である。変換規則9:a1≧a2をa1=a2∨a1>a2に変換変換規則10:a1≦a2をa1=a2∨a1<a2に変換なお、ここで、a1、a2は部分論理式又は原子論理式を示す。境界値制約生成部38は、木構造形式の論理式データから、等号付き不等号がなくなるまで、論理式データに対して上記の変換法則9及び変換法則10を適用する処理を繰り返すことにより、論理式データから等号付き不等号演算子を、等号を用いた論理式と、不等号を用いた論理式との論理和を示す論理式に変換する。境界値制約生成部38は、例えば、図33、図35に示す等号付き不等号を用いた論理式を示す部分木購入個数≦5、購入個数≧10を、図34、図36に示す部分木購入個数=5∨購入個数<5、購入個数=10∨購入個数>10に変換する。ここで、等号を用いた論理式は、入力値に関する上限境界値又は下限境界値を表わす。また、不等号を用いた論理式は、入力値の代表値として上限境界値より小さい値又は下限境界値より大きい値を表わす。境界値制約生成部38は、この処理により、境界値を表わす等号付き不等号で示される論理式を、境界値テストの制約を満たす等号で示される論理式と、代表値を表わす不等号で示される論理式とに分解する変換を行うことが出来る。なお、境界値テストの制約を満たすデータを得るためには、分解した論理式のうち、等号を用いた論理式のみが得られれば良い。従って、境界値制約生成部38は、等号付き不等号を等号のみに変換するようにしても良い。テストデータ生成部40は、境界値制約生成部38によって変換された木構造形式の論理式データに対し、以下に示すような分配法則に基づく変換法則11~12を適用し、論理積∧と論理和∨が連続する部分木のない宣言標準形で表わされた木構造形式の論理式データに変換する。具体的には、テストデータ生成部40は、論理積∧と論理和∨が連続する部分木がなくなるまで、木構造の論理式データに含まれる論理積∧と論理和∨が連続する部分木を論理積∧の2つの下位ノードの内、論理和∨として注目していない方のノードと、論理和として注目しているノードの更に下位のノード各々の2つの論理積∧の論理和で示される部分木に変換する処理を繰り返し実行する。これによって、テストデータ生成部40は、論理和を含まない論理式を1つの節として複数の節が論理和で結合された形式である選言標準形で表わされた木構造形式の論理式データに変換することが出来る。変換法則11:s1∧s2∨s3をs1∧s2∨s1∧s3に変換変換法則12:s1∨s2∧s3をs1∧s3∨s2∧s3に変換変換法則11~12を適用した変換を、図37、図38、図39、図40に示す。なお、図37及び図39、図38及び図40は、ぞれぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図である。テストデータ生成部40は、例えば、以下に示すように、木構造形式の論理式データ図41、図43を参照を、論理和を含まない複数の論理式が論理和で結合された選言標準形で表わされる木構造形式の論理式データに変換する。購入個数=5∨購入個数<5∧住所=東京∨住所=埼玉⇒購入個数=5∧住所=東京∨購入個数=5∧住所=埼玉∨購入個数<5∧住所=東京∨購入個数<5∧住所=埼玉∨購入個数=10∧住所=東京∨購入個数=10∧住所=埼玉∨購入個数>10∧住所=東京∨購入個数>10∧住所=埼玉テストデータ生成部40は、変換した選言標準形で表わされる木構造形式の論理式データを、選言標準形の節論理和を含まず、かつ、論理積で結合された論理式の部分ごとに部分木データに分解する。これによって、選言標準形で表わされた事前条件式が、真理値の取り方が一意に定まる複数の事前条件式に分割される。テストデータ生成部40は、分解した各節について、当該節の部分木データを文字列で記述される論理式データに変換して、データ生成用プロパティ記憶部41に記憶する。テストデータ生成部40は、データ生成用プロパティ記憶部41に記憶された各節の論理式データを順に、充足可能性判定部42へ出力する。また、テストデータ生成部40は、充足可能性判定部42から各節について出力された充足解データを、検査対象のソフトウェアに対する入力値の一組のテストデータとして、テストデータ記憶部44に記憶されたテストデータテーブルに節毎に格納する。充足可能性判定部42は、入力された論理式データが示す制約条件の充足可能性を判定すると共に、制約条件が充足可能であると判定されたときに得られる充足解データを、テストデータ生成部40へ出力する。例えば、以下に示す各節の論理式データが、充足可能性判定部42へ入力されると、図45に示すような、充足解データが各々出力され、複数組のテストデータとして、テストデータ記憶部44に記憶されたテストデータテーブルに格納される。論理式データ1:購入個数=5∧住所=東京論理式データ2:購入個数=5∧住所=埼玉論理式データ3:購入個数<5∧住所=東京論理式データ4:購入個数<5∧住所=埼玉論理式データ5:購入個数=10∧住所=東京論理式データ6:購入個数=10∧住所=埼玉論理式データ7:購入個数>10∧住所=東京論理式データ8:購入個数>10∧住所=埼玉テストデータ生成部40は、この処理により、入力値に関する境界値のバリエーションと入力値に関する制約条件のバリエーションとの組合せを全て考慮した複数組のテストデータを生成することが出来る。次に、本実施の形態の作用を説明する。情報処理装置10に、他の装置から通信インタフェース20を介して、検査対象のソフトウェアの論理的仕様を定める情報であるプロパティが入力され、プロパティ記憶部30に記憶される。プロパティ記憶部30に記憶されているプロパティには、業務仕様が設定されており、業務仕様における事前条件として、検証対象のソフトウェアの入力値に関する制約条件を示す論理式データが含まれている。そして、オペレータが、情報処理装置10の操作部図示省略を操作して、検証対象のソフトウェアの入力値に関するテストデータの生成を指示する。これによって、情報処理装置10のCPU12によって、HDD18に記憶された図46、47に示すテストデータ生成処理ルーチンを実行するためのプログラムが実行される。まず、S100において、情報処理装置10が、プロパティ記憶部30から、検証対象のソフトウェアのプロパティを読み込み、プロパティに含まれている制約条件を示す論理式データの論理構造を解析して、論理式データを木構造形式の論理式データへ変換する。論理式木構造生成部32は、Noの項目に、ノードを識別する番号を格納する。本実施形態では、論理式木構造生成部32は、図3に示す最上位のノードの場合は0、最上位の左の枝の先のノードの場合は1、最上位の右の枝の先のノードの場合は2と、最上位のノードから順次昇順となる番号を格納する。論理式木構造生成部32は、値の項目に、ノードに入る値を格納する。本実施形態では、論理式木構造生成部32は、リーフ末端のノードにのみ値を格納する。論理式木構造生成部32は、演算子の項目に、含意→、論理和∨、論理積∧、否定¬、等号=、不等号>、<、≧、≦のいずれかの演算子を格納する。また、論理式木構造生成部32は、左ノードの項目に左の枝の先のノードのNoを、右ノードの項目に右の枝の先のノードのNoを、それぞれ格納する。本実施形態では、論理式木構造生成部32は、先のノードが1つしかない場合には、左ノードの項目にこの先のノードのNoを格納する図4参照。なお、論理式木構造生成部32はパーサとして知られる任意の公知のプログラムを、テストデータ生成処理ルーチンを実行するためのプログラムに組み込み、このパーサをCPU12が実行することにより実現可能であり、詳細な説明は割愛する。また、この図3Bに示すデータのレイアウトは一例であり、他の公知の木構造形式のデータレイアウトの利用を妨げるものではない。そして、S102において、情報処理装置10が、含意演算子除去の処理を実行する。図18は情報処理装置10による含意演算子除去の処理フローチャートを示す。情報処理装置10は、S201で、図3に示す最上位のノード、つまり図4に示すNoの項目値が0のノードから順に左ノード項目値及び右ノード項目値に格納されたポインタを辿りながら、演算子の項目値が含意→のノードを検索する。そして、情報処理装置10は、S202で、S201での検索の結果、演算子の項目値が含意→であるノードが検索出来たか否かを判定する。否定標準形変換部34は、S202で、検索出来たと判定した場合、S203で、左ノードの項目の値をRAM16の図示しない左ノード項目値退避領域に記憶する。次に、情報処理装置10は、S204で、RAM16に格納された、このノードの演算子の項目値を、含意から論理和に更新する。そして、情報処理装置10は、S205で、RAM16に格納された、このノードの左ノードの項目値を、新しい番号に更新する。例えば、情報処理装置10は、この新しい番号として、RAM16のNoの項目の最大値に1加算した値を採用する。なお、RAM16のNoの項目値にまだ格納されていない任意の番号を採用するようにしてもよい。そして、情報処理装置10は、S206で、Noの項目にS208の処理で用いた新しい番号、演算子の項目に否定、左ノードの項目に左ノード項目値退避領域の値をそれぞれ格納した新しいノードのデータを生成し、RAM16に追加格納する。その後、情報処理装置10は、S201の処理に進む。そして、情報処理装置10は、S201での検索の結果、演算子の項目値が含意→であるノードが検索出来なかったと判定した場合には、含意演算子除去の処理を終了する。このように、情報処理装置10は、処理対象の木構造の論理式データについて、含意演算子が検索出来なくなるまで、含意演算子除去の処理を繰り返し実行することで、木構造形式の論理式データから、含意演算子を除去することが出来る。なお、この含意演算子除去の処理フローチャートは一例であって、論理式に含まれる全ての含意演算子について、含意演算子の前左辺に記述されている論理式の否定と、含意演算子の後右辺に記述されている論理式との論理和に変換する他の任意の処理手順の利用を否定するものではない。S106では、情報処理装置10が、含意演算子が除去された木構造形式の論理式データについて、二重否定除去処理を実行する。図49は、情報処理装置10による二重否定除去の処理フローチャートを示す。情報処理装置10は、S301で、図3に示す最上位のノード、つまり図4に示すNoの項目値が0のノードから順に左ノード項目値及び右ノード項目値に格納されたポインタを辿りながら、演算子の項目値が否定¬であるノードが2つ連続する二重否定の部分木を検索する。次に、情報処理装置10は、S302で、S301での検索の結果、演算子の項目値が否定¬であるノードが2つ連続する二重否定の部分木が検索出来たか否かを判定する。情報処理装置10は、S302で、検索出来たと判定した場合、S303で、検索された部分木の下位のノードの更に下位のノードのNo以外の項目値を取得する。なお、検索された部分木の下位のノードの更に下位のノードとは、つまり上位ノードの演算子項目値及び自ノードの演算子項目値が否定¬であるノードの左ノードの項目値をNoとするノードのことである。また、No以外の項目値とは、値、演算子、左ノード及び右ノードの各項目値のことである。次に、情報処理装置10は、S304で、検索された部分木の上位のノードについてRAM16に格納されたNo以外の各項目値を、S303で取得した各項目値にそれぞれ更新する。その後、情報処理装置10は、S301の処理に進む。そして、情報処理装置10は、S301での検索の結果、演算子の項目値が否定¬であるノードが2つ連続する二重否定の部分木が検索出来なかったと判定した場合には、二重否定除去の処理を終了する。このように、情報処理装置10は、処理対象の木構造の論理式データについて、二重否定が検索出来なくなるまで、二重否定除去の処理を繰り返し実行することで、木構造形式の論理式データから、二重否定を除去することが出来る。なお、この二重否定除去の処理フローチャートは一例であって、論理式に含まれる全ての二重否定を除去する他の任意の処理手順の利用を否定するものではない。S110では、情報処理装置10が、全ての二重否定が除去された木構造形式の論理式データについて、ドモルガンの法則に基づく論理式の否定標準形への変換の処理を実行する。図50は情報処理装置10によるドモルガンの法則に基づく論理式の否定標準形への変換の処理フローチャートを示す。情報処理装置10は、S401で、図3、図13に示す最上位のノード、つまり図3Bに示すNoの項目値が0のノードから順に、左ノード項目値及び右ノード項目値に格納されたポインタを辿りながら、演算子の項目値が否定→のノードと論理演算子論理和∨又は論理積∧であるノードが連続する部分木を検索する。次に、情報処理装置10は、S402で、S401での検索の結果、演算子の項目値が否定→のノードと、演算子の項目値が論理演算子論理和または論理積であるノードとが連続する部分木が検索出来たか否かを判定する。情報処理装置10は、S402で、検索出来たと判定した場合、S403で、演算子項目値は論理和∨か否かを判定する。情報処理装置10は、S403で論理和∨であると判定すると、S404で、検索された部分木の上位のノード、つまり演算子が否定¬のノードについて、RAM16に格納された演算子の項目値を否定¬から論理積∧に更新する。一方、情報処理装置10は、S403で論理和∨でないと判定すると、S405で、検索された部分木の上位のノード、つまり演算子が否定¬のノードについて、RAM16に格納された演算子の項目値を否定¬から論理和∨に更新する。なお、上記S403の説明では論理和か否かを判定することとしたが、論理積か否かを判定することにしても良い。この場合には、論理積であると判定した場合にS405の処理を行い、論理積でないと判定した場合にS404の処理を行うようにすれば良い。情報処理装置10は、S404又はS405の処理が終わると、S406の処理に進み、S406で、検索された部分木の下位ノード、つまり演算子が論理演算子論理和∨又は論理積∧のノードの左ノード及び右ノードの項目値を取得する。情報処理装置10は、S407で、S404又はS405で処理した上位ノードの左ノード及び右ノードの項目値をそれぞれ新しい番号に更新する。例えば、情報処理装置10は、この左ノードの新しい番号として、RAM16のNoの項目の最大値に1加算した値、右ノードの新しい番号として、この左ノードの新しい番号に更に1加算した値を格納する。なお、RAM16のNoの項目値にまだ格納されていない任意の番号をそれぞれ格納するようにしてもよい。情報処理装置10は、S408で、Noの項目にはS407で上位ノードの左ノードの項目に格納した新しい番号を、演算子の項目には否定を、左ノードの項目にはS406で取得した左ノードの項目値を、それぞれ格納した新しいノードのデータを生成し、RAM16に追加格納する。また、情報処理装置10は、S409で、Noの項目にはS406で上位ノードの右ノードの項目に格納した新しい番号を、演算子の項目には否定を、左ノードの項目にはS406で取得した右ノードの項目値を、それぞれ格納した新しいノードのデータを生成し、RAM16に追加格納する。その後、情報処理装置10は、S401の処理に進む。そして、情報処理装置10は、S401での検索の結果、演算子の項目値が否定→のノードと、演算子の項目値が論理演算子論理和または論理積であるノードとが連続する部分木が検索出来なかったと判定した場合には、ドモルガンの法則に基づく論理式の否定標準形への変換の処理を終了する。このように、情報処理装置10は、処理対象の木構造の論理式データについて、演算子の項目値が否定→のノードと論理演算子論理和∨又は論理積∧であるノードが連続する部分木が検索出来なくなるまで、ドモルガンの法則に基づく論理式の否定標準形への変換の処理を繰り返し実行する。否定標準形変換部34は、この処理を実行することにより、論理積、論理和、否定を含む木構造形式の論理式データを、該論理式データに含まれる否定が原子論理式のみに係る否定標準形の論理式データに変換することが出来る。なお、このドモルガンの法則に基づく論理式の否定標準形への変換の処理フローチャートは一例であって、論理積、論理和及び否定以外の論理演算子を含まない論理式を否定標準形に変換可能な他の任意の処理手順の利用を否定するものではない。上記のS102~S110図48から図50の処理によって、木構造形式の論理式データが表す論理式が、否定標準形の論理式に変換される。S114では、情報処理装置10が、否定標準形に変換された木構造形式の論理式データについて、不等号に係る否定の除去の処理を実行する。図51は情報処理装置10による不等号に係る否定の除去の処理フローチャートを示す。否定付き情報処理装置10は、S501で、図14、図25に示す最上位のノード、つまり図16、図27に示すNoの項目値が0のノードから順に左ノード項目値及び右ノード項目値に格納されたポインタを辿りながら、演算子の項目値が否定¬であるノードと、演算子の項目値が不等号不等号<、>及び等号付き不等号≦、≧の内のいずれかであるノードとが連続する、否定つき不等号の部分木を検索する。次に、情報処理装置10は、S502で、S501での検索の結果、演算子の項目値が否定¬であるノードと、演算子の項目値が不等号不等号<、>及び等号付き不等号≦、≧の内のいずれかであるノードとが連続する、否定つき不等号の部分木が検索出来たか否かを判定する。情報処理装置10は、S502で、検索出来たと判定した場合、S503で、検索された部分木の下位ノード、つまり演算子が不等号不等号<、>及び等号付き不等号≦、≧の内のいずれかであるノードについて、演算子項目値の不等号は等号付き不等号≧または≦であるか否かを判定する。情報処理装置10は、S503で等号付き不等号≧または≦であると判定すると、S504で、検索された部分木の上位ノード、つまり演算子が否定¬であるノードについて、RAM16に格納された、演算子の項目値を、否定¬から、このノードの下位ノードの演算子の項目値である等号付き不等号≧または≦と背反となる等号なし且つ逆向きの不等号<または>に更新する。つまり、否定標準形変換部34は、RAM16に格納された下位ノードの演算子の項目値が≧である場合には上位ノードの演算子の項目値を<、下位ノードの演算子の項目値が≦である場合には上位ノードの演算子の項目値を>にそれぞれ更新する。一方、情報処理装置10は、S503で等号付き不等号≧または≦でないと判定すると、S504で、検索された部分木の上位ノード、つまり演算子が否定¬であるノードについて、RAM16に格納された、演算子の項目値を、否定¬から、このノードの下位ノードの演算子の項目値である等号なし不等号>または<と背反となる等号なし且つ逆向きの不等号≦または≧に更新する。つまり、否定標準形変換部34は、検索された部分木について、RAM16に格納された、下位ノードの演算子の項目値が>である場合には上位ノードの演算子の項目値を≦、下位ノードの演算子の項目値が<である場合には上位ノードの演算子の項目値を≧にそれぞれ更新する。なお、上記S503の説明では等号付き不等号か否かを判定することとしたが、統合なし不等号か否かを判定することにしても良い。この場合には、等号なし不等号であると判定した場合にS505の処理を行い、等号なし不等号でないと判定した場合にS504の処理を行うようにすれば良い。情報処理装置10は、S504又はS505の処理が終わると、S506の処理に進み、検索された部分木の下位ノードの左ノード及び右ノードの項目値をそれぞれ取得する。そして、情報処理装置10は、S507で、RAM16に格納された、検索された部分木の上位ノードの左ノード及び右ノードの項目値を、S506で取得した左ノード及び右ノードの項目値にそれぞれ更新する。その後、情報処理装置10は、S501の処理に進む。そして、情報処理装置10は、S501での検索の結果、演算子の項目値が否定¬であるノードと、演算子の項目値が不等号不等号<、>及び等号付き不等号≦、≧の内のいずれかであるノードとが連続する、否定つき不等号の部分木が検索出来なかったと判定した場合には、不等号に係る否定の除去の処理を終了する。このように、情報処理装置10は、処理対象の木構造の論理式データについて、演算子の項目値が否定¬であるノードと、演算子の項目値が不等号不等号<、>及び等号付き不等号≦、≧の内のいずれかであるノードとが連続する、否定つき不等号の部分木が検索出来なくなるまで、不等号に係る否定の除去の処理を繰り返し実行することで、木構造形式の論理式データから、不等号に係る否定を除去することが出来る。なお、この否定付き不等号除去の処理フローチャートは一例であって、論理式に含まれる全ての否定付き不等号を除去する他の任意の処理手順の利用を否定するものではない。S118では、情報処理装置10が、不等号に係る否定が全て除去された木構造形式の論理式データから、等号付き不等号演算子を除去するための変換法則を適用可能な部分木が存在するか否かを判定する。図52は境界値制約生成部38による等号付き不等号の変換の処理フローチャートを示す。境界値制約生成部38は、S601で、図26、図33に示す最上位のノード、つまり図28、図35に示すNoの項目値が0のノードから順に左ノード項目値及び右ノード項目値に格納されたポインタを辿りながら、演算子の項目値が等号付き不等号≦または≧であるノードを検索する。次に、境界値制約生成部38は、S602で、S601での検索の結果、演算子の項目値が等号付き不等号≦または≧であるノードが検索出来たか否かを判定する。境界値制約生成部38は、S602で、検索出来たと判定した場合、S603で、RAM16に格納された、検索されたノードの演算子の項目値を等号付き不等号から論理和∨に更新する。次に、境界値制約生成部38は、S604で、検索されたノードの左ノード及び右ノードの項目値をRAM16の図示しない左ノード項目値退避領域及び右ノード項目値退避領域に格納する。そして、境界値制約生成部38は、S605で、検索されたノードの左ノード及び右ノードの項目にそれぞれ新しい番号を格納する。例えば、境界値制約生成部38は、この左ノードの新しい番号として、RAM16のNoの項目の最大値に1加算した値、右ノードの新しい番号として、この左ノードの新しい番号に更に1加算した値を格納する。なお、RAM16のNoの項目値にまだ格納されていない任意の番号をそれぞれ格納するようにしてもよい。そして、境界値制約生成部38は、S606で、Noの項目にはS605で左ノードの項目に設定した新しい番号を、演算子の項目には等号なし不等号を、左ノードの項目にはRAM16の左ノード項目値退避領域の値を、右ノードの項目にはRAM16の右ノード項目値退避領域の値を、それぞれ設定した設定した新しいノードのデータを生成し、RAM16に追加格納する。つまり、境界値制約生成部38は、演算子の項目値が≦である場合には<、≧である場合には>を格納する。また、境界値制約生成部38は、S607で、Noの項目にはS605で右ノードの項目に設定した新しい番号を、演算子の項目には等号を、左ノードの項目にはRAM16の左ノード項目値退避領域の値を、右ノードの項目にはRAM16の右ノード項目値退避領域の値を、それぞれ設定した設定した新しいノードのデータを生成し、RAM16に追加格納する。なお、S606とS607の処理はいずれが先であっても良い。また、この等号付き不等号の変換の処理フローチャートは一例であって、論理式に含まれる全ての等号付き不等号を等号と不等号の論理式の論理和に変換する他の任意の処理手順の利用を否定するものではない。また、境界値制約を満たす解のみが得られれば良い場合には、境界値制約生成部38は、S604からS607の処理に代わり、検索されたノードの演算子の項目値を等号付き不等号≦または≧から等号=に更新する処理のみを行うようにしても良い。その後、境界値制約生成部38は、S601の処理に進む。そして、否定標準形変換部34は、S601での検索の結果、が検索出来なかったと判定した場合には、等号付き不等号の変換の処理を終了する。このように、境界値制約生成部38は、処理対象の論理式データについて、等号付き不等号が検索出来なくなるまで、等号付き不等号の変換の処理を繰り返し実行することで、等号付き不等号演算子を用いた論理式を分解する。境界値制約生成部38は、等号付き不等号演算子を用いた論理式を、等号を用いた論理式と、不等号を用いた論理式とに分解する。ここで、等号を用いた論理式は、入力値に関する上限境界値又は下限境界値を表わす。また、不等号を用いた論理式は、入力値の代表値として上限境界値より小さい値又は下限境界値より大きい値を表わす。つまり、境界値テストの制約を満たすデータを得るためには、分解した論理式のうち、等号を用いた論理式のみが得られれば良い。従って、境界値制約生成部38は、上述の通り、等号付き不等号を等号のみに変換するようにしても良い。S122では、情報処理装置10が、全ての等号付き不等号演算子が除去された木構造形式の論理式データについて、選言標準形への変換の処理を実行する。図53はテストデータ生成部40による選言標準形への変換の処理フローチャートを示す。テストデータ生成部40は、S701で、図34、図41に示す最上位のノード、つまり図36、図43に示すNoの項目値が0のノードから順に左ノード項目値及び右ノード項目値に格納されたポインタを辿りながら、演算子の項目値が論理積∧であるノードと、演算子の項目値が論理和∨であるノードが連続する部分木を検索する。次に、テストデータ生成部40は、S702で、S701での検索の結果、演算子の項目値が論理積∧であるノードと、演算子の項目値が論理和∨であるノードが連続する部分木が検索出来たか否かを判定する。テストデータ生成部40は、S702で、検索出来たと判定した場合、S703で、RAM16に格納された、検索された部分木の上位のノードつまり演算子の項目値が論理積∧であるノードの、演算子の項目値を、論理積∧から論理和∨に更新する。次に、テストデータ生成部40は、S704で、検索された部分木の上位のノードの左ノード及び右ノードの項目値を、RAM16の図示しない左ノード項目値退避領域及び右ノード項目値退避領域にそれぞれ格納する。次に、テストデータ生成部40は、S705で、検索された部分木の上位のノードの左ノード及び右ノードの項目値を、それぞれ新しい番号に更新する。例えば、テストデータ生成部40は、この左ノードの新しい番号として、RAM16のNoの項目の最大値に1加算した値、右ノードの新しい番号として、この左ノードの新しい番号に更に1加算した値を格納する。なお、RAM16のNoの項目値にまだ格納されていない任意の番号をそれぞれ格納するようにしてもよい。次に、テストデータ生成部40は、S706で、検索された部分木の下位のノード、つまり、演算子の項目値が論理和のノードの左ノード及び右ノードの項目値を取得する。そして、テストデータ生成部40は、S707で、検索された部分木の下位ノードのNoの項目値は左ノード項目値退避領域の値と一致するか否かを判定する。テストデータ生成部40は、S707で、一致すると判定した場合、S708で、Noの項目にはS705で上位ノードの左ノードに格納した新しい番号を、演算子の項目には論理積∧を、左ノードの項目にはS706で取得した下位ノードの左ノードの項目値を、右ノードの項目にはRAM16の左ノード項目値退避領域の値を、それぞれ格納した新しいノードのデータを生成し、RAM16に追加格納する。また、テストデータ生成部40は、S709で、Noの項目にはS705で上位ノードの右ノードに格納した新しい番号を、演算子の項目には論理積∧を、左ノードの項目にはS706で取得した下位ノードの右ノードの項目値を、右ノードの項目にはRAM16の左ノード項目値退避領域の値を、それぞれ格納した新しいノードのデータを生成し、RAM16に追加格納する。一方、テストデータ生成部40は、S707で、一致しないと判定した場合、S710で、Noの項目にはS705で上位ノードの左ノードに格納した新しい番号を、演算子の項目には論理積∧を、左ノードの項目にはRAM16の左ノード項目値退避領域の値を、右ノードの項目にはS706で取得した下位ノードの左ノードの項目値を、それぞれ格納した新しいノードのデータを生成し、RAM16に追加格納する。また、テストデータ生成部40は、S711で、Noの項目にはS705で上位ノードの右ノードに格納した新しい番号を、演算子の項目には論理積∧を、左ノードの項目にはRAM16の左ノード項目値退避領域の値を、右ノードの項目にはS706で取得した下位ノードの右ノードの項目値を、それぞれ格納した新しいノードのデータを生成し、RAM16に追加格納する。その後、否定標準形変換部34は、S701の処理に進む。そして、否定標準形変換部34は、S701での検索の結果、演算子の項目値が論理積∧であるノードと、演算子の項目値が論理和∨であるノードが連続する部分木が検索出来なかったと判定した場合には、選言標準形への変換の処理を終了し、図47に示すS126の処理に進む。上記のS122図53の処理によって、木構造形式の論理式データが表す否定標準形の論理式が、選言標準形の論理式に変換される。図41及び図43に示す論理式データについて、S703からS709の処理を1回実行した後の論理式データの例を図42及び図44に示す。この図に示すように、木構造の論理式データに含まれる論理積∧と論理和∨が連続する部分木を論理積∧の2つの下位ノードの内、論理和∨として注目していない方のノードと、論理和として注目しているノードの更に下位のノード各々の2つの論理積∧の論理和で示される部分木に変換する処理を、この論理式データから論理積∧と論理和∨が連続する部分木がなくなるまで繰り返すことにより、選言標準形の論理式に変換することが出来る。図47の説明に戻って、図47のS126では、情報処理装置10が、選言標準形の論理式を表わす木構造形式の論理式データを、選言標準形の節毎の部分木データに分割する。そして、S128において、情報処理装置10が、各節の部分木データを、各節の論理式を示す文字列データに変換してデータ生成用プロパティ記憶部41に記憶する。次のS130では、情報処理装置10が、データ生成用プロパティ記憶部41から、1つの節の論理式を示す文字列データを取得し、S132において、情報処理装置10が、取得した1つの節の論理式を示す文字列データを、充足可能性判定部42へ出力する。このとき、充足可能性判定部42は、入力された文字列データが示す論理式制約条件の充足可能性を判定すると共に、充足解データを求めて出力する。そして、S134において、情報処理装置10が、充足可能性判定部42から出力された充足解データを取得し、充足解データを一組のテストデータとして、テストデータ記憶部44のテストデータテーブルに格納する。次のS136では、情報処理装置10が、選言標準形の論理式の全ての節について、上記S130~S134の処理が実行されたか否かを判定する。上記S130~S134の処理が実行されていない節が存在すると判定された場合には、情報処理装置10は、上記S130へ戻り、未処理の節について、上記S130~S134の処理を実行する。一方、全ての節について、上記S130~S134の処理が実行されたと判定された場合には、情報処理装置10が、テストデータ生成処理ルーチンを終了する。そして、オペレータが、テストデータ記憶部44に記憶されたテストデータテーブルを用いて、情報処理装置10又は他の装置に、検査対象のソフトウェアの検査プログラムを実行させて、検査対象のソフトウェアの検査処理を行わせる。以上説明したように、本実施の形態に係る情報処理装置10は、検査対象のソフトウェアの入力値に関する制約条件を示す論理式データにおいて、等号付き不等号の論理式を、等号を用いた論理式に変換する。そしてこの論理式を選言標準形となるように変換して、選言標準形に変換した論理式の各節をそれぞれSMTソルバに入力する論理式として出力する。そして、情報処理装置10は、各節の論理式の充足解データを得ることにより、入力値に関する境界値テストを考慮したテストデータを生成することが出来る。また、本実施の形態に係る情報処理装置10は、業務仕様を満たし、且つ、境界値テストが可能なテストデータを自動的に生成することが出来る。本実施の形態に係る情報処理装置10は、入力値に関する境界値のバリエーションと入力値に関する制約条件のバリエーションとの組合せを全て考慮した複数組のテストデータを生成することが出来る。また、情報処理装置10は、テストを意識しない業務仕様記述から、より現実的なテストデータを生成することが出来る。また、境界値制約生成部38は、等号付き不等号演算子を、入力値に関する制約条件を示す論理式内に発見した場合、当該論理式を、ソフトウェアテストにおける経験則的な境界値テストのための論理式と入力値の代表値に関するテストのための論理式とに分解する。これによって、情報処理装置10は、代表値をテストするためのテストデータを生成すると共に、上界境界値又は下界境界値をテストするためのテストデータを生成することが出来る。なお、上記の実施の形態では、1つの情報処理装置で、テストデータを生成する処理と、充足可能性の判定処理とを行う場合を例に説明したが、これに限定されるものではない。例えば、テストデータを生成する処理を行う情報処理装置10とは別の情報処理装置が、充足可能性の判定処理を行うようにしてもよい。この場合には、情報処理装置10は、変換した選言標準形の論理式データの各節について、当該節の論理式を示す文字列データを、充足可能性の判定処理を行う他の情報処理装置へ出力し、当該他の情報処理装置から、充足解データを取得する。また、情報処理装置10は、テストデータ生成処理ルーチンを実行するためのプログラムとは別のプログラムによって、充足可能性の判定処理を実行する場合を例に説明したが、これに限定されるものではない。情報処理装置10は、テストデータ生成処理ルーチンを実行するためのプログラムにより、テストデータを生成する処理と、充足可能性の判定処理とを行うようにしてもよい。また、情報処理装置10は、含意演算子除去のための変換法則、二重否定除去のための変換法則、及びドモルガンの法則に基づく変換法則を順に論理式データに適用する場合を例に説明したが、これに限定されるものではない。情報処理装置10は、論理式データに対して、他の順序例えば、二重否定除去のための変換法則、含意演算子除去のための変換法則、及びドモルガンの法則に基づく変換法則の順で、上記の変換法則を適用してもよい。この場合には、情報処理装置10は、論理式データが、否定標準形の論理式データに変換されるまで、上記の変換法則を繰り返し適用すればよい。また、情報処理装置10は、検査対象のソフトウェアの入力値に関する制約条件を示す論理式データに基づいて、テストデータを生成する場合を例に説明したが、これに限定されるものではない。例えば、情報処理装置10は、ソフトウェアのモジュール部分を、検査対象として、検査対象のモジュール部分の入力値に関する制約条件を示す論理式データに基づいて、モジュール部分の入力値に関するテストデータを生成するようにしてもよい。また、情報処理装置10は、ハードウェアの機構に関して、特に限定されない。上記では、テストデータ生成処理ルーチンを実行するためのプログラムが、HDD18に記憶されている態様を説明したが、当該プログラムは、CD-ROMやDVD-ROM、USBメモリ等の可搬型の記録媒体に記憶されている形態で提供することも可能である。例えば、図54に示すように、テストデータ生成処理ルーチンを実行するためのプログラムを記憶した、CD-ROMやDVD-ROM、USBメモリ等の記録媒体52が、情報処理装置10のドライブ装置50にセットされる。そして、テストデータ生成処理ルーチンを実行するためのプログラムが、記録媒体52からドライブ装置50を介して、HDD18にインストールされる。"