(57)【要約】【課題】プログラムの仕様を効率的に求める。【解決手段】本発明の一態様としてのプログラム仕様推定装置において、述語生成部は、それぞれパラメータを含む複数の述語からなり、かつ、任意の０個以上の述語の連言が、他の述語の連言の否定となる複数の否定被覆集合を生成し、第１矛盾核列挙部は、前記複数の否定被覆集合に含まれるすべての述語に基づき第１矛盾核を列挙し、プログラム変換部は、前記プログラムを論理式の形式に変換してプログラム論理式を取得し、第２矛盾核列挙部は、前記複数の否定被覆集合に含まれるすべての述語にそれぞれ真または偽の値を取る緩和変数を設定し各前記緩和変数と各前記緩和変数に対応する述語との選言と、前記プログラム論理式と、付加制約との連言を含む論理式を真にする解を、各前記第１矛盾核に含まれる述語の少なくとも１つが真になり残りが偽になるとの制約等を満たすように求め、前記緩和変数が真になった述語の集合である訂正集合を矛盾核に変換する。【選択図】図１
2015114898.tif 000002
【特許請求の範囲】
【請求項１】
命令型プログラミング言語によって記述されたプログラムに含まれるパラメータを検出し、前記検出したパラメータに応じて、それぞれ前記パラメータを含む複数の述語からなり、かつ、任意の０個以上の述語の連言が、他の述語の連言の否定となる複数の否定被覆集合を生成する述語生成部と、
前記複数の否定被覆集合に含まれるすべての述語に基づき、連言が矛盾する述語の極小集合である第１矛盾核を列挙する第１矛盾核列挙部と、
前記プログラムを記号実行により論理式の形式に変換することで、プログラム論理式を得るプログラム変換部と、
（Ａ）前記複数の否定被覆集合に含まれるすべての述語にそれぞれ真または偽の値を取る緩和変数を設定し、
（Ｂ）各前記緩和変数と各前記緩和変数に対応する述語との選言と、前記プログラム論理式と、予め与えられた付加制約との連言を含む論理式を真にする解を、前記述語生成部により生成された否定被覆集合の個数に応じて定まる、真になる緩和変数の個数に関する制約と、各前記第１矛盾核に含まれる述語の少なくとも１つが真になり残りが偽になるとの制約を満たすように求め、
（Ｃ）前記緩和変数が真になった述語の集合である訂正集合を、前記プログラム論理式と前記付加制約とともに連言をとった論理式を真にする解を求める場合に前記付加制約と同時に真にできない述語の極小集合である第２矛盾核に変換する、第２矛盾核列挙部と
を備えたプログラム仕様推定装置。
【請求項２】
前記真となる緩和変数の個数に関する制約は、前記真になる緩和変数の個数が前記否定被覆集合の個数以下または当該個数に一致するとの制約である
請求項１に記載のプログラム仕様推定装置。
【請求項３】
前記第２矛盾核列挙部は、前記付加制約に緩和変数を設定し、前記付加制約と当該緩和変数との選言をさらに連言として含む前記論理式を真にする解を求め、前記緩和変数が真になった述語および付加制約の少なくとも一方からなる集合である訂正集合を求め、前記訂正集合を、述語および付加制約の少なくとも一方からなり集合内の各要素の連言が矛盾する極小集合である第３矛盾核に変換し、各第３矛盾核のうち前記付加制約が含まれる第３矛盾核を特定し、特定した第３矛盾核に含まれる述語の集合を、前記第２矛盾核として得る
請求項１ないし２のいずれか一項に記載のプログラム仕様推定装置。
【請求項４】
前記真となる緩和変数の個数に関する制約は、前記真になる緩和変数の個数が前記否定被覆集合の個数に１を加算した値以下または当該値に一致するとの制約である  
請求項３に記載のプログラム仕様推定装置。
【請求項５】
前記述語生成部は、各々パラメータに基づく述語の生成ルールを表す複数の述語パターンからなり、かつ任意の１つの以上の述語パターンにより生成される述語が、他の述語パターンにより生成される述語の連言と矛盾する集合である複数の否定被覆パターン集合を読み込み、
前記否定被覆パターン集合ごとに、各述語パターンに従って前記検出されたパラメータに基づき述語を生成することにより、前記複数の否定被覆集合を得る
請求項１ないし４のいずれか一項に記載のプログラム仕様推定装置。
【請求項６】
前記述語生成部は、前記プログラムから前記パラメータの型を検出し、前記検出したパラメータの型に応じて、前記複数の否定被覆パターン集合のうち、使用する否定被覆パターン集合を特定する
請求項５に記載のプログラム仕様推定装置。
【請求項７】
前記否定被覆パターン集合内の１つの述語パターンにより生成される述語は、当該否定被覆パターン集合内の別の述語パターンにより生成される述語の否定である
請求項５または６に記載のプログラム仕様推定装置。
【請求項８】
前記第１矛盾核列挙部は、前記複数の否定被覆集合に含まれるすべての述語の中から取り除くと、取り除いた後に残る述語の連言が真になるような述語の集合である第１訂正集合を、前記述語生成部により生成された否定被覆集合の個数に応じて定まる、前記第１訂正集合のサイズに関する制約に基づき生成し、前記第１訂正集合を前記第１矛盾核に変換する
請求項１ないし７のいずれか一項に記載のプログラム仕様推定装置。
【請求項９】
前記第１矛盾核列挙部は、前記複数の否定被覆集合からｉ（ｉは１より大きく、前記否定被覆集合の個数より小さい任意の整数）個の集合を選択し、選択したｉ個の集合に含まれるすべての述語の中から取り除くと、取り除いた後に残る述語の連言が真になる述語の集合である訂正集合を、前記選択した否定被覆集合の個数に応じて定まる、当該訂正集合のサイズに関する制約を満たすように生成し、前記訂正集合を、選択したｉ個の集合に含まれるすべての述語のうち同時に真にできない述語の極小集合である矛盾核に変換し、
変換後の矛盾核と、未選択の否定被覆集合との中からｉ個の集合を選択し、選択した集合に含まれるすべての述語の中から取り除くと、取り除いた後に残る述語の連言が真になる述語の集合である訂正集合を、これまでに選択した否定被覆集合の個数に応じて定まる、当該訂正集合のサイズに関する制約を満たすように生成し、前記訂正集合を、選択したｉ個の集合に含まれるすべての述語のうち同時に真にできない述語の極小集合である矛盾核に変換し、
以降、同様の処理を繰り返すことにより最終的に得られた矛盾核を、前記第１矛盾核として取得する
請求項８に記載のプログラム仕様推定装置。
【請求項１０】
前記選択した否定被覆集合の個数に応じて定まる、前記訂正集合のサイズに関する制約は、前記訂正集合のサイズが前記選択した否定被覆集合の個数以下または当該個数に一致するとの制約であり、
前記これまでに選択した否定被覆集合の個数に応じて定まる、前記訂正集合のサイズに関する制約は、前記訂正集合のサイズが前記これまでに選択した否定被覆集合の個数以下または当該個数に一致するとの制約である
請求項９に記載のプログラム仕様推定装置。
【請求項１１】
前記第１矛盾核列挙部は、前記ｉ個の集合の選択、前記訂正集合の生成、前記矛盾核への変換を含む一連の処理を並列に行う
請求項９または１０に記載のプログラム仕様推定装置。
【請求項１２】
命令型プログラミング言語によって記述されたプログラムに含まれるパラメータを検出し、前記検出したパラメータに応じて、それぞれ前記パラメータを含む複数の述語からなり、かつ、任意の０個以上の述語の連言が、他の述語の連言の否定となる複数の否定被覆集合を生成する述語生成ステップと、
前記複数の否定被覆集合に含まれるすべての述語に基づき、連言が矛盾する述語の極小集合である第１矛盾核を列挙する第１矛盾核列挙ステップと、
前記プログラムを記号実行により論理式の形式に変換することで、プログラム論理式を得るプログラム変換ステップと、
（Ａ）前記複数の否定被覆集合に含まれるすべての述語にそれぞれ真または偽の値を取る緩和変数を設定し、
（Ｂ）各前記緩和変数と各前記緩和変数に対応する述語との選言と、前記プログラム論理式と、予め与えられた付加制約との連言を含む論理式を真にする解を、前記述語生成部により生成された否定被覆集合の個数に応じて定まる、真になる緩和変数の個数に関する制約と、各前記第１矛盾核に含まれる述語の少なくとも１つが真になり残りが偽になるとの制約を満たすように求め、
（Ｃ）前記緩和変数が真になった述語の集合である訂正集合を、前記プログラム論理式と前記付加制約とともに連言をとった論理式を真にする解を求める場合に前記付加制約と同時に真にできない述語の極小集合である第２矛盾核に変換する、第２矛盾核列挙ステップと
をコンピュータが実行するプログラム仕様推定装置。
【請求項１３】
命令型プログラミング言語によって記述されたプログラムに含まれるパラメータを検出し、前記検出したパラメータに応じて、それぞれ前記パラメータを含む複数の述語からなり、かつ、任意の０個以上の述語の連言が、他の述語の連言の否定となる複数の否定被覆集合を生成する述語生成ステップと、
前記複数の否定被覆集合に含まれるすべての述語に基づき、連言が矛盾する述語の極小集合である第１矛盾核を列挙する第１矛盾核列挙ステップと、
前記プログラムを記号実行により論理式の形式に変換することで、プログラム論理式を得るプログラム変換ステップと、
（Ａ）前記複数の否定被覆集合に含まれるすべての述語にそれぞれ真または偽の値を取る緩和変数を設定し、
（Ｂ）各前記緩和変数と各前記緩和変数に対応する述語との選言と、前記プログラム論理式と、予め与えられた付加制約との連言を含む論理式を真にする解を、前記述語生成部により生成された否定被覆集合の個数に応じて定まる、真になる緩和変数の個数に関する制約と、各前記第１矛盾核に含まれる述語の少なくとも１つが真になり残りが偽になるとの制約を満たすように求め、
（Ｃ）前記緩和変数が真になった述語の集合である訂正集合を、前記プログラム論理式と前記付加制約とともに連言をとった論理式を真にする解を求める場合に前記付加制約と同時に真にできない述語の極小集合である第２矛盾核に変換する、第２矛盾核列挙ステップと
をコンピュータに実行させるためのプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明の実施形態は、プログラム仕様推定装置およびその方法、ならびにプログラムに関する。
【背景技術】
【０００２】
プログラムの仕様として、プログラムの事前条件を推定する技術が知られている。前条件とはプログラムが正常動作するための前提条件のことである。事前条件が成立する状態で、プログラムが実行されると、予め定められた事後条件が成立する。事後条件とはプログラムが正常動作した際に保証される条件のことである。
【０００３】
事前条件を推定する方法として、プログラムのテキストから生成した述語と、予め与えられた事後条件と、プログラムを論理式に変換したプログラム論理式とを用いて論理式を生成し、生成した論理式から、矛盾する述語の組である矛盾核を列挙する方法が知られている。述語とは、パラメータ（存在すれば）に応じて真または偽が定まる論理式のことであり、制約条件とも呼ばれる。矛盾核とは、論理式の集合に対し、その要素全ての連言（論理積）が充足不能であるとき、その部分集合で、連言がやはり充足不能なものを言う。この方法は、計算量が非常に大きく、処理速度やスケーラビリティに難があった。
【０００４】
また、矛盾核を取得する前に、訂正集合を中間解として取得し、当該中間解を矛盾核に変換する方法がある。訂正集合とは、論理式の集合に対し、その要素全ての連言が充足不能であるとき、その部分集合で、元の集合からそれを取り除くと、連言が充足可能になるものを言う。この方法では、訂正集合を一旦全て列挙する必要があるが、列挙する訂正集合の数が大きくなり、必ずしも処理が効率的とはいえなかった。
【先行技術文献】
【非特許文献】
【０００５】
【非特許文献１】『Minimal Unsatisfiable Core列挙によるプログラムの準最弱な事前条件推定』（東芝）, ソフトウェア工学の基礎XVIII, レクチャーノート/ソフトウェア工学, 近代科学社, Vol.37, 2011, pp.187-196
【非特許文献２】“Algorithms for Computing Minimal Unsatisfiable Subsets of Constraints”, Journal of Automated Reasoning, Springer-Verlag New York, Inc. Vol.40, 2008, pp.1-33）
【発明の概要】
【発明が解決しようとする課題】
【０００６】
本発明の一態様は、プログラムの仕様（事前条件）を効率的に求めることを可能にすることを目的とする。
【課題を解決するための手段】
【０００７】
本発明の一態様としてのプログラム仕様推定装置は、述語生成部と、第１矛盾核列挙部と、プログラム変換部と、第２矛盾核列挙部とを備える。
【０００８】
前記述語生成部は、命令型プログラミング言語によって記述されたプログラムに含まれるパラメータを検出し、前記検出したパラメータに応じて、それぞれ前記パラメータを含む複数の述語からなり、かつ、任意の０個以上の述語の連言が、他の述語の連言の否定となる複数の否定被覆集合を生成する。
【０００９】
前記第１矛盾核列挙部は、前記複数の否定被覆集合に含まれるすべての述語に基づき、連言が矛盾する述語の極小集合である第１矛盾核を列挙する。
【００１０】
前記プログラム変換部は、前記プログラムを記号実行により論理式の形式に変換することで、プログラム論理式を得る。
【００１１】
前記第２矛盾核列挙部は、
（Ａ）前記複数の否定被覆集合に含まれるすべての述語にそれぞれ真または偽の値を取る緩和変数を設定し、
（Ｂ）各前記緩和変数と各前記緩和変数に対応する述語との選言と、前記プログラム論理式と、予め与えられた付加制約との連言を含む論理式を真にする解を、前記述語生成部により生成された否定被覆集合の個数に応じて定まる真になる緩和変数の個数に関する制約と、各前記第１矛盾核に含まれる述語の少なくとも１つが真になり残りが偽になるとの制約を満たすように求め、
（Ｃ）前記緩和変数が真になった述語の集合である訂正集合を、前記プログラム論理式と前記付加制約とともに連言をとった論理式を真にする解を求める場合に前記付加制約と同時に真にできない述語の極小集合である第２矛盾核に変換する。
【図面の簡単な説明】
【００１２】
【図１】本発明の実施形態に係るプログラム仕様推定装置を備えたプログラム仕様推定システムの全体構成を示す図。
【図２】図1のシステムの処理フローを示す図。
【図３】述語生成部の構成を示す図。
【図４】述語間矛盾核列挙部の構成を示す図。
【図５】述語間矛盾核列挙部の処理フローを示す図。
【図６】部分矛盾核列挙部の構成を示す図。
【図７】述語間矛盾核列挙部の処理フローを示す図。
【図８】全体矛盾核列挙部の構成を示す図。
【図９】矛盾核列挙部の構成を示す図。
【図１０】矛盾核列挙部の処理フローを示す図。
【図１１】プログラムテキストの例を示す図。
【図１２】付加制約（事後条件の否定）の例を示す図。
【図１３】属性パターンの例を示す図。
【図１４】述語パターンの例を示す図。
【図１５】述語記憶部および否定被覆記憶部の記憶内容の例を示す図。
【図１６】中間結果記憶部の記憶内容の例を示す図。
【図１７】中間結果記憶部の記憶内容の例を示す図。
【図１８】分割情報記憶部、部分述語記憶部および部分矛盾核記憶部の記憶内容の例を示す図。
【図１９】中間結果記憶部の記憶内容の例を示す図。
【図２０】割当情報記憶部、部分述語記憶部および部分矛盾核記憶部の記憶内容の例を示す図。
【図２１】中間結果記憶部の記憶内容の例を示す図。
【図２２】述語記憶部、不変制約記憶部、個数記憶部および矛盾核記憶部の記憶内容の例を示す図。
【図２３】述語間矛盾核列挙部の他の構成例を示す図。
【図２４】図1のシステムのハードウェアブロック図。
【発明を実施するための形態】
【００１３】
以下に、本明細書で用いる論理学上の記号を示す。
∧：連言（論理積、AND）
∨：選言（論理和、OR）
¬：否定（NOT）
⇒：含意（「ならば」）
⊥：矛盾
∀：全称量化子（「任意の」「すべての」）
【００１４】
更に、本明細書で用いる集合論の記号を以下に示す。
∈：元として含まれる
⊆：部分集合
＼：差集合
【００１５】
また、本明細書で使用する用語の定義を示す。
【００１６】
［サイズ］集合に含まれる要素数のこと。
【００１７】
［連言］論理積、すなわちANDのこと。
【００１８】
［選言］論理和、すなわちORのこと。
【００１９】
［矛盾核］（unsatisfiable core、あるいは unsatisfiable subset）
論理式の集合に対し、その要素全ての連言（論理積）が充足不能である（集合が不整合である）とき、その部分集合で、連言がやはり充足不能なもの。言い換えると、論理式の集合 P に対し∧P＝⊥であるとき、P’⊆Pでやはり∧P’＝⊥となるもの。
【００２０】
［極小矛盾核］（minimal unsatisfiable core、あるいは minimal unsatisfiable subset）
矛盾核のうち極小なもの。すなわち、すべての真部分集合が充足可能な矛盾核。言い換えると、論理式の集合 P に対する矛盾核P’で、∀p∈P’. ∧(P’＼p)≠⊥ であるもの。本明細書においては、特に言及がない限り、「矛盾核」は「極小矛盾核」を指すものとする。
【００２１】
［訂正集合］（correction subset）
論理式の集合に対し、その要素全ての連言が充足不能であるとき、その部分集合で、元の集合からそれを取り除くと、連言が充足可能になるもの。言い換えると、論理式の集合 P に対し∧P＝⊥ であるとき、P’⊆Pでやはり∧(P ＼P’)≠⊥となるもの。
【００２２】
［極小訂正集合］（minimal correction subset）
訂正集合のうち極小なもの。すなわち、いかなる真部分集合を元の訂正集合から取り除いても充足可能にならないもの。言い換えると、論理式の不整合な集合 Pの訂正集合P’のうち、∀p∈P’. ∧(P＼(P’＼p))＝⊥ であるもの。本明細書においては、特に言及がない限り、「訂正集合」は「極小訂正集合」を指す。
【００２３】
［事前条件・事後条件］
プログラムの仕様の1形態。事前条件とはプログラムが正常動作するための前提条件のことである。事後条件とはプログラムが正常動作した際に保証される条件のことである。事前条件および事後条件はペアで扱われる。論理学的には、あるプログラムの事前条件をP、事後条件をT、そのプログラムが動作したことを表す記号をSとすると、P∧S⇒Tである。
【００２４】
以下、図面を参照しながら、本発明の実施形態について説明する。
【００２５】
図1は、本発明の実施形態に係るプログラム仕様推定装置を備えたプログラム仕様推定システムの機能ブロック図である。
【００２６】
このシステムは、命令型プログラミング言語によって記述されたプログラムと、当該プログラムに対する付加制約を入力とし、プログラムの事前条件（プログラム仕様）を求めて出力する。本実施形態では、付加制約が、プログラムの事後条件の否定である場合を示すが、これに限定されない。本システムは、ユーザに対する入出力部11と、プログラム仕様推定装置21と、および各種の記憶部31〜35を備える。図では記憶部31〜35はプログラム仕様推定装置21の外側に配置されているが、プログラム仕様推定装置21の内部に設けられる構成も可能である。
【００２７】
プログラム設定部14は、ユーザから仕様推定の対象となるプログラムのテキストを受ける。ここでは例として、プログラム設定部14は、図11に示すような、絶対値の計算を行うC言語関数のプログラムテキストをユーザから設定されたとする。このプログラムは、int（整数）型である x を入力パラメータとして有する。xが0以上であればxを出力し、xが0未満であれば、xに-1を乗じて出力する。
【００２８】
付加制約設定部13は、仕様推定のために用いる付加制約を入力として受け取る。本実施形態では付加制約として事後条件の否定を受け取る。ここでは付加制約として、図12に示すような事後条件の否定が、ユーザから設定されたとする。これはC言語の文法を用いて「関数の戻り値がxの絶対値である」の否定を表したものである。「関数の戻り値がxの絶対値である」が事後条件である。result は関数の戻り値を表す特別な記号である。resultは、本装置を通じて、この意味に統一的に解釈されるものとする。本明細書において付加制約をQと記述する。
【００２９】
プログラム仕様推定装置21の述語生成部22は、プログラム設定部14からプログラムテキストを取得し、当該プログラムテキストに含まれるパラメータおよびその型に基づき述語群を生成する。述語とは、パラメータ（存在すれば）に応じて真または偽が定まる論理式のことであり、制約条件とも呼ばれる。本実施形態の出力となる仕様（事前条件）は、これらの述語のうちの１つまたは複数の組として得られる。
【００３０】
図3に述語生成部22の構成を示す。
【００３１】
属性パターン記憶部42は、属性パターンを記憶している。属性パターンは、パラメータとその型に応じて、後述の述語の生成に用いる属性への変換ルールを定める。
【００３２】
図13に、属性記憶部42に記憶された属性パターンの例を示す。
【００３３】
2つの属性パターンが示される。各属性パターンは、それぞれ1行ずつのルールとして記されている。1行目「int x → x: INT」は、int型のパラメータxはxに変換する（事実上、何も変換しない）と解釈される。ここで、右辺「x: INT」の「INT」は、変換後の属性がINT（整数）型を持つと解釈される。
【００３４】
2行目「int[] x → \forward_bound(x): NAT」の左辺「int[]」は、intの配列型を意味している。このことから、この2行目の属性パターンは、intの配列型を持つパラメータxは「\forward_bound(x)」という属性のテキストに変換する、と解釈される。また、\forward_bound(x)は「xが指すメモリ領域の大きさ」を表すものとする。この\forward_bound(x)は非特許文献1にも登場するなど、公知の技術で実現可能なものである。そして、右辺にある「NAT」から、\forward_bound(x)はNAT型（非負整数型）を持つと解釈される。
【００３５】
属性生成部41は、属性パターン記憶部42から属性パターンを読み込み、プログラム設定部14からプログラムテキストを読み込む。属性生成部41は、プログラムテキスト中に記載されたパラメータとその型を読み取り、読み取ったパラメータとその型と、属性パターンの左辺とのマッチングを取って、合致する属性パターンを特定する。そして、特定した属性パターンによりパラメータを属性に変換する。本例では、プログラムテキスト中に整数型のパラメータ x があることから、「x: INT」が属性として得られる。属性生成部41は、取得した属性のテキスト「x: INT」を属性記憶部43に格納する。なお、本例では、図13の下側の属性パターンに合致するパラメータは、プログラムテキストに含まれていない。
【００３６】
述語パターン記憶部45は、図14に示すような12個の述語パターンを記憶している。述語パターンは、パラメータに基づく述語の生成ルールを表している。12個の述語パターンはグループ分けされており、cov1〜cov5 の5つの集合が存在する。ここで、「INT_MIN」「INT_MAX」はそれぞれ、int型の最小値、最大値を表す特別な記号である。「INT_MIN」「INT_MAX」は、この意味に本装置を通じて統一的に解釈されるものとする。「INT_MIN」「INT_MAX」はそれぞれ具体的な数値でも構わないし、“INT_MIN”“INT_MAX”の文字ラベルでもよい。
【００３７】
ここでcov1〜cov5は、それぞれ否定被覆の関係を構成する述語パターン群を表し、否定被覆パターン集合とも呼ばれる。同じ否定被覆パターン集合に属する述語パターン群から生成された述語群は、否定被覆集合と呼ばれる。
【００３８】
ここで否定被覆とは、集合を任意の2つに分割した場合に、片方に所属する全述語の連言（論理積）が、もう片方に所属する全述語の連言の否定になるような関係を表す。このような関係を満たす述語の集合を否定被覆集合と呼ぶ。したがって否定被覆集合は矛盾核でもある（否定被覆集合から1つでも要素を取り出すと、残りの要素の連言が真になるため）。
【００３９】
例えば、整数である2つの変数A, B に対し、{A＝B, A≠B}は否定被覆集合である。この理由は、以下の通りである。この集合を2分割する方法は
1.       {}（空集合）と{A＝B, A≠B}
2.       {A＝B}と{A≠B}
の2種類ある。
【００４０】
1番目の分割の場合、{}に所属する全述語の連言は、TRUE（常に真）とみなすのが論理学的に妥当な方法である。また{A＝B, A≠B}に所属する全述語の連言は、A＝B∧A≠Bであり、FALSE（常に偽）である。よって、{}と{A＝B, A≠B}の一方に所属する全述語の連言は、他方に所属する全述語の連言の否定になる。
【００４１】
また2番目の分割の場合、{A＝B}に所属する全述語の連言はA＝Bで、これは{A≠B}に所属する全述語の連言A≠Bの否定になっている。よって、{A＝B}と{A≠B}の一方に所属する全述語の連言は、他方に所属する全述語の連言の否定になる。
【００４２】
他にも、{A≧B, A≦B, A≠B}は否定被覆集合をなす。この理由は、以下の通りである。これを2分割する方法は
1.       {}（空集合）と{A≧B, A≦B, A≠B}
2.       {A≧B}と{A≦B, A≠B}
3.       {A≦B}と{A≠B, A≧B}
4.       {A≠B}と{A≧B, A≦B}
の4つある。この4ついずれも、左右の分割集合ごとに述語の連言を取ると
1.       TRUEとFALSE
2.       A≧BとA＜B
3.       A≦BとA＞B
4.       A≠BとA＝B
となり、いずれも互いが互いの否定となっている。
【００４３】
述語パターン記憶部45には、このような否定被覆をなす述語パターン群をユーザが事前に設定しておく。
【００４４】
否定被覆をなす述語パターン群は、否定被覆を自動的に保証するように述語群を生成する方法を用いて生成してもよい。例えば1つの述語パターンに対し、そのパターンを使って生成できる述語Hと、Hの否定である ¬H とを生成する方法がある。集合{H, ¬H}は、かならず否定被覆となるからである。
【００４５】
図14に示したように、各否定被覆パターン集合cov1〜cov5 の右には、行ごとに述語パターンが記載されている。
【００４６】
各述語パターン内の「{ }」は、属性が適用されるべき箇所を表す。{ }の中に記述されるINTまたはNATが、適用可能な属性を表す。たとえば{INT}はINT型、{INT, NAT}はINT型もしくはNAT型の属性で置換できる。同じ否定被覆パターン集合に含まれる各述語パターンは同じ属性を指定している。したがって、否定被覆パターン集合は、その中の各述語パターンと同じ属性に関連づけられる。
【００４７】
本例では、属性記憶部43に格納されている属性「x: INT」と、述語パターン記憶部45に格納されている図14の否定被覆パターン集合 cov2〜cov4とから、図15の上にある7つの述語を生成する。述語パターン適用部44は、生成した述語を、述語記憶部31に格納する。cov5の述語パターンはINTの型を含まないため、「x: INT」は適用できない。cov1の述語パターンは、後述する理由からここでは利用しない（ただし利用しても本発明の動作上、問題ない）。このようにして、述語生成部22は、複数の否定被覆パターン集合のうち、プログラムから検出したパラメータとその型に応じた否定被覆パターン集合を特定し、特定した否定被覆パターン集合を用いて述語を生成する。
【００４８】
述語パターン適用部44は、生成した述語を述語記憶部31に格納する際は、全体を通してユニークとなるインデックス（通し番号）を、各述語に振る。具体的には、cov2と属性「x: INT」から1_1, 1_2, 1_3を、cov3と同属性から2_1と2_2を、cov4と同属性から3_1, 3_2を生成し、これらのインデックスを、各述語に付与する。述語記憶部31には、インデックスが付与された述語が記憶される。
【００４９】
ここで、cov1に属する述語パターンを利用しない理由を述べる。図14のcov1の述語パターンに同じ属性を適用してできる述語（例えば「n≠n」など）は論理的に自明なものにしかならない。したがって、このような述語を生成しても、後続の処理が冗長になるだけである。そのため、この例では、cov1に属する述語パターンから述語は生成していない。ただし、このような述語を生成しても、何ら問題なく動作可能である。
【００５０】
述語パターン適用部44は、同じ否定被覆関係から生成された述語の集合構成を、図15の下のように、否定被覆記憶部32に格納する。上述の例の場合、{1_1, 1_2, 1_3}, {2_1, 2_2}, および{3_1, 3_2}の3つの否定被覆集合を、否定被覆記憶部32に格納する。この際、各集合にはそれぞれ番号1、2、3を付与する。また各集合の要素は、該当する述語に付与されたインデックスを用いて記述する。なお、インデックスを用いずに、直接、述語を記述する方法も可能である。
【００５１】
図1のプログラム変換部23は、プログラム設定部14から入力されるプログラムテキストを論理式に変換する。
【００５２】
図1のプログラム変換部23は、記号実行（symbolic execution）と言われる、公知の技術を用いることで、プログラムを論理式に変換する。記号実行については、非特許文献（King, Symbolic execution and program testing, Communications of the ACM, Volume 19 Issue 7, July 1976, Pages 385-394）に記載されている。C言語プログラムを記号実行により論理式に変換する方法は、非特許文献（Sakai, Maruchi, and Imai, Model-Checking C Programs against JML-like Specification Language. Proceedings of 19th Asia-Pacific Software Engineering Conference (APSEC 2012), Pages 174-183）に記載があり、本実施形態ではこの文献にある方法を用いるとする。
【００５３】
プログラム変換部23は、プログラムテキストを論理式に変換した結果（プログラム論理式）をプログラム論理式記憶部33に格納する。
【００５４】
図11に示したプログラムを記号実行により論理式に変換すると、結果として 以下と等価な論理式（プログラム論理式）が得られる。プログラム論理式を以降では、Psにより記述する、
(x < 0 ∧ result = x * (-1)) ∨ (¬(x < 0) ∧ result = x)
【００５５】
図1の述語間矛盾核列挙部24は、述語記憶部31内のすべての述語に基づき、連言が矛盾する述語の極小の集合を述語間矛盾核として列挙する（極小とは、当該集合からどの要素を除いても、除いた後に残る要素の連言が真になることを意味する）。本例では、まず上記すべての述語の中から取り除くと、取り除いた後に残る述語の連言が真になるような述語の集合である訂正集合（述語間訂正集合）を求める。求めた訂正集合を公知の手法で述語間矛盾核に変換する。ただし、計算量は多くなる可能性はあるが、訂正集合を求めることなく、直接、上記のすべての述語から、述語間矛盾核を求めてもかまわない。これは、公知のSAT(satisfiablility)ソルバやSMT（SAT Modulo Theories）ソルバ等を用いることで可能である。
【００５６】
図4に、述語間矛盾核列挙部24の構成を示す。また図5に述語間矛盾核列挙部24の処理の流れを示すフローチャートを示す。図4では、分割処理部がAとBの2つ存在するが、1つの分割処理部のみでも構わないし、3つ以上の分割処理部が存在しても構わない。2つ以上の分割処理部がある場合、並行処理ができるため、処理の高速化が可能になる場合がある。以下で説明する例では、結果的に、分割処理部Aのみが使用される場合が示される。
【００５７】
（図5のステップS201）述語間矛盾核列挙部24の分割統合部52が、否定被覆記憶部32の情報を読み出し、否定被覆集合毎に、以下の3つからなるアイテムを生成して、中間結果記憶部53に格納する。
・否定被覆集合の番号
・否定被覆集合の構成情報（矛盾核）
・処理可能かの印
「処理可能かの印」とは、当該アイテムを処理可能か（すなわち選択可能か）を示す印である。
【００５８】
分割統合部52は、否定被覆集合ごとにアイテムを1つ作成する。各アイテムには、上述のように、否定被覆集合の番号と、否定被覆集合の構成情報（矛盾核）と、処理可能かの印の初期値を含める。
【００５９】
本例では、中間結果記憶部53の内容は、図16に示す状態になる。左から「否定被覆集合の番号」「否定被覆集合の構成情報（矛盾核）」「処理可能かの印」である。「OK」が処理可能を示す印である。なお、「NG」の場合は、処理不能を表す。
【００６０】
（図5のステップS202）分割統合部52は、中間結果記憶部53に記憶されているアイテム数が1アイテムのみかを判別する。1アイテムのみの場合は、判定結果はYESとなり、中間結果記憶部53の1アイテムに記述されている否定被覆集合の構成情報（矛盾核）を述語間矛盾核記憶部34に格納する（S208）。2つ以上のアイテムが記憶されている場合は、判定結果はNOとなり、ステップS203に進む。上述した例では、この時点で、中間結果記憶部53に3つのアイテムが記憶されているため、この判定結果はNOである。よってステップS203に進む。
【００６１】
（図5のステップS203）分割処理部A、Bのうち、処理待ち中の分割処理部を用いて、後続の処理を並行に行う。この時点（初期状態）で、2つある分割処理部の両方ともが処理待ち中である。処理待ち中とは、利用可能状態にあることを意味する。
【００６２】
まず処理待ち中の分割処理部Aに対して、中間結果記憶部53に処理可能なアイテムがi個（1＜i≦N個）あるかを判定する。Nはここでは2であるとする。この値はユーザによって装置に予め設定されるものである。処理可能なアイテムとは、「処理可能かの印」が「OK」のアイテムのことである。N＝2であるため、1＜i≦Nを満たすiは、i＝2のみである。Nは、2以上であり、否定被覆集合の個数（本例では3）以下である必要がある。
【００６３】
現時点では、中間結果記憶部53に処理可能なアイテムが3つあるため（S203のYES）、ステップS204に進む。処理可能なアイテムがi個なければ（S203のNO）、本分割処理部に対する処理を終了する。
【００６４】
（図5のステップS204）分割統合部52は、中間結果記憶部53から処理可能なアイテムのうち、N＝2個のアイテムを分割処理部Aに取得させる。ここでは中間結果記憶部53にあるアイテム1とアイテム2（図16参照）を取得するものとする。分割統合部52は、アイテム1、2の状態（「処理可能かの印」）を「NG（取得不能）」にする。その結果、中間結果記憶部53の内容は図17のようになる。同時に、分割情報記憶部51に、分割処理部Aにアイテム1とアイテム2が取得されたことを記録する。
【００６５】
一方、処理可能な分割処理部Bに対して、中間結果記憶部53に存在するアイテムのうち、処理可能なアイテム（「OK」のアイテム）は、この時点では、1つしかない（S203のNO）。よって、1＜i≦Nの条件を満たさないため、分割処理部Bは特段の処理を行わずに、1回目の処理（1回目のループ）を終了する。
【００６６】
（図5のステップS205）分割処理部Aは続けて、分割処理部Aの各記憶部（部分述語記憶部A、個数記憶部A、部分矛盾核記憶部A）を初期化する。
【００６７】
まず、部分述語記憶部Aに、中間結果記憶部53から取得した2つのアイテムに含まれる5つの述語 1_1, 1_2, 1_3, 2_1, 2_2を格納する。
【００６８】
更に、個数記憶部Aに、取得したアイテムに含まれる否定被覆集合の個数を記録する。この場合は2である。
【００６９】
そして更に、部分矛盾核記憶部Aに、各取得したアイテムに含まれる否定被覆集合に属する述語群を格納する。この場合、{1_1, 1_2, 1_3}と{2_1, 2_2}の2つである。
【００７０】
この時点での分割情報記憶部51、部分述語記憶部A、部分矛盾核記憶部Aの内容は図18のようになる。
【００７１】
（図5のステップS206）分割処理部Aの部分矛盾核列挙部Aが、部分述語記憶部Aに記憶されている各述語に基づき、矛盾核（述語間矛盾核）の列挙を行う。
【００７２】
図6に部分矛盾核列挙部Aの具体的な構成を示す。また、図7に部分矛盾核列挙部Aの処理の流れを示す。なお、分割処理部Bの部分矛盾核列挙部Bも図6の構成を有し、図7に示す動作を行うため、以下では、部分矛盾核列挙部Aの説明のみ行い、部分矛盾核列挙部Bの説明は省略する。
【００７３】
（図7のステップS301）まず部分矛盾核列挙部Aの節作成部61が、部分述語記憶部Aに記憶されている各述語に1対1に対応する変数を、述語の個数だけ作成する。変数は、真または偽の値を持つ。以降、この変数を「緩和変数」（relaxing variable）と呼ぶ。ここでは、述語 1_1, 1_2, 1_3, 2_1, 2_2 （図18参照）の5つに対応する、5つの緩和変数r1_1, r1_2, r1_3, r2_1, r2_2を作成する。
【００７４】
（図7のステップS302）次に、節作成部61が、述語とこれに対応する緩和変数の選言（∨）により、節（述語選択節）を作成する。節とは論理式の一部を意味する。節作成部61は、作成した述語選択節を節記憶部62に格納する。ここでは、以下の5つの述語選択節が作成される。各述語選択節では、緩和変数が真であれば、当該緩和変数と組み合わせられた述語は偽でよい（選択されなくてよい）ことを意味する。
(x>=0∨r1_1)
(x<=0∨r1_2)
(x!=0∨r1_3)
(x>INT_MIN∨r2_1)
(x=INT_MIN∨r2_2)
【００７５】
（図7のステップS302）更に、節作成部61は、部分矛盾核記憶部Aにおける否定被覆集合毎に、そこに属する各述語に対応する緩和変数の選言を取ることで、別の節（緩和選択節）を作成する。節作成部61は、否定被覆集合毎に作成した緩和選択節を、節記憶部62に格納する。
【００７６】
ここでは、部分矛盾核記憶部Aには、2つの否定被覆集合{1_1, 1_2, 1_3} と {2_1, 2_2}が格納されている。そこで、これら2つの否定被覆集合から、以下の2つの緩和選択節をそれぞれ作成する。
(r1_1∨r1_2∨r1_3)
(r2_1∨r2_2)
【００７７】
(r1_1∨r1_2∨r1_3)は、r1_1、r1_2、r1_3のうち少なくとも1つが真であり、残りが偽でよいとの制約を意味する。
(r2_1∨r2_2)は、r2_1、r2_2のうち少なくとも1つが真であり、残りが偽でよいとの制約を意味する。
【００７８】
（図7のステップS304）更に、節作成部61は、個数記憶部Aに記憶された個数情報を元に、真になる緩和変数の個数を、当該個数以下（または当該個数と同じ値）に指定する節（個数指定節）を作成する。この節の存在が、制約として働き、後続の訂正集合列挙部63の処理においては、当該個数の緩和変数のみが真になり、残りの緩和変数は偽になる。なお、このような、真になる変数の個数を指定する処理は、文献（Zhaohui Fu, S Malik, “On solving the partial MAX-SAT problem”, Proceedings of the 9th international conference on Theory and Applications of Satisfiability Testing p. 252-265）などで公知の技術であり、いくつかの方法が適用しうる。本実施形態では、以下のような処理を行う。
【００７９】
まず、個数記憶部Aには個数情報として「2」が格納されている。そこで、各緩和変数に対応して真偽の値をとる中間変数を2つ作成し、各緩和変数の一方の中間変数の組と、他方の中間変数の組を作成する。ここでは、まず
緩和変数r1_1に対して、中間変数s1_1_1、s2_1_1 
緩和変数r1_2 に対して、中間変数s1_1_2、s2_1_2
緩和変数r1_3に対して、中間変数s1_1_3、s2_1_3
緩和変数r2_1に対して、中間変数s1_2_1、s2_2_1
緩和変数r2_2に対して、中間変数s1_2_2、s2_2_2
を生成する。そして、これらから、以下の2組の中間変数の組を作成する。
(1)  s1_1_1, s1_1_2, s1_1_3, s1_2_1, s1_2_2
(2)  s2_1_1, s2_1_2, s2_1_3, s2_2_1, s2_2_2
【００８０】
そして、各組のそれぞれで、「全ての選言」「任意の2つの否定の選言」「1つの否定と、元の緩和変数との選言」の3種類の節を作成する。
【００８１】
まず、s1_1_1, s1_1_2, s1_1_3, s1_2_1, s1_2_2 の組から以下の3種類の節（計16節）が作成される。
【００８２】
全ての選言の節：
(s1_1_1 ∨ s1_1_2 ∨ s1_1_3 ∨ s1_2_1 ∨ s1_2_2)
【００８３】
任意の2つの否定の選言の節：
(¬s1_1_1 ∨ ¬s1_1_2)
(¬s1_1_1 ∨ ¬s1_1_3)
(¬s1_1_1 ∨ ¬s1_1_4)
(¬s1_1_1 ∨ ¬s1_1_5)
(¬s1_1_2 ∨ ¬s1_1_3)
(¬s1_1_2 ∨ ¬s1_1_4)
(¬s1_1_2 ∨ ¬s1_1_5)
(¬s1_1_3 ∨ ¬s1_1_4)
(¬s1_1_3 ∨ ¬s1_1_5)
(¬s1_1_4 ∨ ¬s1_1_5)
【００８４】
1つの否定と、元の緩和変数との選言の節：
(¬s1_1_1 ∨ r1_1)
(¬s1_1_2 ∨ r1_2)
(¬s1_1_3 ∨ r1_3)
(¬s1_1_4 ∨ r1_4)
(¬s1_1_5 ∨ r1_5)
【００８５】
s2_1_1, s2_1_2, s2_1_3, s2_2_1, s2_2_2 の組についても同様に、以下の3種類の節（計16節）が作成される。
【００８６】
全ての選言の節：
(s2_1_1 ∨ s2_1_2 ∨ s2_1_3 ∨ s2_2_1 ∨ s2_2_2)
【００８７】
任意の2つの否定の選言の節：
(¬s2_1_1 ∨ ¬s2_1_2)
(¬s2_1_1 ∨ ¬s2_1_3)
(¬s2_1_1 ∨ ¬s2_1_4)
(¬s2_1_1 ∨ ¬s2_1_5)
(¬s2_1_2 ∨ ¬s2_1_3)
(¬s2_1_2 ∨ ¬s2_1_4)
(¬s2_1_2 ∨ ¬s2_1_5)
(¬s2_1_3 ∨ ¬s2_1_4)
(¬s2_1_3 ∨ ¬s2_1_5)
(¬s2_1_4 ∨ ¬s2_1_5)
【００８８】
1つの否定と、元の緩和変数との選言の節：
(¬s2_1_1 ∨ r1_1)
(¬s2_1_2 ∨ r1_2)
(¬s2_1_3 ∨ r1_3)
(¬s2_1_4 ∨ r1_4)
(¬s2_1_5 ∨ r1_5)
【００８９】
このようにして計32個の節が作成される。節作成部61は、これら32個の節も、節記億部62に格納する。
【００９０】
節記憶部62に記憶された全ての節（個数指定節（上記の32個の節）と、述語選択節、緩和選択節）との連言を取り、当該連言の論理式を真にする解を求めると、真となる緩和変数の個数が必ず2個以下となる（実際は、否定被覆集合の性質から2個に一致する）。
【００９１】
（図7のステップS305）次に、訂正集合列挙部63が、節記憶部62に記憶された全ての節の連言を取って論理式F1を作成する。訂正集合列挙部63は、その論理式F1の解を列挙する。解は1つまたは複数存在する。各解において、真になる緩和変数の個数は、2つである。
【００９２】
訂正集合列挙部63は、その解において真となっている緩和変数を特定し、特定した緩和変数に対応する述語のインデックスの集合を得る。ここで得られる集合は、極小訂正集合である。この理由は、極小訂正集合のサイズが、個数記憶部Aに記憶された個数、すなわち、論理式F1に含まれる否定被覆の個数と必ず一致するからである。従って、論理式F1に含まれる否定被覆の個数を指定することが、本実施形態において重要となる。
【００９３】
上述の個数指定節が存在しない場合、訂正集合の定義から、得られる訂正集合の個数は否定被覆集合の個数以上になるが、真になる緩和変数の個数を個数指定節により2に限定することで、訂正集合の要素数を最小にできる。訂正集合列挙部63は、解ごとに得た訂正集合を、訂正集合記憶部64に格納する。
【００９４】
この例では、訂正集合として、{1_1, 2_1}, {1_1, 2_2}, {1_2, 2_2}, {1_3, 2_2} の4つが得られる。
【００９５】
ここで、論理式の解を列挙する処理には、SAT(satisfiablility)ソルバやSMT（SAT Modulo Theories）ソルバなど、広く公知の論理制約ソルバを用いることができる。ただし、解が複数ある場合、1つだけでなく、全てを列挙できるソルバを使用することが条件である。本実施形態では、例えばKodKod（http://alloy.mit.edu/kodkod/）などを利用することができる。
【００９６】
（図7のステップS306）次に、矛盾核変換部65が、訂正集合記憶部64に格納されている訂正集合群を、矛盾核（述語矛盾核）群に変換する。矛盾核変換部65は、取得した矛盾核群を部分矛盾核記憶部Aに格納する。部分矛盾核記憶部Aに元々記憶されていた内容は上書きによって消去されてもよい。訂正集合群から矛盾核群への変換は公知の手法を用いて行えばよい。
【００９７】
極小訂正集合群と極小矛盾核群の間の関係は、下記文献等によって、論理式の加法標準形（DNF、Disjunctive Normal Form）と乗法標準形（CNF、Conjunctive Normal Form）との間の関係と同等であることが知られている。関連文献を下記に列挙する。
・Bailey, J. and P. J. Stuckey: 2005, ‘Discovery of Minimal Unsatisfiable Subsets of Constraints Using Hitting Set Dualization’. In: Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages (PADL’05), Vol. 3350 of LNCS.
・Birnbaum, E. and E. L. Lozinskii: 2003, ‘Consistent subsets of inconsistent systems: structure and behaviour’. Journal of Experimental and Theoretical Artificial Intelligence 15, 25-46.
・Liffiton, M. H., M. D. Moffitt, M. E. Pollack, and K. A. Sakallah: 2005, ‘Identifying Conflicts in Overconstrained Temporal Problems’. In: Proceedings of the 19th International Joint Conference on Artificial Intelligence (IJCAI’05). pp.205-211.
【００９８】
従って、訂正集合群から矛盾核群への変換処理には、たとえば非特許文献2の6.2節（pp. 15-17）に示された方法や、あるいは文献（T Eiter, G Gottlob, K Makino, <<New results on monotone dualization and generating hypergraph transversals>> - SIAM Journal on Computing, 2003）に示されたような公知の乗法標準形／加法標準形（CNF/DNF）変換アルゴリズムなど、多くの公知の技術が利用可能である。
【００９９】
ここでは先に求められた訂正集合群{1_1, 2_1}, {1_1, 2_2}, {1_2, 2_2}, {1_3, 2_2}を変換することで、矛盾核群{1_1, 1_2, 1_3}, {2_1, 2_2}, {1_1, 2_2} が求まる。この変換をCNF/DNF変換に見立てるならば、先の訂正集合 {1_1, 2_1}, {1_1, 2_2}, {1_2, 2_2}, {1_3, 2_2} から、各訂正集合の選言のすべての連言をとって論理式 (1_1 ∨ 2_1)∧(1_1 ∨ 2_2)∧(1_2 ∨ 2_2)∧(1_3 ∨ 2_2) を作る。この論理式を、等価なDNF論理式 (1_1 ∧ 1_2 ∧ 1_3)∨(2_1 ∧ 2_2)∨(1_1 ∧ 2_2) に変換する。この後、DNF論理式の各節に含まれる記号を1つの集合とすれば 、{1_1, 1_2, 1_3}, {2_1, 2_2}, {1_1, 2_2} が得られる。これらが各々、矛盾核変換部65で得られる矛盾核である。
【０１００】
上記では訂正集合を矛盾核に変換する場合を示したが、直接、矛盾核を求める場合は、たとえば、最も単純には、 (x>=0∨r1_1)(x<=0∨r1_2)(x!=0∨r1_3)(x>INT_MIN∨r2_1)(x=INT_MIN∨r2_2)の連言を含む論理式において同時に真にすることが不可能な節を求め、特定した節に含まれる述語の集合を矛盾核として求めることができる。たとえば解の1つとして、(x>=0∨r1_1)と(x=INT_MIN∨r2_2)が同時に真できないとの解が得られれば、｛x>=0、x=INT_MIN｝、すなわち、{1_1, 2_2}が矛盾核の1つとして求まる。
【０１０１】
以上で、分割処理部Aにおける矛盾核列挙が終了したので、その結果に基づき、中間結果記憶部53を更新する（図5のステップS207）。具体的には、中間結果記憶部53が、分割処理部Aが取得した2つのアイテムの否定被覆インデックスをマージしたアイテムを作成し、そのアイテムの矛盾核の欄に、部分矛盾核記憶部Aに格納された矛盾核（述語間矛盾核）を追記し、処理可能かの印の欄に、処理可能の印「OK」を追記する。分割処理部Aが取得した2つのアイテムは、中間結果記憶部53から削除する。これにより、中間結果記憶部53の状態は図19のようになる。1行目の1列目が、元のアイテム1と2の否定被覆のインデックスをマージした結果である。1行目の2列目に、部分矛盾核記憶部Aに記憶された矛盾核（述語間矛盾核）が記録されている。3列目は、処理可能を表す印「OK」に設定されている。
【０１０２】
2つの分割処理部A、Bについて、図5のステップS203〜S207の処理が終わったので、分割統合部52は、ステップS202に戻って、再び同じ処理を繰り返す。まず、中間結果記憶部52に記憶されているアイテム数が1個だけかを判別する。ここでは2個あるので、これはNOと判定され、ステップS203に進む。分割処理部A、Bとも処理可能な状態である。
【０１０３】
（図5のステップS203）分割統合部52が、分割処理部Aに対して、中間結果記憶部53内に、処理可能なアイテム（「OK」のアイテムの数）が、i個（1より大きくN（=2）以下の個数）、存在するかを判定する。現時点では、2個存在するので（図19参照）、この判定はYESである。よって、2個のアイテム、すなわちアイテム{1,2}とアイテム3を中間結果記憶部53から取得し、分割処理部Aに渡す（S204）。分割統合部52は、中間結果記憶部53において、当該2個のアイテムに、取得不能の印「NG」をつける。また、分割統合部52は、分割処理部Aにアイテム{1,2}とアイテム3に渡されたことを分割情報記憶部51に記録する。
【０１０４】
一方、分割処理部Bに対して、中間結果記憶部53に処理可能なアイテムは1つも存在しない（アイテム{1,2}とアイテム3のいずれも「NG」である）。よって、分割統合部52は、分割処理部Bに対し、特段の処理を行わずに、2回目の処理を終了させる（S203のNO）。
【０１０５】
（図5のステップS205）分割処理部Aは、各記憶部を初期化する。まず、分割処理部Aは分割統合部52から取得された2つのアイテムに含まれる述語 1_1, 1_2, 1_3, 2_1, 2_2, 3_1, 3_2 の7つを、部分述語記憶部Aに格納する。更に、分割処理部Aは、分割統合部52から取得した否定被覆集合の個数を記録する。この場合は3である（アイテム{1,2}とアイテム3には、1,2,3の3つの否定被覆集合が含まれる）。そして更に、分割処理部Aは、部分矛盾核記憶部Aに、分割統合部52から取得したアイテムにおける矛盾核を、矛盾核記憶部Aに格納する。この場合、{1_1, 1_2, 1_3}、{2_1, 2_2}、{1_1, 2_2}および{3_1, 3_2}の4つの矛盾核を部分矛盾核記憶部Aに格納する。
【０１０６】
この時点での分割情報記憶部51、部分述語記憶部A、部分矛盾核記憶部Aの内容を図20に示す。
【０１０７】
（図5のステップS206）分割処理部Aの部分矛盾核列挙部Aが、矛盾核の列挙を行う。
【０１０８】
（図7のステップS301）1回目の処理と同様に行い、まず節作成部61が、部分述語記憶部Aに記憶されている7つの述語に対応して、7つの緩和変数 r1_1, r1_2, r1_3, r2_1, r2_2, r3_1, r3_2 を作成する。
【０１０９】
（図7のステップS302）次に節作成部62が、7つの述語と、これらの述語に対応する7つの緩和変数から、以下の7つの節（述語選択節）を作成する。節作成部62は、作成した7つの節（述語選択節）を、節記憶部62に格納する。
(x>=0∨r1_1)
(x<=0∨r1_2)
(x!=0∨r1_3)
(x>INT_MIN∨r2_1)
(x=INT_MIN∨r2_2)
(x>INT_MAX∨r3_1)
(x=INT_MAX∨r3_2)
【０１１０】
（図7のステップS303）また、節作成部62は、部分矛盾核記憶部Aに記憶されている4つの矛盾核に対して、以下の4つの節（緩和選択節）を作成する。節作成部62は、作成した4つの節（緩和選択節）を、節記憶部62に格納する。
(r1_1∨r1_2∨r1_3)
(r2_1∨r2_2)
(r1_1∨r2_2)
(r3_1∨r3_2)
【０１１１】
（図7のステップS304）更に、真になる緩和変数の個数を3個以下に指定する節（個数指定節）を作成する。作成方法は、前述した方法を用いればよい。作成される節の具体例は、数が多いため省略する。節作成部62は、作成した個数指定節を、節記憶部62に格納する。
【０１１２】
（図7のステップS305）そして訂正集合列挙部63が、節記憶部62に記憶された全ての節の連言を取って論理式F2を生成する。訂正集合列挙部63は、生成した論理式F2の解を列挙する。各解で、真になった緩和変数に対応する述語の集合をそれぞれ訂正集合として取得する。ここでは、{1_1, 2_1, 3_2}, {1_1, 2_2, 3_2}, {1_2, 2_2, 3_1}, {1_2, 2_2, 3_2}, {1_3, 2_2, 3_2} の5つの訂正集合が得られる。訂正集合列挙部63は、これら5つの訂正集合を訂正集合記憶部64に格納する。
【０１１３】
（図7のステップS306）次に、矛盾核変換部65が、訂正集合記憶部64内の訂正集合群を矛盾核群に変換する。ここでは、{1_1, 1_2, 1_3}, {2_1, 2_2}, {1_1, 2_2}, {3_1, 3_2}, {1_2, 3_2}, {2_2, 3_2} の6つ矛盾核が求まる。矛盾核変換部65は、これら6つの矛盾核を部分矛盾核記憶部Aに格納する。部分矛盾核記憶部Aに元々記憶されていた内容は上書きによって消去されてもよい。
【０１１４】
分割処理部A，Bの処理が終了したので、分割統合部52は、1回目の処理と同様、部分矛盾核記憶部Aの内容に基づき、中間結果記憶部53の内容を更新する。更新の結果、中間結果記憶部53の内容は、図21に示すように、1つのアイテムのみが格納された状態となる。
【０１１５】
（図5のステップS202）次に、分割統合部52は、中間結果記憶部53に記憶されているアイテムの個数を確認する。ここではアイテム数は1であるため、YESと判定され、ステップS208に進む。
【０１１６】
（図5のステップS208）分割統合部52は、中間結果記憶部53に1つだけ記憶されているアイテムに含まれる矛盾核群（述語間矛盾核群）を取り出して、述語間矛盾核記憶部34に格納する。述語間矛盾核記憶部に、{1_1, 1_2, 1_3}, {2_1, 2_2}, {1_1, 2_2}, {3_1, 3_2}, {1_2, 3_2}, {2_2, 3_2}の6個の述語間矛盾核が格納される。以上により、述語間矛盾核列挙部24の処理が終了する。
【０１１７】
図1の全体矛盾核列挙部25は、述語間矛盾核記憶部34に記憶された述語間矛盾核と、プログラム論理式記憶部33に記憶されたプログラム論理式と、付加制約設定部13により設定される付加制約（ここでは事後条件の否定）と、述語記憶部31に記憶されている述語群に基づき、矛盾核を列挙する。
【０１１８】
図8に全体矛盾核列挙部25の具体的な構成例を示す。
【０１１９】
初期矛盾核設定部45が、述語間矛盾核記憶部34に記憶されたすべての述語間矛盾核を矛盾核記憶部49に格納する。ここでは図21に示したように、6個の矛盾核（述語間矛盾核）が矛盾核記憶部49に格納される。
【０１２０】
否定被覆設定部43が、否定被覆記憶部32に記憶された否定被覆集合の個数に1を加算し、加算後の値を個数記憶部44に格納する。このように1を加算するのは、後述する矛盾核列挙部48で列挙される訂正集合のサイズは、必ず否定被覆集合の個数と同じか、それに1（付加制約（事後条件の否定）が真の場合）を加算した数に等しくなるためである。ここでは、図15の下に示したように否定被覆集合の個数が3であるため、3に1を加算した4を個数記憶部44に格納する。
【０１２１】
また、プログラム論理式設定部46が、プログラム論理式記憶部33に格納されたプログラム論理式Psを読み出して、不変制約記憶部47に格納する。
【０１２２】
また、可変制約設定部41が、述語記憶部31に記憶された述語をすべて読み出して、可変制約記憶部42に格納する。ここでは、図15の上に示したように、7個の述語が可変制約記憶部42に格納される。また、可変制約設定部41が、付加制約設定部13により設定された付加制約（事後条件の否定）を取得して、可変制約記憶部42に格納する。
【０１２３】
以上の初期化処理によって、各記憶部42、44、47、49の状態は図22のようになる。
【０１２４】
次に、全体矛盾核列挙部25の矛盾核列挙部48が矛盾核を列挙する。図9に矛盾核列挙部48の構成を示す。図10に矛盾核列挙部48の処理のフローチャートを示す。
【０１２５】
（図10のステップS401）節作成部51が、まず、可変制約記憶部42に格納される7つの述語に対応する緩和変数 r1_1, r1_2, r1_3, r2_1, r2_2, r3_1, r3_2,を作成し、また可変制約記憶部42に格納される付加制約（事後条件の否定）にインデックス０を割り当て、対応する緩和変数r0 を作成する。すなわち、計8個の緩和変数を作成する。
【０１２６】
（図10のステップS402）節作成部51が、これらの述語と緩和変数の選言、および付加制約と緩和変数の選言により、以下の節（述語選択節と付加制約選択節）を作成する。節作成部51は、作成した節（述語選択節と付加制約選択節）を節記憶部52に格納する。
(x>=0∨r1_1)
(x<=0∨r1_2)
(x!=0∨r1_3)
(x>INT_MIN∨r2_1)
(x=INT_MIN∨r2_2)
(x>INT_MAX∨r3_1)
(x=INT_MAX∨r3_2)
(Q∨r0)
【０１２７】
（図10のステップS403）節作成部51が、矛盾核記憶部49に記憶された6個の矛盾核（述語間矛盾核）に基づき、以下の節（緩和選択節）を作成する。節作成部51は、作成した緩和選択節を節記憶部52に格納する。
(r1_1∨r1_2∨r1_3)
(r2_1∨r2_2)
(r1_1∨r2_2)
(r3_1∨r3_2)
(r1_2∨r3_2)
(r2_2∨r3_2)
【０１２８】
（図10のステップS404）節作成部51が、8個の緩和変数（r1_1, r1_2, r1_3, r2_1, r2_2, r3_1, r3_2,r0）のうち、真になる緩和変数の個数を4個以下に指定する節（個数指定節）を作成する。作成方法は、前述した方法を用いればよい。個数指定節は、節の数が多いため、表記を省略する（Zと表記する）。節作成部51は、作成した個数指定節を、節記憶部52に格納する。
【０１２９】
更に、節作成部51は、不変制約記憶部47に格納されているプログラム論理式Psを、そのまま節として節記憶部52に格納する。
【０１３０】
（図10のステップS405）訂正集合列挙部53が、節記憶部52に記憶されている全ての節の連言を取って論理式F3を作成する。すなわち下記の全ての節の連言を取った論理式F3を生成する。
Ps
Q
Z
(x>=0∨r1_1)
(x<=0∨r1_2)
(x!=0∨r1_3)
(x>INT_MIN∨r2_1)
(x=INT_MIN∨r2_2)
(x>INT_MAX∨r3_1)
(x=INT_MAX∨r3_2)
(Q∨r0)
(r1_1∨r1_2∨r1_3)
(r2_1∨r2_2)
(r1_1∨r2_2)
(r3_1∨r3_2)
(r1_2∨r3_2)
(r2_2∨r3_2)
【０１３１】
訂正集合列挙部53は、作成した論理式F3の解を列挙する。解ごとに、真になった緩和変数に対応する述語の集合を訂正集合（全体訂正集合）として取得する。訂正集合列挙部53は、各取得した訂正集合を、訂正集合記憶部54に格納する。ここでは、{1_1, 2_1, 3_2}, {0, 1_1, 2_2, 3_2}, {0, 1_2, 2_2, 3_1}, {0, 1_2, 2_2, 3_2}, {0, 1_3, 2_2, 3_2} の5つの訂正集合が、訂正集合記憶部54に格納される。
【０１３２】
（ステップS406）矛盾核変換部55が、訂正集合記憶部54に記憶されている訂正集合群を、矛盾核群に変換する。矛盾核変換部55は、生成した矛盾核群を、矛盾核記憶部49に格納する。ここでは、{1_1, 1_2, 1_3}, {2_1, 2_2}, {1_1, 2_2}, {3_1, 3_2}, {1_2, 3_2}, {2_2, 3_2}, {0, 1_1}, {0, 2_1}, {0, 3_2} の8つの矛盾核が生成される。これらの矛盾核が矛盾核記憶部49に格納される。矛盾核記憶部49に元々記憶されていた内容は、上書きによって消去されてもよい。
【０１３３】
以上で、図8の矛盾核列挙部48の処理が終了する。
【０１３４】
なお、矛盾核列挙部48は、前述した部分矛盾核列挙部（図6参照）とほぼ同様の処理（図7参照）を行っている。従って、矛盾核列挙部48は、部分矛盾核列挙部と共有可能な構成として、矛盾核列挙部と部分矛盾核列挙部を1つにまとめてもよい。この場合、図9の可変制約記憶部42は、図6の部分述語記憶部に対応する。また図9の矛盾核列挙部48には、不変制約記憶部47からの入力が存在するが、図6の部分矛盾核列挙部では不変制約記憶部47からの入力はない。このため、部分矛盾核列挙の動作の際は、不変制約記憶部47の内容を空として処理をすればよい。これについては変形例1として後に詳述する。
【０１３５】
矛盾核取得部50は、矛盾核記憶部49内に記憶されている矛盾核群を読み出して、全体矛盾核記憶部35にそのまま格納する。これで、全体矛盾核列挙部25の処理は終了する。
【０１３６】
図1の仕様導出部26は、全体矛盾核記憶部35に記憶された矛盾核群を元に仕様（事前条件）を生成する。まず、仕様導出部26は、全体矛盾核記憶部35に記憶された矛盾核群のうち、付加制約に相当するインデックス0を含むもののみを特定する。
【０１３７】
{1_1, 1_2, 1_3}, {2_1, 2_2}, {1_1, 2_2}, {3_1, 3_2}, {1_2, 3_2}, {2_2, 3_2}, {0, 1_1}, {0, 2_1}, {0, 3_2}のうち、インデックス0を含むものは、{0, 1_1}, {0, 2_1}, {0, 3_2}の3つである。よって、この3つの矛盾核を特定する。
【０１３８】
次に、仕様導出部26は、各特定した矛盾核から、付加制約に相当するインデックス0を除き、かつ、他のインデックスを、元の述語に置換する。
【０１３９】
{0, 1_1}からインデックス0を除くと、{1_1}であり、インデックス1_1をx>=0（図22参照）に置換すると、{x>=0}が得られる。
【０１４０】
{0, 2_1}からインデックス0を除くと、{2_1}であり、インデックス2_1をx>INT_MIN（図22参照）に置換すると、{x>INT_MIN}が得られる。
【０１４１】
{0, 3_2}からインデックス0を除くと、{3_2}であり、インデックス3_2をx=INT_MAX（図22参照）に置換すると、{x=INT_MAX }が得られる。
【０１４２】
よって、{x>=0}, {x>INT_MIN}, {x=INT_MAX} の3つの集合が得られる。この例では各集合は、単一の述語のみから構成されているが、一般には複数の述語が1つの集合を構成しうる。
【０１４３】
仕様導出部26は、このように得られた集合ごとに、全要素の連言を取って1つの論理式を生成する。この結果、以下の3つの論理式が得られる。
x>=0
x>INT_MIN
x=INT_MAX
【０１４４】
これら3つの論理式はいずれも、最初にユーザがプログラム設定部14に設定したプログラムと、付加制約設定部13に設定した付加制約に含まれる事後条件（図12に示した付加制約から否定“！”を除去したもの）とに対する事前条件になる。
【０１４５】
仕様導出部26は、生成した仕様（3つの事前条件）を仕様提示部12に渡す。仕様提示部12は、仕様導出部26から渡された仕様を、表示装置の画面に表示する。これにより、ユーザに仕様を提示する。仕様提示部12は、仕様導出部26から渡された仕様をハードディスク、メモリ装置等の記憶装置に保存しても良い。また、仕様提示部12は、当該仕様をネットワークを介して別の装置に送信してもよい。
【０１４６】
上述した例では、付加制約Qと緩和変数の選言(Q∨r0)を論理式F3に含めたが、選言(Q∨r0)を論理式から除去する構成も可能である。この場合、個数指定節も4から3を指定するように変更する。Qが常に真であるとの制約で解が列挙することで、訂正集合から変換された矛盾核は付加制約（インデックス0）を含まない。すなわち、変換後の矛盾核は、プログラム論理式と付加制約との連言をとった論理式を真にする解を求める場合に付加制約と同時に真にできない述語の極小集合（集合サイズは1以上）である。
【０１４７】
図1に示したシステムは、例えば、図24に示すように、汎用のコンピュータ装置を基本ハードウェアとして用いることでも実現することが可能である。このコンピュータ装置200は、バス201に制御部（プロセッサ）202、主記憶部（メモリ）203、ハードディスク等の補助記憶部204が接続されている。また外部IF205を介して記憶媒体206が接続され、入出力IF207を介して入力部51または出力部52に接続可能になっている。システムの各処理ブロックは、上記のコンピュータ装置に搭載されたプロセッサ202にプログラムを実行させることにより実現することができる。このとき、システムは、上記のプログラムをコンピュータ装置の主記憶部203または補助記憶部204にあらかじめインストールすることで実現してもよいし、CD−ROMなどの記憶媒体206に記憶して、あるいはネットワークを介して上記のプログラムを配布して、このプログラムをコンピュータ装置に適宜インストールすることで実現してもよい。また、システム内の各記憶部は、上記のコンピュータ装置に内蔵あるいは外付けされた主記憶部203、補助記憶部204もしくはCD−R、CD−RW、DVD−RAM、DVD−Rなどの記憶媒体206などを適宜利用して実現することができる。
【０１４８】
図2は、図1のシステムの全体の処理手順を示すフローチャートである。
【０１４９】
（ステップS101）プログラム設定部14は、ユーザから仕様推定の対象となるプログラムのテキストを受ける。付加制約設定部13は、当該プログラムの付加制約を入力として受け取る。付加制約として、たとえば事後条件の否定を入力を受け取る。プログラム仕様推定装置21の述語生成部22は、プログラム設定部14からプログラムテキストを取得する。述語生成部22は、当該プログラムテキストに含まれるパラメータおよびその型を検出し、検出したパラメータおよびその型に基づき、当該パラメータを含む述語群を生成する。また当該述語群に基づく複数の否定被覆集合を生成する。述語生成部22は、生成した述語群を述語記憶部31に格納し、否定被覆集合を否定被覆記憶部32に格納する。
【０１５０】
（ステップS102）図1のプログラム変換部23が、プログラム設定部14から入力されるプログラムテキストを論理式に変換する。なお、当該プログラム変換部14の処理は、前記の述語生成部22の前に行っても、あるいは述語間矛盾核列挙部24の処理の後に行っても構わない。
【０１５１】
（ステップS103）図1の述語間矛盾核列挙部24が、述語記憶部31内のすべて述語に基づき、連言が矛盾する述語の極小集合である矛盾核（述語間矛盾核）を列挙する。この際、否定被覆記憶部32内の否定被覆集合を利用して訂正集合を求め、訂正集合を変換することで矛盾核を取得してもよい。述語間矛盾核列挙部24は、取得した矛盾核（述語間矛盾核）を述語間矛盾核記憶部３４に格納する。本ステップS103の詳細フローは、既に説明した図5および図7に示される。
【０１５２】
（ステップS104）図１の全体矛盾核列挙部25が、述語間矛盾核記憶部34に記憶された述語間矛盾核群と、プログラム論理式記憶部33に記憶されたプログラム論理式と、付加制約設定部13により設定される付加制約（ここでは事後条件の否定）と、述語記憶部31に記憶されている述語群に基づき、訂正集合を生成する。具体的に、各述語と各述語に対応する緩和変数との選言と、付加制約と付加制約に対応する緩和変数の選言と、プログラム論理式と、付加制約との連言を含む論理式を真にする解を求める。この際、真になる緩和変数の個数が否定被覆集合の個数以下になるとの制約と、述語間矛盾核に含まれる述語の少なくとも１つが真になり残りが偽になるとの制約とに従う。そして、緩和変数が真になった述語の集合を訂正集合として得る。全体矛盾核列挙部25は、取得した訂正集合を矛盾核に変換する。全体矛盾核列挙部25は、取得した矛盾核群を全体矛盾核記憶部35に格納する。本ステップS104の詳細フローは、既に説明した図10に示される。
【０１５３】
（図2のステップS105）仕様導出部26は、全体矛盾核記憶部35に記憶された矛盾核群を元に仕様（事前条件）を生成する。まず、仕様導出部26は、全体矛盾核記憶部35に記憶された矛盾核群のうち、付加制約を含むもののみを特定する。仕様導出部26は、各特定した矛盾核から、付加制約を除く。付加制約を除去して得られた集合ごとに、全要素の連言を取ってそれぞれ1つの論理式を仕様（事前条件）として生成する。仕様導出部26は、生成した仕様を仕様提示部12に渡す。仕様提示部12は、仕様導出部26から渡された仕様を、表示装置の画面に表示する。これにより、ユーザに仕様を提示する。
【０１５４】
以上、本実施形態によれば、プログラム実行と付加制約を考慮した全体の矛盾核の列挙を一度に行うのではなく、まず事前条件の候補部品となる述語群から、述語間の矛盾核を求め、これを利用して、全体の矛盾核を求めるという２段階の処理を行う。これにより解の探索空間を削減し、処理を高速化できる。よって、高速かつスケーラブルに、矛盾核（特に極小矛盾核）を全列挙することができる。
【０１５５】
更に、述語間矛盾核群も複数の処理で多段階に求めることで、更なる効率化が期待できる。よって、従来では扱えなかった数の述語数を対象にできる。また、述語間矛盾核群を求める多段処理も並列化することで、更なる高速化も期待できる。
【０１５６】
また否定被覆集合をなすように述語群を用意したため、述語群から述語間訂正集合を効率的に求めることができる。また述語間矛盾核群から全体訂正集合を効率的に求めることができる。
【０１５７】
本実施形態によれば、従来は計算量が大きすぎて推定できなかったような事前条件も推定できるようになる。
【０１５８】
（変形例1）
図23は、変形例1に係る述語間矛盾核列挙部を示す。図1または図4に示した述語間矛盾核列挙部に替えて、図23に示す述語間矛盾核列挙部を用いることができる。
【０１５９】
可変制約設定部41が、述語記憶部31に記憶されている述語群を可変制約記憶部42に格納する。否定被覆設定部43が、否定被覆記憶部32の内容を矛盾核記憶部49に格納する。また、否定被覆設定部43が、否定被覆記憶部32に記憶されている否定被覆集合の個数を個数記憶部44に格納する。不変制約初期化部61が、不変制約記憶部47の内容を何も格納されていない状態に初期化する。矛盾核列挙部48は、図8または図9に示した矛盾核列挙部48と同様の構成を有し、図10のフローチャートの処理を行うことで、矛盾核を生成する。矛盾核列挙部48は、生成した矛盾核（述語間矛盾核）を矛盾核記憶部49に格納する。矛盾核取得部50は、矛盾核記憶部49に格納されている矛盾核を読み出して、述語間矛盾核記憶部34に格納する。
【０１６０】
図23に示した構成は、先に示した図8の全体矛盾核列挙部の構成の一部を共用したものである。ただし、図8のプログラム論理式設定部46が不変制約初期化部61に変わり、図8の矛盾核取得部50の出力先が、述語間矛盾核記憶部34に変わっている。
【０１６１】
よって、図8に示した全体矛盾核列挙部を流用して、述語間矛盾核列挙部の処理を行うこともできる。
【０１６２】
（変形例2）
先の実施形態では、図6に示した部分矛盾核列挙部A内の訂正集合列挙部63、または図9に示した矛盾核列挙部48内の訂正集合列挙部53の処理において、個数記憶部Aまたは44に記憶された個数Nに対し、真となる緩和変数の個数をN個以下との条件で、訂正集合を求めた。
【０１６３】
別の方法として、真となる緩和変数の個数を（N個以下ではなく）厳密にN個とする条件で、同じ結果を得る方法も可能である。
【０１６４】
この場合、述語間矛盾核列挙部24は、部分矛盾核列挙部Aに含まれる訂正集合記憶部64に記憶された訂正集合（述語間訂正集合）を、中間結果記憶部53・述語間矛盾核記憶部34に追加的に格納するようにする。そして、全体矛盾核列挙部25の矛盾核変換部55（図9参照）の処理で、述語間矛盾核記憶部34内の述語間訂正集合を参照して解を補完することで、訂正集合を得る。具体的には以下の通りである。
先の実施形態では、訂正集合記憶部64（図6参照）に記憶された述語間訂正集合は、以下であった。 
{1_1, 2_1, 3_2}, {1_1, 2_2, 3_2}, {1_2, 2_2, 3_1}, {1_2, 2_2, 3_2}, {1_3, 2_2, 3_2}
【０１６５】
これは、真となる緩和変数の個数の条件がN≦3であっても、厳密にN＝3としても変わらない。
【０１６６】
一方、全体矛盾核列挙部25内で求められる訂正集合（全体訂正集合）は 以下であった。
{1_1, 2_1, 3_2}, {0, 1_1, 2_2, 3_2}, {0, 1_2, 2_2, 3_1}, {0, 1_2, 2_2, 3_2}, {0, 1_3, 2_2, 3_2}
【０１６７】
しかし、真となる緩和変数の個数をN≦4でなく、厳密にN＝4として、訂正集合を求めると、以下のみが求まる。
{0, 1_1, 2_2, 3_2}, {0, 1_2, 2_2, 3_1}, {0, 1_2, 2_2, 3_2}, {0, 1_3, 2_2, 3_2}
【０１６８】
以上のように、述語間訂正集合と全体訂正集合は、後者が前者の集合に対して、インデックス0を含むか含まないかの差しかない。そのため、真となる緩和変数の個数がN以下との条件でなく、厳密にN個に一致するとの条件で求めた場合は、述語間訂正集合を使って解を補完すれば、真となる緩和変数の個数がN以下との条件を用いた場合と同じ全体訂正集合を得ることができる。つまり、述語間訂正集合群のうちインデックス0を追加しても、全体訂正集合群に存在しない訂正集合を特定し、特定した訂正集合を全体訂正集合に追加すればよい。
【０１６９】
上述の例では、述語間訂正集合に含まれる{1_1, 2_1, 3_2}を、厳密にN＝4として求めた訂正集合{0, 1_1, 2_2, 3_2}, {0, 1_2, 2_2, 3_1}, {0, 1_2, 2_2, 3_2}, {0, 1_3, 2_2, 3_2}に追加すれば、{1_1, 2_1, 3_2}, {0, 1_1, 2_2, 3_2}, {0, 1_2, 2_2, 3_1}, {0, 1_2, 2_2, 3_2}, {0, 1_3, 2_2, 3_2}が得られる。
【０１７０】
本発明のいくつかの実施形態を説明したが、これらの実施形態は、例として提示したものであり、発明の範囲を限定することは意図していない。これら新規な実施形態は、その他の様々な形態で実施されることが可能であり、発明の要旨を逸脱しない範囲で、種々の省略、置き換え、変更を行うことができる。これら実施形態やその変形は、発明の範囲や要旨に含まれるとともに、特許請求の範囲に記載された発明とその均等の範囲に含まれる。
【図１】
2015114898.tif 000003
【図２】
2015114898.tif 000004
【図３】
2015114898.tif 000005
【図４】
2015114898.tif 000006
【図５】
2015114898.tif 000007
【図６】
2015114898.tif 000008
【図７】
2015114898.tif 000009
【図８】
2015114898.tif 000010
【図９】
2015114898.tif 000011
【図１０】
2015114898.tif 000012
【図１１】
2015114898.tif 000013
【図１２】
2015114898.tif 000014
【図１３】
2015114898.tif 000015
【図１４】
2015114898.tif 000016
【図１５】
2015114898.tif 000017
【図１６】
2015114898.tif 000018
【図１７】
2015114898.tif 000019
【図１８】
2015114898.tif 000020
【図１９】
2015114898.tif 000021
【図２０】
2015114898.tif 000022
【図２１】
2015114898.tif 000023
【図２２】
2015114898.tif 000024
【図２３】
2015114898.tif 000025
【図２４】
2015114898.tif 000026