"自然言語から形式言語に変換して仕様書を作成する仕様書作成支援装置であって、要件ごとに、当該要件の自然言語による表現形式と、当該要件の形式言語による表現形式と、当該自然言語による表現形式に求められる入力情報の各々について当該入力情報の仕様書における参照元を示す入力参照元と、を有する記述変換ルールと、自然言語で記載された不足要件導出要件形式と形式言語で記載された不足要件導出要件形式とを有する不足要件導出要件形式と、自然言語で記載された不足要件形式と、を有する要件補間ルールと、前記記述変換ルールに基づき、一以上の自然言語による表現形式の候補を出力する自然言語形式出力手段と、前記一以上の自然言語による表現形式の候補から一以上の自然言語による表現形式の選択を受け付ける自然言語表現受付手段と、前記記述変換ルールに基づき、前記事前言語表現受付手段が受け付けた前記一以上の自然言語による表現形式各々に対応する入力参照元を当該一以上の自然言語による表現形式に求められる入力情報の候補として出力する入力情報候補出力手段と、前記入力情報の候補から前記一以上の自然言語による表現形式各々に対する入力情報の選択を受け付ける入力情報受付手段と、選択された前記一以上の自然言語による表現形式と前記入力情報から、自然言語により表現された一以上の要件を生成し、当該自然言語により表現された一以上の要件を有する自然言語の仕様書を作成する自然言語仕様書作成手段と、前記自然言語の仕様書に含まれる各要件について、当該要件の生成に用いられた自然言語による表現形式と対応する自然言語で記載された不足要件導出要件形式が前記要件補間ルールに登録されているか検索する不足要件導出要件形式検索手段と、前記不足要件導出要件形式検索手段によって抽出された自然言語で記載された不足要件導出要件形式と対応付けられている形式言語で記載された不足要件導出要件形式に前記要件の作成に用いられた入力情報を適用し、不足要件導出情報を生成する不足要件導出情報生成手段と、前記要件補間ルールに基づき、前記不足要件導出要件形式検索手段によって抽出された自然言語で記載された不足要件導出要件形式についての不足要件形式を抽出し、当該不足要件形式に前記不足要件導出情報を適用して自然言語で記載された不足要件を生成する不足要件生成手段と、前記自然言語で記載された不足要件を前記自然言語の仕様書に追記する不足要件追記手段と、当該自然言語の仕様書を前記記述変換ルールに基づいて形式言語の仕様書に変換し形式言語の仕様書を生成する言語変換手段と、前記形式言語の仕様書を検証する仕様書検証手段と、を有することを特徴とする仕様書作成支援装置。請求項1にかかる仕様書作成支援装置であって、前記要件補間ルールの前記不足要件導出要件形式は、第一の自然言語で記載された不足要件導出要件形式と、第一の形式言語で記載された不足要件導出要件形式と、第二の自然言語で記載された不足要件導出要件形式と、第二の形式言語で記載された不足要件導出要件形式と、を有し、前記不足要件導出要件形式検索手段は、前記自然言語による仕様書に含まれる各要件について、当該要件の生成に用いられた自然言語による表現形式と対応する第一の自然言語で記載された不足要件導出要件形式が前記要件補間ルールに登録されているか検索し、前記不足要件導出情報生成手段は、前記不足要件導出要件形式検索手段によって抽出された前記第一の自然言語で記載された不足要件導出要件形式と対応づけられている第一の形式言語で記載された不足要件導出要件形式に、前記要件の作成に用いられた入力情報を適用し、第一の不足要件導出情報を生成し、前記不足要件導出要件形式検索手段は、前記要件補間ルールに基づき、当該不足要件導出要件形式検索手段によって抽出された前記第一の自然言語で記載された不足要件導出要件形式に対応する第二の自然言語で記載された不足要件導出要件形式を抽出し、当該第二の自然言語で記載された不足要件導出要件形式と対応する要件が、前記自然言語による仕様書に存在するか検索し、前記不足要件導出情報生成手段は、前記第二の自然言語で記載された不足要件導出要件形式と対応する要件が前記自然言語による仕様書に存在する場合に、前記第二の自然言語で記載された不足要件導出要件形式と前記第一の不足要件導出情報から、第二の不足要件導出情報を生成し、前記不足要件生成手段は、前記要件補間ルールに基づき、前記第一の自然言語で記載された不足要件導出要件形式及び前記第二の自然言語で記載された不足要件導出要件形式に対応する自然言語で記載された不足要件形式を抽出し、当該自然言語で記載された不足要件形式に前記第一の不足要件導出情報と前記第二の不足要件導出情報を適用して自然言語で記載された不足要件を生成することを特徴とする仕様書作成支援装置。請求項2にかかる仕様書作成支援装置であって、さらに、前記仕様書検証手段による前記形式言語の仕様書の検証に失敗した場合に、前記自然言語の仕様書または前記形式言語の仕様書の修正を受け付ける仕様書修正手段を有し、前記仕様書修正手段により前記自然言語の仕様書の修正を受け付けた場合は、前記仕様書作成支援装置は、修正された自然言語の仕様書に含まれる各要件について、自然言語で記載された不足要件を生成して当該修正された自然言語の仕様書に追記することを特徴とする仕様書作成支援装置。請求項3にかかる仕様書作成支援装置であって、前記記述変換ルールは、さらに、要件ごとに当該要件を一意に識別する変換識別子を有し、前記要件補間ルールの不足要件導出要件形式の各々は、さらに、当該不足要件導出要件形式と対応する要件の変換識別子を有し、前記不足要件導出要件形式検索手段は、前記自然言語の仕様書に記載された各々の要件について、当該要件の変換識別子と同じ変換識別子を有する不足要件導出要件形式が前記要件補間ルールに登録されているか検索することを特徴とする仕様書作成支援装置。形式言語で仕様書を生成する仕様書作成支援装置であって、形式言語で記載された第一の不足要件導出要件形式と、形式言語で記載された第二の不足要件導出要件形式と、形式言語で記載された不足要件形式と、を有する要件補間ルールと、形式言語による仕様書に記載された要件各々について、当該要件の形式と対応する第一の不足要件導出要件形式が前記要件補間ルールに登録されているか検索する第一不足要件導出要件形式検索手段と、前記第一不足要件導出要件形式検索手段によって抽出された前記第一の不足要件導出要件形式に前記要件を構成する入力情報を適用し、第一の不足要件導出情報を生成する第一不足要件導出情報生成手段と、前記要件補間ルールに基づき、前記第一不足要件導出要件形式検索手段によって抽出された前記第一の不足要件導出要件形式に対応する第二の不足要件導出要件形式を抽出し、当該第二の不足要件導出要件形式に対応する要件が前記形式言語による仕様書に存在するか検索する第二不足要件導出要件形式検索手段と、前記第二不足要件導出要件検索手段によって抽出された前記第二の不足要件導出要件形式に前記第一の不足要件導出情報を適用し、第二の不足要件導出情報を生成する第二不足要件導出情報生成手段と、前記要件補間ルールに基づき、前記第一の不足要件導出要件形式及び前記第二の不足要件導出要件形式に対応する不足要件形式を抽出し、当該不足要件形式に前記第一の不足要件導出情報と第二の不足要件導出情報を適用して、形式言語で記載された不足要件を生成する不足要件生成手段と、前記形式言語で記載された不足要件を前記形式言語の仕様書に追記する不足要件追記手段と、前記形式言語の仕様書を検証する仕様書検証手段と、を有することを特徴とする仕様書作成支援装置。自然言語から形式言語に変換して仕様書を作成する仕様書作成支援装置における方法であって、前記仕様書作成支援装置は、自然言語仕様作成部と、モデル変換部と、形式検証実行部と、要件ごとに、当該要件の自然言語による表現形式と、当該要件の形式言語による表現形式と、当該自然言語による表現形式に求められる入力情報の各々について当該入力情報の仕様書における参照元を示す入力参照元と、を有する記述変換ルールと、自然言語で記載された不足要件導出要件形式と形式言語で記載された不足要件導出要件形式とを有する不足要件導出要件形式と、自然言語で記載された不足要件形式と、を有する要件補間ルールと、を有し、前記自然言語仕様作成部が、前記記述変換ルールに基づき、一以上の自然言語による表現形式の候補を出力する自然言語形式出力ステップと、前記一以上の自然言語による表現形式の候補から一以上の自然言語による表現形式の選択を受け付ける自然言語表現受付ステップと、前記記述変換ルールに基づき、前記事前言語表現受付ステップが受け付けた前記一以上の自然言語による表現形式各々に対応する入力参照元を当該一以上の自然言語による表現形式に求められる入力情報の候補として出力する入力情報候補出力ステップと、前記入力情報の候補から前記一以上の自然言語による表現形式各々に対する入力情報の選択を受け付ける入力情報受付ステップと、選択された前記一以上の自然言語による表現形式と前記入力情報から、自然言語により表現された一以上の要件を生成し、当該自然言語により表現された一以上の要件を有する自然言語の仕様書を作成する自然言語仕様書作成ステップと、前記自然言語の仕様書に含まれる各要件について、当該要件の生成に用いられた自然言語による表現形式と対応する自然言語で記載された不足要件導出要件形式が前記要件補間ルールに登録されているか検索する不足要件導出要件形式検索ステップと、前記不足要件導出要件形式検索ステップによって抽出された自然言語で記載された不足要件導出要件形式と対応付けられている形式言語で記載された不足要件導出要件形式に前記要件の作成に用いられた入力情報を適用し、不足要件導出情報を生成する不足要件導出情報生成ステップと、前記要件補間ルールに基づき、前記不足要件導出要件形式検索ステップによって抽出された自然言語で記載された不足要件導出要件形式についての不足要件形式を抽出し、当該不足要件形式に前記不足要件導出情報を適用して自然言語で記載された不足要件を生成する不足要件生成ステップと、前記自然言語で記載された不足要件を前記自然言語の仕様書に追記する不足要件追記ステップと、を有し、前記モデル変換部が、当該自然言語の仕様書を前記記述変換ルールに基づいて形式言語の仕様書に変換し形式言語の仕様書を生成する言語変換ステップと、前記形式検証実行部が、前記形式言語の仕様書を検証する仕様書検証ステップと、を有することを特徴とする方法。請求項6にかかる方法であって、前記要件補間ルールの前記不足要件導出要件形式は、第一の自然言語で記載された不足要件導出要件形式と、第一の形式言語で記載された不足要件導出要件形式と、第二の自然言語で記載された不足要件導出要件形式と、第二の形式言語で記載された不足要件導出要件形式と、を有し、前記不足要件導出要件形式検索ステップは、前記自然言語による仕様書に含まれる各要件について、当該要件の生成に用いられた自然言語による表現形式と対応する第一の自然言語で記載された不足要件導出要件形式が前記要件補間ルールに登録されているか検索し、前記不足要件導出情報生成ステップは、前記不足要件導出要件形式検索ステップによって抽出された前記第一の自然言語で記載された不足要件導出要件形式と対応づけられている第一の形式言語で記載された不足要件導出要件形式に、前記要件の作成に用いられた入力情報を適用し、第一の不足要件導出情報を生成し、前記不足要件導出要件形式検索ステップは、前記要件補間ルールに基づき、当該不足要件導出要件形式検索ステップによって抽出された前記第一の自然言語で記載された不足要件導出要件形式に対応する第二の自然言語で記載された不足要件導出要件形式を抽出し、当該第二の自然言語で記載された不足要件導出要件形式と対応する要件が、前記自然言語による仕様書に存在するか検索し、前記不足要件導出情報生成ステップは、前記第二の自然言語で記載された不足要件導出要件形式と対応する要件が前記自然言語による仕様書に存在する場合に、前記第二の自然言語で記載された不足要件導出要件形式と前記第一の不足要件導出情報から、第二の不足要件導出情報を生成し、前記不足要件生成ステップは、前記要件補間ルールに基づき、前記第一の自然言語で記載された不足要件導出要件形式及び前記第二の自然言語で記載された不足要件導出要件形式に対応する自然言語で記載された不足要件形式を抽出し、当該自然言語で記載された不足要件形式に前記第一の不足要件導出情報と前記第二の不足要件導出情報を適用して自然言語で記載された不足要件を生成することを特徴とする方法。請求項7にかかる方法であって、さらに、前記仕様書検証ステップによる前記形式言語の仕様書の検証に失敗した場合に、前記自然言語の仕様書または前記形式言語の仕様書の修正を受け付ける仕様書修正ステップを有し、前記仕様書修正ステップにより前記自然言語の仕様書の修正を受け付けた場合は、前記方法は、修正された自然言語の仕様書に含まれる各要件について、自然言語で記載された不足要件を生成して当該修正された自然言語の仕様書に追記することを特徴とする方法。請求項8にかかる方法であって、前記記述変換ルールは、さらに、要件ごとに当該要件を一意に識別する変換識別子を有し、前記要件補間ルールの不足要件導出要件形式の各々は、さらに、当該不足要件導出要件形式と対応する要件の変換識別子を有し、前記不足要件導出要件形式検索ステップは、前記自然言語の仕様書に記載された各々の要件について、当該要件の変換識別子と同じ変換識別子を有する不足要件導出要件形式が前記要件補間ルールに登録されているか検索することを特徴とする方法。形式言語で仕様書を生成する仕様書作成支援装置における方法であって、前記仕様書作成支援装置は、形式言語仕様作成部と、形式検証実行部と、形式言語で記載された第一の不足要件導出要件形式と、形式言語で記載された第二の不足要件導出要件形式と、形式言語で記載された不足要件形式と、を有する要件補間ルールと、を有し、前記形式言語仕様作成部が、形式言語による仕様書に記載された要件各々について、当該要件の形式と対応する第一の不足要件導出要件形式が前記要件補間ルールに登録されているか検索する第一不足要件導出要件形式検索ステップと、前記第一不足要件導出要件形式検索ステップによって抽出された前記第一の不足要件導出要件形式に前記要件を構成する入力情報を適用し、第一の不足要件導出情報を生成する第一不足要件導出情報生成ステップと、前記要件補間ルールに基づき、前記第一不足要件導出要件形式検索ステップによって抽出された前記第一の不足要件導出要件形式に対応する第二の不足要件導出要件形式を抽出し、当該第二の不足要件導出要件形式に対応する要件が前記形式言語による仕様書に存在するか検索する第二不足要件導出要件形式検索ステップと、前記第二不足要件導出要件検索ステップによって抽出された前記第二の不足要件導出要件形式に前記第一の不足要件導出情報を適用し、第二の不足要件導出情報を生成する第二不足要件導出情報生成ステップと、前記要件補間ルールに基づき、前記第一の不足要件導出要件形式及び前記第二の不足要件導出要件形式に対応する不足要件形式を抽出し、当該不足要件形式に前記第一の不足要件導出情報と第二の不足要件導出情報を適用して、形式言語で記載された不足要件を生成する不足要件生成ステップと、前記形式言語で記載された不足要件を前記形式言語の仕様書に追記する不足要件追記ステップと、を有し、前記形式検証実行部が、前記形式言語の仕様書を検証する仕様書検証ステップと、を有することを特徴とする方法。従来技術では、自然言語仕様から形式言語仕様への変換規則を定めることによって、自然言語を用いて、形式検証技術に基づく曖昧さや誤りのない設計書の作成を支援することを目的としている。しかしながら、形式言語仕様の作成に当たっては、従来の自然言語による仕様作成と比較して、より厳密な仕様記述の作成が必要となる。そのため、従来の自然言語仕様では意識しなかった要件も明示的に記述することが必要となる。そこで、形式検証技術を用いた仕様作成に当たって、仕様内に記述された要件から不足している要件を生成することで、曖昧さや誤りのない仕様作成を支援することを目的とする。上記の課題に対し、本発明では、要件ごとに、当該要件の自然言語による表現形式と、当該要件の形式言語による表現形式と、当該自然言語による表現形式に求められる入力情報の各々について当該入力情報の仕様書における参照元を示す入力参照元と、を有する記述変換ルールと、自然言語で記載された不足要件導出要件形式と形式言語で記載された不足要件導出要件形式とを有する不足要件導出要件形式と、自然言語で記載された不足要件形式と、を有する要件補間ルール有し、前記記述変換ルールに基づき、一以上の自然言語による表現形式の候補を出力し、前記一以上の自然言語による表現形式の候補から一以上の自然言語による表現形式の選択を受け付け、前記記述変換ルールに基づき、前記事前言語表現受付手段が受け付けた前記一以上の自然言語による表現形式各々に対応する入力参照元を当該一以上の自然言語による表現形式に求められる入力情報の候補として出力し、前記入力情報の候補から前記一以上の自然言語による表現形式各々に対する入力情報の選択を受け付け、選択された前記一以上の自然言語による表現形式と前記入力情報から、自然言語により表現された一以上の要件を生成し、当該自然言語により表現された一以上の要件を有する自然言語の仕様書を作成し、前記自然言語の仕様書に含まれる各要件について、当該要件の生成に用いられた自然言語による表現形式と対応する自然言語で記載された不足要件導出要件形式が前記要件補間ルールに登録されているか検索し、抽出された自然言語で記載された不足要件導出要件形式と対応付けられている形式言語で記載された不足要件導出要件形式に前記要件の作成に用いられた入力情報を適用し、不足要件導出情報を生成し、前記要件補間ルールに基づき、抽出された自然言語で記載された不足要件導出要件形式についての不足要件形式を抽出し、当該不足要件形式に前記不足要件導出情報を適用して自然言語で記載された不足要件を生成し、前記自然言語で記載された不足要件を前記自然言語の仕様書に追記し、当該自然言語の仕様書を前記記述変換ルールに基づいて形式言語の仕様書に変換し形式言語の仕様書を生成し、前記形式言語の仕様書を検証することを特徴とする。形式検証技術を用いたソフトウェア仕様の作成に当たって、厳密な仕様作成を支援し、曖昧さや誤りのない仕様作成の支援が可能となる。図1は、本実施例の仕様作成支援装置100の構成図である。仕様作成支援装置100は、入力部101、表示部106、入出力制御部107、自然言語仕様作成部102、モデル変換部103、形式仕様作成部104、形式検証実行部105、及び、要件補間ルール格納データベース要件補間ルール格納DB120、自然言語仕様格納データベース自然言語仕様格納DB121、及び、記述変換ルール格納データベース記述変換ルール格納DB122、及び、形式仕様格納データベース形式仕様格納DB123を備える。また、自然言語仕様作成部は、設計書作成部108、要件補間部109、及び、要件記述部110を備える。ここで、自然言語仕様格納DB121は、自然言語仕様を格納するための格納領域であり、形式仕様格納DB113は、形式言語仕様を格納するための格納領域である。また、記述変換ルール格納DB112は、自然言語仕様作成のための記述ルールと作成された自然言語仕様と形式言語仕様とを相互に変換するための変換ルールを格納した格納領域であり、要件補間ルール格納DB110は、作成された自然言語仕様内で、不足している要件を補完するためのルールを格納した格納領域である。形式検証実行部105は、形式仕様格納DB123に格納された形式言語仕様を基に、形式言語の構文チェック、検証等を行う。また、モデル変換部103は、記述変換ルール格納DB122の変換ルールに従い、自然言語仕様格納DB121に格納された自然言語仕様を形式仕様言語への変換、又は、その逆変換を行うとともに、形式検証実行部105における検証結果を自然言語仕様格納DB121に反映する。自然言語仕様作成部102は設計書作成部108、要件補間部109、及び、要件記述部110とを含んで構成される。設計書作成部108は、自然言語仕様に基づく設計書を作成するための処理部であり、設計書作成部108は、要件記述部110と通信し、記述変換ルールに従い、入力部101からのユーザ入力を受付、自然言語による要件記述、及び、仕様作成を行う。さらに、設計書作成部108は、要件補間部109と通信し、作成された要件から不足している要件を生成する。なお、形式言語仕様作成部104は、直接形式言語仕様を作成するための処理部であり、形式仕様作成部104、形式仕様格納DB123、形式検証実行部105は、形式検証技術に関わる、仕様記述、及び、構文チェック、検証を行う、既存の形式検証技術の仕様作成支援ツール例えば、非特許文献1を用いて構成よい。本実施例によれば、ユーザは仕様作成支援装置100内の記述変換ルール格納DB122内に格納された記述変換ルールに格納された記述ルールに基づき自然言語仕様を作成することで、形式言語仕様への変換を行う。また、要件補間ルール格納DB120内に格納された要件補間ルールを用いることで、自然言語仕様内に記述された要件から不足している要件を生成する。これによって、ユーザに対し、形式言語仕様を利用した曖昧さや誤りのない仕様作成のための支援を行う。図2は、図1に示した仕様作成支援装置100を実現するハードウェア構成の一例を示している。図2の構成例では、仕様作成支援装置100は、CPUCentralProcessorUnit201、RAMRandomAccessMemory202、入力装置101、表示装置204、及び、外部記憶装置210がインターフェイス205を介して接続された、一般的な構成を有するコンピュータ電子計算機である。入力装置101は、例えば、キーボードやマウスなどであり、表示装置204は、表示用ディスプレイ、外部記憶装置210は、HDDHardDiskDriveなどである。CPU201は、RAM202上にロードしたプログラムを実行することで、図1に示す自然言語仕様作成部102、モデル変換部103、形式言語仕様作成部104、及び、形式検証実行部105をプロセスとして具現化する。また、インターフェイス205は、装置内の各構成要素間のデータを送受信する内部パスであり、外部記憶装置210には、各データベース、及び、自然言語仕様作成部102、モデル変換部103、形式言語仕様作成部104、及び、形式検証実行部105の実行プログラムが格納される。表示装置203は、自然言語仕様作成部102、形式言語仕様作成部104において、作成中の自然言語仕様、又は、形式言語仕様をディスプレイ等に表示する。以下、本実施例では、形式言語仕様としてモデル規範型仕様記述言語Event-Bを用いた場合を例として、設計書支援装置100について説明する。なお、以下ではEvent-Bを例として仕様作成支援装置100の具体的な構成について説明するが、本発明は、例えばB-methodなど、他のモデル規範型仕様記述言語でも同様に実現可能である。図3は、Event-Bを用いた場合の本実施例における自然言語仕様301と形式言語仕様320の対応関係を表している。形式言語Event-Bでは、形式言語仕様は、Context321、MACHINE323から構成される。Context321内には、形式言語仕様を作成するための集合331、定数に関する情報332が含まれ、MACHINE323には、システムの状態を表す変数333、及び、変数の満たすべき条件を示した不変条件334、変数の初期化339、及び、変数の状態変化の事前条件337、事後条件338を記述するイベント335が含まれる。図3に図示したごとく、第一の実施例では、形式言語仕様320に対応する自然言語仕様301は、集合一覧305、定数一覧306からなるモデリング情報302、変数一覧307、データ要件一覧308からなるデータ要件関連情報303、及び、ユースケース設計書304から構成される。ここでユースケース設計書304は、各ユースケースのユースケース名309、ユースケース概要310、パラメータ311、事前条件312、アクション313から構成される。なお、図3の矢印は、モデリング情報302、データ要件関連情報303、ユースケース設計書304が、形式言語仕様320内の対応する構成要素を表している。図3に示した設計書の構成、及び、名称は特に上記に限らなくてもよい。また、設計書の作成単位も、上記に限らず、例えば、モデリング情報302、及び、データ要件関連情報303を、ひとつの設計書としてまとめてもよい。また、設計書の記載内容は、上記以外の項目を含んで構成されてもよい。図4は、図3に示した自然言語仕様による仕様作成フローの概略を示している。そのフローは以下のとおりである。401:開始402:入力部101がユーザから記述変換ルール112に基づく入力を受け付け、自然言語作成部102の設計書作成部108、要件記述部111が、モデリング情報302を作成する。403:入力部101がユーザから記述変換ルール112に基づく入力を受け付け、自然言語作成部102の設計書作成部108、要件記述部111が、データ要件関連303を作成する。404:入力部101がユーザから記述変換ルール112に基づく入力を受け付け、自然言語作成部102の設計書作成部108、要件記述部111が、ユースケース設計書304を作成する。405:すべてのユースケース設計書を作成した場合にはステップ406へ。まだ作成するユースケース設計書がある場合にはステップ404に進む。406:自然言語作成部102の設計書作成部108、及び、要件補間部112が、要件補間ルール120に基づき作成した仕様内の要件から不足要件を生成し、設計書に反映する。407:ユーザが自然言語仕様作成部102から、モデル変換部103を呼び出し、モデル変換部103を用いて、自然言語作成部102で作成した自然言語仕様302を形式言語仕様320に変換する。408:仕様作成支援装置100が、形式検証実行部を用いて、ステップ407で生成した形式言語仕様320の構文チェック、検証を行い、その結果を自然言語仕様320に反映する。409:すべての要件が検証に成功した場合にはステップ411に進み、検証に失敗した要件があれば410に進む。410:ユーザが自然言語仕様作成部102を用いて、ステップ402、403、404と同様の作業を行い、自然言語仕様の修正を行う。411:終了なお、上記の作成フローでは、すべてのユースケース設計書が作成された後、ステップ406以降で、要件の補間ステップ406、形式言語仕様への変換ステップ407、形式言語仕様の検証ステップ408を行っているが、上記に限らず、例えば、各設計書の作成段階ごとにステップ406、407、408の処理を実行してもよい。また、ユーザが明示的にステップ406、407、408等の処理を呼び出すのではなく、ユーザの要件記述に合わせ、設計書作成部108が自動で呼び出すようにしてもよい。ステップ410における仕様の修正は、自然言語仕様作成部102ではなく、形式言語仕様作成部104を用いて、形式言語仕様320に対して直接行い、その結果を、モデル変換部103を用いて、自然言語仕様301に反映してもよい。上記処理では、自然言語仕様から形式言語仕様を全て作成することを想定した処理フローとなっているが、上記と異なっていてもよい。例えば、既存のシステム、或いは、複数のシステムで共通的に使われる項目がある場合には、モデリング情報302、或いは、データ要件関連情報303の一部を予め作成しておき、これらを用いて仕様作成を行ってもよい。図5は、本実施例における記述変換ルールDB122内に格納された記述変換ルールの一例を示している。図5に示したごとく、本実施例における記述変換ルールDB122は、記述変換ルールの識別子を表す変換ID501、自然言語仕様内での要件記述パターンを表した自然言語表現503、自然言語表現に対応する形式言語仕様内での要件記述パターンを表した形式言語表現504を含み構成される。また、各記述変換ルールには、変数、不変条件など、その記述変換ルールが利用可能な対象502、及び、各記述変換ルールを用いて要件インスタンスを生成する際に必要となる入力情報505が含まれる。本実施例の入力情報505の参照元506、508、及び、次に示す図6の不足要件導出要件602及び不足要件605の対象606、608、610では、自然言語仕様書301の集合一覧305を参照する場合はSSet、定数一覧306を参照する場合は、CConstant、変数一覧307を参照する場合はVVariables、データ要件一覧308を参照する場合はIInvariants、イベントのパラメータ311を参照する場合にはPParameter,事前条件312を参照する場合はWWhere、アクション313を参照する場合はAActionと略記している。なお、入力情報505の参照元506、508には、仕様記述のために宣言した集合一覧305、定数一覧306、変数一覧307、パラメータ311のいずれかから選択するため、S,C,V,Pのいずれかとなる。同様に、種別507,509は、入力情報の種別が要素の場合はEElement,集合の場合はSSetと略記している。なお、種別は、要素や集合だけでなく、例えば写像等、上記以外の種別を追加してもよい。また、例えばクラスや属性など、異なる観点で纏めてもよい。次に図6は、本実施例における要件補間ルールDB120内に格納された記述変換ルールの一例を示している。図6に示したごとく、要件補間ルールDB120は、要件補間ルールの識別子を表す補間ID601と、不足要件の記述パターンを記述した不足要件605と不足要件を生成するための条件仕様内の要件記述パターンを記述した不足要件導出要件602とからなる。不足要件導出要件602は、さらに基底要件603、従属要件604から構成される。なお、基底要件603、従属要件604は、不足要件導出要件602として、ひとつの列としてまとめてもよいが、本実施例では、不足要件の導出を容易にするため、基底要件603、従属要件604の二つの列に分けている。これは、仕様内から不足要件導出要件602を用いて不足要件の生成を行う際、全ての不足要件導出要件を纏めて検索する手間を低減するためである。不足要件の生成に当たっては、まず基底要件603を元に該当する不足要件の候補を探索し、該当する候補に対して、仕様内の要件記述から従属要件604を絞り込むことで、不足している要件の特定、生成を行う。以下に、図5、図6を用いた、要件記述部110による要件の記述処理、モデル変換部103による形式言語仕様への変換処理、及び、要件補間部109による不足要件の生成処理の処理フローについて説明する。なお、具体例は図10から図13を用いて後述する。図7は、本実施例における各設計書内への要件記述の処理フロー要件記述部110における処理フロー、図4ステップ402~ステップ404の処理の概略を示している。701:開始702:要件記述部110が、記述変換ルールDB122から、対象502に基づき、記述項目に応じた記述変換ルールを読み込み、読み込んだ記述変換ルールの一覧を表示する。703:表示した記述変換ルールの一覧からユーザが選択した記述変換ルールを入力部101が受け付け、要件記述部110に送る。704:要件記述部110が、受け付けた記述変換ルールから、対応する入力情報505を読み込む。705:入力情報がまだあればステップ705に、なければ711に進む。706:要件記述部110が、入力情報505から参照元情報を取得する。707:要件記述部110が、参照元506、508の記述に従い、入力情報の候補入力候補を取得する。708:要件記述部110が種別507、509を取得し、ステップ707の入力候補から該当する入力候補のみを取得する。709:ステップ708で取得した入力候補を一覧表示する。710:表示した入力候補の一覧からユーザが選択した入力候補選択を入力部101が受け付け要件記述部110に送り、ステップ705に進む。711:要件記述部110が、記述変換ルールの変換ID501,及び、ステップ710で取得した入力候補入力情報インスタンスと呼ぶを自然言語仕様格納DB121に要件インスタンスとして保管する。712:終了図3に示した例では、自然言語仕様301は、複数の設計書モデリング情報302、データ要件関連情報303、ユースケース設計書304から構成され、各設計書内の記載項目データ要件一覧308などが、形式言語仕様の各構成要素不変条件334などに対応する。上記の処理は、自然言語仕様301の各記載項目内に記述する要件を個別に作成するための処理フローであり、例えば、データ要件一覧308を記載する場合には、対象502の欄がデータ要件となっている記述変換ルールを一覧表示し、アクション313を記載する場合には、対象502がアクションとなっている記述変換ルールを一覧表示し、変数307を記載する場合には、対象502が変数となっている記述変換ルールを一覧表示するステップ702。そして、ユーザ選択を受け付けステップ703、選択された記述変換ルールを取得する。たとえば、図5の変換ID501がT11の記述変換ルールをユーザが選択した場合には、AはBを含むという記述変換ルールの入力情報A,Bに対し、入力情報インスタンスを生成するための処理ステップ705からステップ710を実行する。ステップ706、ステップ707では、T11の入力情報Aに関する参照元情報と種別情報を参照し、入力情報Aの入力候補を取得する。具体的には、T11の入力情報Aに関する参照情報はV変数一覧であるため変数一覧307から入力候補を取得する。そして、入力情報Aに関する種別がE要素であるため、ステップ708では、取得した入力候補から要素として宣言された変数を取得する。そして、取得された変数を入力情報Aの入力候補として一覧表示し、入力情報Aのユーザ選択を受け付けるステップ709、710。同様の処理ステップ705からステップ710を入力情報Bに対しても実施し、入力情報Bのユーザ選択を受け付ける。そして、ユーザが選択した入力情報A及び入力情報Bから入力情報インスタンスを作成し、変換ID501と入力情報インスタンスから要件インスタンスを生成する。生成された要件インスタンスは、設計書作成部108により自然言語仕様格納DB121内に保管されるステップ121。上記の処理フローでは、入力情報インスタンスを入力候補の中から選択する方法を示したが、集合一覧305、定数一覧306、変数一覧307、及び、パラメータ310は、システム内で用いる集合や定数、変数、或いは、ユースケース内で用いるパラメータを定義するための項目であるので、入力候補から受け付けるのではなく、ユーザからのテキスト入力を受付けるようにする。例えば、図5に示した変換ID501がT01,T02の記述変換ルールは、変数への記述変換テンプレートとなっている。このとき、自然言語表現503には、T01のBの要素のように、入力情報Aの情報がない。また、入力情報505のAに関して、参照元506、及び、種別507には―が記載されている。これは、入力情報Aについては、ユーザからのテキストによる自由入力を受け付け、その結果を用いて変数を宣言することを表している。また、T11の自然言語表現AはBを含むは、T12の自然言語表現と同じになっている。この場合、ユーザがT11、T12を明示的に指名するのではなく、自然言語表現から記述変換ルール候補を取得し、その後の入力情報インスタンスにおいて、ユーザから選択された入力情報インスタンスを基に変換IDを特定するようにしてもよい。このようにすることによって、ユーザは形式言語表現を意識することなく、自然言語表現による仕様記述が可能となる。また、図5に示した記述変換テンプレートでは、自然言語表現としてテキスト表現による記述変換ルールを記述したが、例えば、自然言語表現としてUMLのクラス図などを用いてもよい。次に、図7の処理によって作成された要件インスタンスにより構成された自然言語仕様301から、形式言語仕様320を生成するための処理図4ステップ407の処理を説明する。図3に示した如く、自然言語仕様301内のデータ要件一覧308等の各記載項目は、形式言語仕様320内の各構成要素に対応する。モデル変換部103の自然言語仕様301から形式言語仕様320への変換に当たっては、まず作成された各設計書モデリング情報、データ要件関連情報、ユースケース設計書の各記載項目から対応する形式言語仕様の各構成要素を生成し、各記載項目に記述された要件インスタンスを、形式言語表現に変換することによって、形式言語仕様320を生成する。図8は、モデル変換部103における、上記の各記載項目内に格納された要件インスタンスから形式言語表現に変換するための処理フローを示している。801:開始802:モデル変換部103が自然言語仕様格納DB121から要件インスタンスを取得する。803:モデル変換部103がステップ802で取得した要件インスタンスから、変換IDを取得する。804:ステップ802で取得した要件インスタンス内に入力情報インスタンスがまだある場合にはステップ805に、そうでない場合にはステップ806に進む。805:モデル変換部103が要件インスタンス内の入力情報インスタンスを取得する。806:モデル変換部103が記述変換ルールDB122から、ステップ803で取得した変換IDと一致する変換ID501を有する記述変換ルールを取得する。807:モデル変換部103が、ステップ806で取得した変換ID501を有する記述変換ルールの形式言語表現504にステップ805で取得した入力情報インスタンスを代入する。808:終了図7の要件インスタンスの処理フローで述べたとおり、各要件インスタンスは、変換ID、及び、入力情報インスタンスから構成される。また、図5に示した記述変換ルールの構成により、変換ID501から対応する形式言語表現504が定まるため、入力情報の実体値入情報インスタンスが与えられれば、形式言語表現への変換が可能である。従って、上記のステップ803による変換IDの取得、及び、ステップ805における入力情報インスタンスの取得、さらにステップ806による形式言語表現の取得によって、各要件インスタンスの形式言語仕様内での記述への変換ステップ807が可能となる。上記の変換処理を全ての要件インスタンスに対して実行することで、自然言語仕様301が形式言語仕様320に変換される。図9は、要件補間部109による、要件補間ルール格納DB120を用いた不足要件生成の処理フローを示している図4ステップ406の処理901:開始902:要件補間部109が、自然言語仕様格納DB121から要件インスタンスを取得する。903:要件補間部109が、要件補間ルールDB120の要件補間ルールを探索し、ステップ902で取得した要件インスタンスと一致する変換IDを有する基底要件603の要件補間ルールがあれば、ステップ904へ、なければステップ905に進む。904:要件補間部109が、ステップ902で取得した要件インスタンス、及び、ステップ903で取得した変換IDから基底要件603のインスタンスを作成する。905:要件補間部109が、ステップ903で取得した要件補間ルールの従属要件604を取得する。906:要件補間部109が、ステップ905で取得した従属要件の各々について、従属要件の有する変換IDと一致する変換IDを有する要件インスタンスがないか、自然言語仕様格納DB121内の要件インスタンスを探索する。全ての従属要件について、変換IDが一致する要件インスタンスがあれば、ステップ907へ、なければステップ910に進む。907:要件補間部109が、ステップ906で取得された要件インスタンスに対し、基底要件603のインスタンスを用いて、従属要件604のインスタンスの生成を試み、生成可能であればステップ908へ、そうでなければステップ910へ進む。908:要件補間部109が、ステップ903で取得した要件補間ルールの不足要件505を取得する。909:要件補間部109が、取得された不足要件605を用いて不足要件を生成する。910:終了ステップ902において取得された要件インスタンスに対し、ステップ903において要件補間ルールDB120内から変換IDが要件インスタンスと一致する基底要件603を探索する。基底要件603の要件に記述された変換IDと要件インスタンスの変換IDが一致する場合には、基底要件内のX,XX、Y、...に要件インスタンスの入力情報インスタンスを代入し、基底要件603のインスタンスを作成するステップ904。ここで、XはXXの部分集合であることを意味し、YはYYの部分集合であることを意味する。次に前記の基底要件603に対応する従属要件604を取得しステップ905、従属要件604の対象608が一致する要件インスタンスを抽出し、抽出した要件インスタンスについて、従属要件604内に記載された変換IDと一致する変換IDを持つ要件インスタンスの有無を検索するステップ906。全ての従属要件604について要件インスタンスがある場合には、従属要件のインスタンスの生成を試みるステップ907。このとき、X,XX,...が基底要件にある場合には、基底要件と同じ入力情報インスタンスを用いる。ない場合には、ステップ906で取得した入力情報インスタンスを用いる。上記の処理によって、従属要件604内のすべての要件について従属要件の要件インスタンスが生成できた場合には、不足要件605に記載された不足要件のインスタンスを生成し、設計書内の不足要件605の対象で指定された場所に不足要件を生成する。なお、不足要件にA’のようにシングルクォーテーションがついている場合には、その入力情報を新たに生成することを表すものとする。なお、上記により生成された不足要件は、設計書作成部108が自動で設計書への反映を行ってもよいし、不足要件候補として表示し、ユーザに反映の確認作業を行うようにしてもよい。また、前述のように設計書への自動反映を行う場合には、設計書への直接的な反映を行わず設計書上には表示せず、非表示要件として自然言語仕様格納DB121内に格納し、モデル変換部103内で形式言語仕様へ変換するようにしてもよい。このようにすることによって、形式言語仕様に精通していないユーザに、形式検証固有の冗長な表現を意識させることなく設計書の作成を支援することができ、設計書を見やすくすることができる。上記の処理によって生成された不足要件が、ひとつでない場合には、例えば不足要件候補として一覧表示し、ユーザからの入力を受け付けることにより、不足要件を各設計書の該当箇所に反映するようにすればよい。また、複数の不足要件が表示される場合には、あらかじめ要件補間ルールDB120ないに優先度欄を別途設け、優先度欄に応じて優先順位の高い要件から順に不足要件を表示するようにしてもよい。以下、図10から図13を用いて、図7,8,9の処理について説明する。図10は、本実施例によって作成された設計書の一例を示している。図10内のデータ要件関連情報1000は、図3内のデータ要件関連情報303の一例であり、記述変換ルールDB122を用いて変数一覧1001、及び、データ要件一覧1002が記載されている。また、図10内のユースケース設計書1010は、図3内のユースケース設計書304の一例であり、データ要件関連情報1000と同様、記述変換ルールDB122を用いてユースケース名1011、パラメータ1013、事前条件1014、アクション1015が記載されている。さらに、ユースケース概要1012は、ユースケースの概要を説明する欄であり、形式言語仕様への変換が不要な自由記述欄である。なお、図10の検証結果欄1020は、形式言語仕様320に変換し、形式検証実行部105による仕様検証証明責務の生成とその検証を行った結果、モデル変換部103が、その結果を表示する欄である。図10の場合、仕様検証の結果、全ての登録帳票は帳票フォルダに割り当てられるという要件を満たしていないことを意味する。図11は、図10のデータ要件関連情報1000、及び、ユースケース設計書1010の自然言語仕様格納DB121内でのデータ表現を部分的に表した例である。図11に示したとおり、自然言語仕様格納DB121は、図10に示した設計書をそのまま保管する必要はない。図11の例では、自然言語仕様格納DB121は、XMLeXtensibleMarkupLanguageを用いて各設計書の情報を変換IDと入力情報インスタンスから構成されている。図10のデータ要件関連情報1000は、図11のデータ要件関連情報要素1101から構成されるXMLデータとして、変数一覧を表す変数一覧要素1103、データ要件一覧を表すデータ要件一覧要素1104を含み記述される。また、ユースケース設計書1010は、ユースケース設計書要素1102から構成されるXMLデータとして、ユースケース名要素1105、パラメータ要素1107、事前条件要素1108、アクション要素1109から構成される。なお、補足情報要素1106は、形式言語仕様に変換する必要のない情報を記載する欄であり、図11にはユースケースの概要を説明する概要要素概要1012、ユースケース概要310に対応を含む。図11の例では、各要件要素1120~1124は、各要件インスタンスを表しており、変換ID要件要素のID属性と入力情報インスタンス要件要素のA、B、...子要素を含み構成される。変換ID、及び、入力情報インスタンスが自然言語仕様格納DB121内に格納されることにより、図8に示した処理フローにより、各要件インスタンスを形式言語表現に変換することが可能である。また、変換ID,及び、入力情報インスタンスから、図5に示した表を用いることによって、図11の自然言語仕様格納DB121内の情報から、図10に示した自然言語仕様を復元することができる。例えば、要件要素1124は、その属性としてid=T44が格納されており、子要素A,Bにそれぞれ、新規帳票、登録済帳票が格納されている。図5より、変換IDがT44の自然言語表現は、AをBに追加するであり、子要素A,Bの入力情報インスタンスより、要件インスタンスの自然言語表現が新規帳票を登録済帳票に追加するとなることが分かる。同様にして、形式言語表現はB:=B∪{A}であることから、登録済帳票:=登録済帳票∪{新規帳票}となることが分かる変換結果は、後述する図13の要件41311のact1を参照。なお、図10、図11の例では、記述変換ルールに基づき、各設計書を作成し、自然言語仕様格納DB121に格納した例を示した。図10の設計書の作成に当たって、記述変換ルールにない要件を記述できるようにしてもよい。この場合には、例えば、対応する形式言語表現も合わせて入力できるようにし、自然言語表現に対応する形式言語表現が分かるようにすることが望ましい。また、図11の自然言語仕様320では、自由記述に対して入力された自然言語表現、及び、形式言語表現を、自由記述を表す特殊な変換ID例えば、T9999などをあらかじめ定めておき、子要素として自然言語表現、及び、形式言語表現を記述するための要素を定義することによって、自由記述による自然言語表現、及び、形式言語表現を格納するようにすればよい。なお、自由記述した要件に対して、必ずしも形式言語表現への変換が不要な要件例えば補足情報などは、子要素として形式言語表現を含める必要はない。また、図10の自然言語仕様301の表示に当たっては、例えば各要件の形式言語表現との対応が分かるよう、記述変換ルール格納DB122を用いて変換後の形式言語表現をポップアップ表示する自由記述の場合には、形式言語表現を記述するための要素を用いればよい。また、対応する形式言語表現がない場合には、例えば文字や背景色を変更するなどして、対応する形式言語表現がないことを明示してもよい。図11では、自然言語仕様301の一実現例として、XMLによるデータ表現を用いたが、これと異なっていてもよい。また、XMLを用いた場合でも、要素名やXMLの構造は、必ずしも図11に示した限りでなくてもよい。図12は、図10、図11に示した自然言語仕様から、図6、及び、図9に示した要件補間ルール格納DB120を用いた不足要件の生成処理に基づき、不足要件を補間した結果を表している。図12内の要件1、2が追加された不足要件を表している。要件1の生成は、図9の処理フローによって、以下により生成される。まず、ステップ902の処理によって、データ要件一覧の要件全ての登録済み帳票は帳票フォルダに割当てられる。について要件インスタンスを取得する。この要件インスタンスは、図11の要件要素1121に示すように、要件id変換IDがT13である。次に、ステップ903の処理により、変換IDがT13である補間IDA11の要件補間ルールが取得され、要件インスタンスの入力情報インスタンスA=登録済帳票、B=帳票フォルダに基づきX=登録済帳票、Y=帳票フォルダを代入することにより、基底要件603のインスタンスが生成されるステップ904。さらに、ステップ905により、対応する従属要件604から要件が取得され、ステップ906、ステップ907の処理により、変換IDがT01である要件インスタンスを取得する。この場合、図11の変数一覧要素1120が示すように、取得した要件インスタンスの入力情報インスタンスが登録済帳票、帳票フォルダであるため、従属要件604ではX=登録済帳票、XX=帳票全体、Y=帳票フォルダYY=フォルダ全体となり、従属要件604のインスタンスが生成可能である。以上の処理から、ステップ908、ステップ909によって、対応する不足要件の不足要件T02:BからCへの関係のインスタンス登録済帳票to帳票フォルダが生成される。生成された要件は、対象欄と対応する設計書の該当箇所変数一覧に追加される要件11201。要件2も同様にして、ユースケース設計書1010内のアクションに記載された要件、新規帳票を登録済帳票に追加する。変換ID:T44登録先フォルダを帳票フォルダに追加する。変換ID:T44から、補間IDがA23となる基底要件が選択されステップ901~ステップ904、従属要件の検索、インスタンスの生成ステップ905~907を通して、要件21202が生成されるステップ908~ステップ910。図13は、図12に示した設計書から、形式言語仕様Event-Bによる仕様記述の生成結果を示した例である。設計書作成部108を用いてユーザが作成した各設計書は、自然言語格納DB121内に保管される。モデル変換部103によって、図8に示した処理フローにより、個々の要件が記述変換ルールに基づき形式言語仕様に変換される本実施例では、前述したとおり、個々の要件インスタンスは、変換IDと入力情報インスタンスの情報を含み構成されるため、これの情報から形式言語表現への変換が可能である。さらに、モデル変換部103は、形式言語表現に変換された各要件を、形式言語本例では、Event-Bの構文規則にのっとり、該当部分に記述する。これによって、ユーザが作成した自然言語仕様に対応する形式言語仕様が作成される。なお、図13は、図5、図6に示した記述変換ルール、及び、要件補間ルールの例に基づき生成された形式言語仕様の例を示しており、異なる記述変換ルール、要件補間ルールを用いた場合には、必ずしも図13のような形式言語仕様が生成されるとは限らない。記述変換ルール格納DB122内に格納する記述変換ルールは、形式言語仕様に誤りなく変換でき、かつ、設計書内で検証したい性質に合わせて、適切な記述変換ルールを格納することが望ましい。また、要件補間ルール格納DB120内に格納する要件補間ルールは記述変換ルールに合わせて、形式言語仕様に変換された際に誤りのない仕様を作成するための、不足要件、あるいは、不足要件候補が生成されるように、適切な情報を格納することが望ましい。第一の実施例では、ユーザは、あらかじめ用意された記述変換ルールを用いて、自然言語仕様により設計書の作成を行う。また、生成された設計書に対して不足要件の生成を行い、作成された設計書から形式言語仕様への変換を行う。これによって、形式検証技術に精通していないユーザが、形式検証技術に基づき、曖昧さや誤りのない設計書の作成を支援する方法を述べた。第二の実施例では、不足要件の導出を形式言語仕様上で行う方法を述べる。これによって、形式言語による仕様作成が可能なユーザに対しても、形式言語仕様作成の過程で忘れがちな要件や従属的に導かれる追加要件の記述支援を行う。これによって、直接形式言語仕様を作成する場合の支援を行う。図14は、第二の実施例における設計書作成支援装置100の最小構成を示す図である。第二の実施例では、第一の実施例と異なり、形式言語仕様上で不足要件の生成を行う。そのため、自然言語仕様の作成にかかわる処理部自然言語仕様作成部102、モデル変換部103、及び、格納領域自然言語仕様格納DB121、記述変換ルール格納DB122はなくてもよい。ただし、図14の構成に、第一の実施例の構成を含めてもよい。この場合、不足要件の補間は形式言語仕様上で行うため、図1の要件補間部109、要件補間ルール格納DB120は、なくてもよい。第二の実施例では、形式言語仕様上で不足要件の生成を行うため、形式言語仕様作成部104が形式仕様記述部104a、要件補間部112aから構成される。ここで、形式言語仕様記述部104aは、形式言語による仕様作成を直接行うための処理部であり、形式言語のための作成支援ソフトウェア例えば、非特許文献1を用いてよい。前述の通り、第二の実施例における要件補間部112aは、ユーザにより作成された形式言語仕様から、要件補間ルール格納DB120a内に格納された要件補間ルールに基づき不足要件の生成を行う。図15は、第二の実施例における要件補間ルール格納DB120a内の構成を表す一例である。図15に示したとおり、要件補間ルール格納DB120aは、第一の実施例図6の構成と同様、補間ID601a、基底条件603a、前提条件604a、及び、従属条件605aから構成される。ただし、第二の実施例における要件補間ルール格納DB120aは、第一の実施例図6と異なり、基底要件603a、従属要件604a、不足要件605a内に格納される要件補間ルールは、形式言語表現が直接記述される。これは、第一の実施例では、自然言語仕様を形式言語仕様に変換し、自然言語仕様上で不足要件の生成を行っていたのに対し、第二の実施例では、形式言語仕様上で直接不足要件の補間を行うため、自然言語表現から形式言語表現への変換が必要ないためである。不足要件の生成処理は、第一の実施例における不足要件の生成処理図9と同様にして生成することが可能である。ただし、第一の実施例と第二の実施例では、以下の点が異なる。前述のとおり、第一の実施例では、自然言語表現から形式言語表現への変換処理に基づき、不足要件の生成を行う。このため、第一の実施例では、記述変換ルールの変換IDを用いて、自然言語仕様から基底要件、従属要件の探索を行い、その結果から、記述変換ルールに基づき、不足要件の生成を行う生成される不足要件は、変換IDと入力情報インスタンスによって表現される。一方、第二の実施例では、形式言語仕様上で不足要件の生成を行うため、その要件補間ルール格納DB120a内には、基底要件603a、従属要件604a、不足要件605aには、形式言語表現で直接記載される。そのため、例えば、ステップ903、ステップ906における変換IDによる要件インスタンスの検索は、形式表現上で記載された要件間の一致、不一致を検索する。また、その他、基底要件、従属要件等のインスタンスの生成は、形式言語表現でのインスタンスを直接生成する。図13に示した形式言語仕様において、要件3、要件4がユーザによって作成されていた場合には、図9の処理フローと図15の要件補間ルール格納DB120aを用いて、第一の実施例の要件21202図12と同様、以下のように要件5が生成される。まず、要件補間部112aによって、アクション内の要件41311と基底要件603aから、補間ID601aがA23の基底要件が選択されステップ902~903、XX=登録済帳票、X=新規帳票、YY=帳票フォルダ、Y=登録先フォルダとして、基底要件のインスタンスが生成されるステップ904。次に、対応する従属要件を取得しステップ905、従属用件に対応する要件として要件31310が存在しステップ906、基底要件のインスタンスから従属要件の対応するインスタンスが生成されるステップ907。そして、対応する不足要件の要件補間ルールを取得しステップ908、不足要件のインスタンスとして、登録済帳票to帳票フォルダ登録済帳票to帳票フォルダ登録済帳票∪新規帳票帳票フォルダが生成されるステップ910。なお、前述の通り、第二の実施例では、形式言語仕様上での直接要件の補間を行うため、図14の構成図では、自然言語仕様の作成にかかわる処理部自然言語仕様作成部102、モデル変換部103、及び、格納領域自然言語仕様格納DB121、記述変換ルール格納DB122は含まれていないが、これらを含む構成であってもよい。この場合、第二の実施例に基づき生成された不足要件、あるいは、形式仕様記述部104aによって作成された各要件は、記述変換ルール格納DB122内の形式言語表現を元に、変換ID,及び、入力情報インスタンスを特定し、対応する自然言語表現に変換すればよい。記述変換ルール格納DB122に複数の形式言語表現が該当する場合には、記述変換ルールDB122内にあらかじめ優先度を設けておき、優先度に基づき、自然言語表現を決定する。あるいは、対応する複数の自然言語表現を優先度に基づき、一覧表示し、ユーザ選択により決定するようにしてもよい。また、記述変換ルール格納DB122に該当する形式言語表現がない場合には、ユーザに対応する自然言語表現を直接記述させるようにしてもよい。このような実施例の実現方法は、仕様作成支援装置100を形式検証に精通していないユーザに設計書の基本部分を作成し、形式検証による検証、修正を形式検証の専門家が行う、などの利用の際に有用である。"