(57)【特許請求の範囲】
【請求項１】
コンピュータに、
検査対象のソフトウェアの動作テスト用テストデータを生成するための、前記ソフトウェアの入力値に関する制約条件を示す論理式のデータが記憶された記憶部を参照して、前記論理式のデータに、等号付き不等号が含まれるか否かを判定し、
前記判定において含まれると判定した場合に、前記記憶部に記憶された前記等号付き不等号で示される論理式を、前記等号付き不等号を等号に変換した論理式と、前記等号付き不等号を不等号に変換した論理式との論理和で示される論理式のデータに変換し、
前記論理式に否定が係る不等号が含まれるか否かを更に判定し、
前記判定において前記否定が係る不等号が含まれると判定した場合に、前記記憶部に記憶された前記否定が係る不等号で示される論理式を、前記不等号と背反となる不等号で示される論理式のデータに変換する
処理を実行させることを特徴とする論理式変換プログラム。
【請求項２】
前記論理式に否定が係る論理積が含まれるか否かを判定し、
前記判定において前記否定が係る論理積が含まれると判定した場合に、前記記憶部に記憶された前記否定が係る論理積で示される論理式のデータを、前記論理積の左辺及び右辺の論理式に各々否定が係る論理式及び該否定が係る論理式のうちの一方を左辺、他方を右辺とする論理和で示される論理式のデータに変換する
処理を前記コンピュータに実行させることを特徴とする請求項１に記
載の論理式変換プログラム。
【請求項３】
前記論理式に否定が係る論理和が含まれるか否かを判定し、
前記判定において前記否定が係る論理和が含まれると判定した場合に、前記記憶部に記憶された前記否定が係る論理和で示される論理式のデータを、前記論理和演算子の左辺及び右辺の論理式の各々に否定が係り、該否定が係る論理式のうちの一方を左辺、他方を右辺とする論理積で示される論理式のデータに変換する
処理を前記コンピュータに実行させることを特徴とする請求項１または２に記載の論理式変換プログラム。
【請求項４】
前記論理式に含意が含まれるか否かを判定し、
前記判定において前記含意が含まれると判定した場合に、前記記憶部に記憶された前記含意で示される論理式のデータを、前記含意の左辺の論理式に否定が付いた第１の論理式と、前記第１の論理式と、前記含意の右辺のうち、一方を左辺、他方を右辺とする論理積で示される論理式とに変換する
処理を前記コンピュータに実行させることを特徴とする請求項１から３のいずれかに記載の論理式変換プログラム。
【請求項５】
前記論理式に論理積が係る論理和が含まれるか否かを判定し、
前記判定において前記論理積が係る論理和が含まれると判定した場合に、前記記憶部に記憶された前記論理積が係る論理和で示される論理式のデータを、前記論理積の左辺を第１の辺とし前記論理和の前記論理積が係らない辺である他方の辺を第２の辺とする第１の論理和と、前記論理積の右辺を第１の辺とし前記他方の辺を第２の辺とする第２の論理和と、前記第１の論理和を第１の辺とし前記第２の論理和を第２の辺とする論理積とで示される論理式のデータに変換する
処理を前記コンピュータに実行させることを特徴とする請求項１から４のいずれかに記載の論理式変換プログラム。
【請求項６】
前記判定において、前記論理積が係る論理和が含まれないと判定した場合に、前記記憶部に記憶された前記論理式のデータを、論理和を含まず、かつ、論理積で結合された論理式の部分論理式毎に分割し、
前記分割した各々の部分論理式のデータを、充足可能性の判定対象の論理式のデータとして前記記憶部に記憶する
処理を前記コンピュータに実行させることを特徴とする請求項５に記載の論理式変換プログラム。
【請求項７】
検査対象のソフトウェアの動作テスト用テストデータを生成するための、前記ソフトウェアの入力値に関する制約条件を示す論理式のデータを記憶する記憶部と、
前記記憶部に記憶された論理式に、等号付き不等号が含まれるか否かを判定する判定部と、
前記判定において含まれると判定した場合に、前記記憶部に記憶された前記等号付き不等号で示される論理式を、前記等号付き不等号を等号に変換した論理式と、前記等号付き不等号を不等号に変換した論理式との論理和で示される論理式のデータに変換し、
前記論理式に否定が係る不等号が含まれるか否かを更に判定し、
前記判定において前記否定が係る不等号が含まれると判定した場合に、前記記憶部に記憶された前記否定が係る不等号で示される論理式を、前記不等号と背反となる不等号で示される論理式のデータに変換する論理式変換部と、
を備える論理式変換装置。
【請求項８】
コンピュータが、
検査対象のソフトウェアの動作テスト用テストデータを生成するための、前記ソフトウェアの入力値に関する制約条件を示す論理式のデータが記憶された記憶部を参照して、前記論理式に、等号付き不等号が含まれるか否かを判定し、
前記判定において含まれると判定した場合に、前記記憶部に記憶された前記等号付き不等号で示される論理式を、前記等号付き不等号を等号に変換した論理式と、前記等号付き不等号を不等号に変換した論理式との論理和で示される論理式のデータに変換し、
前記論理式に否定が係る不等号が含まれるか否かを更に判定し、
前記判定において前記否定が係る不等号が含まれると判定した場合に、前記記憶部に記憶された前記否定が係る不等号で示される論理式を、前記不等号と背反となる不等号で示される論理式のデータに変換する
処理を実行することを特徴とする論理式変換方法。
【発明の詳細な説明】
【技術分野】
【０００１】
開示する技術は、テストデータ生成プログラム、装置、及び方法に関する。
【背景技術】
【０００２】
業務システムのソフトウェアプログラムの動作をテストするためのテストデータを自動的に生成する従来技術として、テストしたい状況が表現された制約式の充足可能性判定問題を解くことで充足値をテストデータとして用いる技術がある。制約式としては、画面の項目、ＤＢの項目、又はプログラム変数を用いた論理式が使用される。例えば、充足可能性問題を解くＳＭＴ（Ｓａｔｉｓｆｉａｂｉｌｉｔｙ  Ｍｏｄｕｌｏ  Ｔｈｅｏｒｉｅｓ：充足可能性モジュロ理論)ソルバを利用したホワイトボックステスト用のテストデータ生成技術が知られている（非特許文献１)。このＳＭＴソルバは、入力された制約式毎に、充足可能性をまず判定し、充足可能であると判定した場合に、この制約式を満たす１つの解（充足解）を出力するものである。なお、この「１つ」とは、値を求めるべき項目や変数の各々について１つずつ、という意味である。
【先行技術文献】
【非特許文献】
【０００３】
【非特許文献１】Nikolai Tillmann and Jonathan de Halleux, "Pex-White Box Test Generation for .NET", TAP 2008, LNCS 4966, pp.134-153, 2008.
【発明の概要】
【発明が解決しようとする課題】
【０００４】
業務システムのソフトウェアをテストするにあたり、プログラムのエラーはデータの境界で起こりやすいという経験則に鑑みたテストデータを用意する必要がある。この経験則に鑑みたテストを境界値テストと呼ぶ。境界値テストとは、入力を、有効なデータの範囲と無効なデータの範囲に分け、その境界となる値、即ち境界値を用いて行うテストである。
【０００５】
この境界値は、上述の制約式の充足値の範囲に含まれる値であり、完全に同一となる値ではない。
【０００６】
例えば、項目Ａのデータの値の範囲を表わす制約式として、５≦Ａという制約式が与えられたとする。
【０００７】
上記のＳＭＴソルバは、この制約式について、５以上のいかなる値も充足値として出力し得る。一方、境界値テストとして有意な値は５である。
【０００８】
このように、テストしたい状況として、項目や変数の値の範囲が論理式で表わされた制約式を、ＳＭＴソルバを用いて解いても、上記境界値テストの条件を満足する充足解、つまり、境界値となるテストデータが得られる保証はなかった。
【０００９】
開示する技術が解決しようとする課題は、論理式に境界値に係る制約が含まれる場合に、この論理式を、ＳＭＴソルバが境界値を確実に出力可能な論理式に変換することにある。
【課題を解決するための手段】
【００１０】
開示する技術は、検査対象のソフトウェアの入力値に関する制約条件を示す論理式のデータが記憶された記憶部を参照して、前記論理式のデータに、等号付き不等号が含まれるか否かを判定する。開示する技術は、前記判定において含まれると判定した場合に、前記記憶部に記憶された前記等号付き不等号を等号に変換する。
【発明の効果】
【００１１】
開示する技術によれば、論理式に境界値に係る制約が含まれる場合に、この論理式を、ＳＭＴソルバが境界値を確実に出力可能な論理式に変換することが出来る、という効果が得られる。
【図面の簡単な説明】
【００１２】
【図１】本実施の形態に係る情報処理装置の構成を示す概略図である。
【図２】本実施の形態に係る情報処理装置の機能ブロック図である。
【図３】木構造形式の論理式データを模式的に示す図である。
【図４】木構造形式の論理式データの格納例を示す図である。
【図５】含意演算子を除去するための変換法則を説明するための図である。
【図６】含意演算子を除去するための変換法則を説明するための図である。
【図７】二重否定を除去するための変換法則を説明するための図である。
【図８】二重否定を除去するための変換法則を説明するための図である。
【図９】ド・モルガンの法則に基づく変換法則を説明するための図である。
【図１０】ド・モルガンの法則に基づく変換法則を説明するための図である。
【図１１】ド・モルガンの法則に基づく変換法則を説明するための図である。
【図１２】ド・モルガンの法則に基づく変換法則を説明するための図である。
【図１３】ド・モルガンの法則に基づく変換法則が適用される前の、木構造形式の論理式データを模式的に示す図である。
【図１４】ド・モルガンの法則に基づく変換法則が適用されて変換された、木構造形式の論理式データを模式的に示す図である。
【図１５】ド・モルガンの法則に基づく変換法則が適用される前の、木構造形式の論理式データの格納例を示す図である。
【図１６】ド・モルガンの法則に基づく変換法則が適用されて変換された、木構造形式の論理式データの格納例を示す図である。
【図１７】不等号演算子に係る否定を除去するための変換法則を説明するための図である。
【図１８】不等号演算子に係る否定を除去するための変換法則を説明するための図である。
【図１９】不等号演算子に係る否定を除去するための変換法則を説明するための図である。
【図２０】不等号演算子に係る否定を除去するための変換法則を説明するための図である。
【図２１】不等号演算子に係る否定を除去するための変換法則を説明するための図である。
【図２２】不等号演算子に係る否定を除去するための変換法則を説明するための図である。
【図２３】不等号演算子に係る否定を除去するための変換法則を説明するための図である。
【図２４】不等号演算子に係る否定を除去するための変換法則を説明するための図である。
【図２５】不等号演算子に係る否定を除去するための変換法則が適用される前の、木構造形式の論理式データを模式的に示す図である。
【図２６】不等号演算子に係る否定を除去するための変換法則が適用されて変換された、木構造形式の論理式データを模式的に示す図である。
【図２７】不等号演算子に係る否定を除去するための変換法則が適用される前の、木構造形式の論理式データの格納例を示す図である。
【図２８】不等号演算子に係る否定を除去するための変換法則が適用されて変換された、木構造形式の論理式データの格納例を示す図である。
【図２９】等号付き不等号演算子を除去するための変換法則を説明するための図である。
【図３０】等号付き不等号演算子を除去するための変換法則を説明するための図である。
【図３１】等号付き不等号演算子を除去するための変換法則を説明するための図である。
【図３２】等号付き不等号演算子を除去するための変換法則を説明するための図である。
【図３３】等号付き不等号演算子を除去するための変換法則が適用される前の、木構造形式の論理式データを模式的に示す図である。
【図３４】等号付き不等号演算子を除去するための変換法則が適用されて変換された、木構造形式の論理式データを模式的に示す図である。
【図３５】等号付き不等号演算子を除去するための変換法則が適用される前の、木構造形式の論理式データの格納例を示す図である。
【図３６】等号付き不等号演算子を除去するための変換法則が適用されて変換された、木構造形式の論理式データの格納例を示す図である。
【図３７】分配法則に基づく変換法則を説明するための図である。
【図３８】分配法則に基づく変換法則を説明するための図である。
【図３９】分配法則に基づく変換法則を説明するための図である。
【図４０】分配法則に基づく変換法則を説明するための図である。
【図４１】分配法則に基づく変換法則が適用される前の、木構造形式の論理式データを示す図である。
【図４２】分配法則に基づく変換法則が適用されて変換された、木構造形式の論理式データを模式的に示す図である。
【図４３】分配法則に基づく変換法則が適用される前の、木構造形式の論理式データの格納例を示す図である。
【図４４】分配法則に基づく変換法則が適用されて変換された、木構造形式の論理式データの格納例を示す図である。
【図４５】テストデータテーブルの例を示す図である。
【図４６】本実施の形態に係る情報処理装置のテストデータ生成処理ルーチンの内容を示すフローチャートである。
【図４７】本実施の形態に係る情報処理装置のテストデータ生成処理ルーチンの内容を示すフローチャートである。
【図４８】本実施の形態に係る情報処理装置の含意除去処理ルーチンの内容を示すフローチャートである。
【図４９】本実施の形態に係る情報処理装置の二重否定除去処理ルーチンの内容を示すフローチャートである。
【図５０】本実施の形態に係る情報処理装置のド・モルガンの法則による否定標準形への変換の処理ルーチンの内容を示すフローチャートである。
【図５１】本実施の形態に係る情報処理装置の不等号の否定除去処理ルーチンの内容を示すフローチャートである。
【図５２】本実施の形態に係る情報処理装置の等号付き不等号の変換処理ルーチンの内容を示すフローチャートである。
【図５３】本実施の形態に係る情報処理装置の選言標準形への変換処理ルーチンの内容を示すフローチャートである。
【図５４】記録媒体に記憶されたプログラムが、ＨＤＤにインストールされる様子を示す図である。
【発明を実施するための形態】
【００１３】
以下、実施形態について詳細に説明する。
【００１４】
図１に示すように、情報処理装置１０は、ＣＰＵ１２、ＲＯＭ１４、ＲＡＭ１６、ＨＤＤ１８、通信インタフェース２０、及びこれらを相互に接続するためのバス２２を備えている。
【００１５】
ＣＰＵ１２は、各種プログラムを実行する。ＲＯＭ１４には、各種プログラムやパラメータ等が記憶されている。ＲＡＭ１６は、ＣＰＵ１２による各種プログラムの実行時におけるワークエリア等として用いられる。記録媒体としてのＨＤＤ１８には、後述するテストデータ生成処理ルーチンを実行するためのプログラム及び充足可能性を判定する処理を行うプログラムを含む各種プログラムや各種データが記憶されている。
【００１６】
情報処理装置１０を、テストデータ生成処理ルーチンを実行するためのプログラム及び充足可能性を判定する処理を行うプログラムに沿って、機能ブロックで表わすと、図２に示すようになる。情報処理装置１０は、プロパティ記憶部３０、論理式木構造生成部３２、否定標準形変換部３４、否定付き不等号除去変換部３６、及び境界値制約生成部３８を備えている。情報処理装置１０は、更に、テストデータ生成部４０、データ生成用プロパティ記憶部４１、及び充足可能性判定部４２、及びテストデータ記憶部４４を備えている。なお、境界値制約生成部３８は、等号付き不等号変換部及び選言標準形変換部の一例である。
【００１７】
プロパティ記憶部３０には、情報処理装置１０に入力された、検査対象のソフトウェアの論理的仕様を定める情報であるプロパティが記憶されている。
【００１８】
検査対象のソフトウェアは、例えば画面とＤＢ（データベース）を有するウェブシステムのためのソフトウェアであり、当該画面には、例えば「ユーザ」、「住所」、「購入個数」及び「合計」などの項目が含まれている。
【００１９】
また、本実施形態において、プロパティには、例えば、"合計が５０００円以上かつ購入個数が５個以内で、住所が東京又は神奈川で会った場合、郵送料が無料となる"という業務仕様が設定されている。
【００２０】
また、上記の業務仕様における事前条件として、検証対象のソフトウェアの入力値に関する制約条件を示す論理式データが、プロパティ記憶部３０に記憶されている。例えば、以下に示す論理式データが記憶されている。
【００２１】
事前条件： （（合計≧５０００）∧（購入個数≧１）∧（購入個数≦５））∧（（住所＝"東京"）∨（住所＝"神奈川"））
【００２２】
上記のように、論理式データは、文字列、数値、論理演算子（含意（→)、論理和（∨）、論理積（∧）、否定（¬)）、関係演算子（等号（＝）、不等号（＞、＜、≧、≦)、）、及び括弧を用いて記述されている。
【００２３】
論理式木構造生成部３２は、プロパティ記憶部３０から、事前条件を示す論理式データを読み込み、読み込んだ論理式データの論理構造を解析して、図３及び図４に示すような木構造形式のデータを生成して、ＲＡＭ１６に格納する。図３は、木構造形式のデータの模式図である。また、図４は、ＲＡＭ１６に格納された木構造形式のデータの一例を示す図である。論理式木構造生成部３２は、図３に円形又は矩形で示す木構造データのノード毎に、図４に示す「Ｎｏ」、「値」、「演算子」、「左ノード」、「右ノード」の各項目値を含むレコードをＲＡＭ１６に格納する。図３の最上位のノードは、図４の「Ｎｏ」が０の行に相当する。
【００２４】
否定標準形変換部３４は、木構造形式の論理式データを参照し、入力された論理式を否定標準形に変換する処理を行う。否定標準形とは、部分論理式を持たない論理式である原子論理式にのみ否定が係り、他には論理和と論理積のみが論理演算子として用いられる形の論理式である。入力された論理式に境界値に係る制約を示す等号付き不等号が含まれない場合でも、この処理を行うことにより、原子論理式にのみ否定が係るように変形出来、境界値に係る制約を示す等号付き不等号部分を見出せるようになる。従って、入力された論理式が否定標準形である場合には、否定標準形変換部３４によるこの処理は不要である。
【００２５】
否定標準形変換部３４は、木構造形式の論理式データに対し、以下に示すような変換法則（１）を適用し、含意演算子（→）を含む部分木を、含意演算子を含まない（含意演算子が除去された）部分木に変換する（図５、図６を参照）。具体的には、否定標準形変換部３４は、含意演算子を含む論理式を、含意演算子の前（左辺）に記述されている論理式の否定と、含意演算子の後（右辺）に記述されている論理式との論理和に変換する処理を行う。
【００２６】
なお、入力された論理式に含意演算子が含まれない場合には、この変換法則（１）の適用処理は不要である。
【００２７】
変換法則（１）：「ｓ１→ｓ２」を「¬ｓ１∨ｓ２」に変換
【００２８】
なお、ここで、ｓ１、ｓ２は部分論理式又は原子論理式を示す。
【００２９】
否定標準形変換部３４は、木構造形式の論理式データから、含意演算子がなくなるまで、論理式データに対して上記の変換法則（１）を適用する処理を繰り返すことで、論理式データから含意演算子を除去し、論理式データ内の論理演算子を論理積、論理和、否定の３種類のみとすることが出来る。
【００３０】
また、否定標準形変換部３４は、木構造形式の論理式データに対し、以下に示すような変換法則（２）を適用し、二重否定を含む部分木を、二重否定を含まない（二重否定が除去された）部分木に変換する（図７，図８を参照。なお、図７及び図８は、ぞれぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図である）。この処理は、入力された論理式に含意演算子が含まれ、上述の変換法則（１）の適用（含意演算子の除去処理）により否定（¬）が生じ、この否定が、入力された論理式に元から存在した否定（¬）に係るようになった場合又は含意演算子が含まれていなくても二重否定が含まれている場合に必要となる処理である。従って、入力された論理式データに、含意演算子と否定を含む部分木、又は、二重否定を含む部分木のいずれも含まれない場合は、この変換法則（２）の適用処理は不要である。
【００３１】
変換法則（２）：（「¬¬ｓ１」を「ｓ１」に変換）
【００３２】
なお、ここでｓ１は部分論理式又は原子論理式を示す。
【００３３】
否定標準形変換部３４は、木構造形式の論理式データから、二重否定がなくなるまで、論理式データに対して上記の変換法則（２）を適用する処理を繰り返すことで、論理式データから二重否定（冗長な否定の部分木）を除去することが出来る。
【００３４】
また、否定標準形変換部３４は、木構造形式の論理式データに対し、以下に示すようなド・モルガンの法則として知られている変換法則（３）、（４）を適用する。これによって、否定標準形変換部３４は、論理積の否定及び論理和の否定を含む部分木を、論理積の否定及び論理和の否定を含まない（論理積の否定及び論理和の否定が除去された）部分木に変換する（図９、図１０、図１１、図１２を参照。なお、図９及び図１１、図１０及び図１２は、ぞれぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図である）。具体的には、否定標準形変換部３４は、論理積の否定を、論理積の前（左辺）に記述されている論理式の否定と、論理積の後（右辺）に記述されている論理式の否定との論理和に、また、論理和の否定を、論理和の前（左辺）に記述されている論理式の否定と、論理和の後（右辺）に記述されている論理式の否定との論理積に変換する処理を行う。
なお、入力された論理式が否定標準形である場合には、この変換法則（３）、（４）の適用処理は不要である。
【００３５】
変換法則（３）： 「¬（ｓ１∧ｓ２）」を「¬ｓ１∨¬ｓ２」に変換
変換法則（４）： 「¬（ｓ１∨ｓ２）」を「¬ｓ１∧¬ｓ２」に変換
【００３６】
なお、ここで、ｓ１、ｓ２は部分論理式又は原子論理式を示す。
【００３７】
否定標準形変換部３４は、例えば、以下に示すように、ド・モルガンの法則に基づく変換法則を適用可能な部分木が表わす論理積の否定（図１３、図１５参照。なお、図１３及び図１５は、それぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図である）を、部分木が表わす２つの論理式の各々の否定の論理和（図１４、図１６参照。なお、図１４及び図１６はそれぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図である）に変換する。
【００３８】
¬（購入個数＞５∧購入個数＜１０）
⇒¬（購入個数＞５）∨¬（購入個数＜１０）
【００３９】
否定標準形変換部３４は、木構造形式の論理式データが、否定が原始論理式のみに係る木構造形式の論理式データに変換されるまで、論理式データに対して上記の変換法則（３）、（４）を適用する処理を繰り返すことで、論理積、論理和、否定を含む論理式を否定標準形に変換することが出来る。
【００４０】
このように、否定標準形変換部３４は、木構造形式の論理式データに対し、含意演算子（→）を除去するための変換法則（１）、二重否定を除去するための変換法則（２）、及びド・モルガンの法則に基づく変換法則（３）、（４）を適用する。これによって、否定標準形変換部３４は、事前条件を示す木構造形式の論理式データを、否定が原子論理式のみに係り、かつ、論理和又は論理積で結合された形式である否定標準形で表わされる木構造形式の論理式データに変換する。
【００４１】
また、否定付き不等号除去変換部３６は、否定標準形の論理式データに変換された木構造形式の論理式データに対し、以下に示すような変換法則（５）〜（８）を適用し、不等号に係る否定の部分木を、不等号に係る否定を含まない（不等号に係る否定が除去された）部分木に変換する（図１７〜図２４を参照。なお図１７及び図２１、図１１８及び図２２、図１９及び図２３、図２０及び図２４は、それぞれ、ぞれぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図である）。具体的には、否定付き不等号除去変換部３６は、各々、不等号に否定が係っている論理式を、当該不等号と背反の不等号を用いた論理式に変換する。
【００４２】
なお、入力された論理式が、連言標準形又は選言標準形であって、且つ、否定を含まない場合には、この変換法則（５）〜（８）の適用処理は不要である。
【００４３】
変換法則（５）：「¬（ａ１＜ａ２）」を「ａ１≧ａ２」に変換
変換法則（６）：「¬（ａ１≦ａ２）」を「ａ１＞ａ２」に変換
変換法則（７）：「¬（ａ１＞ａ２）」を「ａ１≦ａ２」に変換
変換法則（８）：「¬（ａ１≧ａ２）」を「ａ１＜ａ２」に変換
【００４４】
なお、ここで、ａ１、ａ２は部分論理式又は原子論理式を示す。
【００４５】
否定付き不等号除去変換部３６は、図２５、図２７に示すような不等号に係る否定を除去するための変換法則を適用可能な部分木（¬（購入個数＞５）、¬（購入個数＜１０））を、図２６、図２８に示すような部分木（購入個数≦５、購入個数≧１０）に変換する。
【００４６】
否定付き不等号除去変換部３６は、この処理を実行することにより、入力された論理式を、否定付きの不等号で示される無効な範囲を示す論理式から、否定のない不等号で示される有効な範囲を示す論理式に変換することが出来る。
【００４７】
境界値制約生成部３８は、不等号に係る否定が除去された木構造形式の論理式データに対し、以下に示すような変換法則（９）、（１０）を適用する。これによって、境界値制約生成部３８は、等号付き不等号演算子を用いた論理式を、等号を用いた論理式と等号なし不等号演算子を用いた論理式との論理和を示す論理式に変換する（図２９、図３０、図３１、図３２を参照。なお、図２９及び図３１、図３０及び図３２は、それぞれ、ぞれぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図である）。
【００４８】
変換規則（９）：「ａ１≧ａ２」を「（ａ１＝ａ２）∨（ａ１＞ａ２）」に変換
変換規則（１０）：「ａ１≦ａ２」を「（ａ１＝ａ２）∨（ａ１＜ａ２）」に変換
【００４９】
なお、ここで、ａ１、ａ２は部分論理式又は原子論理式を示す。
【００５０】
境界値制約生成部３８は、木構造形式の論理式データから、等号付き不等号がなくなるまで、論理式データに対して上記の変換法則（９）及び変換法則（１０）を適用する処理を繰り返すことにより、論理式データから等号付き不等号演算子を、等号を用いた論理式と、不等号を用いた論理式との論理和を示す論理式に変換する。
【００５１】
境界値制約生成部３８は、例えば、図３３、図３５に示す等号付き不等号を用いた論理式を示す部分木（購入個数≦５、購入個数≧１０）を、図３４、図３６に示す部分木（（購入個数＝５）∨（購入個数＜５）、（購入個数＝１０）∨（購入個数＞１０））に変換する。
【００５２】
ここで、等号を用いた論理式は、入力値に関する上限境界値又は下限境界値を表わす。また、不等号を用いた論理式は、入力値の代表値として上限境界値より小さい値又は下限境界値より大きい値を表わす。
【００５３】
境界値制約生成部３８は、この処理により、境界値を表わす等号付き不等号で示される論理式を、境界値テストの制約を満たす等号で示される論理式と、代表値を表わす不等号で示される論理式とに分解する変換を行うことが出来る。
【００５４】
なお、境界値テストの制約を満たすデータを得るためには、分解した論理式のうち、等号を用いた論理式のみが得られれば良い。従って、境界値制約生成部３８は、等号付き不等号を等号のみに変換するようにしても良い。
【００５５】
テストデータ生成部４０は、境界値制約生成部３８によって変換された木構造形式の論理式データに対し、以下に示すような分配法則に基づく変換法則（１１）〜（１２）を適用し、論理積（∧）と論理和（∨）が連続する部分木のない（宣言標準形）で表わされた木構造形式の論理式データに変換する。具体的には、テストデータ生成部４０は、論理積（∧）と論理和（∨）が連続する部分木がなくなるまで、木構造の論理式データに含まれる論理積（∧）と論理和（∨）が連続する部分木を論理積（∧）の２つの下位ノードの内、論理和（∨）として注目していない方のノードと、論理和として注目しているノードの更に下位のノード各々の２つの論理積（∧）の論理和で示される部分木に変換する処理を繰り返し実行する。これによって、テストデータ生成部４０は、論理和を含まない論理式を１つの節として複数の節が論理和で結合された形式である選言標準形で表わされた木構造形式の論理式データに変換することが出来る。
【００５６】
変換法則（１１）：「ｓ１∧（ｓ２∨ｓ３）」を「（ｓ１∧ｓ２）∨（ｓ１∧ｓ３）」に変換
変換法則（１２）：「（ｓ１∨ｓ２）∧ｓ３」を「（ｓ１∧ｓ３）∨（ｓ２∧ｓ３）」に変換
【００５７】
変換法則（１１）〜（１２）を適用した変換を、図３７、図３８、図３９、図４０に示す。なお、図３７及び図３９、図３８及び図４０は、ぞれぞれ、同一の木構造の論理式データを模式的に示す図及び格納例を示す図である。
【００５８】
テストデータ生成部４０は、例えば、以下に示すように、木構造形式の論理式データ（図４１、図４３を参照）を、論理和を含まない複数の論理式が論理和で結合された選言標準形で表わされる木構造形式の論理式データに変換する。
【００５９】
（（購入個数＝５）∨（購入個数＜５））∧（（住所＝”東京”）∨（住所＝”埼玉”））
⇒
（（購入個数＝５）∧（住所＝”東京”））∨
（（購入個数＝５）∧（住所＝”埼玉”））∨
（（購入個数＜５）∧（住所＝”東京”））∨
（（購入個数＜５）∧（住所＝”埼玉”））∨
（（購入個数＝１０）∧（住所＝”東京”））∨
（（購入個数＝１０）∧（住所＝”埼玉”））∨
（（購入個数＞１０）∧（住所＝”東京”））∨
（（購入個数＞１０）∧（住所＝”埼玉”））
【００６０】
テストデータ生成部４０は、変換した選言標準形で表わされる木構造形式の論理式データを、選言標準形の節（論理和を含まず、かつ、論理積で結合された論理式の部分）ごとに部分木データに分解する。これによって、選言標準形で表わされた事前条件式が、真理値の取り方が一意に定まる複数の事前条件式に分割される。テストデータ生成部４０は、分解した各節について、当該節の部分木データを文字列で記述される論理式データに変換して、データ生成用プロパティ記憶部４１に記憶する。テストデータ生成部４０は、データ生成用プロパティ記憶部４１に記憶された各節の論理式データを順に、充足可能性判定部４２へ出力する。また、テストデータ生成部４０は、充足可能性判定部４２から各節について出力された充足解データを、検査対象のソフトウェアに対する入力値の一組のテストデータとして、テストデータ記憶部４４に記憶されたテストデータテーブルに節毎に格納する。
【００６１】
充足可能性判定部４２は、入力された論理式データが示す制約条件の充足可能性を判定すると共に、制約条件が充足可能であると判定されたときに得られる充足解データを、テストデータ生成部４０へ出力する。
【００６２】
例えば、以下に示す各節の論理式データが、充足可能性判定部４２へ入力されると、図４５に示すような、充足解データが各々出力され、複数組のテストデータとして、テストデータ記憶部４４に記憶されたテストデータテーブルに格納される。
【００６３】
論理式データ１：（購入個数＝５）∧（住所＝”東京”）
論理式データ２：（購入個数＝５）∧（住所＝”埼玉”）
論理式データ３：（購入個数＜５）∧（住所＝”東京”）
論理式データ４：（購入個数＜５）∧（住所＝”埼玉”）
論理式データ５：（購入個数＝１０）∧（住所＝”東京”）
論理式データ６：（購入個数＝１０）∧（住所＝”埼玉”）
論理式データ７：（購入個数＞１０）∧（住所＝”東京”）
論理式データ８：（購入個数＞１０）∧（住所＝”埼玉”）
【００６４】
テストデータ生成部４０は、この処理により、入力値に関する境界値のバリエーションと入力値に関する制約条件のバリエーションとの組合せを全て考慮した複数組のテストデータを生成することが出来る。
【００６５】
次に、本実施の形態の作用を説明する。
【００６６】
情報処理装置１０に、他の装置から通信インタフェース２０を介して、検査対象のソフトウェアの論理的仕様を定める情報であるプロパティが入力され、プロパティ記憶部３０に記憶される。プロパティ記憶部３０に記憶されているプロパティには、業務仕様が設定されており、業務仕様における事前条件として、検証対象のソフトウェアの入力値に関する制約条件を示す論理式データが含まれている。
【００６７】
そして、オペレータが、情報処理装置１０の操作部（図示省略）を操作して、検証対象のソフトウェアの入力値に関するテストデータの生成を指示する。これによって、情報処理装置１０のＣＰＵ１２によって、ＨＤＤ１８に記憶された図４６、４７に示すテストデータ生成処理ルーチンを実行するためのプログラムが実行される。
【００６８】
まず、Ｓ１００において、情報処理装置１０が、プロパティ記憶部３０から、検証対象のソフトウェアのプロパティを読み込み、プロパティに含まれている制約条件を示す論理式データの論理構造を解析して、論理式データを木構造形式の論理式データへ変換する。論理式木構造生成部３２は、「Ｎｏ」の項目に、ノードを識別する番号を格納する。本実施形態では、論理式木構造生成部３２は、図３に示す最上位のノードの場合は「０」、最上位の左の枝の先のノードの場合は「１」、最上位の右の枝の先のノードの場合は「２」と、最上位のノードから順次昇順となる番号を格納する。論理式木構造生成部３２は、「値」の項目に、ノードに入る値を格納する。本実施形態では、論理式木構造生成部３２は、リーフ（末端のノード）にのみ値を格納する。論理式木構造生成部３２は、「演算子」の項目に、「含意（→)）、「論理和（∨）」、「論理積（∧）」、「否定（¬)）、「等号（＝）」、「不等号（＞、＜、≧、≦)））のいずれかの演算子を格納する。また、論理式木構造生成部３２は、「左ノード」の項目に左の枝の先のノードのＮｏを、「右ノード」の項目に右の枝の先のノードのＮｏを、それぞれ格納する。本実施形態では、論理式木構造生成部３２は、先のノードが１つしかない場合には、左ノードの項目にこの先のノードのＮｏを格納する（図４参照）。
【００６９】
なお、論理式木構造生成部３２はパーサとして知られる任意の公知のプログラムを、テストデータ生成処理ルーチンを実行するためのプログラムに組み込み、このパーサをＣＰＵ１２が実行することにより実現可能であり、詳細な説明は割愛する。また、この図３Ｂに示すデータのレイアウトは一例であり、他の公知の木構造形式のデータレイアウトの利用を妨げるものではない。
【００７０】
そして、Ｓ１０２において、情報処理装置１０が、含意演算子除去の処理を実行する。
【００７１】
図１８は情報処理装置１０による含意演算子除去の処理フローチャートを示す。
【００７２】
情報処理装置１０は、Ｓ２０１で、図３に示す最上位のノード、つまり図４に示す「Ｎｏ」の項目値が「０」のノードから順に「左ノード」項目値及び「右ノード」項目値に格納されたポインタを辿りながら、「演算子」の項目値が「含意（→）」のノードを検索する。
【００７３】
そして、情報処理装置１０は、Ｓ２０２で、Ｓ２０１での検索の結果、「演算子」の項目値が「含意（→）」であるノードが検索出来たか否かを判定する。
【００７４】
否定標準形変換部３４は、Ｓ２０２で、検索出来たと判定した場合、Ｓ２０３で、「左ノード」の項目の値をＲＡＭ１６の図示しない左ノード項目値退避領域に記憶する。
【００７５】
次に、情報処理装置１０は、Ｓ２０４で、ＲＡＭ１６に格納された、このノードの「演算子」の項目値を、「含意」から「論理和」に更新する。
【００７６】
そして、情報処理装置１０は、Ｓ２０５で、ＲＡＭ１６に格納された、このノードの「左ノード」の項目値を、「新しい番号」に更新する。例えば、情報処理装置１０は、この「新しい番号」として、ＲＡＭ１６のＮｏの項目の最大値に１加算した値を採用する。なお、ＲＡＭ１６のＮｏの項目値にまだ格納されていない任意の番号を採用するようにしてもよい。
【００７７】
そして、情報処理装置１０は、Ｓ２０６で、「Ｎｏ」の項目にＳ２０８の処理で用いた「新しい番号」、「演算子」の項目に「否定」、「左ノード」の項目に左ノード項目値退避領域の値をそれぞれ格納した新しいノードのデータを生成し、ＲＡＭ１６に追加格納する。
【００７８】
その後、情報処理装置１０は、Ｓ２０１の処理に進む。
【００７９】
そして、情報処理装置１０は、Ｓ２０１での検索の結果、「演算子」の項目値が「含意（→）」であるノードが検索出来なかったと判定した場合には、含意演算子除去の処理を終了する。  このように、情報処理装置１０は、処理対象の木構造の論理式データについて、含意演算子が検索出来なくなるまで、含意演算子除去の処理を繰り返し実行することで、木構造形式の論理式データから、含意演算子を除去することが出来る。
【００８０】
なお、この含意演算子除去の処理フローチャートは一例であって、論理式に含まれる全ての含意演算子について、含意演算子の前（左辺）に記述されている論理式の否定と、含意演算子の後（右辺）に記述されている論理式との論理和に変換する他の任意の処理手順の利用を否定するものではない。
【００８１】
Ｓ１０６では、情報処理装置１０が、含意演算子が除去された木構造形式の論理式データについて、二重否定除去処理を実行する。
【００８２】
図４９は、情報処理装置１０による二重否定除去の処理フローチャートを示す。
【００８３】
情報処理装置１０は、Ｓ３０１で、図３に示す最上位のノード、つまり図４に示す「Ｎｏ」の項目値が「０」のノードから順に「左ノード」項目値及び「右ノード」項目値に格納されたポインタを辿りながら、「演算子」の項目値が「否定（¬）」であるノードが２つ連続する二重否定の部分木を検索する。
【００８４】
次に、情報処理装置１０は、Ｓ３０２で、Ｓ３０１での検索の結果、「演算子」の項目値が「否定（¬）」であるノードが２つ連続する二重否定の部分木が検索出来たか否かを判定する。
【００８５】
情報処理装置１０は、Ｓ３０２で、検索出来たと判定した場合、Ｓ３０３で、検索された部分木の下位のノードの更に下位のノードのＮｏ以外の項目値を取得する。なお、検索された部分木の下位のノードの更に下位のノードとは、つまり上位ノードの演算子項目値及び自ノードの演算子項目値が「否定（¬）」であるノードの「左ノード」の項目値をＮｏとするノードのことである。また、Ｎｏ以外の項目値とは、「値」、「演算子」、「左ノード」及び「右ノード」の各項目値のことである。
【００８６】
次に、情報処理装置１０は、Ｓ３０４で、検索された部分木の上位のノードについてＲＡＭ１６に格納されたＮｏ以外の各項目値を、Ｓ３０３で取得した各項目値にそれぞれ更新する。
【００８７】
その後、情報処理装置１０は、Ｓ３０１の処理に進む。
【００８８】
そして、情報処理装置１０は、Ｓ３０１での検索の結果、「演算子」の項目値が「否定（¬）」であるノードが２つ連続する二重否定の部分木が検索出来なかったと判定した場合には、二重否定除去の処理を終了する。
【００８９】
このように、情報処理装置１０は、処理対象の木構造の論理式データについて、二重否定が検索出来なくなるまで、二重否定除去の処理を繰り返し実行することで、木構造形式の論理式データから、二重否定を除去することが出来る。
【００９０】
なお、この二重否定除去の処理フローチャートは一例であって、論理式に含まれる全ての二重否定を除去する他の任意の処理手順の利用を否定するものではない。
【００９１】
Ｓ１１０では、情報処理装置１０が、全ての二重否定が除去された木構造形式の論理式データについて、ド・モルガンの法則に基づく論理式の否定標準形への変換の処理を実行する。
【００９２】
図５０は情報処理装置１０によるド・モルガンの法則に基づく論理式の否定標準形への変換の処理フローチャートを示す。
【００９３】
情報処理装置１０は、Ｓ４０１で、図３、図１３に示す最上位のノード、つまり図３Ｂに示す「Ｎｏ」の項目値が「０」のノードから順に、「左ノード」項目値及び「右ノード」項目値に格納されたポインタを辿りながら、「演算子」の項目値が「否定（→）」のノードと論理演算子（「論理和（∨）」又は「論理積（∧）」）であるノードが連続する部分木を検索する。
【００９４】
次に、情報処理装置１０は、Ｓ４０２で、Ｓ４０１での検索の結果、「演算子」の項目値が「否定（→）」のノードと、「演算子」の項目値が論理演算子（「論理和」または「論理積」）であるノードとが連続する部分木が検索出来たか否かを判定する。
【００９５】
情報処理装置１０は、Ｓ４０２で、検索出来たと判定した場合、Ｓ４０３で、演算子項目値は「論理和（∨）」か否かを判定する。
【００９６】
情報処理装置１０は、Ｓ４０３で「論理和（∨）」であると判定すると、Ｓ４０４で、検索された部分木の上位のノード、つまり演算子が「否定（¬）」のノードについて、ＲＡＭ１６に格納された「演算子」の項目値を「否定（¬）」から「論理積（∧）」に更新する。
【００９７】
一方、情報処理装置１０は、Ｓ４０３で「論理和（∨）」でないと判定すると、Ｓ４０５で、検索された部分木の上位のノード、つまり演算子が「否定（¬）」のノードについて、ＲＡＭ１６に格納された「演算子」の項目値を「否定（¬）」から「論理和（∨）」に更新する。
【００９８】
なお、上記Ｓ４０３の説明では論理和か否かを判定することとしたが、論理積か否かを判定することにしても良い。この場合には、論理積であると判定した場合にＳ４０５の処理を行い、論理積でないと判定した場合にＳ４０４の処理を行うようにすれば良い。
【００９９】
情報処理装置１０は、Ｓ４０４又はＳ４０５の処理が終わると、Ｓ４０６の処理に進み、Ｓ４０６で、検索された部分木の下位ノード、つまり演算子が論理演算子（「論理和（∨）」又は「論理積（∧）」）のノードの「左ノード」及び「右ノード」の項目値を取得する。
【０１００】
情報処理装置１０は、Ｓ４０７で、Ｓ４０４又はＳ４０５で処理した上位ノードの「左ノード」及び「右ノード」の項目値をそれぞれ「新しい番号」に更新する。例えば、情報処理装置１０は、この「左ノード」の「新しい番号」として、ＲＡＭ１６のＮｏの項目の最大値に１加算した値、「右ノード」の「新しい番号」として、この「左ノード」の「新しい番号」に更に１加算した値を格納する。なお、ＲＡＭ１６のＮｏの項目値にまだ格納されていない任意の番号をそれぞれ格納するようにしてもよい。
【０１０１】
情報処理装置１０は、Ｓ４０８で、「Ｎｏ」の項目にはＳ４０７で上位ノードの「左ノード」の項目に格納した「新しい番号」を、「演算子」の項目には「否定」を、「左ノード」の項目にはＳ４０６で取得した「左ノード」の項目値を、それぞれ格納した新しいノードのデータを生成し、ＲＡＭ１６に追加格納する。
【０１０２】
また、情報処理装置１０は、Ｓ４０９で、「Ｎｏ」の項目にはＳ４０６で上位ノードの「右ノード」の項目に格納した「新しい番号」を、「演算子」の項目には「否定」を、「左ノード」の項目にはＳ４０６で取得した「右ノード」の項目値を、それぞれ格納した新しいノードのデータを生成し、ＲＡＭ１６に追加格納する。
【０１０３】
その後、情報処理装置１０は、Ｓ４０１の処理に進む。
【０１０４】
そして、情報処理装置１０は、Ｓ４０１での検索の結果、「演算子」の項目値が「否定（→）」のノードと、「演算子」の項目値が論理演算子（「論理和」または「論理積」）であるノードとが連続する部分木が検索出来なかったと判定した場合には、ド・モルガンの法則に基づく論理式の否定標準形への変換の処理を終了する。
【０１０５】
このように、情報処理装置１０は、処理対象の木構造の論理式データについて、「演算子」の項目値が「否定（→）」のノードと論理演算子（「論理和（∨）」又は「論理積（∧）」）であるノードが連続する部分木が検索出来なくなるまで、ド・モルガンの法則に基づく論理式の否定標準形への変換の処理を繰り返し実行する。否定標準形変換部３４は、この処理を実行することにより、論理積、論理和、否定を含む木構造形式の論理式データを、該論理式データに含まれる否定が原子論理式のみに係る否定標準形の論理式データに変換することが出来る。
【０１０６】
なお、このド・モルガンの法則に基づく論理式の否定標準形への変換の処理フローチャートは一例であって、論理積、論理和及び否定以外の論理演算子を含まない論理式を否定標準形に変換可能な他の任意の処理手順の利用を否定するものではない。
【０１０７】
上記のＳ１０２〜Ｓ１１０（図４８から図５０）の処理によって、木構造形式の論理式データが表す論理式が、否定標準形の論理式に変換される。
【０１０８】
Ｓ１１４では、情報処理装置１０が、否定標準形に変換された木構造形式の論理式データについて、不等号に係る否定の除去の処理を実行する。図５１は情報処理装置１０による不等号に係る否定の除去の処理フローチャートを示す。
【０１０９】
否定付き情報処理装置１０は、Ｓ５０１で、図１４、図２５に示す最上位のノード、つまり図１６、図２７に示す「Ｎｏ」の項目値が「０」のノードから順に「左ノード」項目値及び「右ノード」項目値に格納されたポインタを辿りながら、「演算子」の項目値が「否定（¬）」であるノードと、「演算子」の項目値が不等号（不等号（＜、＞）及び等号付き不等号（≦、≧）の内のいずれか）であるノードとが連続する、否定つき不等号の部分木を検索する。
【０１１０】
次に、情報処理装置１０は、Ｓ５０２で、Ｓ５０１での検索の結果、「演算子」の項目値が「否定（¬）」であるノードと、「演算子」の項目値が不等号（不等号（＜、＞）及び等号付き不等号（≦、≧）の内のいずれか）であるノードとが連続する、否定つき不等号の部分木が検索出来たか否かを判定する。
【０１１１】
情報処理装置１０は、Ｓ５０２で、検索出来たと判定した場合、Ｓ５０３で、検索された部分木の下位ノード、つまり演算子が不等号（不等号（＜、＞）及び等号付き不等号（≦、≧）の内のいずれか）であるノードについて、演算子項目値の「不等号」は「等号付き不等号（≧または≦）」であるか否かを判定する。
【０１１２】
情報処理装置１０は、Ｓ５０３で「等号付き不等号（≧または≦）」であると判定すると、Ｓ５０４で、検索された部分木の上位ノード、つまり演算子が「否定（¬）」であるノードについて、ＲＡＭ１６に格納された、「演算子」の項目値を、「否定（¬）」から、このノードの下位ノードの「演算子」の項目値である「等号付き不等号（≧または≦）」と背反となる「等号なし且つ逆向きの不等号（＜または＞）」に更新する。つまり、否定標準形変換部３４は、ＲＡＭ１６に格納された下位ノードの「演算子」の項目値が「≧」である場合には上位ノードの「演算子」の項目値を「＜」、下位ノードの「演算子」の項目値が「≦」である場合には上位ノードの「演算子」の項目値を「＞」にそれぞれ更新する。
【０１１３】
一方、情報処理装置１０は、Ｓ５０３で「等号付き不等号（≧または≦）」でないと判定すると、Ｓ５０４で、検索された部分木の上位ノード、つまり演算子が「否定（¬）」であるノードについて、ＲＡＭ１６に格納された、「演算子」の項目値を、「否定（¬）」から、このノードの下位ノードの「演算子」の項目値である「等号なし不等号（＞または＜）」と背反となる「等号なし且つ逆向きの不等号（≦または≧）」に更新する。つまり、否定標準形変換部３４は、検索された部分木について、ＲＡＭ１６に格納された、下位ノードの「演算子」の項目値が「＞」である場合には上位ノードの「演算子」の項目値を「≦」、下位ノードの「演算子」の項目値が「＜」である場合には上位ノードの「演算子」の項目値を「≧」にそれぞれ更新する。
【０１１４】
なお、上記Ｓ５０３の説明では等号付き不等号か否かを判定することとしたが、統合なし不等号か否かを判定することにしても良い。この場合には、等号なし不等号であると判定した場合にＳ５０５の処理を行い、等号なし不等号でないと判定した場合にＳ５０４の処理を行うようにすれば良い。
【０１１５】
情報処理装置１０は、Ｓ５０４又はＳ５０５の処理が終わると、Ｓ５０６の処理に進み、検索された部分木の下位ノードの「左ノード」及び「右ノード」の項目値をそれぞれ取得する。
【０１１６】
そして、情報処理装置１０は、Ｓ５０７で、ＲＡＭ１６に格納された、検索された部分木の上位ノードの「左ノード」及び「右ノード」の項目値を、Ｓ５０６で取得した「左ノード」及び「右ノード」の項目値にそれぞれ更新する。
【０１１７】
その後、情報処理装置１０は、Ｓ５０１の処理に進む。
【０１１８】
そして、情報処理装置１０は、Ｓ５０１での検索の結果、「演算子」の項目値が「否定（¬）」であるノードと、「演算子」の項目値が不等号（不等号（＜、＞）及び等号付き不等号（≦、≧）の内のいずれか）であるノードとが連続する、否定つき不等号の部分木が検索出来なかったと判定した場合には、不等号に係る否定の除去の処理を終了する。
【０１１９】
このように、情報処理装置１０は、処理対象の木構造の論理式データについて、「演算子」の項目値が「否定（¬）」であるノードと、「演算子」の項目値が不等号（不等号（＜、＞）及び等号付き不等号（≦、≧）の内のいずれか）であるノードとが連続する、否定つき不等号の部分木が検索出来なくなるまで、不等号に係る否定の除去の処理を繰り返し実行することで、木構造形式の論理式データから、不等号に係る否定を除去することが出来る。
【０１２０】
なお、この否定付き不等号除去の処理フローチャートは一例であって、論理式に含まれる全ての否定付き不等号を除去する他の任意の処理手順の利用を否定するものではない。
【０１２１】
Ｓ１１８では、情報処理装置１０が、不等号に係る否定が全て除去された木構造形式の論理式データから、等号付き不等号演算子を除去するための変換法則を適用可能な部分木が存在するか否かを判定する。
【０１２２】
図５２は境界値制約生成部３８による等号付き不等号の変換の処理フローチャートを示す。
【０１２３】
境界値制約生成部３８は、Ｓ６０１で、図２６、図３３に示す最上位のノード、つまり図２８、図３５に示す「Ｎｏ」の項目値が「０」のノードから順に「左ノード」項目値及び「右ノード」項目値に格納されたポインタを辿りながら、「演算子」の項目値が「等号付き不等号（≦または≧）」であるノードを検索する。
【０１２４】
次に、境界値制約生成部３８は、Ｓ６０２で、Ｓ６０１での検索の結果、「演算子」の項目値が「等号付き不等号（≦または≧）」であるノードが検索出来たか否かを判定する。
【０１２５】
境界値制約生成部３８は、Ｓ６０２で、検索出来たと判定した場合、Ｓ６０３で、ＲＡＭ１６に格納された、検索されたノードの演算子の項目値を「等号付き不等号」から「論理和（∨）」に更新する。
【０１２６】
次に、境界値制約生成部３８は、Ｓ６０４で、検索されたノードの「左ノード」及び「右ノード」の項目値をＲＡＭ１６の図示しない左ノード項目値退避領域及び右ノード項目値退避領域に格納する。
【０１２７】
そして、境界値制約生成部３８は、Ｓ６０５で、検索されたノードの「左ノード」及び「右ノード」の項目にそれぞれ「新しい番号」を格納する。例えば、境界値制約生成部３８は、この「左ノード」の「新しい番号」として、ＲＡＭ１６のＮｏの項目の最大値に１加算した値、「右ノード」の「新しい番号」として、この「左ノード」の「新しい番号」に更に１加算した値を格納する。なお、ＲＡＭ１６のＮｏの項目値にまだ格納されていない任意の番号をそれぞれ格納するようにしてもよい。
【０１２８】
そして、境界値制約生成部３８は、Ｓ６０６で、「Ｎｏ」の項目にはＳ６０５で「左ノード」の項目に設定した「新しい番号」を、「演算子」の項目には「等号なし不等号」を、「左ノード」の項目にはＲＡＭ１６の左ノード項目値退避領域の値を、「右ノード」の項目にはＲＡＭ１６の右ノード項目値退避領域の値を、それぞれ設定した設定した新しいノードのデータを生成し、ＲＡＭ１６に追加格納する。つまり、境界値制約生成部３８は、「演算子」の項目値が「≦」である場合には「＜」、「≧」である場合には「＞」を格納する。
【０１２９】
また、境界値制約生成部３８は、Ｓ６０７で、「Ｎｏ」の項目にはＳ６０５で「右ノード」の項目に設定した「新しい番号」を、「演算子」の項目には「等号」を、「左ノード」の項目にはＲＡＭ１６の左ノード項目値退避領域の値を、「右ノード」の項目にはＲＡＭ１６の右ノード項目値退避領域の値を、それぞれ設定した設定した新しいノードのデータを生成し、ＲＡＭ１６に追加格納する。
【０１３０】
なお、Ｓ６０６とＳ６０７の処理はいずれが先であっても良い。また、この等号付き不等号の変換の処理フローチャートは一例であって、論理式に含まれる全ての等号付き不等号を等号と不等号の論理式の論理和に変換する他の任意の処理手順の利用を否定するものではない。また、境界値制約を満たす解のみが得られれば良い場合には、境界値制約生成部３８は、Ｓ６０４からＳ６０７の処理に代わり、検索されたノードの「演算子」の項目値を「等号付き不等号（≦または≧）」から「等号（＝）」に更新する処理のみを行うようにしても良い。
【０１３１】
その後、境界値制約生成部３８は、Ｓ６０１の処理に進む。
【０１３２】
そして、否定標準形変換部３４は、Ｓ６０１での検索の結果、が検索出来なかったと判定した場合には、等号付き不等号の変換の処理を終了する。
【０１３３】
このように、境界値制約生成部３８は、処理対象の論理式データについて、等号付き不等号が検索出来なくなるまで、等号付き不等号の変換の処理を繰り返し実行することで、等号付き不等号演算子を用いた論理式を分解する。境界値制約生成部３８は、等号付き不等号演算子を用いた論理式を、等号を用いた論理式と、不等号を用いた論理式とに分解する。ここで、等号を用いた論理式は、入力値に関する上限境界値又は下限境界値を表わす。また、不等号を用いた論理式は、入力値の代表値として上限境界値より小さい値又は下限境界値より大きい値を表わす。つまり、境界値テストの制約を満たすデータを得るためには、分解した論理式のうち、等号を用いた論理式のみが得られれば良い。従って、境界値制約生成部３８は、上述の通り、等号付き不等号を等号のみに変換するようにしても良い。
【０１３４】
Ｓ１２２では、情報処理装置１０が、全ての等号付き不等号演算子が除去された木構造形式の論理式データについて、選言標準形への変換の処理を実行する。
図５３はテストデータ生成部４０による選言標準形への変換の処理フローチャートを示す。
【０１３５】
テストデータ生成部４０は、Ｓ７０１で、図３４、図４１に示す最上位のノード、つまり図３６、図４３に示す「Ｎｏ」の項目値が「０」のノードから順に「左ノード」項目値及び「右ノード」項目値に格納されたポインタを辿りながら、「演算子」の項目値が「論理積（∧）」であるノードと、「演算子」の項目値が「論理和（∨）」であるノードが連続する部分木を検索する。
【０１３６】
次に、テストデータ生成部４０は、Ｓ７０２で、Ｓ７０１での検索の結果、「演算子」の項目値が「論理積（∧）」であるノードと、「演算子」の項目値が「論理和（∨）」であるノードが連続する部分木が検索出来たか否かを判定する。
【０１３７】
テストデータ生成部４０は、Ｓ７０２で、検索出来たと判定した場合、Ｓ７０３で、ＲＡＭ１６に格納された、検索された部分木の上位のノードつまり「演算子」の項目値が「論理積（∧）」であるノードの、「演算子」の項目値を、「論理積（∧）」から「論理和（∨）」に更新する。
【０１３８】
次に、テストデータ生成部４０は、Ｓ７０４で、検索された部分木の上位のノードの「左ノード」及び「右ノード」の項目値を、ＲＡＭ１６の図示しない左ノード項目値退避領域及び右ノード項目値退避領域にそれぞれ格納する。
【０１３９】
次に、テストデータ生成部４０は、Ｓ７０５で、検索された部分木の上位のノードの「左ノード」及び「右ノード」の項目値を、それぞれ「新しい番号」に更新する。例えば、テストデータ生成部４０は、この「左ノード」の「新しい番号」として、ＲＡＭ１６のＮｏの項目の最大値に１加算した値、「右ノード」の「新しい番号」として、この「左ノード」の「新しい番号」に更に１加算した値を格納する。なお、ＲＡＭ１６のＮｏの項目値にまだ格納されていない任意の番号をそれぞれ格納するようにしてもよい。
【０１４０】
次に、テストデータ生成部４０は、Ｓ７０６で、検索された部分木の下位のノード、つまり、「演算子」の項目値が「論理和」のノードの「左ノード」及び「右ノード」の項目値を取得する。
【０１４１】
そして、テストデータ生成部４０は、Ｓ７０７で、検索された部分木の下位ノードのＮｏの項目値は左ノード項目値退避領域の値と一致するか否かを判定する。
【０１４２】
テストデータ生成部４０は、Ｓ７０７で、一致すると判定した場合、Ｓ７０８で、「Ｎｏ」の項目にはＳ７０５で上位ノードの「左ノード」に格納した「新しい番号」を、「演算子」の項目には「論理積（∧）」を、「左ノード」の項目にはＳ７０６で取得した下位ノードの「左ノード」の項目値を、「右ノード」の項目にはＲＡＭ１６の左ノード項目値退避領域の値を、それぞれ格納した新しいノードのデータを生成し、ＲＡＭ１６に追加格納する。
【０１４３】
また、テストデータ生成部４０は、Ｓ７０９で、「Ｎｏ」の項目にはＳ７０５で上位ノードの「右ノード」に格納した「新しい番号」を、「演算子」の項目には「論理積（∧）」を、「左ノード」の項目にはＳ７０６で取得した下位ノードの「右ノード」の項目値を、「右ノード」の項目にはＲＡＭ１６の左ノード項目値退避領域の値を、それぞれ格納した新しいノードのデータを生成し、ＲＡＭ１６に追加格納する。
【０１４４】
一方、テストデータ生成部４０は、Ｓ７０７で、一致しないと判定した場合、Ｓ７１０で、「Ｎｏ」の項目にはＳ７０５で上位ノードの「左ノード」に格納した「新しい番号」を、「演算子」の項目には「論理積（∧）」を、「左ノード」の項目にはＲＡＭ１６の左ノード項目値退避領域の値を、「右ノード」の項目にはＳ７０６で取得した下位ノードの「左ノード」の項目値を、それぞれ格納した新しいノードのデータを生成し、ＲＡＭ１６に追加格納する。
【０１４５】
また、テストデータ生成部４０は、Ｓ７１１で、「Ｎｏ」の項目にはＳ７０５で上位ノードの「右ノード」に格納した「新しい番号」を、「演算子」の項目には「論理積（∧）」を、「左ノード」の項目にはＲＡＭ１６の左ノード項目値退避領域の値を、「右ノード」の項目にはＳ７０６で取得した下位ノードの「右ノード」の項目値を、それぞれ格納した新しいノードのデータを生成し、ＲＡＭ１６に追加格納する。
【０１４６】
その後、否定標準形変換部３４は、Ｓ７０１の処理に進む。
【０１４７】
そして、否定標準形変換部３４は、Ｓ７０１での検索の結果、「演算子」の項目値が「論理積（∧）」であるノードと、「演算子」の項目値が「論理和（∨）」であるノードが連続する部分木が検索出来なかったと判定した場合には、選言標準形への変換の処理を終了し、図４７に示すＳ１２６の処理に進む。
【０１４８】
上記のＳ１２２（図５３）の処理によって、木構造形式の論理式データが表す否定標準形の論理式が、選言標準形の論理式に変換される。
【０１４９】
図４１及び図４３に示す論理式データについて、Ｓ７０３からＳ７０９の処理を１回実行した後の論理式データの例を図４２及び図４４に示す。この図に示すように、木構造の論理式データに含まれる論理積（∧）と論理和（∨）が連続する部分木を論理積（∧）の２つの下位ノードの内、論理和（∨）として注目していない方のノードと、論理和として注目しているノードの更に下位のノード各々の２つの論理積（∧）の論理和で示される部分木に変換する処理を、この論理式データから論理積（∧）と論理和（∨）が連続する部分木がなくなるまで繰り返すことにより、選言標準形の論理式に変換することが出来る。
【０１５０】
図４７の説明に戻って、図４７のＳ１２６では、情報処理装置１０が、選言標準形の論理式を表わす木構造形式の論理式データを、選言標準形の節毎の部分木データに分割する。そして、Ｓ１２８において、情報処理装置１０が、各節の部分木データを、各節の論理式を示す文字列データに変換してデータ生成用プロパティ記憶部４１に記憶する。
【０１５１】
次のＳ１３０では、情報処理装置１０が、データ生成用プロパティ記憶部４１から、１つの節の論理式を示す文字列データを取得し、Ｓ１３２において、情報処理装置１０が、取得した１つの節の論理式を示す文字列データを、充足可能性判定部４２へ出力する。このとき、充足可能性判定部４２は、入力された文字列データが示す論理式（制約条件）の充足可能性を判定すると共に、充足解データを求めて出力する。
【０１５２】
そして、Ｓ１３４において、情報処理装置１０が、充足可能性判定部４２から出力された充足解データを取得し、充足解データを一組のテストデータとして、テストデータ記憶部４４のテストデータテーブルに格納する。
【０１５３】
次のＳ１３６では、情報処理装置１０が、選言標準形の論理式の全ての節について、上記Ｓ１３０〜Ｓ１３４の処理が実行されたか否かを判定する。上記Ｓ１３０〜Ｓ１３４の処理が実行されていない節が存在すると判定された場合には、情報処理装置１０は、上記Ｓ１３０へ戻り、未処理の節について、上記Ｓ１３０〜Ｓ１３４の処理を実行する。一方、全ての節について、上記Ｓ１３０〜Ｓ１３４の処理が実行されたと判定された場合には、情報処理装置１０が、テストデータ生成処理ルーチンを終了する。
【０１５４】
そして、オペレータが、テストデータ記憶部４４に記憶されたテストデータテーブルを用いて、情報処理装置１０又は他の装置に、検査対象のソフトウェアの検査プログラムを実行させて、検査対象のソフトウェアの検査処理を行わせる。
【０１５５】
以上説明したように、本実施の形態に係る情報処理装置１０は、検査対象のソフトウェアの入力値に関する制約条件を示す論理式データにおいて、等号付き不等号の論理式を、等号を用いた論理式に変換する。そしてこの論理式を選言標準形となるように変換して、選言標準形に変換した論理式の各節をそれぞれＳＭＴソルバに入力する論理式として出力する。そして、情報処理装置１０は、各節の論理式の充足解データを得ることにより、入力値に関する境界値テストを考慮したテストデータを生成することが出来る。
【０１５６】
また、本実施の形態に係る情報処理装置１０は、業務仕様を満たし、且つ、境界値テストが可能なテストデータを自動的に生成することが出来る。
【０１５７】
本実施の形態に係る情報処理装置１０は、入力値に関する境界値のバリエーションと入力値に関する制約条件のバリエーションとの組合せを全て考慮した複数組のテストデータを生成することが出来る。また、情報処理装置１０は、テストを意識しない業務仕様記述から、より現実的なテストデータを生成することが出来る。
【０１５８】
また、境界値制約生成部３８は、等号付き不等号演算子を、入力値に関する制約条件を示す論理式内に発見した場合、当該論理式を、ソフトウェアテストにおける経験則的な境界値テストのための論理式と入力値の代表値に関するテストのための論理式とに分解する。これによって、情報処理装置１０は、代表値をテストするためのテストデータを生成すると共に、上界境界値又は下界境界値をテストするためのテストデータを生成することが出来る。
【０１５９】
なお、上記の実施の形態では、１つの情報処理装置で、テストデータを生成する処理と、充足可能性の判定処理とを行う場合を例に説明したが、これに限定されるものではない。例えば、テストデータを生成する処理を行う情報処理装置１０とは別の情報処理装置が、充足可能性の判定処理を行うようにしてもよい。この場合には、情報処理装置１０は、変換した選言標準形の論理式データの各節について、当該節の論理式を示す文字列データを、充足可能性の判定処理を行う他の情報処理装置へ出力し、当該他の情報処理装置から、充足解データを取得する。
【０１６０】
また、情報処理装置１０は、テストデータ生成処理ルーチンを実行するためのプログラムとは別のプログラムによって、充足可能性の判定処理を実行する場合を例に説明したが、これに限定されるものではない。情報処理装置１０は、テストデータ生成処理ルーチンを実行するためのプログラムにより、テストデータを生成する処理と、充足可能性の判定処理とを行うようにしてもよい。
【０１６１】
また、情報処理装置１０は、含意演算子除去のための変換法則、二重否定除去のための変換法則、及びド・モルガンの法則に基づく変換法則を順に論理式データに適用する場合を例に説明したが、これに限定されるものではない。情報処理装置１０は、論理式データに対して、他の順序（例えば、二重否定除去のための変換法則、含意演算子除去のための変換法則、及びド・モルガンの法則に基づく変換法則の順）で、上記の変換法則を適用してもよい。この場合には、情報処理装置１０は、論理式データが、否定標準形の論理式データに変換されるまで、上記の変換法則を繰り返し適用すればよい。
【０１６２】
また、情報処理装置１０は、検査対象のソフトウェアの入力値に関する制約条件を示す論理式データに基づいて、テストデータを生成する場合を例に説明したが、これに限定されるものではない。例えば、情報処理装置１０は、ソフトウェアのモジュール部分を、検査対象として、検査対象のモジュール部分の入力値に関する制約条件を示す論理式データに基づいて、モジュール部分の入力値に関するテストデータを生成するようにしてもよい。
【０１６３】
また、情報処理装置１０は、ハードウェアの機構に関して、特に限定されない。上記では、テストデータ生成処理ルーチンを実行するためのプログラムが、ＨＤＤ１８に記憶されている態様を説明したが、当該プログラムは、ＣＤ−ＲＯＭやＤＶＤ−ＲＯＭ、ＵＳＢメモリ等の可搬型の記録媒体に記憶されている形態で提供することも可能である。例えば、図５４に示すように、テストデータ生成処理ルーチンを実行するためのプログラムを記憶した、ＣＤ−ＲＯＭやＤＶＤ−ＲＯＭ、ＵＳＢメモリ等の記録媒体５２が、情報処理装置１０のドライブ装置５０にセットされる。そして、テストデータ生成処理ルーチンを実行するためのプログラムが、記録媒体５２からドライブ装置５０を介して、ＨＤＤ１８にインストールされる。
【符号の説明】
【０１６４】
１０  情報処理装置
１２  ＣＰＵ
１４  ＲＯＭ
１６  ＲＡＭ
１８  ＨＤＤ
３０  プロパティ記憶部
３２  論理式木構造生成部
３４  否定標準形変換部
３６  不等号除去変換部
３８  境界値制約生成部
４０  テストデータ生成部
４１  データ生成用プロパティ記憶部
４２  充足可能性判定部
４４  テストデータ記憶部
【図１】
0005655650.tif 000002
【図２】
0005655650.tif 000003
【図３】
0005655650.tif 000004
【図４】
0005655650.tif 000005
【図５】
0005655650.tif 000006
【図６】
0005655650.tif 000007
【図７】
0005655650.tif 000008
【図８】
0005655650.tif 000009
【図９】
0005655650.tif 000010
【図１０】
0005655650.tif 000011
【図１１】
0005655650.tif 000012
【図１２】
0005655650.tif 000013
【図１３】
0005655650.tif 000014
【図１４】
0005655650.tif 000015
【図１５】
0005655650.tif 000016
【図１６】
0005655650.tif 000017
【図１７】
0005655650.tif 000018
【図１８】
0005655650.tif 000019
【図１９】
0005655650.tif 000020
【図２０】
0005655650.tif 000021
【図２１】
0005655650.tif 000022
【図２２】
0005655650.tif 000023
【図２３】
0005655650.tif 000024
【図２４】
0005655650.tif 000025
【図２５】
0005655650.tif 000026
【図２６】
0005655650.tif 000027
【図２７】
0005655650.tif 000028
【図２８】
0005655650.tif 000029
【図２９】
0005655650.tif 000030
【図３０】
0005655650.tif 000031
【図３１】
0005655650.tif 000032
【図３２】
0005655650.tif 000033
【図３３】
0005655650.tif 000034
【図３４】
0005655650.tif 000035
【図３５】
0005655650.tif 000036
【図３６】
0005655650.tif 000037
【図３７】
0005655650.tif 000038
【図３８】
0005655650.tif 000039
【図３９】
0005655650.tif 000040
【図４０】
0005655650.tif 000041
【図４１】
0005655650.tif 000042
【図４２】
0005655650.tif 000043
【図４３】
0005655650.tif 000044
【図４４】
0005655650.tif 000045
【図４５】
0005655650.tif 000046
【図４６】
0005655650.tif 000047
【図４７】
0005655650.tif 000048
【図４８】
0005655650.tif 000049
【図４９】
0005655650.tif 000050
【図５０】
0005655650.tif 000051
【図５１】
0005655650.tif 000052
【図５２】
0005655650.tif 000053
【図５３】
0005655650.tif 000054
【図５４】
0005655650.tif 000055