(57)【要約】【課題】ソフトウェアの設計情報に含まれる式に、要件が明示的に定義されていない変数が出現する場合であっても、該式を、出現する各変数に対する要件を適切に反映した、形式言語による式として表現する技術を提供すること。【解決手段】ソフトウェアの設計情報における式（入力式）の情報および入力式における属性値が確定された変数の情報から、属性値が確定されていない変数（補間対象変数）の属性値を確定する規則を表す補間規則を用いて、処理対象の入力式における補間対象変数の属性値を確定する補間部１１と、入力式から、入力式に含まれる変数の属性値を考慮して、形式言語で記された出力式を生成する規則を表す生成規則を用いて、処理対象の入力式から出力式を生成する生成部１２と、を備える。【選択図】      図１
2015204028.tif 000002
【特許請求の範囲】
【請求項１】
ソフトウェアの設計情報における式（入力式）の情報および前記入力式における属性値が確定された変数の情報から、属性値が確定されていない変数（補間対象変数）の属性値を確定する規則を表す補間規則を用いて、処理対象の前記入力式における前記補間対象変数の属性値を確定する補間部と、
前記入力式から、前記入力式に含まれる変数の前記属性値を考慮して、形式言語で記された出力式を生成する規則を表す生成規則を用いて、前記処理対象の入力式から前記出力式を生成する生成部と、
を備えた情報処理装置。
【請求項２】
前記補間部は、前記補間規則として、前記補間対象変数および属性値が確定された他の変数の関係性に関する条件と、前記他の変数の属性値に基づき前記補間対象変数の属性値を補間する処理内容を表す補間処理内容とを対応付けた情報を用いて、前記処理対象の入力式における前記補間対象変数が適合する前記条件に対応付けられた前記補間処理内容にしたがって、前記属性値を確定することを特徴とする請求項１に記載の情報処理装置。
【請求項３】
前記生成部は、前記生成規則として、前記入力式の形式（入力式形式）と、前記入力式に出現する変数の属性値に関する条件と、前記出力式の形式（出力式形式）とを対応付けた情報を用いて、前記処理対象の入力式の形式が適合する前記入力式形式、および、前記処理対象の入力式に出現する変数の属性値が適合する前記条件に対応付けられた前記出力式形式にしたがって、前記出力式を生成することを特徴とする請求項１または請求項２に記載の情報処理装置。
【請求項４】
ソフトウェアの設計情報における式（入力式）の情報および前記入力式における属性値が確定された変数の情報から、属性値が確定されていない変数（補間対象変数）の属性値を確定する規則を表す補間規則を用いて、処理対象の前記入力式における前記補間対象変数の属性値を確定し、
前記入力式から、前記入力式に含まれる変数の前記属性値を考慮して、形式言語で記された出力式を生成する規則を表す生成規則を用いて、前記処理対象の入力式から前記出力式を生成する、情報処理方法。
【請求項５】
ソフトウェアの設計情報における式（入力式）の情報および前記入力式における属性値が確定された変数の情報から、属性値が確定されていない変数（補間対象変数）の属性値を確定する規則を表す補間規則を用いて、処理対象の前記入力式における前記補間対象変数の属性値を確定する補間ステップと、
前記入力式から、前記入力式に含まれる変数の前記属性値を考慮して、形式言語で記された出力式を生成する規則を表す生成規則を用いて、前記処理対象の入力式から前記出力式を生成する生成ステップと、
をコンピュータ装置に実行させるコンピュータ・プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、ソフトウェアの設計情報の形式検証を支援する技術に関する。
【背景技術】
【０００２】
ソフトウェアの設計情報の形式検証を支援する技術が知られている。形式検証は、形式言語を用いてソフトウェアの設計情報を表現することにより、設計情報の検証を行う手法である。
【０００３】
このような形式検証の支援に関連する技術が、特許文献１に記載されている。この関連技術は、集合論や一階述語論理にもとづく形式言語を用いてソフトウェアの設計情報を式として表現し、要件補間ルールに記載された形式言語による式と照合して、設計情報としては明示されていない要件を補間する。
【０００４】
また、このような形式検証の支援に関連する他の技術が、特許文献２に記載されている。この関連技術は、形式的手法の記法で記された実行可能なシステム仕様情報を用いて、システムに対する試験仕様を作成する。具体的には、この関連技術は、システム仕様情報に定義された条件に基づいて、各変数がとり得る値を特定し、各変数の値の組み合わせをシステムの状態とする。そして、この関連技術は、システムのある状態から実行可能な機能の実行を繰り返して状態の探索を行い、状態遷移に基づき得られる機能の系列を、試験項目として作成する。
【先行技術文献】
【特許文献】
【０００５】
【特許文献１】特開２０１３−８４０２３号公報
【特許文献２】特開２０１１−２４８５８１号公報
【発明の概要】
【発明が解決しようとする課題】
【０００６】
しかしながら、特許文献１に記載された関連技術には、以下の問題がある。
【０００７】
それは、ソフトウェアの設計情報としては明示されない要件には、形式言語で表現した式の照合からは補間できないものがあるという点である。例えば、文字列変数の値が空文字列であるかどうかによって、形式言語における表現が異なる場合がある。この場合、文字列変数の値が空文字列になりうるかどうかが要件として必要となる。同様に、変数が集合であるか集合の要素であるかによって、形式言語における表現が異なる場合がある。この場合、変数が集合であるか集合の要素であるかが要件として必要となる。このように、ソフトウェアの設計情報を形式言語で表現するためには、設計情報に含まれる式に出現する個々の変数に対する要件が、形式言語によって表現するよりも前にまず必要となる。
【０００８】
このため、設計情報において変数に対する要件が明示的に定義されていない場合、形式言語での表現が適切でなくなる。しかしながら、そのような変数に対する明示的に定義されていない要件を補間すべきかどうかは、特許文献１に記載された関連技術による形式言語で表現された式の照合では、判断できない。
【０００９】
また、特許文献２に記載された関連技術では、システム仕様情報において各変数がとりうる値を、システム仕様情報に定義された条件に基づいて特定している。しかしながら、特許文献２には、各変数がとりうる値が、システム仕様情報において明示的に定義されていない場合に、とりうる値をどのように特定するかについては、記載も示唆もない。
【００１０】
本発明は、上述の課題を解決するためになされたもので、ソフトウェアの設計情報に含まれる式に、要件が明示的に定義されていない変数が出現する場合であっても、該式を、出現する各変数に対する要件を適切に反映した、形式言語による式として表現する技術を提供することを目的とする。
【課題を解決するための手段】
【００１１】
本発明の情報処理装置は、ソフトウェアの設計情報における式（入力式）の情報および前記入力式における属性値が確定された変数の情報から、属性値が確定されていない変数（補間対象変数）の属性値を確定する規則を表す補間規則を用いて、処理対象の前記入力式における前記補間対象変数の属性値を確定する補間部と、前記入力式から、前記入力式に含まれる変数の前記属性値を考慮して、形式言語で記された出力式を生成する規則を表す生成規則を用いて、前記処理対象の入力式から前記出力式を生成する生成部と、を備える。
【００１２】
また、本発明の情報処理方法は、ソフトウェアの設計情報における式（入力式）の情報および前記入力式における属性値が確定された変数の情報から、属性値が確定されていない変数（補間対象変数）の属性値を確定する規則を表す補間規則を用いて、処理対象の前記入力式における前記補間対象変数の属性値を確定し、前記入力式から、前記入力式に含まれる変数の前記属性値を考慮して、形式言語で記された出力式を生成する規則を表す生成規則を用いて、前記処理対象の入力式から前記出力式を生成する。
【００１３】
また、本発明のコンピュータ・プログラムは、ソフトウェアの設計情報における式（入力式）の情報および前記入力式における属性値が確定された変数の情報から、属性値が確定されていない変数（補間対象変数）の属性値を確定する規則を表す補間規則を用いて、処理対象の前記入力式における前記補間対象変数の属性値を確定する補間ステップと、前記入力式から、前記入力式に含まれる変数の前記属性値を考慮して、形式言語で記された出力式を生成する規則を表す生成規則を用いて、前記処理対象の入力式から前記出力式を生成する生成ステップと、をコンピュータ装置に実行させる。
【発明の効果】
【００１４】
本発明は、ソフトウェアの設計情報に含まれる式に、要件が明示的に定義されていない変数が出現する場合であっても、該式を、出現する各変数に対する要件を適切に反映した、形式言語による式として表現する技術を提供することができる。
【図面の簡単な説明】
【００１５】
【図１】本発明の実施の形態としての情報処理装置の機能ブロック図である。
【図２】本発明の実施の形態としての情報処理装置のハードウェア構成図である。
【図３】本発明の実施の形態における入力式情報の一例を示す図である。
【図４】本発明の実施の形態における基本変数情報の一例を示す図である。
【図５】本発明の実施の形態における補間対象変数情報の一例を示す図である。
【図６】本発明の実施の形態における補間規則情報の一例を示す図である。
【図７】本発明の実施の形態における生成規則情報の一例を示す図である。
【図８】本発明の実施の形態としての情報処理装置の動作を説明するフローチャートである。
【図９】本発明の実施の形態において属性値が補間された補間対象変数情報の一例を示す図である。
【図１０】本発明の実施の形態によって生成される出力式情報の一例を示す図である。
【発明を実施するための形態】
【００１６】
以下、本発明の実施の形態について、図面を参照して詳細に説明する。
【００１７】
本発明の実施の形態としての情報処理装置１の機能ブロック構成を図１に示す。図１において、情報処理装置１は、補間部１１と、生成部１２とを備える。
【００１８】
補間部１１は、処理対象の入力式に出現する補間対象変数について、補間規則にしたがって、その属性値を確定する。ここで、処理対象の入力式とは、検証対象となるソフトウェアの設計情報に含まれる式である。また、補間規則とは、入力式の情報および入力式において属性値が確定されている変数の情報に基づいて、補間対象変数の属性値を確定する規則を表す。ここで、補間対象変数とは、前述の入力式において属性値が確定されていない変数である。また、入力式において属性値が確定されている変数とは、設計情報において属性値が明示されている変数（基本変数）であってもよいし、補間部１１の処理によって属性値が確定された他の補間対象変数であってもよい。なお、変数の属性値は、その変数に対する要件を表す。
【００１９】
例えば、補間規則は、補間対象変数および属性値が確定された他の変数の関係性に関する条件と、そのような他の変数の属性値に基づき補間対象変数の属性値を補間する処理内容（補間処理内容）とを対応付けた情報であってもよい。
【００２０】
具体的には、補間部１１は、基本変数およびその属性値を表す基本変数情報と、基本変数および属性値が確定していない変数とを用いた入力式の情報である入力式情報と、補間規則とを読み込む。そして、補間部１１は、入力式情報から基本変数以外の変数を補間対象変数として抽出する。さらに、補間部１１は、抽出した補間対象変数に対して適用可能な補間規則を適用することにより、補間対象変数の属性値を確定する。例えば、補間部１１は、その補間対象変数および属性値が確定された他の変数の関係性が適合する条件を有する補間規則を検索し、検索した補間規則の示す補間処理内容にしたがって、その補間対象変数の属性値を確定すればよい。以降、補間対象変数の属性値を確定することを、属性値を補間するとも記載する。そして、補間部１１は、補間対象変数および補間した属性値を表す補間対象変数情報を生成する。
【００２１】
生成部１２は、処理対象の入力式について、生成規則にしたがって、出力式を生成する。ここで、生成規則とは、上述の入力式から、入力式に出現する変数の属性値を考慮して、形式言語で記された出力式を生成する規則を表す。例えば、生成規則は、入力式の形式（入力式形式）と、入力式に出現する変数の属性値に関する条件と、出力式の形式（出力式形式）とを対応付けた情報であってもよい。
【００２２】
具体的には、生成部１２は、入力式を表す入力式情報と、基本変数情報と、補間部１１によって生成された補間対象変数情報と、生成規則とを読み込む。そして、生成部１２は、入力式情報の示す入力式に対して適用可能な生成規則を適用することにより、その入力式を変換した出力式を表す出力式情報を生成する。
【００２３】
ここで、情報処理装置１のハードウェア構成の一例を図２に示す。図２に示すように、情報処理装置１は、ＣＰＵ（Central Processing Unit）１００１と、ＲＡＭ（Random Access Memory）１００２と、ＲＯＭ（Read Only Memory）１００３と、ストレージ１００４と、ネットワークインタフェース１００５と、入力装置１００６と、出力装置１００７とを備えたコンピュータ装置によって構成可能である。
【００２４】
ＣＰＵ１００１は、演算制御用のプロセッサである。図２には、１つのＣＰＵ１００１を示しているが、情報処理装置１を構成するコンピュータ装置が備えるプロセッサの数を限定するものではない。ＣＰＵ１００１は、複数のプロセッサによって構成されていてもよいし、画像処理用のＧＰＵ（Graphics Processing Unit）を含んでいてもよい。ＣＰＵ１００１は、ＲＯＭ１００３またはストレージ１００４に格納されたコンピュータ・プログラムおよび各種データをＲＡＭ１００２に読み込んで実行する。
【００２５】
ＲＡＭ１００２は、ＣＰＵ１００１によって一時記憶のワークエリアとして使用されるランダムアクセスメモリである。また、ＲＡＭ１００２には、図２に示すように、本実施形態の実現に必要な以下のデータを記憶する領域が確保されている。
【００２６】
入力式情報は、検証対象となるソフトウェアの設計情報に含まれる入力式を表す情報である。例えば、入力式情報は、図３に示すように、ある変数の値を複数の変数あるいは定数の値から導出する代入式、複数の変数あるいは定数の間で値の関係を調べる比較式等であってもよい。また、例えば、入力式情報は、検証対象のソフトウェアによって実行される順番どおりに入力式を含んでいてもよい。なお、図３の詳細については後述する。
【００２７】
基本変数情報は、上述のように、検証対象となるソフトウェアの設計情報に含まれる入力式において属性値が明示された変数を表す情報である。例えば、基本変数情報は、図４に示すように、属性が明示された変数の変数名および属性値の組からなる情報であってもよい。なお、図４の詳細については後述する。
【００２８】
補間対象変数情報は、上述のように、検証対象となるソフトウェアの設計情報に含まれる入力式において属性値が明示されていない変数を表す情報である。例えば、補間対象変数情報は、図５に示すように、入力式情報の示す入力式に出現する変数のうち、基本変数情報に含まれない変数についての変数名および属性値の組からなる情報であってもよい。なお、補間対象変数情報の変数は、当初は属性値が決まっていない。補間部１１による処理の過程で属性値が定まる。図５の詳細については後述する。
【００２９】
補間規則情報は、上述の補間規則を表す情報であり、あらかじめ定められている。例えば、補間規則情報は、図６に示すように、補間対象変数および属性値が確定された他の変数の関係性に関する適用条件と、そのような他の変数の属性値に基づき補間対象変数の属性値を補間する補間処理内容とからなる情報であってもよい。なお、図６の詳細については後述する。
【００３０】
生成規則情報は、上述の生成規則を表す情報であり、あらかじめ定められている。例えば、生成規則情報は、入力式形式と、入力式に出現する変数の属性値に関する適用条件と、出力式形式とを対応付けた情報であってもよい。なお、図７の詳細については後述する。
【００３１】
出力式情報は、形式言語で表現された出力式を表す情報である。
【００３２】
ストレージ１００４には、図２に示すように、以下のコンピュータ・プログラムが格納される。
【００３３】
情報処理装置制御プログラムは、情報処理装置１の全体を制御する制御プログラムである。
【００３４】
補間モジュールは、情報処理装置制御プログラムにおいて、入力式から補間対象変数を抽出し、補間規則を用いて補間対象変数の属性値を決定するアルゴリズム（図８におけるステップＳ１からＳ６まで）を表す実行可能な情報である。
【００３５】
生成モジュールは、情報処理装置制御プログラムにおいて、生成規則にしたがって入力式から出力式を生成するアルゴリズム（図８のステップＳ７からＳ１０まで）を表す実行可能な情報である。なお、図８の詳細については後述する。
【００３６】
また、ストレージ１００４には、図２に示すように、以下の各領域にデータが格納される。補間規則格納領域には、ＲＡＭ１００２に読み込まれる補間規則情報が格納される。また、生成規則格納領域には、ＲＡＭ１００２に読み込まれる生成規則情報が格納される。また、入力式格納領域には、ＲＡＭ１００２に読み込まれる入力式情報が格納される。また、基本変数格納領域には、ＲＡＭ１００２に読み込まれる基本変数情報が格納される。また、補間対象変数格納領域には、ＲＡＭ１００２との間で入出力される補間対象変数情報が格納される。なお、補間対象変数情報は、ＲＡＭ１００２だけに記憶され、ストレージ１００４に格納されなくてもよい。この場合、ストレージ１００４における補間対象変数格納領域は不要となる。また、出力式格納領域には、ＲＡＭ１００２から出力される出力式情報が格納される。
【００３７】
なお、ストレージ１００４は、ネットワークインタフェース１００５を介して接続される外部装置に配置されていてもよい。また、ストレージ１００４に格納されるものとして説明した上述のコンピュータ・プログラムおよびデータの一部または全部は、ＲＯＭ１００３に格納されていてもよい。また、ＲＡＭ１００２、ＲＯＭ１００３およびストレージ１００４には、上述したコンピュータ・プログラムおよびデータの他に、情報処理装置１が有する汎用の機能や他の機能に関連するコンピュータ・プログラムおよびデータ（図示せず）が格納される。
【００３８】
情報処理装置１が図２に示すように構成される場合、図１に示した各機能ブロックは、次のハードウェア要素によって構成可能である。例えば、補間部１１は、ＲＯＭ１００３またはストレージ１００４に格納された補間モジュール、入力式情報、基本変数情報、および、補間規則情報をＲＡＭ１００２に読み込んで補間モジュールを実行することにより、補間対象変数情報をＲＡＭ１００２とストレージ１００４との間で入出力するＣＰＵ１００１によって構成される。また、生成部１２は、ＲＯＭ１００３またはストレージ１００４に格納された生成モジュール、生成規則情報をＲＡＭ１００２に読み込むとともに、既にＲＡＭ１００２に読み込まれている入力式情報および基本変数情報を用いて、生成モジュールを実行することにより、出力式情報を生成してストレージ１００４に出力するＣＰＵ１００１によって構成される。
【００３９】
なお、情報処理装置１およびその各機能ブロックのハードウェア構成は、上述の構成に限定されない。
【００４０】
以上のように構成された情報処理装置１の動作について、図８を参照して説明する。このフローチャートに示した動作を、図２に示したＣＰＵ１００１がＲＡＭ１００２を使用して実行することにより、図１に示した補間部１１および生成部１２の機能が実現される。ただし、図８では、フローチャートに示した動作の実行前後に、ストレージ１００４の各格納領域から必要となる情報を読み込んでＲＡＭ１００２に記憶する処理と、ＲＡＭ１００２に記憶される情報をストレージ１００４の各格納領域に書き出す処理とを省略している。
【００４１】
まず、補間部１１は、入力式情報の示す各入力式のうち、以下のステップＳ２〜Ｓ６の補間処理が済んでいない入力式があるか否かを判断する（ステップＳ１）。
【００４２】
ここで、補間処理が済んでいない入力式があれば（ステップＳ１でＹｅｓ）、補間部１１は、そのような入力式の１つを対象とする。そして、補間部１１は、対象の入力式から、基本変数情報に登録されていない変数を抽出し、抽出した変数を補間対象変数として、補間対象変数情報に登録する（ステップＳ２）。
【００４３】
次に、補間部１１は、補間対象変数情報に登録されている補間対象変数のうち、属性値が補間済みでないものがあるか否かを判断する（ステップＳ３）。
【００４４】
ここで、補間済みでない補間対象変数がある場合（ステップＳ３でＹｅｓ）、補間部１１は、そのうちの１つの補間対象変数について、適用可否が未判定の補間規則があるか否かを判断する（ステップＳ４）。
【００４５】
ここで、未判定の補間規則がない場合（ステップＳ４でＮｏ）、情報処理装置１は、動作を終了する。
【００４６】
一方、未判定の補間規則がある場合（ステップＳ４でＹｅｓ）、補間部１１は、この補間対象変数について、未判定の補間規則のうちの１つが適用可能であるか否かを判断する（ステップＳ５）。例えば、補間部１１は、この補間対象変数および属性値が確定された他の変数の関係性が、その補間規則の適用条件に合致するか否かを判断すればよい。
【００４７】
ここで、適用可能でない場合（ステップＳ５でＮｏ）、補間部１１は、他の補間規則について、ステップＳ４からの処理を繰り返す。
【００４８】
一方、適用可能である場合（ステップＳ５でＹｅｓ）、補間部１１は、この補間対象変数について、該当する補間規則を適用して属性値を決定する（ステップＳ６）。例えば、補間部１１は、該当する補間規則の示す補間処理内容にしたがって、補間対象変数の属性値を決定すればよい。
【００４９】
そして、補間部１１は、この補間対象変数についての処理を終了し、他の補間対象変数について、ステップＳ３からの処理を繰り返す。
【００５０】
そして、ステップＳ３において、この入力式では補間済みでない補間対象変数がないと判断された場合（ステップＳ３でＮｏ）、補間部１１は、この入力式についての処理を終了し、他の入力式について、ステップＳ１からの処理を繰り返す。
【００５１】
そして、ステップＳ１において、補間処理が済んでいない入力式がないと判断された場合（ステップＳ１でＮｏ）、生成部１２は、補間処理が済んだ各入力式のうち、以下のステップＳ８〜Ｓ１０の出力式生成処理が済んでいない入力式があるか否かを判断する（ステップＳ７）。
【００５２】
ここで、出力式生成処理が済んでいない入力式がある場合（ステップＳ７でＹｅｓ）、生成部１２は、そのような入力式の１つを対象とする。そして、生成部１２は、対象の入力式について、適用可否が未判定の生成規則があるか否かを判断する（ステップＳ８）。
【００５３】
ここで、未判定の生成規則がない場合（ステップＳ８でＮｏ）、情報処理装置１は、動作を終了する。
【００５４】
一方、未判定の生成規則がある場合（ステップＳ８でＹｅｓ）、生成部１２は、対象の入力式について、未判定の生成規則の１つが適用可能であるか否かを判断する（ステップＳ９）。例えば、生成部１２は、その生成規則の入力形式が、対象の入力式の形式に合致し、かつ、その生成規則の適用条件が、対象の入力式に出現する変数について真となるか否かを判断すればよい。
【００５５】
ここで、適用可能でない場合、生成部１２は、他の生成規則について、ステップＳ８からの処理を繰り返す。
【００５６】
一方、適用可能である場合、生成部１２は、対象の入力式に対してその生成規則を適用し、出力式を示す出力式情報を生成する（ステップＳ１０）。例えば、生成部１２は、対象の入力式を用いて、その生成規則に含まれる出力式形式にしたがって、出力式情報を生成すればよい。
【００５７】
そして、生成部１２は、この入力式について出力式生成処理を終了し、他の入力式について、ステップＳ７からの処理を繰り返す。
【００５８】
そして、ステップＳ７において、出力式生成処理が済んでいない入力式がないと判断された場合（ステップＳ７でＮｏ）、情報処理装置１は、動作を終了する。
【００５９】
なお、図８において、ステップＳ４でＮｏとなった場合、および、ステップＳ８でＮｏとなった場合は、基本変数または入力式が、補間規則および生成規則が期待するとおりになっていない可能性がある。この場合、基本変数情報または入力式情報に誤りがあることも考えられるため、情報処理装置１は、動作を終了する際に、エラー情報を出力してもよい。
【００６０】
次に、本発明の第１の実施の形態の動作を具体例で示す。
【００６１】
この具体例では、出力式を表現する形式言語がＥｖｅｎｔ−Ｂである例について説明する。また、この具体例では、変数の属性として、変数が空文字列あるいはＮＵＬＬをとりうることを示す無効性について属性値（偽、または、真）が定義または設定されるものとする。すなわち、無効性が真である変数は、空文字列あるいはＮＵＬＬを値としてとりうる変数である。また、無効性が偽である変数は、空文字列あるいはＮＵＬＬを値としてとらない変数である。また、この具体例では、入力画面で入力された入庫数をリレーショナルデータベースの在庫テーブルの在庫フィールドに加算するソフトウェアを例として、その設計情報において、無効性が定義されていない変数の無効性を補間する動作について説明する。なお、以下では、無効性の値が真である変数を、無効変数とも記載する。
【００６２】
また、ここでは、以下の動作に先だって、補間部１１および生成部１２は、ストレージ１００４からＲＡＭ１００２に、図３に示す入力式情報と、図４に示す基本変数情報と、図６に示す補間規則情報と、図７に示す生成規則情報とを読み込むものとする。
【００６３】
ここで、図３に示す入力式情報は、３つの入力式の情報を含んでいる。１番目の入力式「０≦入力画面_入庫数」は、入力画面の入庫数フィールドの文字列が数値として扱える場合に、その数値が０以上であることを示す。また、２番目の入力式「確認画面_入庫数 := 入力画面_入庫数」は、確認画面の入庫数フィールドに入力画面の入庫数の値を設定することを示す。また、３番目の入力式「在庫_在庫数 := 在庫_在庫数 + 確認画面_入庫数」は、在庫テーブルの在庫数フィールドの値に確認画面の入庫数フィールドの値を加算した値を、在庫テーブルの在庫数フィールドに新たな値として設定することを示す。
【００６４】
また、図４に示す基本変数情報は、２つの基本変数の情報を含んでいる。１番目の基本変数「在庫_在庫数」は、在庫テーブルの在庫フィールドの値を表す。また、「在庫_在庫数」は、その無効性として偽が確定されている。すなわち、在庫テーブルの在庫フィールドには、ＮＯＴＮＵＬＬ制約が設定されており、ＮＵＬＬ値をとりえないものとして定義されていることを示している。また、２番目の基本変数「入力画面_入庫数」は入力画面の入庫数フィールドの値を表す。また、「入力画面_入庫数」は、その無効性として真が確定されている。すなわち、入庫数フィールドの値は空文字列であってもよいものとして定義されていることを示している。
【００６５】
また、図６に示す補間規則情報は、３つの補間規則の情報を含んでいる。これらの補間規則は、適用条件として、補間対象変数と基本変数または補間済みの他の補間対象変数との名称が同一であること、一方が他方から導出される関係にあること、または、互いに比較される関係となっていることを表す情報を含んでいる。また、これらの補間規則は、補間処理内容として、補間対象変数の属性値に、適用条件を満たした基本変数または補間済みの他の補間対象変数と同一の属性値を設定することを表す情報を含んでいる。
【００６６】
また、図７に示す生成規則情報は、５つの生成規則の情報を含んでいる。これらの生成規則は、入力式形式として、論理式であること、または、代入式であることを表す情報を含んでいる。また、これらの生成規則は、適用条件として、式に無効変数が出現するか否か、左辺値の無効性が真であるか偽であるか、または、これらを組み合わせた条件を表す情報を含んでいる。また、これらの生成規則は、出力式形式として、図７の表外に示した凡例および記法を用いて入力式から変換可能な式の情報を含んでいる。
【００６７】
これらのＲＡＭ１００２に読み込まれた情報を用いて、情報処理装置１が図８に示した動作を実行する具体例について、以下に説明する。
【００６８】
まず、補間部１１は、ＲＡＭ１００２から、図３に示す入力式情報と、図４に示す基本変数情報と、図６に示す補間規則情報とを読み込む。
【００６９】
例えば、情報処理装置１は、図３の入力式を上から順にアクセスし、まだ補間処理が済んでいない式があるかどうかを調べる。動作の開始時点では、すべての式は補間処理が済んでいない状態にある。
【００７０】
そこで、まず、補間部１１は、入力式情報（図３）の１番目の入力式「0≦入力画面_入庫数」について、まだ補間処理が済んでいないので（ステップＳ１でＹｅｓ）、この入力式から、基本変数ではない変数を補間対象変数として抽出する（ステップＳ２）。ここで、入力式「0≦入力画面_入庫数」に出現する変数は「入力画面_入庫数」のみであり、この変数は基本変数情報（図４）の２番目の変数として登録されている。したがって、この入力式に、補間対象変数は出現しない（ステップＳ３でＮｏ）
そこで、補間部１１は、制御をステップＳ１に戻す。
【００７１】
次に、補間部１１は、入力式情報（図３）の２番目の入力式「確認画面_入庫数 := 入力画面_入庫数」について、まだ補間処理が済んでいないので（ステップＳ１でＹｅｓ）、この入力式から、基本変数ではない変数を補間対象変数として抽出する。ここで、入力式「確認画面_入庫数 := 入力画面_入庫数」に出現する変数は「確認画面_入庫数」および「入力画面_入庫数」である。そこで、補間部１１は、基本変数情報（図４）に出現しない前者の「確認画面_入庫数」を、補間対象変数として、補間対象変数情報（図５）に登録する（ステップＳ２）。登録した時点では「確認画面_入庫数」の属性である無効性の値が真であるか偽であるかは、まだ確定されていない。
【００７２】
次に、補間部１１は、この補間対象変数「確認画面_入庫数」の無効性がまだ補間されていないので（ステップＳ３でＹｅｓ）、制御をステップＳ４に進める。
【００７３】
次に、補間部１１は、補間規則情報（図６）の補間規則についてまだいずれの補間規則の適用も試みられていないので（ステップＳ４でＹｅｓ）、１番目の補間規則の適用条件が、この補間対象変数「確認画面_入庫数」に適用可能か否かを判断する。ここで、この補間対象変数「確認画面_入庫数」と同名の基本変数あるいは補間済みの他の補間対象変数はないため、１番目の補間規則の適用条件「補間対象変数と同名の基本変数あるいは補間済みの補間対象変数がある」は適用できない（ステップＳ５でＮｏ）。
【００７４】
そこで、次に、補間部１１は、補間規則情報（図６）の２番目の補間規則の適用条件が、まだ未判定であるため（ステップＳ４でＹｅｓ）、この補間対象変数「確認画面_入庫数」に対して適用可能か否かを判断する。ここで、この補間対象変数「確認画面_入庫数」の値は、基本変数「入力画面_入庫数」の値から導出されるものである。これは、図３の２番目の入力式「確認画面_入庫数 := 入力画面_入庫数」によって定義されている。したがって、この補間対象変数「確認画面_入庫数」について、２番目の補間規則の適用条件「補間対象変数が基本変数あるいは補間済みの補間対象変数から導出される」は適用可能である（ステップＳ５でＹｅｓ）。
【００７５】
そこで、補間部１１は、この補間対象変数「確認画面_入庫数」について、２番目の補間規則にしたがって、補間処理を行う（ステップＳ６）。ここで、２番目の補間規則の補間処理内容は、「補間対象変数の無効性に、その値がまだ設定されていない場合あるいは偽の場合は、導出に用いた基本変数あるいは補間済みの補間対象変数の無効性と同じ値を設定する」となっている。したがって、この補間処理により、補間対象変数「確認画面_入庫数」の無効性には、基本変数「入力画面_入庫数」の無効性と同じ値「真」が設定される。そして、補間部１１は、図９に示すように、補間対象変数「確認画面_入庫数」の属性値を更新する。
【００７６】
そして、補間部１１は、制御をステップＳ３に戻す。ここで、入力式「確認画面_入庫数 := 入力画面_入庫数」の補間対象変数は「確認画面_入庫数」だけであったため、すべての補間対象変数の属性が決まったことになる（ステップＳ３でＮｏ）。
【００７７】
そこで、補間部１１は、制御をステップＳ１に戻す。
【００７８】
次に、補間部１１は、図３の入力式情報における最後の入力式「在庫_在庫数 := 在庫_在庫数 + 確認画面_入庫数」について、ステップＳ２からの補間処理を行う。この入力式に出現する変数は、基本変数「在庫_在庫数」および補間済みの「確認画面_入庫数」である（ステップＳ３でＮｏ）。
【００７９】
これにより、図３に示すすべての入力式について補間処理が済んだため（ステップＳ１でＮｏ）、情報処理装置１は、制御をステップＳ７に進める。
【００８０】
ここで、生成部１２は、ＲＡＭ１００２から、図３に示す入力式情報と、図４に示す基本変数情報と、図９に示すように更新された補間対象変数情報と、図７に示す生成規則情報とを読み込む。
【００８１】
そして、生成部１２は、図３に示す入力式について、まだいずれも出力式生成処理が済んでいないと判断する（ステップＳ７でＹｅｓ）。
【００８２】
そこで、生成部１２は、図３における１番目の入力式「0≦入力画面_入庫数」について、生成規則情報（図７）のうち１番目の生成規則が未判定であるため（ステップＳ８でＹｅｓ）、適用可能か否かの判断を行う。ここで、１番目の入力式「0≦入力画面_入庫数」は、結果が真あるいは偽となる論理式であるため、１番目の生成規則の入力式形式「論理式」に合致する。しかし、１番目の入力式「0≦入力画面_入庫数」に出現する基本変数「入力画面_入庫数」はその無効性が真であることから無効変数である。そのため、１番目の入力式「0≦入力画面_入庫数」は、１番目の生成規則の適用条件「論理式に無効変数が出現しない」に合致しない。したがって、生成部１２は、１番目の入力式に、１番目の生成規則が合致しないと判断する（ステップＳ９でＮｏ）。
【００８３】
次に、生成部１２は、１番目の入力式について、２番目の生成規則が未判定であるため（ステップＳ８でＹｅｓ）、適用可能か否かの判断を行う。ここで、１番目の入力式「0≦入力画面_入庫数」は、前述のように論理式であるため、２番目の生成規則の入力式形式「論理式」に合致する。また、１番目の入力式「0≦入力画面_入庫数」には、前述のように、無効変数が出現する。そのため、１番目の入力式「0≦入力画面_入庫数」は、２番目の生成規則の適用条件「論理式に無効変数が出現する」に合致する。したがって、生成部１２は、１番目の入力式に、２番目の生成規則が合致すると判断する（ステップＳ９でＹｅｓ）。
【００８４】
そこで、生成部１２は、１番目の入力式「0≦入力画面_入庫数」に対して、２番目の生成規則の出力式形式「[無効変数=無効値 ∨]+ 論理式」を適用し、出力式を生成する。生成される出力式は、「入力画面_入庫数=空文字列 ∨ 0≦入力画面_入庫数」となる（図１０の１番目の式）。そして、生成部１２は、生成した出力式を出力式情報に登録して（ステップＳ１０）、制御をステップＳ７に戻す。
【００８５】
次に、生成部１２は、図３における２番目の入力式「確認画面_入庫数 := 入力画面_入庫数」について、略同様にステップＳ８〜Ｓ９を実行することにより、３番目の生成規則が合致すると判断する。そこで、生成部１２は、２番目の入力式「確認画面_入庫数 := 入力画面_入庫数」に、３番目の生成規則の出力式形式「左辺値 := 式」を適用し、出力式を生成する。生成される出力式は、「確認画面_入庫数 := 入力画面_入庫数」となる（図１０の２番目の式）。そして、生成部１２は、生成した出力式を出力式情報に登録して（ステップＳ１０）、制御をステップＳ７に戻す。
【００８６】
次に、生成部１２は、図３における３番目の入力式「在庫_在庫数 := 在庫_在庫数 + 確認画面_入庫数」について、略同様にステップＳ８〜Ｓ９を実行することにより、５番目の生成規則が合致すると判断する。そこで、生成部１２は、３番目の入力式「在庫_在庫数 := 在庫_在庫数 + 確認画面_入庫数」に、５番目の生成規則の出力式形式を適用し、出力式を生成する。生成される出力式は、「在庫_在庫数 :|  ((確認画面_入庫数=空文字列) ∧ 在庫_在庫数’=在庫_在庫数) ∨ (¬確認画面_入庫数=空文字列 ∧ 在庫_在庫数’=在庫_在庫数 + 確認画面_入庫数)」となる（図１０の３番目の式）。そして、生成部１２は、生成した出力式を出力式情報に登録して（ステップＳ１０）、制御をステップＳ７に戻す。
【００８７】
そして、情報処理装置１は、図３に示した全ての入力式について、図１０に示す出力式を生成したので（ステップＳ７でＮｏ）、処理全体を終了する。
【００８８】
以上で、具体例の動作の説明を終了する。
【００８９】
次に、本発明の実施の形態の効果について述べる。
【００９０】
本発明の実施の形態としての情報処理装置は、ソフトウェアの設計情報に含まれる式に、要件が明示的に定義されていない変数が出現する場合であっても、該式を、出現する各変数に対する要件を適切に反映した、形式言語による式に変換することができる。
【００９１】
その理由は、補間部が、ソフトウェアの設計情報における入力式の情報および入力式における属性値が確定された変数の情報に基づいて、属性値が確定されていない変数（補間対象変数）の属性値を確定する補間規則を用いて、処理対象の入力式における補間対象変数の属性値を補間するからである。また、生成部が、入力式から、入力式に含まれる変数の属性値を考慮して、形式言語で記された出力式を生成する生成規則を用いて、処理対象の入力式から出力式を生成するからである。
【００９２】
このように、本実施の形態は、ソフトウェアの設計情報に含まれる式に出現する変数に属性が確定されていないものがあっても、属性値が確定している他の変数の属性値を用いて、属性値が確定していない変数の属性値を補間する。そして、本実施の形態は、変数の属性値がすべて補間された状態で、元の式から形式言語による式を生成する。これにより、本実施の形態は、形式言語の表現が変数の属性値に応じて異なってくる場合にも、より適切に、設計情報における式から、形式言語による式を生成することができる。その結果、本実施の形態は、本実施の形態により生成された式を用いた形式手法による検証の精度をより向上させることができ、ソフトウェアの設計情報の緻密な整合性検証を支援することができる。
【００９３】
なお、本発明の実施の形態では、出力式を表現する形式言語がＥｖｅｎｔ−Ｂである例を中心に説明したが、本発明の生成部が生成する出力式の形式言語を限定するものではない。本発明の生成部が生成する出力式は、他の形式言語による出力式であってもよい。
【００９４】
また、本発明の実施の形態では、変数の属性値として、変数が空文字列あるいはＮＵＬＬをとりうることを示す無効性についての真偽が設定される例を中心に説明したが、本発明における変数の属性値が表す要件を限定するものではない。例えば、本発明における変数の属性値は、変数が集合であるか集合の要素であるかを示す論理値であってもよい。
【００９５】
また、本発明の実施の形態では、補間規則および生成規則が、コンピュータ・プログラムとは別に独立した情報としてストレージに格納される例を中心に説明したが、コンピュータ・プログラムの一部として実装されていてもよい。
【００９６】
また、本発明の実施の形態では、補間部は、ストレージに格納された入力式および基本変数を読み込む例を中心に説明したが、入力装置またはネットワークインタフェース等を介して接続された外部の装置から、入力式および基本変数を読み込んでもよい。
【００９７】
また、本発明の実施の形態では、生成部は、生成した出力式を、ストレージに格納する例を中心に説明したが、出力装置またはネットワークインタフェースを介して接続された外部の装置に出力してもよい。
【００９８】
また、上述した本発明の各実施の形態において、情報処理装置の各機能ブロックが、記憶装置またはＲＯＭに記憶されたコンピュータ・プログラムを実行するＣＰＵによって実現される例を中心に説明したが、各機能ブロックの一部、全部、または、それらの組み合わせが専用のハードウェアにより実現されていてもよい。
【００９９】
また、上述した本発明の各実施の形態において、情報処理装置の機能ブロックは、複数の装置に分散されて実現されてもよい。
【０１００】
また、上述した本発明の各実施の形態において、フローチャートを参照して説明した情報処理装置の動作を、本発明のコンピュータ・プログラムとしてコンピュータの記憶装置（記憶媒体）に格納しておき、係るコンピュータ・プログラムを当該ＣＰＵが読み出して実行するようにしてもよい。そして、このような場合において、本発明は、係るコンピュータ・プログラムのコードあるいは記憶媒体によって構成される。
【０１０１】
また、本発明は、上述した各実施の形態に限定されず、様々な態様で実施されることが可能である。
【符号の説明】
【０１０２】
１    情報処理装置
１１    補間部
１２    生成部
１００１    ＣＰＵ
１００２    ＲＡＭ
１００３    ＲＯＭ
１００４  ストレージ
１００５  ネットワークインタフェース
１００６  入力装置
１００７  出力装置
【図１】
2015204028.tif 000003
【図２】
2015204028.tif 000004
【図３】
2015204028.tif 000005
【図４】
2015204028.tif 000006
【図５】
2015204028.tif 000007
【図６】
2015204028.tif 000008
【図７】
2015204028.tif 000009
【図８】
2015204028.tif 000010
【図９】
2015204028.tif 000011
【図１０】
2015204028.tif 000012