"ソフトウェア仕様の開発を支援する装置であって、複数の条件を有する条件部および複数の結果を有する結果部からなる複数の命題形式の仕様を受け付ける命題仕様受付手段と、各行が前記複数の条件の1つまたは前記複数の結果の1つを示し、各列が前記複数の命題形式の各々を示す表形式で表した決定表を前記複数の命題形式の仕様から作成する決定表作成手段と、前記複数の命題形式の仕様の各々が互いに矛盾しないかどうかを判定する整合性検証手段とを備え、前記決定表作成手段は、前記命題仕様受付手段から前記複数の命題形式の仕様を取得すると、前記複数の命題形式の仕様の各々について、当該命題形式の仕様の条件部と結果部を取り出して前記決定表の行を作成し、当該命題形式の仕様に対応する列の当該行の欄に印付けし、前記整合性検証手段は、複数の命題形式の仕様のうち任意の2つの命題形式の仕様を前記決定表から取り出し、前記2つの命題形式の仕様の条件部の論理積が充足可能かどうかを判定し、充足可能であるならば前記複数の命題形式の仕様の各々が互いに矛盾すると出力することを特徴とする装置。前記命題仕様受付手段が新たな命題形式の仕様を受け付け、前記決定表作成手段が前記命題仕様受付手段から前記新たな命題形式の仕様を取得すると、前記決定表作成手段が前記新たな命題形式の仕様の条件部と結果部を取り出して前記決定表の行に挿入することを特徴とする請求項1に記載の装置。1つまたは複数の条件を有する必要条件部と1つまたは複数の条件を有する十分条件部からなる、複数の条件間の制約関係を示す条件制約を受け付ける条件制約受付手段と、前記複数の命題形式の仕様が前記条件制約を満たすかどうかをチェックする条件制約検査手段と、をさらに備え、前記条件制約検査手段は、前記条件制約受付手段から前記条件制約を取得すると、前記決定表の各列について、当該列にかかる命題仕様が前記条件制約の十分条件部を構成する複数の条件を全て有し、かつ、当該命題仕様の結果部と前記条件制約の必要条件部とが同時に成立しえない場合には、当該列を前記決定表から削除することを特徴とする請求項1に記載の装置。前記決定表の複数の列のうち、条件部の一部のみが異なり、かつ、結果部が同一である複数の列について、当該複数の列を1つの列に統合し、任意値を表す記号で前記条件部の前記一部を置き換える、任意値記号置換手段をさらに備える請求項1乃至3に記載の装置。前記決定表から、当該決定表の仕様を満たすソフトウェアプログラムを生成することを特徴とする請求項1乃至3に記載の装置。前記整合性検証手段は、SATソルバを用いて前記論理積が充足可能かどうかを判定することを特徴とする請求項1に記載の装置。ソフトウェア仕様の開発を支援する装置におけるソフトウェア仕様開発支援方法であって、前記装置は、複数の条件を有する条件部および複数の結果を有する結果部からなる複数の命題形式の仕様を受け付ける命題仕様受付手段と、各行が前記複数の条件の1つまたは前記複数の結果の1つを示し、各列が前記複数の命題形式の各々を示す表形式で表した決定表を前記複数の命題形式の仕様から作成する決定表作成手段と、前記複数の命題形式の仕様の各々が互いに矛盾しないかどうかを判定する整合性検証手段とを備え、前記決定表作成手段が、前記命題仕様受付手段から前記複数の命題形式の仕様を取得すると、前記複数の命題形式の仕様の各々について、当該命題形式の仕様の条件部と結果部を取り出して前記決定表の行を作成し、当該命題形式の仕様に対応する列の当該行の欄に印付けするステップと、前記整合性検証手段が、複数の命題形式の仕様のうち任意の2つの命題形式の仕様を前記決定表から取り出し、前記2つの命題形式の仕様の条件部の論理積が充足可能かどうかを判定し、充足可能であるならば前記複数の命題形式の仕様の各々が互いに矛盾すると出力するステップとを含むことを特徴とする方法。前記命題仕様受付手段が新たな命題形式の仕様を受け付け、前記決定表作成手段が前記命題仕様受付手段から前記新たな命題形式の仕様を取得すると、前記決定表作成手段が前記新たな命題形式の仕様の条件部と結果部を取り出して前記決定表の行に挿入することを特徴とする請求項7に記載の方法。前記装置は、1つまたは複数の条件を有する必要条件部と1つまたは複数の条件を有する十分条件部からなる、複数の条件間の制約関係を示す条件制約を受け付ける条件制約受付手段と、前記複数の命題形式の仕様が前記条件制約を満たすかどうかをチェックする条件制約検査手段と、をさらに備え、前記条件制約検査手段が、前記条件制約受付手段から前記条件制約を取得すると、前記決定表の各列について、当該列にかかる命題仕様が前記条件制約の十分条件部を構成する複数の条件を全て有し、かつ、当該命題仕様の結果部と前記条件制約の必要条件部とが同時に成立しえない場合には、当該列を前記決定表から削除するステップをさらに含む請求項7に記載の方法。前記決定表の複数の列のうち、条件部の一部のみが異なり、かつ、結果部が同一である複数の列について、当該複数の列を1つの列に統合し、任意値を表す記号で前記条件部の前記一部を置き換える、任意値記号置換手段をさらに備える請求項7乃至9に記載の方法。前記決定表から、当該決定表の仕様を満たすソフトウェアプログラムを生成することを特徴とする請求項7乃至9に記載の方法。前記整合性検証手段が、SATソルバを用いて前記論理積が充足可能かどうかを判定することを特徴とする請求項7に記載の方法。特許文献1で開示されている従来技術を用いると、決定表を可読性の高い形式で表示できる。しかし決定表の記述量は変わらないため、決定表の入力量が増え作成工数が増加するという問題や決定表を保存するために必要な記憶容量が増大すること、それに伴い決定表に記載された仕様の検証に必要な時間を多く要すること、仕様の冗長性を発見しにくくなることという問題は解決できない。上記に鑑み、上記課題に対処し、可読性は確保しつつ決定表の作成解読工数削減と記憶容量削減を達成するための技術を提供することを目的とする。上記課題を解決し、上記目的を達成するため、ソフトウェア仕様の開発を支援する装置であって、複数の条件を有する条件部および複数の結果を有する結果部からなる複数の命題形式の仕様を受け付ける命題仕様受付手段と、各行が上記複数の条件の1つまたは上記複数の結果の1つを示し、各列が上記複数の命題形式の各々を示す表形式で表した決定表を上記複数の命題形式の仕様から作成する決定表作成手段と、上記複数の命題形式の仕様の各々が互いに矛盾しないかどうかを判定する整合性検証手段とを備え、上記決定表作成手段は、上記命題仕様受付手段から上記複数の命題形式の仕様を取得すると、上記複数の命題形式の仕様の各々について、当該命題形式の仕様の条件部と結果部を取り出して上記決定表の行を作成し、当該命題形式の仕様に対応する列の当該行の欄に印付けし、上記整合性検証手段は、複数の命題形式の仕様のうち任意の2つの命題形式の仕様を上記決定表から取り出し、上記2つの命題形式の仕様の条件部の論理積が充足可能かどうかを判定し、充足可能であるならば上記複数の命題形式の仕様の各々が互いに矛盾すると出力することを特徴とする装置を提供する。一実施形態によれば、決定表の作成解決に必要な工数を削減し、決定表を保存表示するために必要な記憶容量を削減することができる。以下、本発明の実施の一形態を、図面を参照しながら詳細に説明する。本実施形態は、決定表作成支援検証装置に適用される。本実施形態では、命題形式の仕様入力命題仕様と呼ぶの入力を受け付けて、その入力命題仕様の内容に基づいて決定表を作成する。つまりユーザは、決定表の各列にマルなどの記号を直接記入するのではなく、入力命題仕様を入力することで決定表を作成する。よって本実施形態によれば、決定表作成のための入力量を削減できる。また、決定表作成の際に参照する要求定義文書の文を大きく変更することなく命題仕様として直接的に本装置に入力できるため、要求定義文書の解読作業を軽減できる。さらに本実施形態では、入力した命題仕様と、その命題仕様に基づいて記入した決定表の列を対応付けて表示する。よって本実施形態によれば、命題仕様のもとになった要求定義文書に変更があった場合に、要求定義文書の変更による決定表への影響を誤りなく特定できる。また本実施形態では、条件に関する命題形式の制約条件制約と呼ぶの入力を受け付け、その条件制約の内容に基づいて、成立し得ない決定表の列を削除する。あるいは、任意値記号置換えの命令を受け付け、マルなどの記号を任意値記号に置き換えることで、複数の列を1列に集約する。よって本実施形態によれば、不要な列を削除して決定表を最小化するため、決定表保存表示のために必要な記憶容量を削減できる。また本実施形態では、作成した決定表の表す仕様を命題形式の仕様出力命題仕様と呼ぶとして出力する。よって本実施形態によれば、決定表が定義する仕様の全体像を容易に読み取ることができる。また、決定表の最小化後に出力命題仕様の出力を行うことで、入力命題仕様とは異なり、冗長な情報あるいは重複した情報を含まない命題形式の仕様が得られる。そのため、命題形式の仕様の保存表示のために必要な記憶容量を削減できる。また本実施形態では、入力命題仕様や決定表の矛盾を検証し、矛盾する入力命題仕様や決定表の列を対応付けて表示する。さらに矛盾検証の問題を充足可能性問題に帰着し、充足可能性問題を高速に解くことができるSATソルバを使用することで、上記矛盾検証を高速化する。さらに本実施形態では、決定表から、その対象ソフトウェアの処理を表すプログラムを生成する。よって本実施形態によれば、矛盾のない決定表から、その仕様を実現する処理を表す正しいプログラムを効率的に取得できる。図1は、本実施形態における決定表作成支援検証装置201の構成例を示すブロック図である。決定表作成支援検証装置201は、入力命題仕様入力表示部101、条件/結果項目入力部102、条件/結果項目抽出部103、決定表結果記入部104、決定表見出し作成部105、任意値記号置換部106、条件制約入力表示部107、不成立条件削除部108、決定表保持部109、整合性検証部110、入力命題仕様保持部111、決定表変換部112、出力命題仕様保持部113、決定表表示編集部114、出力命題仕様表示部115、プログラム生成部116、条件制約保持部117を含む。入力命題仕様入力表示部101は、入力命題仕様を受け付け、受け付けた入力命題仕様を入力命題仕様保持部111に登録する。条件/結果項目抽出部103は、入力命題仕様保持部111から入力命題仕様を取得し、取得した入力命題仕様から条件項目、及び結果項目を抽出する。抽出した条件項目、及び結果項目は、決定表見出し作成部105に渡す。条件/結果項目入力部は、条件項目、及び結果項目の入力を受け付け、決定表見出し作成部105に受け渡す。決定表見出し作成部105は、条件/結果項目抽出部103あるいは条件/結果項目入力102から条件項目、及び結果項目を受け取り、決定表の見出し部分を作成する。決定表の見出しは、図5に示す通り、1列目502に条件/結果項目を縦に並べ、そして各条件/結果項目の右隣の列に、条件/結果項目の取り得る値503を縦に並べて作成する。さらに上記決定表の条件部を全パタン分作成する。前記条件部のパタンは、条件項目の総数と、その条件項目が何通りの値をとるかに基づいて網羅的に作成される。例えば、条件項目Aと条件項目Bが存在し、条件項目Aは値a1と値a2をとり、条件項目Bが値b1と値b2と値b3をとると定義する。この場合、条件部に作成されるパタンはa1、b1a1、b2a1、b3a2、b1a2、b2a2、b3の6通りである。これは上記定義から機械的に作成される。よって仮に条件項目Aが現実には存在しない条件項目だったとしても、あるいは値a1が条件項目の取り得えない値だったとしても、上記定義に従って条件部を作成する。また、条件項目が1つも定義されていない場合は、決定表の条件部は作成しない。作成した決定表は決定表保持部109に登録する。決定表結果記入部104は、入力命題仕様保持部111から入力命題仕様を取得し、同時に決定表保持部109から結果記入対象の決定表を取得する。そして、上記入力命題仕様に基づいて、上記決定表の結果部を記入する。決定表表示編集部114は、決定表保持部109から決定表を取得して画面表示するとともに、ユーザによる決定表の編集を受け付ける。決定表を画面表示する際は、決定表結果記入部104によって結果部を記入した列と、そのもとになった上記入力命題仕様を対応付けて表示する。決定表と入力命題仕様の対応表示の例を図21に示す。図21では,決定表2101と入力命題仕様2103を対応付けて表示している。決定表2101の決定表列2102は,入力命題仕様2103に基づいて記入されたため,入力命題仕様2103と決定表列2102を同色に色づけて表示する。または,ユーザが入力命題仕様を選択した場合のみ,選択した入力命題仕様とその対応する決定表列を色づけて表示してもよい。また、結果部が未記入の列も強調表示する。編集した決定表は、決定表保持部109に再登録する。整合性検証部110は、入力命題仕様保持部111から入力命題仕様を取得し、さらに取得した入力命題仕様に基づいて記入した決定表を決定表保持部109から取得する。そして、上記入力命題仕様間の整合性、及び上記入力命題仕様と上記決定表間の整合性を検証し、検証結果を上記入力命題仕様及び上記決定表に対応付けて、それぞれ入力命題仕様保持部111及び決定表保持部109に登録する。条件制約入力表示部107は、条件制約の入力を受け付け、受け付けた上記条件制約を条件制約保持部117に登録する。不成立条件削除部108は、条件制約保持部117から条件制約を取得し、さらに取得した条件制約の対象となる決定表を決定表保持部109から取得する。そして、上記条件制約に基づいて成立し得ないパタンを特定し、そのパタンを表す列を上記決定表から削除する。その後、成立し得ない列を削除した上記決定表を決定表保持部109に再登録する。任意値記号置換部106は、決定表の任意値記号置換えの命令を受け付け、指定された決定表を決定表保持部109から取得する。そして、決定表の列が含むマル記号を、任意値記号であるアスタリスク記号に置き換え、複数の列を1列に集約する。さらに、集約後の上記決定表を決定表保持部109に再登録する。決定表変換部112は、決定表変換の命令を受け付け、指定された決定表を決定表保持部109から取得する。そして取得した上記決定表の表す仕様を、命題形式の仕様である出力命題仕様に変換する。変換した上記出力命題仕様は、出力命題仕様保持部113に登録される。出力命題仕様表示部115は、出力命題仕様保持部113から出力命題仕様を取得し、取得した上記出力命題仕様を画面表示する。プログラム生成表示部116は、決定表保持部109から決定表を取得し、上記決定表が仕様を表すソフトウェアの、処理を表すプログラムを生成する。さらに、生成した上記プログラムを画面表示する。図2は、決定表作成支援検証装置のハードウェア構成例を示すブロック図である。決定表作成支援検証装置201は、CPU202、メモリ203、外部記憶装置204、表示装置205、入力装置206、及び外部媒体入出力装置207を備える。CPU202は、メモリ203に記憶されたプログラムを実行することによって、各種処理を実行する。メモリ203は、CPU202のワークエリアとして機能し、プログラム及びプログラムの実行に必要なデータを記憶する。具体的には、入力命題仕様入力表示部101、条件/結果項目入力部102、条件制約入力表示部107、条件/結果項目抽出部103、決定表結果記入部104、決定表見出し作成部105、不成立条件削除部108、整合性検証部110、決定表表示編集部114、任意値記号置換部106、決定表変換部112、プログラム生成表示部116、及び出力命題仕様表示部115を構成するプログラムが記憶され、同時に入力命題仕様保持部111、条件制約保持部117、決定表保持部109、及び出力命題仕様保持部113の保持するデータが記憶される。外部記憶装置204は、各種データを格納する。外部記憶装置204は、例えば、ハードディスク装置などである。具体的には、入力命題仕様保持部111、条件制約保持部117、決定表保持部109、及び出力命題仕様保持部113が格納される。あるいは、入力命題仕様入力表示部101、条件/結果項目入力部102、条件制約入力表示部107、条件/結果項目抽出部103、決定表結果記入部104、決定表見出し作成部105、不成立条件削除部108、整合性検証部110、決定表表示編集部114、任意値記号置換部106、決定表変換部112、プログラム生成表示部116、及び出力命題仕様表示部115を構成するプログラムの少なくとも一部についても、外部記憶装置204に格納され、各種処理実行の際にCPU202がメモリ203へ読み出してプログラムを実行することとしてもよい。また各プログラムは、あらかじめメモリ203または外部記憶装置204に格納されていても良いし、必要に応じて、利用可能な媒体を介して、他の装置からメモリ203または外部記憶装置204に導入されてもよい。媒体とは、例えば、外部媒体入出力装置207に着脱可能な記憶媒体、または、ネットワークや、ネットワークを伝搬する搬送波やデジタル信号などの通信媒体を指す。表示装置205は、プログラムの処理結果などを表示する。表示装置205は、例えば、ディスプレイなどである。入力装置206は、処理の実行指示及び処理に必要な情報の入力などを利用者から受け付ける。入力装置206は、例えば、キーボード及びマウスなどである。外部媒体入出力装置207は、外部媒体と、外部記憶装置204に格納されているデータなどの入出力を行う。外部媒体は、外部媒体入出力装置207に着脱可能で可搬性のある記憶媒体であり、外部媒体出力装置207は、外部媒体に読み書き可能なドライブ装置などである。図3は、入力命題仕様入力表示部が受け付ける入力命題仕様の例である。入力命題仕様301、302、303、304は自然言語形式の入力命題仕様であり、入力命題仕様305は論理式形式の入力命題仕様である。入力命題仕様中の括弧に囲まれた用語は、条件及び結果項目、あるいはそれらの値を表す。例えば入力命題仕様301に含まれる保険加入有無という用語は条件項目であり、加入済みという用語はその値である。また、入力命題仕様305は、入力命題仕様301と同じ意味を表す。図4は、条件項目及び結果項目のデータの例である。条件項目のデータ401は、条件項目402と条件の値403を含む。条件項目402は条件の項目名称を表し、条件の値403はその項目が取り得る値の名称を表す。結果項目のデータ404は、結果項目405と結果の値406を含む。結果項目405は結果の項目名称を表し、結果の値406はその項目が取り得る値の名称を表す。図5は、決定表の例であり、条件項目のデータ401と、結果項目のデータ404と、入力命題仕様301、302、303、及び304から作成した決定表である。決定表501は、条件/結果項目の欄502、条件/結果項目の値の欄503、及び条件と結果の対応関係を表す列504を含む。列504の表す対応関係は、列504のマル記号が、条件/結果項目の欄502及び条件/結果項目の値の欄503のどの行に記入されているかによって定義される。例えば、決定表501の最左列は、保険加入有無が加入済みで、保険加入額が2万円以上で、国籍が日本ならば、補助金は交付ありで、納税義務は義務ありという対応関係を表す。図6は、決定表作成の手順例を示すフローチャートである。以下に示す処理は、決定表作成支援検証装置201の備えるCPU202が、メモリ203で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。CPU202は、入力命題仕様入力表示部101を実行することによって、入力命題仕様を受け付け、上記入力命題仕様を入力命題仕様保持部111に登録するステップ601。CPU202は、条件/結果項目入力部102を実行することによって、ユーザからの条件項目データあるいは結果項目データの入力の有無を判定する。入力がある場合はステップ603を、入力がない場合はステップ604を実行するステップ602。CPU202は、条件/結果項目抽出部103を実行することによって、上記入力命題仕様から条件項目データ及び結果項目データを抽出するステップ603。CPU202は、条件結果項目入力102を実行することによって、条件項目データ及び結果項目データの入力を受け付けるステップ604。CPU202は、決定表見出し作成部105を実行することによって、上記条件項目データ及び結果項目データに基づいて、決定表の見出し部分を作成する。さらに決定表の条件部を全列分作成する。作成した決定表は決定表保持部109に登録する。ステップ605。CPU202は、決定表結果記入部104を実行することによって、上記決定表を決定表保持部109から取得する。さらに、上記入力命題仕様を解釈して、上記決定表の結果部を記入するステップ606。決定表結果記入部104は、結果記入済みの上記決定表を決定表保持部109に登録するステップ607。CPU202は、決定表表示編集部114を実行することによって、決定表保持部109から決定表を取得し、画面表示する。決定表を画面表示する際は、決定表結果記入部104によって記入した列と、そのもとになった入力命題仕様を対応付けて表示する。加えて、結果部が未記入の列を強調表示する。また、ユーザからの上記決定表の編集入力を受け付け、上記決定表を編集するステップ608。決定表表示編集部114は、編集済みの上記決定表を決定表保持部109に再登録するステップ609。図7は、入力命題仕様を解釈して決定表に記入する手順例を示すフローチャートであり、ステップ606の詳細手順である。以下に示す処理は、決定表作成支援検証装置201の備えるCPU202が、メモリ203で実行するプログラムによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。CPU202は、決定表結果記入部104を実行することによって、入力命題仕様の条件部と結果部を分割するステップ701。決定表結果記入部104は、決定表保持部109から入力命題仕様の記入対象である決定表を取得するステップ702。決定表結果記入部104は、上記決定表から、条件が上記入力命題仕様の条件部と一致する列を検索し、取得するステップ703。決定表結果記入部104は、前ステップで取得した列の結果に、上記入力命題仕様の結果部の内容を記入するステップ704。図8は、整合性検証の結果に基づく修正後の決定表の例である。決定表801は整合性検証部110の検証結果に基づいて、決定表501を修正した結果である。決定表501は、結果の矛盾505、506と、結果の未定義507、508、及び509を含む。整合性検証部110は、検証の結果として、結果の矛盾505、506をその矛盾する入力命題仕様と対応付けてハイライト表示する。検証結果のハイライト表示の例を図22に示す。結果の矛盾505,506を含む決定表列2202は,入力命題仕様2203,2204に基づいて記入される。よって図22に示す通り,入力命題仕様2203,2204,及び決定表列2202を同色で色づけ表示する。または,ユーザが矛盾する複数の入力命題仕様を選択した場合のみ,選択された入力命題仕様とその矛盾を含む決定表列を色づけて表示してもよい。また検証の結果としてではないが、結果の未定義507、508も検出し、ハイライト表示する。ユーザはこれらのハイライト表示に基づいて、入力命題仕様の追加削除や決定表の直接編集を行い、決定表801を作成する。図9は、決定表及び入力命題仕様の整合性検証の手順例を示すフローチャートである。以下に示す処理は、決定表作成支援検証装置201に備えられたCPU202が、メモリ203内に格納されたプログラムを実行することによって実現される。そしてこのプログラムは、以下に説明する各種の動作を行うためのコードから構成されている。CPU202は、整合性検証部110を実行することによって、決定表保持部109から決定表を取得するステップ901。整合性検証部110は、入力命題仕様保持部111から、上記決定表の結果部の記入に用いた入力命題仕様を取得するステップ902。整合性検証部110は、取得した上記入力命題仕様から、異なる2つの入力命題仕様を選択し、整合性を検証するステップ903。整合性の検証には例えば次の方法を用いる。検証対象の2つの入力命題仕様から、乗法標準形ConjunctiveNormalFormの検証用論理式を作成する。上記検証用論理式は、その充足可能性と、上記2つの入力命題仕様の整合性とが対応付くように作成する。例えば、保険加入有無が保険加入済みで、かつ保険納入額が2万円以上の場合、補助金は交付ありという入力命題仕様1と、保険加入有無が保険加入済みで、かつ国籍が日本の場合、補助金は交付なしという入力命題仕様2の整合性検証について考える。まず、2つの入力命題仕様の条件部と結果部を分割し、それぞれ条件部1保険加入有無が保険加入済みで、かつ保険納入額が2万円以上、結果部1補助金は交付あり、条件部2保険加入有無が保険加入済みで、かつ国籍が日本、結果部2補助金は交付なしとする。次に条件部、結果部をそれぞれ乗法標準系の論理式に変換する。条件項目あるいは結果項目が2通りの値をとる場合、その条件あるいは結果を1つの命題記号で表現することができる。例えば保険加入有無が保険加入済みを論理式Aで表現でき、逆に保険加入有無が未加入を論理式¬Aで表現できる。条件項目あるいは結果項目がn≧3通りの値をとる場合、その条件あるいは結果をn個の命題記号で表現できる。例えば保険納入額が2万円以上を論理式B_1∧¬B_2∧¬B_3で表現でき、逆に保険納入額が1万円以上2万円未満を論理式¬B_1∧B_2∧¬B_3で表現できる。同様に,国籍が日本は論理式Cで表現できる。また,条件部に含まれるかつという言葉は,論理式における∧に変換できる。よって条件部1は論理式A∧B_1∧¬B_2∧¬B_3で表せる。同様に条件部2は論理式A∧Cで表せる。そして、条件部1の論理式A∧B_1∧¬B_2∧¬B_3と条件2の論理式A∧Cをアンド結合することで、検証用論理式αA∧B_1∧¬B_2∧¬B_3∧A∧Cを作成する。この検証用論理式αが充足不能であれば、入力命題仕様1と入力命題仕様2は同一のパタンに対して重複して結果を定義することはないため、結果の矛盾が発生することはない。言い換えると,入力命題仕様1と入力命題仕様2は,同一の決定表列への記入を行わないため,同一の決定表列に異なる結果を記入するという矛盾を引き起こす可能性はない。つまり検証用論理式αが充足不能であれば、入力命題仕様1と入力命題仕様2には不整合は生じ得ないと判断できる。上記の例では,A,B_1,Cがそれぞれ真であり,B_2,B_3がそれぞれ偽であるとき,検証用論理式αは充足されることが分かる。さらに、検証用論理式αが充足可能であった場合は以下の手順を続行する。結果部1の論理式と結果部2の論理式をアンド結合することで、検証用論理式βを作成する。この検証用論理式βが充足可能であれば、入力命題仕様1と入力命題仕様2による結果の定義は矛盾しないと言える。つまり、検証用論理式βが充足可能であれば、入力命題仕様1と入力命題仕様2は整合すると判断できる。さらに上記検証用論理式α、及び上記検証用論理式βの充足可能性判定には、SATソルバを用いることができる。ここで、SATソルバとは、論理式の充足可能性問題SATを解く種々のアルゴリズムSATアルゴリズムを実装するツールの総称である。SATソルバを用いることで、整合性検証を高速化できる。このように、入力命題仕様から乗法標準系の検証用論理式を作成することで、SATソルバを活用した高速な整合性検証を実現できる。整合性検証部110は、入力命題仕様保持部111から取得した上記入力命題仕様の全組合せについて整合性検証を実施済みであれば、ステップ905を実行する。未検証の組合せがある場合は、ステップ903に戻るステップ904。整合性検証部110は、入力命題仕様保持部111から取得した上記入力命題仕様から1つの入力命題仕様を選択し、さらに上記決定表から列を1列選択する。そして選択した上記入力命題仕様と上記列の整合性を検証するステップ905。整合性の検証には例えば次の方法を用いる。ステップ903で述べた方法と同様に、上記入力命題仕様と上記列の整合性検証は、検証対象の入力命題仕様と決定表の列から、乗法標準系の検証用論理式を作成し、その充足可能性を判定するという問題に帰着する。決定表の列は入力命題仕様と同等にみなせるため、ステップ903で述べた方法と全く同じ方法にて検証できる。例えば、決定表501の最左列は、保険加入有無が加入済みで、かつ保険加入額が2万円以上で、かつ国籍が日本の場合、補助金は交付ありで、かつ納税義務は義務ありという入力命題仕様と同等である。整合性検証部110は、入力命題仕様保持部111から取得した上記入力命題仕様と決定表の列の全組合せについて整合性検証を実施済みであれば、ステップ907を実行する。未検証の組合せがある場合は、ステップ905に戻るステップ906。整合性検証部110は、整合性検証の結果、矛盾のあった入力命題仕様、及び決定表の列に、矛盾があることを表すデータを追加する。そして、入力命題仕様は入力命題仕様保持部111に、決定表は決定表保持部109に再登録するステップ907。たとえば、入力命題仕様入力表示部101は、矛盾のあった入力命題仕様を対応付けてハイライト表示してもよい。ステップ903の結果から入力命題仕様間に矛盾があった場合は、入力命題仕様の一覧画面において矛盾のあった入力命題仕様を同色で色付けして表示する。ステップ908。決定表表示編集部114は、矛盾のあった決定表の列を、ステップ908の入力命題仕様の表示と対応付けてハイライト表示する。ステップ905の結果から入力命題仕様と決定表列に矛盾があった場合は、入力命題仕様の一覧画面において矛盾のあった前記入力命題仕様を色付けして表示するとともに、決定表表示画面において矛盾のあった前記列の条件部および結果部全体を前記入力命題仕様と同色で色付けして表示するステップ909。ハイライト表示の例は図22に示す。図22では,入力命題仕様2203,2204,及び決定表列2202を同色で色づけ表示している。上記の整合性検証により、要求定義文書に変更があった場合は決定表のどの範囲に影響があるかを従来は人手で判断していたため変更の影響範囲を誤って特定してしまう等の問題を解決することができる。図10は、条件制約入力表示部が受け付ける条件制約の例である。条件制約1001は自然言語形式の条件制約であり、条件制約1002は論理式形式の条件制約の例である。条件制約中の括弧に囲まれた用語は、条件項目及びその値を表す。例えば条件制約1001に含まれる保険加入有無という用語は条件項目であり、未加入という用語はその値である。図3の入力命題仕様と異なる点は、結果項目及びその値が現れない点である。これは、入力命題仕様が条件に対する結果を定義するのに対し、条件制約は条件と条件の制約条件を定義しているためである。また、入力命題仕様1002は、入力命題仕様1001と同じ意味を表す。ここで、条件制約は決定表の各条件から選択されて構成されており、条件制約を構成する条件を表す内部データと、決定表の項目を構成する条件を表す内部データとは同形式のデータ例えば、文字列形のデータであるものとする。さらに同一の条件は同一のデータになるようにデータ化を行う。例えば、条件制約を構成する条件名称Aをデータ化した結果がデータαで、決定表の項目を構成する条件名称Aをデータ化した結果がデータβの場合は、データα=データβとなる。これにより、後述の不成立条件削除部108の動作において、条件制約の条件を表す文字列型データと,決定表の条件を表す文字列型データを比較することにより、条件制約で指定された必要条件または十分条件が、決定表の条件部または結果部を構成する各条件のうちどの条件またはその否定に該当するかが判断される。条件制約は、作成した決定表から現実には成立し得ない列を除去する目的で与えるものである。例えば条件制約1001は、保険加入が未加入である場合は、保険納入額は0円であるという現実の制約を与えており、これに違反する条件は現実には成立し得ないことを意味する。つまりこの条件制約1001を与えると、保険加入が未加入である、かつ保険納入額が2万円以上である場合、という意味を表す決定表列や、保険加入が未加入である、かつ保険納入額が2万円以上である場合、という意味を表す決定表列は現実には成立し得ない列と判断されるため、決定表から除去される。図11は、条件制約に基づいて列を削除した後の決定表の例であり、条件制約1001に基づいて決定表801から列集合802を削除した後の決定表である。上述の通り、条件制約1001は保険加入が未加入である場合は、保険納入額は0円であるという制約を表す。また,前記列集合802の最左列は保険加入が未加入である、かつ保険納入額が2万円以上である、かつ国籍が日本である場合、補助金は交付無である,かつ納税義務は義務なしであるという意味を表す。前記列集合802の最左列は、保険加入が未加入である、かつ保険納入額が2万円以上であるという条件を含むため、条件制約1001の表す制約に違反すると言える。よって前記列集合802の最左列は、条件制約1001によって削除される。列集合802の含む他の列についても同様である。図12は、任意値記号置換後の決定表の例であり、決定表1101の列集合1102を1列に集約し、列集合1103を1列に集約し、列集合1104を1列に集約し、列集合1105を1列に集約した後、列集合1104と列集合1105の集約によってできた2列をさらに1列に集約してできた決定表である。本集約では,結果項目に影響を与えない条件項目がある決定表列集合を抽出し,前記条件項目の値を任意値記号に置き換えると同時に前記列集合を1つの列に集約するという処理を行う。例として,列集合1102の集約について説明する。列集合1102は,保険加入有無が加入済みであり,かつ保険納入額が2万円以上であり,かつ国籍が日本である場合,補助金は交付ありであり,納税義務は義務ありであるという意味を表す列1と,保険加入有無が加入済みであり,かつ保険納入額が2万円以上であり,かつ国籍が日本以外である場合,補助金は交付ありであり,納税義務は義務ありであるという意味を表す列2で構成される。ここで国籍の条件項目に着目すると,国籍の条件項目の値が日本でも日本以外でも,結果項目の補助金および納税義務の値は同じであることが分かる。つまり列1と列2を合わせると保険加入有無が加入済みであり,かつ保険納入額が2万円以上であり,かつ国籍が任意値である場合,補助金は交付ありであり,納税義務は義務ありであるという意味になる。そしてこれは決定表列1202の表す意味と一致する。以上の理由から,列集合1102に含まれる列1と列2は,決定表列1202に集約できる。このように決定表列を集約することで,決定表の列数を削減できるため,決定表を保持するために必要な記憶容量を削減できるという効果が得られるとともに,決定表の可読性が向上するという効果が得られる。さらに,決定表の列数を削減することで,決定表列と入力命題仕様の間の検証を行う際に検証の対象となる列の数を削減できるため,前記検証にかかるステップ数を削減できるという効果も得られる。図13は、決定表を最小化する手順の例を示すフローチャートである。以下に示す処理は、決定表作成支援検証装置201の備えるCPU202が、メモリ203内に格納されたプログラムを実行することによって実現される。そしてこのプログラムは、以下に説明する各種の動作を行うためのコードから構成されている。CPU202は、条件制約入力表示部107を実行することによって、条件制約の入力を受け付け、受け付けた上記条件制約を、条件制約保持部117に登録するステップ1301。CPU202は、不成立条件削除部108を実行することによって、条件制約保持部から条件制約を取得し、さらに決定表保持部109から制約対象の決定表を取得する。そして上記制約条件を満たさないパタンを表す列を、上記決定表から削除するステップ1302。不成立条件削除部108は、列削除済みの決定表を決定表保持部109に再登録するステップ1303。CPU202は、任意値記号置換部106を実行することによって、決定表に対する任意値記号置換えの命令を受け付け、指定された決定表を決定表保持部109から取得し、上記決定表の条件の値を任意値記号に置換するステップ1304。任意記記号置換部106は、任意値記号にて置換済みの決定表を決定表保持部109に再登録する。図14は、決定表から条件制約を満たさない列を削除する手順例を表すフローチャートであり、ステップ1302の詳細手順である。以下に示す処理は、決定表作成支援検証装置201に備えられたCPU202が、メモリ203内に格納されたプログラムを実行することによって実現される。そしてこのプログラムは、以下に説明される各種の動作を行うためのコードから構成されている。CPU202は、不成立条件削除部108を実行することによって、条件制約保持部から条件制約を取得し、条件制約の十分条件部と必要条件部を分割する。例えば条件制約1001の場合、保険加入有無が未加入であるが十分条件部で、保険納入額は0円であるが必要条件部であるステップ1401。不成立条件削除部108は、決定表保持部109から制約対象の決定表を取得し、上記決定表の列から、条件が上記条件制約の十分条件部を構成する条件を全て含む列、つまり当該列の条件部が成立する場合に上記条件制約の十分条件部が必ず成立するような列を検索するステップ1402。不成立条件削除部108は、ステップ1402の検索によって取得した列集合から、列の結果部と上記条件制約の必要条件とをAND結合した式が充足不可能な列,つまり当該列の条件部と上記条件制約の必要条件とが同時に成立し得ないような列を検索するステップ1403。不成立条件削除部108は、ステップ1403の検索によって取得した列集合を、上記決定表から削除するステップ1404。このように列集合を削除することで,決定表の列数を削減できるため,決定表を保持するために必要な記憶容量を削減できるという効果が得られるとともに,決定表の可読性が向上するという効果も得られる。さらに,決定表の列数を削減することで,決定表列と入力命題仕様間の検証を行う際の検証対象列を削減できるため,前記検証にかかるステップ数を削減できる効果もある。図15は、決定表に対する任意値記号置換えの手順例を表すフローチャートであり、ステップ1304の詳細手順である。以下に示す処理は、決定表作成支援検証装置201に備えられたCPU202が、メモリ203内に格納されたプログラムを実行することによって実現される。そしてこのプログラムは、以下に説明する各種の動作を行うためのコードから構成されている。CPU202は、任意値記号置換部106を実行することによって、決定表に対する任意値記号置換えの命令を受け付け、指定された決定表を決定表保持部109から取得するステップ1501。任意値記号置換部106は、上記決定表から結果が等しい列を検索するステップ1502。任意値記号置換部106は、決定表の条件項目を1つ選択するステップ1503。任意値記号置換部106は、ステップ1502の検索によって取得した列集合から、ステップ1503にて選択した条件項目の値は異なるが、その他の全ての条件項目の値が等しい列を検索するステップ1504。任意値記号置換部106は、ステップ1504の検索によって得た列集合が、ステップ1503にて選択した条件項目の全通りの値を含む場合、ステップ1506を実行する。そうでない場合、ステップ1507を実行するステップ1505。任意値記号置換部106は、ステップ1504の検索によって得た列集合が含む列を、任意の1列を残して削除し、残した列の条件のうち、ステップ1503にて選択した条件項目の値を任意値記号に置換する。同時に、同列の同条件項目のセルを結合するステップ1506。任意値記号置換部106は、ステップ1503にて全条件項目を選択済みの場合、処理を終了する。そうでない場合、ステップ1503に戻るステップ1507。図16は、決定表から変換した出力命題仕様の例であり、出力命題仕様1601、1602、1603、1604は決定表1201から変換して得た出力命題仕様である。出力命題仕様1601、1602、1603、1604は自然言語形式の入力命題仕様であり、出力命題仕様1605は論理式形式の入力命題仕様である。入力命題仕様と同様、出力命題仕様中の括弧に囲まれた用語は、条件及び結果項目、あるいはそれらの値を表す。また、出力命題仕様1605は、出力命題仕様1601と同じ意味を表す。例として,決定表1201を変換して出力命題仕様1601を得る方法を述べる。決定表から出力命題仕様を作成する方針は複数考えられるが,本例では結果項目の値ごとに出力命題仕様を作成する方針を採用する。その他にも,条件項目に優先度を設定し,優先度の高い条件項目の値ごとに出力命題仕様を作成する方針もある。まず,決定表1201の結果項目のうち補助金の結果項目を選択し,さらにその値から交付ありの値を選択する。次に決定表1201を参照すると,補助金が交付ありとなるパタンの条件は,条件項目保険加入有無の値が加入済みであり,かつ条件項目保険納入額の値が2万円以上である場合と分かる。最後にこの条件と結果を結合することで,保険加入有無が加入済みである,かつ保険納入額が2万円以上である場合,補助金は交付ありであるという出力命題仕様1601を得る。上記決定表から出力命題仕様への変換により,決定表と同等の情報を命題仕様形式で保持できるようになるため,前記情報の保持に必要な記憶容量を削減できるという効果がある。また,決定表から仕様を読み取るのには時間がかかるが,同等の情報を命題仕様形式で表示することで,仕様の読み取りにかかる時間を短縮できるという効果もある。上記の任意値置き換え処理により、成立する可能性のない条件に対して結果を定義するという仕様の冗長性や、同じ仕様を異なる文で複数回定義するという仕様の重複、および保持する文形式仕様の分量が必要以上に大きくなるといった問題を解決することができる。図17は、決定表変換及び出力命題仕様表示の手順例を示すフローチャートである。以下に示す処理は、決定表作成支援検証装置201に備えられたCPU202が、メモリ203内に格納されたプログラムを実行することによって実現される。そしてこのプログラムは、以下に説明する各種の動作を行うためのコードから構成されている。CPU202は、決定表変換部112を実行することによって、決定表変換の命令を受け付け、指定された決定表を決定表保持部109から取得するステップ1701。決定表変換部112は、上記決定表の結果項目を選択し、選択した結果項目の値が等しい列の集合を作成する。上記結果項目の選択方法は様々考えられ、少なくとも、予め結果項目に優先度を設定しておいて、その優先度に従って選択する方法があるステップ1702。決定表変換部112は、ステップ1702にて取得した列集合から、その意味を表す出力命題仕様を作成し、出力命題仕様保持部113に登録するステップ1703。決定表変換部112は、上記決定表が含む全ての列が、ステップ1702にて取得したいずれかの列集合に含まれる場合、つまり全ての列が出力命題仕様に反映済みの場合、ステップ1705を実行する。そうでない場合、ステップ1702に戻り、未選択の条件項目を選択するステップ1704。CPU202は、出力命題仕様表示部115を実行することによって、出力命題仕様保持部113から出力命題仕様を取得し、画面に表示するステップ1705。図18は、決定表作成支援検証装置201の画面表示の例である。決定表作成支援検証装置201の画面表示1801は、決定表表示領域1804、整合性検証ボタン1802、決定表最小化ボタン1803、命題仕様変換ボタン1810、入力命題仕様表示領域1805、条件制約表示領域1806、出力命題仕様表示領域1811、入力命題仕様登録領域1807、条件制約登録領域1808、及び条件/結果項目登録領域1809を含む。ユーザが整合性検証ボタンを押下すると、CPU202は、整合性検証部110を実行する。ユーザが決定表最小化ボタン1803を押下すると、CPU202は、不成立条件削除部108を実行した後、任意値記号置換部106を実行する。ユーザが命題仕様変換ボタン1810を押下すると、CPU202は、決定表変換部112を実行する。図19は、プログラム生成の手順例を表すフローチャートである。以下に示す処理は、決定表作成支援検証装置201に備えられたCPU202が、メモリ203内に格納されたプログラムを実行することによって実現される。そしてこのプログラムは、以下に説明する各種の動作を行うためのコードから構成されている。CPU202は、プログラム生成表示部116を実行することによって、決定表保持部109から決定表を取得するステップ1901。プログラム生成表示部116は、上記決定表が示す仕様の通りに条件判定を行うプログラムを生成する。プログラム生成の方法としては、少なくとも、上記決定表の列ごとにIF文を作成する方法があるステップ1902。プログラムを生成する方法の例を,決定表1201と関数プログラム2001を用いて説明する。まず決定表1201を参照すると,前記決定表は3つの条件項目と2つの結果項目を持つことが分かる。そこで条件項目の値を表す変数c1,c2,c3と,結果項目の値を表す変数r1,r2を引数として持つ関数プログラム2001を定義する。結果項目の引数はポインタ引数とする。次に,決定表の列ごとにIF文を作成する。列1202は保険加入有無が加入済みである,かつ保険納入額が2万円以上である,かつ国籍が任意値である場合,補助金は交付ありであり,納税義務は義務ありであるという意味を表すが,このうち国籍が任意値であるという条件は省略可能であるため,結局保険加入有無が加入済みである,かつ保険納入額が2万円以上である場合,補助金は交付ありであり,納税義務は義務ありであるという意味を表す。ここで条件項目を変数に変換し,条件項目の値を変数値に変換する。上で定義した通り,条件項目保険加入有無の値は変数c1で,条件項目保険納入額の値は変数c2で表す。さらに保険加入有無の値加入済みを1で表し,未加入を0で表すとする。同様に保険納入額の値2万円以上を2で表し,1円以上2万円未満を1で表し,0円を0で表すとする。すると保険加入有無が加入済みである,かつ保険納入額が2万円以上である場合という条件は,IF文2002に示すifという条件で表せる。さらに結果項目も同様に変数に変換すると,補助金は交付ありであり,納税義務は義務ありであるという結果は,IF文2002に示すr11r21という代入文で表せる。他の決定表列も同様の方法でIFに変換し,IF文2003および2004を生成する。以上より,決定表1201から関数プログラム2001を生成できることが分かる。図20は決定表1201から生成したプログラムの例である。関数プログラム2001は,IF文2002,2003,2004から構成される。IF文2002は,決定表列1202から生成される。同様にIF文2003は決定表1201の2列目から,IF文2004は3列目から生成される。決定表からプログラムを生成することにより,決定表を仕様とした実装の工数を削減するともに,人手による実装の誤りを防止する効果が得られる。以上のようにして、ソフトウェア仕様を表す決定表に対して、命題仕様の入力による決定表作成支援手段と、上記命題仕様間の整合性を検証する手段と、上記命題仕様と上記決定表間の整合性を検証する手段と、条件制約に基づく上記決定表の不成立条件削除手段と、任意値記号置換による上記決定表の列集約手段と、上記決定表をその仕様を表す命題仕様へ変換する手段と、上記決定表が示す仕様の通りに条件判定を行うプログラムを生成する手段を提供する、決定表作成支援検証装置を提供できる。"