(57)【要約】【課題】フローチャートやアクティビティ図の各アクションノードに対して、処理の流れや局所事後条件の有効範囲などに基づくソフトウェアの設計内容の緻密な整合性検証をすること。【解決手段】データの静的な構造および制約を記述したクラス図と、データを逐次的に処理するソフトウェアの処理の流れおよび実行内容を記述したアクティビティ図と、からなる設計情報を読み込む入力処理部と、ソフトウェアの設計で用いるデータの型または定数を記述した既定識別子情報を読み込み、入力処理部により読み込まれた設計情報および既定識別子情報から、形式記述の作成に必要となる定数または変数の名称、型および静的制約からなる識別子情報と、アクティビティ図に記述された実行内容を実行した結果を示す論理式である局所事後条件および局所事後条件の有効範囲を示す局所事後条件情報と、を生成する局所事後条件生成部と、を備える。【選択図】  図１
2014241051.tif 000002
【特許請求の範囲】
【請求項１】
データの静的な構造および制約を記述したクラス図と、データを逐次的に処理するソフトウェアの処理の流れおよび実行内容を記述したアクティビティ図と、からなる設計情報を読み込む入力処理手段と、
ソフトウェアの設計で用いるデータの型または定数を記述した既定識別子情報を読み込み、前記入力処理手段により読み込まれた前記設計情報および前記既定識別子情報から、形式記述の作成に必要となる定数または変数の名称、型および静的制約からなる識別子情報と、前記アクティビティ図に記述された前記実行内容を実行した結果を示す論理式である局所事後条件および該局所事後条件の有効範囲を示す局所事後条件情報と、を生成する局所事後条件生成手段と、
を備える情報処理装置。
【請求項２】
前記局所事後条件生成手段は、
前記アクティビティ図に含まれる各ノードに前記ソフトウェアの処理の流れにしたがって一意のノード番号を割り当てるノード番号割当手段と、
前記アクティビティ図に含まれる各ノードの実行内容と前記ノード番号とに基づいて、前記局所事後条件の有効範囲を生成する有効範囲生成手段と、
を含む請求項１に記載の情報処理装置。
【請求項３】
前記有効範囲生成手段は、前記局所事後条件において有効範囲を示すノードの開始番号とノードの終了番号が等しい場合に、当該局所事後条件を無効とする請求項２に記載の情報処理装置。
【請求項４】
前記設計情報、前記識別子情報および前記局所事後条件情報を用いて、前記ソフトウェアの仕様を形式手法の記法で表現した形式記述を生成する形式記述生成手段、をさらに備える請求項１乃至３のいずれか１項に記載の情報処理装置。
【請求項５】
前記形式記述生成手段は、
前記形式記述に対して、前記アクティビティ図に含まれる先行ノードに割り当てられたノード番号を局所事前条件として追加する局所事前条件追加手段と、
前記形式記述に対して、前記有効範囲を記述した局所事後条件を追加する局所事後条件追加手段と、
を含む請求項４に記載の情報処理装置。
【請求項６】
前記形式記述生成手段は、Ｅｖｅｎｔ−Ｂの形式手法により形式記述を行ない、
前記局所事前条件追加手段は、Ｅｖｅｎｔ−Ｂマシンにおいて、前記ノード番号を変数として追加して、前記ノード番号のアクションノードのガード(Guard)節として先行ノードのノード番号を記述し、
前記局所事後条件追加手段は、Ｅｖｅｎｔ−Ｂマシンにおいて、前記有効範囲としてのノードの開始番号と終了番号とを含んだ局所事後条件を不変条件(Invariants）節に記述する請求項５に記載の情報処理装置。
【請求項７】
データの静的な構造および制約を記述したクラス図と、データを逐次的に処理するソフトウェアの処理の流れおよび実行内容を記述したアクティビティ図と、からなる設計情報を読み込む入力処理ステップと、
ソフトウェアの設計で用いるデータの型または定数を記述した既定識別子情報を読み込み、前記入力処理ステップにおいて読み込まれた前記設計情報および前記既定識別子情報から、形式記述の作成に必要となる定数または変数の名称、型および静的制約からなる識別子情報と、前記アクティビティ図に記述された前記実行内容を実行した結果を示す論理式である局所事後条件および該局所事後条件の有効範囲を示す局所事後条件情報と、を生成する局所事後条件生成ステップと、
を含む情報処理方法。
【請求項８】
前記設計情報、前記識別子情報および前記局所事後条件情報を用いて、前記ソフトウェアの仕様を形式手法の記法で表現した形式記述を生成する形式記述生成ステップ、をさらに含む請求項７に記載の情報処理方法。
【請求項９】
データの静的な構造および制約を記述したクラス図と、データを逐次的に処理するソフトウェアの処理の流れおよび実行内容を記述したアクティビティ図と、からなる設計情報を読み込む入力処理ステップと、
ソフトウェアの設計で用いるデータの型または定数を記述した既定識別子情報を読み込み、前記入力処理ステップにおいて読み込まれた前記設計情報および前記既定識別子情報から、形式記述の作成に必要となる定数または変数の名称、型および静的制約からなる識別子情報と、前記アクティビティ図に記述された前記実行内容を実行した結果を示す論理式である局所事後条件および該局所事後条件の有効範囲を示す局所事後条件情報と、を生成する局所事後条件生成ステップと、
をコンピュータに実行させる情報処理プログラム。
【請求項１０】
前記設計情報、前記識別子情報および前記局所事後条件情報を用いて、前記ソフトウェアの仕様を形式手法の記法で表現した形式記述を生成する形式記述生成ステップ、をさらにコンピュータに実行させる請求項９に記載の情報処理プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、設計情報の形式検証を支援する技術に関する。
【背景技術】
【０００２】
上記技術分野において、非特許文献１には、形式手法の１つであるEvent-Bによって、ソフトウェアの設計内容を集合や一階述語論理の式で記述し、複数の式の間に整合があることをツールの支援を受けながら数学的に証明することにより、Event-Bの記述に欠陥がないことを保証する技術が開示されている。そして、非特許文献１の(II) Event-B: Structure and Laws - P7, "2.6 Consistency Proofs for an Event System: Feasibility and Invariance Preservation,"には、"INV"とラベル付けされた式で不変条件保存則が記載されている。
【先行技術文献】
【非特許文献】
【０００３】
【非特許文献１】C. Metayer, J.-R. Abrial, L. Voisin, "RODIN Deliverable 3.2 Event-B Language," RODIN(Rigorous Open Development Environment for Complex Systems), Project IST-511599, 31st May 2005
【発明の概要】
【発明が解決しようとする課題】
【０００４】
しかしながら、ソフトウェアの設計では、当該ソフトウェアが操作するデータをＥＲ図(Entity Relationship Diagram)やＵＭＬ(Unified Modeling Language)のクラス図で表現し、当該ソフトウェアが行う処理の流れをフローチャートやＵＭＬのアクティビティ図で表現する。上記文献に記載の技術において、クラス図およびアクティビティ図などから生成された情報に基づいてEvent-BコンテキストおよびEvent-Bマシンを生成するが、フローチャートやアクティビティ図の各アクションノードごとに、ソフトウェアの設計内容の緻密な整合性検証ができなかった。
【０００５】
本発明の目的は、上述の課題を解決する技術を提供することにある。
【課題を解決するための手段】
【０００６】
上記目的を達成するため、本発明に係る情報処理装置は、
データの静的な構造および制約を記述したクラス図と、データを逐次的に処理するソフトウェアの処理の流れおよび実行内容を記述したアクティビティ図と、からなる設計情報を読み込む入力処理手段と、
ソフトウェアの設計で用いるデータの型または定数を記述した既定識別子情報を読み込み、前記入力処理手段により読み込まれた前記設計情報および前記既定識別子情報から、形式記述の作成に必要となる定数または変数の名称、型および静的制約からなる識別子情報と、前記アクティビティ図に記述された前記実行内容を実行した結果を示す論理式である局所事後条件および該局所事後条件の有効範囲を示す局所事後条件情報と、を生成する局所事後条件生成手段と、
を備える。
【０００７】
上記目的を達成するため、本発明に係る情報処理方法は、
データの静的な構造および制約を記述したクラス図と、データを逐次的に処理するソフトウェアの処理の流れおよび実行内容を記述したアクティビティ図と、からなる設計情報を読み込む入力処理ステップと、
ソフトウェアの設計で用いるデータの型または定数を記述した既定識別子情報を読み込み、前記入力処理ステップにおいて読み込まれた前記設計情報および前記既定識別子情報から、形式記述の作成に必要となる定数または変数の名称、型および静的制約からなる識別子情報と、前記アクティビティ図に記述された前記実行内容を実行した結果を示す論理式である局所事後条件および該局所事後条件の有効範囲を示す局所事後条件情報と、を生成する局所事後条件生成ステップと、
を含む。
【０００８】
上記目的を達成するため、本発明に係る情報処理プログラムは、
データの静的な構造および制約を記述したクラス図と、データを逐次的に処理するソフトウェアの処理の流れおよび実行内容を記述したアクティビティ図と、からなる設計情報を読み込む入力処理ステップと、
ソフトウェアの設計で用いるデータの型または定数を記述した既定識別子情報を読み込み、前記入力処理ステップにおいて読み込まれた前記設計情報および前記既定識別子情報から、形式記述の作成に必要となる定数または変数の名称、型および静的制約からなる識別子情報と、前記アクティビティ図に記述された前記実行内容を実行した結果を示す論理式である局所事後条件および該局所事後条件の有効範囲を示す局所事後条件情報と、を生成する局所事後条件生成ステップと、
をコンピュータに実行させる。
【発明の効果】
【０００９】
本発明によれば、フローチャートやアクティビティ図の各アクションノードごとに、ソフトウェアの設計内容の緻密な整合性検証をすることができる。
【図面の簡単な説明】
【００１０】
【図１】本発明の第１実施形態に係る情報処理装置の構成を示すブロック図である。
【図２Ａ】本発明の第２実施形態に係る情報処理装置の機能構成を示すブロック図である。
【図２Ｂ】本発明の第２実施形態に係る情報処理装置のハードウェア構成を示すブロック図である。
【図３】本発明の第２実施形態に係る情報処理装置の処理手順を示すフローチャートである。
【図４】本発明の第２実施形態に係る設計情報としてのクラス図およびアクティビティ図の構成を示す図である。
【図５】本発明の第２実施形態に係る識別子情報生成処理の手順を示すフローチャートである。
【図６】本発明の第２実施形態に係る生成された識別子情報の構成を示す図である。
【図７】本発明の第２実施形態に係る既定識別子情報の構成を示す図である。
【図８】本発明の第２実施形態に係る局所事後条件情報生成処理の手順を示すフローチャートである。
【図９】本発明の第２実施形態に係るノード番号割り当てを示す図である。
【図１０】本発明の第２実施形態に係るアクティビティ図を元に生成された局所事後条件情報の構成を示す図である。
【図１１】本発明の第２実施形態に係る条件追加ルールの構成を示す図である。
【図１２】本発明の第２実施形態に係る条件追加後の局所事後条件情報の構成を示す図である。
【図１３】本発明の第２実施形態に係る有効範囲設定後の局所事後条件情報の構成を示す図である。
【図１４Ａ】本発明の第３実施形態に係る情報処理装置の機能構成を示すブロック図である。
【図１４Ｂ】本発明の第３実施形態に係る情報処理装置のハードウェア構成を示すブロック図である。
【図１５】本発明の第３実施形態に係る情報処理装置の処理手順を示すフローチャートである。
【図１６】本発明の第３実施形態に係る形式記述生成処理の手順を示すフローチャートである。
【図１７】本発明の第３実施形態に係る形式記述としてのEvent-Bコンテキストの記述を示す図である。
【図１８】本発明の第３実施形態に係る拡張したEvent-Bコンテキストの記述を示す図である。
【図１９】本発明の第３実施形態に係るノード番号および有効範囲の無い形式記述としてのEvent-Bマシンの記述を示す図である。
【図２０】本発明の第３実施形態に係るノード番号追加後のEvent-Bマシンの記述を示す図である。
【図２１】本発明の第３実施形態に係る有効範囲のある局所事後条件設定後のEvent-Bマシンの記述を示す図である。
【発明を実施するための形態】
【００１１】
以下に、図面を参照して、本発明の実施の形態について例示的に詳しく説明する。ただし、以下の実施の形態に記載されている構成要素は単なる例示であり、本発明の技術範囲をそれらのみに限定する趣旨のものではない。例えば、形式記述として以下ではEvent-Bについて示すが、本発明により生成された情報は、Event-Bに限定されず他の形式記述によるソフトウェア設計の整合性判定にも同様の効果を奏する。
【００１２】
［第１実施形態］
本発明の第１実施形態としての情報処理装置１００について、図１を用いて説明する。情報処理装置１００は、設計情報の形式検証を支援する装置である。
【００１３】
図１に示すように、情報処理装置１００は、入力処理部１０１と、局所事後条件生成部１０２と、を含む。入力処理部１０１は、データの静的な構造および制約を記述したクラス図と、データを逐次的に処理するソフトウェアの処理の流れおよび実行内容を記述したアクティビティ図と、からなる設計情報１１１を読み込む。局所事後条件生成部１０２は、ソフトウェアの設計で用いるデータの型または定数を記述した既定識別子情報１２１を込む。そして、局所事後条件生成部１０２は、入力処理部１０１により読み込まれた設計情報１１１および既定識別子情報１２１から、形式記述の作成に必要となる定数または変数の名称、型および静的制約からなる識別子情報１２２を生成する。さらに、局所事後条件生成部１０２は、アクティビティ図に記述された実行内容を実行した結果を示す論理式である局所事後条件および局所事後条件の有効範囲を示す局所事後条件情報１２３を生成する。
【００１４】
本実施形態によれば、フローチャートやアクティビティ図の各アクションノードごとに、ソフトウェアの設計内容の緻密な整合性検証をすることができる。
【００１５】
［第２実施形態］
次に、本発明の第２実施形態に係る情報処理装置について説明する。本実施形態に係る情報処理装置は、クラス図とアクティビティ図とから、形式記述生成に使用される、識別子情報と、有効範囲を有する局所事後条件とを生成する。
【００１６】
最初に、本実施形態に係る技術分野における背景を簡単に説明する。
【００１７】
《背景》
ソフトウェア開発では、ソフトウェアの品質を確保するために、その設計内容が正しいことを検証する必要がある。そのため、ソフトウェア開発において、設計情報をＵＭＬで記述したり、形式手法で検証することが多くなってきている。ここで、ＵＭＬは、ソフトウェアの静的な構造や制約を表すクラス図や、ソフトウェアが行う処理の流れを表すアクティビティ図といったグラフィカルな図式の記法である。形式手法とは、集合や論理といった数学的な概念に基づいて、対象システムを正確で曖昧さのない記法で表現し、記述に不整合がないことを検証する手法である。すなわち、逐次処理を行うソフトウェアの設計では、当該ソフトウェアが操作するデータをＥＲ図やＵＭＬのクラス図で表現し、当該ソフトウェアが行う処理の流れをフローチャートやＵＭＬのアクティビティ図で表現する。逐次処理を表すアクティビティ図では、処理の各ステップを図上のアクションノードとして表現する。先行するステップに対応するアクションノードから後続のステップに対応するアクションノードへ有向線分を引くことによって、複数の処理ステップが連続して行われることを表現する。各アクションノードには、データが正しい状態あることをチェックするか、データに新しい値を設定するか、あるいは両方を行うことを記述する（図４参照）。
【００１８】
従来は、これらの図式で表現された設計内容が正しいかどうかは人間がレビューで検証してきた。レビューは目視による確認作業であり、レビューを行う人間のスキルが低ければ、欠陥の多くを見逃すことになる。そこで、例えば、形式手法の１つであるEvent-Bでは、ソフトウェアの設計内容を集合や一階述語論理の式で記述し、複数の式の間に整合があることをツールの支援を受けながら数学的に証明することにより、Event-Bの記述に欠陥がないことを保証する。Event-Bでは、データを定数や変数として、データに関する制約を不変条件として、データを操作する処理をイベント（以降、Event-Bイベントと称す）として表す。イベントはガード節とアクション節から成り、ガード節に記述された全ての論理式（以降、Event-Bガードと称す）が真となる場合のみ、アクション節に記述された全ての代入式（以降、Event-Bアクションと称す）が実行される。重要な整合性の１つに不変条件保存則があり、Event-Bイベントと不変条件の一組ごとに、当該不変条件が成り立っている任意の状態から、当該Event-Bイベントを実行した後の状態では再び当該不変条件が成り立たねばならない（非特許文献１参照）。
【００１９】
アクティビティ図で表された逐次処理とクラス図で表されたデータとの間に不整合がないことをEvent-Bを用いて検証するには、アクティビティ図の各アクションノード、すなわち逐次処理の各処理ステップをEvent-Bイベントと見なすことが考えられる。しかし、この素朴な考え方には次の２つの問題がある。
【００２０】
１番目の問題は、アクティビティ図では有向線分に沿ってアクションノードを辿ることで実行順序が決まるが、Event-Bでは一般にEvent-Bイベントの実行順序は決まらないことである。Event-Bでは複数のEvent-Bイベントについて、それぞれのEvent-Bガードが真となるときに、どのEvent-Bイベントが実行されるかは一意には決まらない。Event-Bガードが真となるEvent-Bイベントのうち任意の1つだけ非決定的に選ばれて、そのEvent-Bアクションが他のEvent-Bイベントからの割り込みなしに実行される。その結果、アクティビティ図でのアクションノードの実行順序どおりにEvent-Bイベントを実行することが保証されないことである。
【００２１】
２番目の問題は、アクティビティ図では各アクションノードを実行した結果として、どのような条件がいつまで成立するのかを明示しないが、Event-Bでは論理式として明示する必要があることである。例えば、３個の連続した処理ステップがあり、１番目のステップでは変数ｘに“０”を代入し、２番目のステップでは変数ｘと関係のない処理を行い、３番目のステップでは変数ｘに“１”を代入することを考える。アクティビティ図では、１番目と３番目のアクションノードに変数ｘへの代入式が記述される。この記述によって暗黙のうちに、１番目の処理ステップの直後から１番目の処理ステップの直前まで「変数ｘの値は“０”である」という条件が成り立ち、３番目の処理ステップの直後からは「変数ｘの値は“１”である」という条件が成り立つと解釈される。Event-Bではこれらの暗黙に解釈される条件を明示的に記述する必要がある。すなわち、アクティビティ図のアクションノードの実行結果は暗黙に後続のアクションノードを実行する際の前提条件となる。さらに、先行するアクションノードでの変数への値の代入結果が、後続のアクションノードにおける同じ変数への別の値の代入によって無効となるようにアクションノードの実行結果には有効範囲がある。しかし、アクションノードの記述内容を素朴にEvent-Bイベントとして記述すると、暗黙の実行結果は記述されず、その有効範囲も記述されないことである。
【００２２】
本実施形態においては、逐次処理を行うソフトウェアの設計内容を示すＵＭＬのアクティビティ図とクラス図をEvent-Bで記述した場合に、アクティビティ図の制御フローどおりにEvent-Bイベントが実行される。そして、アクティビティ図に記載された逐次処理がクラス図に記載のデータ構造と制約を守っていることを検証できるようなEvent-Bの記述を可能とする、識別子情報と局所事後条件情報とを提供する。なお、実施形態の先頭にも記載の通り、本実施形態により生成された識別子情報と有効範囲を有する局所事後条件情報とは、他の形式手法にも効果的に適用される。
【００２３】
《情報処理装置の機能構成》
図２Ａは、本実施形態に係る情報処理装置２００の機能構成を示すブロック図である図２Ａを参照すると、本実施形態における情報処理装置２００は、機能的には、入力処理部２０１と、局所事後条件生成部２０２と、出力処理部２０３と、を有する。
【００２４】
入力処理部２０１は、設計情報を検索可能に格納する設計情報格納部２７０からクラス図とアクティビティ図とからなる設計情報を読み込む（図４参照）。
【００２５】
局所事後条件生成部２０２は、入力処理部２０１により読み込まれた設計情報から識別子を抽出し、既定識別子情報格納部２０４から読み込んだ既定識別子情報と合わせて、識別子情報とする。識別子情報は、識別子と基本型と分類と静的制約を含む。クラス図においては、クラスおよび属性の名称が識別子となる。アクティビティ図においては、その名称がクラス図に出現しない変数の名称が識別子となる。
【００２６】
また、局所事後条件生成部２０２は、入力処理部２０１により読み込まれたアクティビティ図から、アクティビティ図の各アクションノードの実行後に成立すべき局所事後条件を抽出し、局所事後条件情報として保持する。アクションノードに記載された論理式は、そのまま局所事後条件とする。代入式は、例えば、代入演算子「:=」を等価演算子「=」で置換することにより、局所事後条件とする。また、局所事後条件生成部２０２が、抽出した局所事後条件が条件追加ルール格納部２０５から読み込んだ条件追加ルールの入力条件に合致すれば、追加条件ルールから新たな局所事後条件を導出し、局所事後条件情報に追加する。さらに、本実施形態においては、局所事後条件生成部２０２が、局所事後条件情報を調べて、各局所事後条件の有効範囲を特定する。
【００２７】
出力処理部２０３は、局所事後条件生成部２０２により作成された識別子情報と局所事後条件情報とをそれぞれ、関連付けて検索可能に識別子情報格納部２８０と局所事後条件情報格納部２９０とに書き出す。
【００２８】
《情報処理装置のハードウェア構成》
図２Ｂ、本実施形態に係る情報処理装置２００のハードウェア構成を示すブロック図である。
【００２９】
図２Ｂで、ＣＰＵ２１０は演算制御用のプロセッサであり、ＣＰＵ２１０がＲＡＭ２４０を使用しながらストレージ２５０に格納されたプログラムおよびモジュールを実行することで、図２Ａに示された情報処理装置２００の各機能構成部の機能が実現される。ＲＯＭ２２０は、初期データおよびプログラムなどの固定データおよびプログラムを記憶する。また、通信制御部２３０は、ネットワークを介して外部装置と通信する。なお、ＣＰＵ２１０は１つに限定されず、複数のＣＰＵであっても、あるいは画像処理用のＧＰＵを含んでもよい。
【００３０】
ＲＡＭ２４０は、ＣＰＵ２１０が一時記憶のワークエリアとして使用するランダムアクセスメモリである。ＲＡＭ２４０には、本実施形態の実現に必要なデータを記憶する領域が確保されている。クラス図データ２４１は、設計情報におけるソフトウェアの静的な構造や制約を表すクラス図のデータである（図４参照）。アクティビティ図データ２４２は、設計情報におけるソフトウェアが行う処理の流れを表すアクティビティ図のデータである（図４参照）。アクティビティ図データ（ノード番号）２４３は、本実施形態により一意のノード番号が割り当てされたアクティビティ図のデータである（図９参照）。識別子情報２４４は、本実施形態により生成される情報である（図６参照）。局所事後条件情報２４５は、本実施形態により生成される情報である（図１０、図１２および図１３参照）。入出力データ２４６は、入出力インタフェース２６０を介して入出力される入出力データを示す。送受信データ２４７は、通信制御部２３０を介して送受信される送受信データを示す。
【００３１】
ストレージ２５０には、データベースや各種のパラメータ、あるいは本実施形態の実現に必要な以下のデータまたはプログラムが記憶されている。既定識別子情報格納部２０４は、処理対象のソフトウェアにおける規定の識別子を示す情報を格納する（図７参照）。条件追加ルール格納部２０５は、局所事後条件を追加するためのルールを格納する（図１１参照）。識別子情報生成アルゴリズム２５１は、本実施形態における識別子情報を生成するために使用されるアルゴリズムである。ノード番号割当アルゴリズム２５２は、本実施形態におけるアクティビティ図のアクションノードに一意のノード番号を割り当てるために使用されるアルゴリズムである。局所事後条件情報生成アルゴリズム２５３は、本実施形態における有効範囲を有する局所事後条件情報を生成するために使用されるアルゴリズムである。
【００３２】
ストレージ２５０には、以下のプログラムが格納される。情報処理装置制御プログラム２５４は、本情報処理装置２００の全体を制御する制御プログラムである。識別子情報生成モジュール２５５は、情報処理装置制御プログラム２５４において、識別子情報生成アルゴリズム２５１を使用して識別子情報を生成するモジュールである。局所事後条件情報生成モジュール２５６は、情報処理装置制御プログラム２５４において、ノード番号割当アルゴリズム２５２に従いアクションノードに一意のノード番号を割り当てる。そして、局所事後条件情報生成アルゴリズム２５３に従い有効範囲を有する局所事後条件情報を生成するモジュールである。生成情報出力処理モジュール２５７は、情報処理装置制御プログラム２５４において、生成された識別子情報を識別子情報格納部２８０に出力し、生成された有効範囲を有する局所事後条件情報を局所事後条件情報格納部２９０に出力するモジュールである。
【００３３】
入出力インタフェース２６０は、入出力機器との入出力データをインタフェースする。入出力インタフェース２６０には、表示部２６１、キーボード、タッチパネル、ポインティンデバイスなどの操作部２６２が接続される。また、設計情報であるクラス図とアクティビティ図とを検索可能に格納する設計情報格納部２７０が接続される。さらに、識別子情報を検索可能に格納する識別子情報格納部２８０と、有効範囲を有する局所事後条件情報を識別子情報と関連付けて検索可能に格納する局所事後条件情報格納部２９０と、が接続される。なお、上記格納部２７、２８０、２９０は、通信制御部２３０によりネットワークを介して接続されていてもよい。
【００３４】
なお、図２ＢのＲＡＭ２４０やストレージ２５０には、情報処理装置２００が有する汎用の機能や他の実現可能な機能に関連するプログラムやデータは図示されていない。
【００３５】
《情報処理装置の処理手順》
図３は、本実施形態に係る情報処理装置２００の処理手順を示すフローチャートである。このフローチャートは、図２ＢのＣＰＵ２１０がＲＡＭ２４０を使用して実行し、図２Ａの機能構成部を実現する。
【００３６】
最初に、情報処理装置２００は、設計情報格納部２７０からクラス図とアクティビティ図とから成る設計情報を読み込む（ステップＳ３０１）。次に、情報処理装置２００は、ステップＳ３０１で読み込まれた設計情報から、識別子情報を生成する（ステップＳ３０３：詳細は図５参照）。次に、情報処理装置２００は、ステップＳ３０１で読み込まれた設計情報から、有効範囲を有する局所事後条件情報を生成する（ステップＳ３０５：詳細は図８参照）。そして、情報処理装置２００は、ステップＳ３０３において生成された識別子情報と、ステップＳ３０５において生成された有効範囲を有する局所事後条件情報とをそれぞれ、識別子情報格納部２８０と局所事後条件情報格納部２９０とに書き出す（ステップＳ３０７）。
【００３７】
以下、上記ステップＳ３０１〜Ｓ３０７における処理について、詳細に説明する。
【００３８】
《設計情報の読み込み：Ｓ３０１》
図４は、本実施形態に係る設計情報としてのクラス図（４０１）およびアクティビティ図（４０２）の構成を示す図である。かかる設計情報は、設計情報格納部２７０に格納されており、本実施形態の情報処理装置２００に読み込まれる。逐次処理を行うを行うソフトウェアの設計にＵＭＬを用いる場合、ソフトウェアが扱うデータの構造や制約をクラス図で表現し、ソフトウェアが行う処理をアクティビティ図で表現することができる。データについては、データ全体を１つのクラス図とし、個々のデータはクラス図のクラスに、データ項目は対応するクラスのメンバ属性として表現する。処理については、処理全体を１つのアクティビティ図とし、処理を構成する一連の処理ステップをアクションノードとする。そして、先に実行される処理ステップと後続の処理ステップとの関係を対応するアクションノード間の有向線分（制御フロー）として記述し、処理ステップでチェックすべきことや実行すべきことをアクションノードのラベルに記述することになる。
【００３９】
クラス図（４０１）は、クラスの情報を含む。クラスの情報は、名称と複数のメンバ属性の情報を含む。メンバ属性の情報は、名称と型を含む。また、メンバ属性には、ステレオタイプ（ギムレット“＜＜”と“＞＞”とで囲まれた文字列）や、制約の内容（例えば、“｛”と“｝”とで囲まれた論理式）を記載したコメントによって、制約を与えることができる。
【００４０】
アクティビティ図（４０２）は、開始ノードと、１つまたは複数のアクションノードと、終了ノードと、これらのノード間をつなぐ有向線分である制御フローとを含む。アクティビティ図（４０２）は、ソフトウェアが行う処理の流れを示すものであり、開始ノードから制御フローをたどり、アクションノードに記載されたアクションの内容を実行し、終了ノードに至れば一連の処理全体が終わったものとする。アクションノードには、そのノードの箇所で行う処理内容を記す。ここで、論理式（真偽値をとる式）が記されていれば、そのアクションノードでは当該論理式が真であることを調べ、代入式（変数に値を設定する式）が記されていれば、そのアクションノードでは当該代入式どおりに変数に値を設定する、ものとする。
【００４１】
（本実施形態で使用するクラス図とアクティビティ図）
以降の具体的説明においては、図４のクラス図（４０１）とアクティビティ図（４０２）とを読み込んだものとして説明する。
【００４２】
図４のクラス図（４０１）は、データベースの表「商品」を表す。表「商品」は、列「商品ＣＤ」を持つ。列「商品ＣＤ」の型は、「非空文字列」である。ここで、全ての文字列が属する型を「文字列」とし、文字列の長さが“０”である文字列を「空文字列」とし、「空文字列」を除いた全ての文字列が属する型を「非空文字列」とする。また、列「商品ＣＤ」は、表「商品」の行を一意に識別する値を持つ。すなわち、表「商品」から任意に選んだ２個の行について、それぞれの行の列「商品ＣＤ」の値が同じであれば２個の行は同じ行であり、列「商品ＣＤ」の値が異なれば２個の行は異なる行である。
【００４３】
図４のクラス図（４０１）では、表「商品」をクラス「商品」とし、列「商品ＣＤ」をメンバ属性「商品ＣＤ」としている。「商品ＣＤ」の型は「非空文字列」である。「商品ＣＤ」の前に付されたステレオタイプ“＜＜pk＞＞”（primary key：主キー）は、そのメンバ属性には必ず値が設定されねばならず、かつそのメンバ属性の値によってクラスのインスタンスが一意に識別される、ことを表す。
【００４４】
図４のアクティビティ図（４０２）は、変数「新規ＣＤ」の値を列「商品ＣＤ」の値としてもつような新しい行「新規商品」を、データベースの表「商品」に追加する逐次処理を表す。行「新規商品」を表「商品」に登録する逐次処理では、まず、変数「新規ＣＤ」の値が、空文字列ではないことと、表「商品」の列「商品ＣＤ」にまだ登録されていないことと、を確認する。次に、行「新規商品」が表「商品」には登録されていないことを確認し、表「商品」に行「新規商品」を追加し、行「新規商品」の列「商品ＣＤ」の値として、変数「新規ＣＤ」の値を設定する。
【００４５】
図４のアクティビティ図（４０２）で、開始ノードは、逐次処理を開始することを表す。アクティビティ図（４０２）で、開始ノードから制御フローを１回たどって到達するアクションノードＳ４０１は、２個の論理式を持ち、これらの論理式が真であることを確認する。論理式「新規ＣＤ≠空文字列」は、変数「新規ＣＤ」の値が「空文字列」でないことを意味し、論理式「新規ＣＤ∈/ran(商品_商品ＣＤ)」は、変数「新規ＣＤ」の値がクラス「商品」の属性「商品ＣＤ」の値の集合に含まれていないことを意味する。ここで、クラスＣの属性Ｆを、Ｃのインスタンスの集合「Ｃ」からＦの型に属する値の集合への関数「Ｃ_Ｆ」と表現し、Ｃの全てのインスタンスのＦの値の集合をran(Ｃ_Ｆ)と表現している。関数「Ｃ_Ｆ」は、ＣインスタンスとＦの型に属する値の組の集合である。なお、記号“∈/”および図面の類似表示は、∈の否定を表わす。
【００４６】
アクティビティ図（４０２）で、さらに制御フローを１回たどって到達するアクションノードＳ４０２は、１個の論理式と２個の代入式を持ち、論理式が真であることを確認した後に、各代入式を実行する。論理式「新規商品∈/商品」は、変数「新規商品」がクラス「商品」のインスタンスの集合に含まれないことを意味する。代入式「商品:=商品∪{新規商品}」は、「商品」インスタンスの集合と「新規商品」からなる集合の集合和を新たな「商品」インスタンスの集合とすることを意味する。これは、データベースの表「商品」に行「新規商品」を追加したことを表している。代入式「商品_商品ＣＤ:=商品_商品ＣＤ∪{新規商品|→新規ＣＤ}」は、「商品」インスタンスと非空文字列の組の集合である「商品_商品ＣＤ」と、「新規商品」と「新規ＣＤ」の組からなる集合との集合和を、新たな「商品_商品ＣＤ」とすることを意味する。これは、データベースの表「商品」に追加された行「新規商品」の列「商品ＣＤ」の値として変数「新規ＣＤ」の値を設定することを表している。なお、記号“|→”および図面の類似表示は、元の対応を表わす。
【００４７】
アクティビティ図（４０２）で、さらに制御フローを１回たどって到達する終了ノードは、逐次処理を終了することを表す。
【００４８】
なお、図４のアクションノードＳ４０１およびＳ４０２における、“check”は、これに続く式が論理式であることを意味し、“do”は、これに続く式が代入式であることを意味する。“check”と“do”は、読みやすさのために付与したものであり、省略可能である。
【００４９】
《識別子情報生成処理：Ｓ３０３》
図５は、本実施形態に係る識別子情報生成処理（Ｓ３０３）の手順を示すフローチャートである。
【００５０】
情報処理装置２００は、既定識別子情報格納部２０４から既定識別子情報（図７参照）を読み込む（ステップＳ５０１）。そして、情報処理装置２００は、読み込んだ既定識別子情報を識別子情報２４４に転記する（ステップＳ５０３：図６の(a)参照）。このとき、既定欄に“true”を設定する。
【００５１】
次に、情報処理装置２００は、クラス図（４０１）から識別子を抽出し、識別子情報２４４に登録する（ステップＳ５０５：図６の(b)参照）。クラスごとに２つの識別子を抽出し、クラスのメンバ属性ごとに１つの識別子を抽出する。
【００５２】
次に、情報処理装置２００は、アクティビティ図（４０２）から、まだ識別子情報２４４に登録されていない変数を抽出し、識別子情報２４４に登録する（ステップＳ５０７：図６の(c)参照）。
【００５３】
さらに、情報処理装置２００は、アクティビティ図（４０２）において、代入式の両辺に出現する変数について、代入実行前の変数の値を保持する変数（以降、事前変数と称す）を導入し、識別子情報２４４に登録する（ステップＳ５０９：図６の(d)参照）。
【００５４】
（識別子情報）
図６は、本実施形態に係る生成された識別子情報２４４の構成を示す図である。ステップＳ３０３において生成された識別子情報２４４は、識別子情報格納部２８０に検索可能に格納される。
【００５５】
識別子情報２４４（２８０）は、識別子６０１に対応付けて、基本型６０２と、分類６０３と、静的制約６０４と、規定６０５と、を記憶する。識別子６０１は、クラス図およびアクティビティ図が含む全てのクラス名、メソッド名、変数名、定数名などである。基本型６０２は、識別子６０１として記述可能なあるいは代入可能な値を決めるものである。分類６０３は、識別子６０１が集合を表わすか、要素を表わすかを示す。静的制約６０４は、識別子６０１の不変条件である。規定６０５は、識別子６０１が既定識別子か否かを表わす（既定識別子=true／非既定識別子=faise）。
【００５６】
そして、図６の右端には、上記図５の各ステップで生成された識別子情報が示されている。以下、上記図５の各ステップにおける識別子情報の生成を詳細に説明する。
【００５７】
（識別子情報の(a)生成：Ｓ５０１、Ｓ５０３）
情報処理装置２００は、既定識別子情報格納部２０４から既定識別子情報を読み込み（ステップＳ５０１）、読み込んだ既定識別子情報を識別子情報２４４（図６の(a)）に転記する（ステップＳ５０３）。このとき、既定欄に“true”を設定する。
【００５８】
（既定識別子情報）
図７は、本実施形態に係る既定識別子情報格納部２０４の既定識別情報の構成を示す図である。
【００５９】
既定識別子情報は、ソフトウェアの設計で必要となる典型的な定数と、定数が属する基本的な型（以降、基本型）と、集合か要素であるかの分類と、識別子間に常に成り立つ制約（以降、静的制約）と、を含む。静的制約は、ソフトウェアが行う処理の影響を受けずに、常に成り立つべき条件である。
【００６０】
図４の具体例によれば、識別子「文字列」は、基本型が「文字列」自体であり、集合に分類され、静的制約を持たない。識別子「空文字列」は、基本型が「文字列」であり、要素に分類され、「空文字列は文字列の要素である（空文字列∈文字列）」という静的制約を持つ。識別子「非空文字列」は、基本型が「文字列」であり、集合に分類され、「非空文字列は文字列から空文字列を除いた集合である（非空文字列=文字列＼{空文字列}）」（記号“＼”および図面の類似表示は差集合を表わす）という静的制約を持つ。
【００６１】
（識別子情報の(b)生成：Ｓ５０５）
情報処理装置２００は、クラス図（４０１）から識別子を抽出し、識別子情報（図６の(b)）に登録する（ステップＳ５０５）。クラスごとに２つの識別子を抽出し、クラスのメンバ属性ごとに１つの識別子を抽出する。
【００６２】
クラスの名称が「Ｃ」のとき、１つ目の識別子として「Ｃ型」を導入する。「Ｃ型」の識別子情報は、基本型を「Ｃ型」、分類を「集合」、静的制約を持たず、既定を“false”とする。２つ目の識別子「Ｃ」の識別子情報は、基本型を「Ｃ型」、分類を「集合」、静的制約を持たず、既定欄を“false”とする。
【００６３】
メンバ属性の名称が「Ｍ」のとき、識別子として「Ｃ_Ｍ」を導入する。「Ｃ_Ｍ」の識別子情報は、基本型を「Ｃ型」から「Ｍ」の型の基本型への半関数（Ｃ型+-＞Ｍの型の基本型）、分類を「集合」、特別な制約がなければ「ＣからＭの型への半関数である（Ｃ+-＞Ｍの型）」という静的制約を持ち、既定欄を“false”とする。
【００６４】
図４のクラス図（４０１）によれば、「商品」クラスの「商品ＣＤ」メンバ属性には、ステレオタイプ「＜＜pk＞＞」によって、「商品ＣＤ」によって「商品」クラスのオブジェクトが一意に識別できる、という制約が付与されている。したがって、図６の識別子「商品_商品ＣＤ」は、「商品」から「商品ＣＤ」の型である「非空文字列」への全域単射関数である（商品_商品ＣＤ∈商品|→非空文字列）、という静的制約をもつ。
【００６５】
（識別子情報の(c)生成：５０７）
情報処理装置２００は、アクティビティ図（４０２）から、まだ識別子情報に登録されていない変数を抽出し、識別子情報（図６の(c)）に登録する（ステップＳ５０７）。
【００６６】
変数ｖの識別子情報において、ｖの基本型は、その変数が初めて出現する論理式あるいは代入式において、ｖと比較あるいは代入される定数や変数の基本型とする。また、ｖの分類は、前記式において、ｖと比較あるいは代入される定数や変数の分類と、比較演算子あるいは代入演算子の種類と、によって決める。
【００６７】
図４のアクティビティ図（４０２）で、変数「商品ＣＤ」は、論理式「商品ＣＤ≠空文字列」において、「空文字列」と比較されており、「空文字列」の基本型は「文字列」なので（図８の(a)参照）、「商品ＣＤ」の基本型は「文字列」とする。また、「空文字列」の分類は「要素」であり、上述の式では「商品ＣＤ」を要素とは同じではない（≠）としているので、「商品ＣＤ」の分類は「要素」とする。
【００６８】
変数「新規商品」は、論理式「新規商品∈/商品」において、「商品」と比較されており、「商品」の基本型は「商品型」なので（図８の(b)参照）、「新規商品」の基本型は「商品型」となる。また、「商品」の分類は「集合」であり、上述の式では「新規商品」を集合の要素ではない（∈/）としているので、「新規商品」の分類も「要素」とする。
【００６９】
（識別子情報の(d)生成：Ｓ５０９）
さらに、局所事後条件生成部２０２は、アクティビティ図（４０２）において、代入式の両辺に出現する変数について、代入実行前の変数の値を保持する変数（以降、事前変数）を導入し、識別子情報（図６の(d)）に登録する（ステップＳ５０７）。
【００７０】
変数ｖに対応する事前変数は、識別子をpre_ｖ、基本型をｖの基本型、分類をｖの基本型とし、ｖに静的制約があれば、そこに出現する変数のうち対応する事前変数があるものを全て事前変数で置換した式をpre_ｖの静的変数とする。
【００７１】
図４のアクティビティ図（４０２）によれば、代入式「商品:=商品∪{新規商品}」の両辺に「商品」が、代入式「商品_商品ＣＤ:=商品_商品ＣＤ∪{新規商品|→商品ＣＤ}」の両辺に「商品.商品ＣＤ」が出現するので、それぞれについて事前変数「pre_商品」と「pre_商品_商品ＣＤ」を導入する。識別子「商品_商品ＣＤ」は静的制約「商品_商品ＣＤ∈商品|→非空文字列」を持つので、対応する事前変数「pre_商品_商品ＣＤ」は静的制約「pre_商品_商品ＣＤ∈pre_商品|→非空文字列」を持つこととする。
【００７２】
《局所事後条件情報生成処理：Ｓ３０５》
図８は、本実施形態に係る局所事後条件情報生成処理（Ｓ３０５）の手順を示すフローチャートである。
【００７３】
情報処理装置２００は、アクティビティ図（４０２）の開始ノードから制御フローをたどってノードを探索して、ノードに番号（以降、ノード番号）を割り当てる（ステップＳ８０１）。そして、ノード番号の割り当てに続いて、情報処理装置２００は、アクションノードの式をもとに、局所事後条件情報２４５Ａを生成する（ステップＳ８０３：図１０参照）。
【００７４】
次に、情報処理装置２００は、条件追加ルール格納部２０５から条件追加ルール（図１１参照）を読み込む。そして、情報処理装置２００は、前述の局所事後条件情報２４５Ａ（図１０）の各局所事後条件が追加ルール格納部の照合条件と合致すれば、対応する追加条件を追加して局所事後条件情報２４５Ｂを生成する（図１２参照）。このとき、開始番号欄と枝番欄は合致した局所事後条件と同じ値とし、区分欄は「追加」とする。
【００７５】
そして、情報処理装置２００は、追加後の局所事後条件情報２４５Ｂ（図１２）を調べて、局所事後条件の有効範囲を特定し、終了番号を追記した局所事後条件情報２４５Ｃを得る（ステップＳ８０７：図１３参照）。この終了番号を追記した局所事後条件情報２４５Ｃが、局所事後条件情報格納部２９０に格納される。
【００７６】
以下、上記図８の各ステップにおける局所事後条件情報の生成を詳細に説明する。
【００７７】
（ノード番号割り当て：Ｓ８０１）
図９は、本実施形態に係るノード番号割り当てを示す図である。情報処理装置２００は、アクティビティ図（４０２）の開始ノードから制御フローをたどってノードを探索して、ノード番号を割り当てる（ステップＳ８０１）。
【００７８】
ノード番号割り当ては、次のアルゴリズムに従う。
(1) 開始ノードのノード番号を“０”とする。
(2) 先行するノードから制御フローを１回たどって到達するノードのノード番号は、先行ノードのノード番号に“１”を加えた値とする。
(3) すでにノード番号を割り当て済みのノードに到達した場合、そのノードが開始ノードから直前にノード番号を割り当てたノードまでの経路上に出現しているか、経路上には出現していないが新たに割り当てようとしたノード番号よりも割り当て済みのノード番号が大きければ、探索をやめる。そして、制御フローを逆向きにたどり、まだ辿ったことのない制御フローが見つかれば、その制御フローに沿ってノード番号を割り当てるための探索を行う。
(4) 到達したノード（到達ノード）のノード番号が割り当て済みで、かつそのノードが前述の経路上に出現しておらず、かつ新たに割り当てようとした値よりも割り当て済みのノード番号が小さければ、新たな値でノード番号を上書きする。そして、新たな値と割り当て済みのノード番号との差分を、到達ノードの後続の全てのノードのノード番号に加える。さらに、到達ノードから制御フローを逆にたどり、まだ辿ったことのない制御フローが見つかれば、その制御フローに沿ってノード番号を割り当てるための探索を行う。
(5) 全てのノードにノード番号を割り当てれば、アクティビティ図（４０２）の探索を終える。
【００７９】
図９には、上記アルゴリズムに従って、アクティビティ図（４０２）について、ノード番号を割り当てたアクティビティ図（９０２）を示す。
【００８０】
（アクティビティ図を元に局所事後条件情報生成：Ｓ８０３）
図１０は、本実施形態に係るアクティビティ図を元に生成された局所事後条件情報２４５Ａの構成を示す図である。局所事後条件情報２４５Ａは、ＲＡＭ２４０の局所事後条件情報２４５に一時記憶される。
【００８１】
局所事後条件情報２４５Ａにおいて、各局所事後条件１００５は、有効範囲の開始となるノード番号である開始番号１００１と、論理式か代入式かを示す枝番１００２と、有効範囲の終了となるノード番号である終了番号１００３と、有効／無効／新規などの区分１００４とを有する。
【００８２】
アクションノードの式が論理式である場合は、その論理式をそのまま局所事後条件とする。
【００８３】
また、アクションノードの式が代入式であり、代入式の両辺に同じ変数が出現しない場合は、代入式の代入演算子を等価演算子などに置き換えて得られる論理式を、局所事後条件とする。例えば、右辺の値を左辺に代入する代入演算子「:=」は等価演算子「=」に、右辺の集合から任意に選んだ要素を左辺に代入する代入演算子「:∈」は左辺の要素が右辺の集合に属することを意味する演算子「∈」に置き換える。
【００８４】
また、アクションノードの式が代入式であり、代入式の両辺に同じ変数が出現する場合は、その変数に対応する事前変数とその変数との等式を１つめの局所事後条件とする。そして、右辺に出現する変数のうち対応する事前変数がある変数を全て事前変数に置き換えた代入式について、代入式の代入演算子を等価演算子などに置き換えて得られる論理式を２つめの局所事後条件とする。
【００８５】
局所事後条件情報の開始番号欄にはアクションノードのノード番号を設定し、枝番欄にはアクションノードの式が論理式であれば“０”を設定し、代入式であれば“１”を設定する。また、区分欄には、事前変数と変数との等式の場合は「追加」を設定し、それ以外の場合は「有効」を設定し、局所事後条件欄には上記で生成した局所事後条件を設定する。
【００８６】
例えば、図９のアクティビティ図（９０２）で、ノード番号１のアクションノードＳ４０１における論理式「新規ＣＤ≠空文字列」は、そのまま局所事後条件となり、図１０の局所事後条件情報２４５Ａでは、１行目〜３行目として登録されている。
【００８７】
ノード番号２のアクションノードＳ４０２における代入式「商品:=商品∪{新規商品}」は、両辺に「商品」が出現するので、まず、事前変数との等式「pre_商品=商品」を局所事後条件として、局所事後条件情報に登録する（図１０の４行目）。続いて、もとの代入式から右辺の変数を事前変数で置き換えた代入式「商品:=pre_商品∪{新規商品}」を得る。さらに、代入演算子「:=」を等価演算子「=」に置き換えて得られる論理式「商品=pre_商品∪{新規商品}」を局所事後条件として、局所事後条件情報に登録する（図１０の５行目）。
【００８８】
（局所事後条件追加：Ｓ８０５）
情報処理装置２００は、条件追加ルール格納部２０５から条件追加ルール（図１１）を読み込み、図１０の局所事後条件情報２４５Ａの各局所事後条件が追加ルール格納部の照合条件と合致すれば、対応する追加条件を追加した局所事後条件情報２４５Ｂ（図１２）を生成する。このとき、開始番号欄と枝番欄は合致した局所事後条件と同じ値とし、区分欄は「追加」とする。
【００８９】
（条件追加ルール）
図１１は、本実施形態に係る条件追加ルールの構成を示す図である。条件追加ルールは、条件追加ルール格納部２０５に格納されている。
【００９０】
条件追加ルールは、パラメータ１１０１に対応付けて、追加するか否かの照合条件１１０２と、照合した場合に追加する追加条件１１０３とを格納する。
【００９１】
（条件追加後の局所事後条件情報）
図１２は、本実施形態に係る条件追加後の局所事後条件情報２４５Ｂの構成を示す図である。
【００９２】
図１０の局所事後条件情報２４５Ａによれば、図１０の１行目の局所事後条件「新規ＣＤ≠空文字列」は、図１１の１行目の条件追加ルールの照合条件「e≠空文字列」について、パラメータ「e」を「新規ＣＤ」と見なした式に合致する。したがって、照合条件に対応する追加条件「e∈非空文字列」のパラメータ「e」を「新規ＣＤ」で置き換えて得られる式「新規ＣＤ∈非空文字列」を新たな局所事後条件として、局所事後条件情報に追加する（図１２の２行目）。このようにして得られる局所事後条件情報２４５Ｂ（図１２）では、区分欄の「追加」を破線で囲んだ２行目と７行目と１０行目と１１行目とに局所事後条件１２１０が追加されている。
【００９３】
（有効範囲生成：Ｓ８０７）
情報処理装置２００は、局所事後条件情報２４５Ｂ（図１２）を調べて、局所事後条件の有効範囲を特定し、終了番号を追記した局所事後条件情報２４５Ｃ（図１３）を得る（ステップＳ８０７）。
【００９４】
局所事後条件の有効範囲は、局所事後条件情報の開始番号と終了番号で示す。局所事後条件は、前記開始番号をノード番号とするアクションノードの実行直後から終了番号をノード番号とするアクションノードの実行直前まで成立する。終了番号が無い場合には、局所事後条件は、開始番号をノード番号とするアクションノードの実行直後から逐次処理全体の終了まで成立する。情報処理装置２００は、局所事後条件情報２４５Ｂの各行について、当該行と開始番号が同じで枝番が大きい行および当該行よりも開始番号が大きい行の局所事後条件を調べて、当該行の変数が出現する最初の行が見つかれば、その行の開始番号を当該行の終了番号に設定することを繰り返す。さらに、情報処理装置２００は、局所事後条件情報の各行において、終了番号が開始番号と同じ行があれば、その行の区分欄に「無効」を設定する。
【００９５】
（有効範囲設定後の局所事後条件情報）
図１３は、本実施形態に係る有効範囲設定後の局所事後条件情報２４５Ｃの構成を示す図である。
【００９６】
図１２の局所事後条件情報２４５Ｂによれば、図１２の４行目の局所事後条件「新規商品∈/商品」の開始番号は“２”、枝番は“０”である。したがって、開始番号が“２”で枝番が“０”より大きい行（図１２の５行目から最後まで）と、開始番号が“２”よりも大きい行（図１２にはなし）とを調べ、４行目の局所事後条件に出現する変数「新規商品」が最初に出現する７行目の開始番号“２”を４行目の終了番号に設定する。これにより、４行目は、開始番号と終了番号が同じ“２”となるので、その区分欄に「無効」を設定する（図１３の４行目）。このようにして得られる局所事後条件情報２４５Ｃ（図１３）では、１行目から４行目までの終了番号欄に有効範囲の終了を示す“２”が設定され（１３１０）、４行目の区分欄に「無効」が設定されている。
【００９７】
本実施形態によれば、フローチャートやアクティビティ図の各アクションノードに対して一意のノード番号を割り振るので、各アクションノードごとに処理の流れや局所事後条件の有効範囲などに基づくソフトウェアの設計内容の緻密な整合性検証をすることができる。
【００９８】
例えば、本実施形態によれば、アクティビティ図でのアクションノードの実行順序どおりにEvent-Bイベントを実行することを保証できる。その理由は、アクティビティ図のノードにノード番号を付与し、アクティビティ図の有向線分に沿った順序で、開始ノードを“０”とし後続の未割当てのノードに連番を割り当てる。これにより、番号Ｘのアクションノードの後続のアクションノードでは、その前提条件として「直前に実行されたノード番号がＸであること」という条件を明示できるからである。
【００９９】
また、本実施形態によれば、アクティビティ図の各アクションノードの実行結果をEvent-Bの不変条件として明示できる。その際に、局所事後条件の有効範囲も明示できる。その理由は、アクティビティ図のアクションノードにある条件（論理式）をチェックすべきことが記述されていれば、その条件をそのまま局所事後条件とし、データに値を代入することが記述されていれば代入式における代入演算子を等価演算子に置換した論理式を局所事後条件とするからである。また、局所事後条件全体を調べて、ある変数についてノードＸと後続のノードＹで局所事後条件があれば、ノードＸにおける局所事後条件はＸの直後からＹの直前までである。したがって、ノードＹにおける局所事後条件はＹの直後から（逐次処理の終了まで）であることを特定し、ノード番号を用いて有効範囲の開始と終了を示すからである。
【０１００】
［第３実施形態］
次に、本発明の第３実施形態に係る情報処理装置について説明する。本実施形態に係る情報処理装置は、上記第２実施形態と比べると、生成した識別子情報と有効範囲を有する局所事後条件情報とに基づいてソフトウェア処理の形式記述を生成する点で異なる。その他の構成および動作は、第２実施形態と同様であるため、同じ構成および動作については同じ符号を付してその詳しい説明を省略する。
【０１０１】
なお、本実施形態では、形式手法の１つであるEvent-Bに生成した識別子情報と有効範囲を有する局所事後条件情報とを適用するが、形式手法はEvent-Bに限定されない。Event-Bでは、対象システムが扱うデータをEvent-Bにおける定数や変数として宣言し、データ構造やデータに関する制約を集合や一階述語論理に基づく論理式である不変条件として記述する。また、対象システムが行う処理を、その処理を実行すべきことを論理式で表したEvent-Bガードと、その処理が実行することを代入式で表したEvent-BアクションからなるEvent-Bイベントとして記述する。
【０１０２】
《情報処理装置の機能構成》
図１４Ａは、本実施形態に係る情報処理装置１４００の機能構成を示すブロック図である。なお、図１４Ａにおいて、図２Ａと同様の機能構成部には同じ参照番号を付して、説明を省略する。
【０１０３】
図１４Ａの情報処理装置１４００は、図２Ａと同じ入力処理部２０１を有する。局所事後条件生成部１４０２は、生成した識別子情報と局所事後条件情報とをそのまま、情報処理装置１４００内部の識別子情報格納部１４０８と局所事後条件情報格納部１４０９とに格納する。図１４Ａの情報処理装置１４００は、入力処理部２０１によって読み込まれた設計情報と局所事後条件生成部１４０２によって生成された識別子情報と局所事後条件とを用いて形式記述を生成する形式記述生成部１４０６を有する。また、情報処理装置１４００は、形式記述生成部１４０６によって生成された形式記述を形式記述格納部１４９０に出力する形式記述出力処理部１４０７を有する。
【０１０４】
《情報処理装置のハードウェア構成》
図１４Ｂは、本実施形態に係る情報処理装置１４００のハードウェア構成を示すブロック図である。図１４Ｂにおいて、図２Ｂと同様の構成要素には同じ参照番号を付して、説明を省略する。
【０１０５】
情報処理装置１４００は、ＲＡＭ１４４０に、生成されEvent-Bコンテキスト１４４８と、生成されたEvent-Bマシン１４４９と、を記憶する。
【０１０６】
また、情報処理装置１４００は、ストレージ１４５０に、識別子情報格納部１４０８と、局所事後条件情報格納部１４０９と、を有する。また、ストレージ１４５０に、形式記述を生成するために使用される形式記述生成アルゴリズム１４５１を記憶する。また、情報処理装置１４００を制御する情報処理装置制御プログラム１４５４は、以下のモジュールを有する。１つは、形式記述生成アルゴリズム１４５１に従って、識別子情報格納部１４０８の識別子情報と局所事後条件情報格納部１４０９の有効範囲を有する局所事後条件情報とから形式記述（本例では、Event-B）を生成する形式記述生成モジュール１４５７である。もう１つは、情報処理装置制御プログラム１４５４は、生成された形式記述を形式記述格納部１４９０に格納する形式記述出力処理モジュール１４５８である。
【０１０７】
また、入出力インタフェース１４６０には、生成した形式記述を格納する形式記述格納部１４９０が接続される。
【０１０８】
なお、図１４ＢのＲＡＭ１４４０やストレージ１４５０には、情報処理装置１４００が有する汎用の機能や他の実現可能な機能に関連するプログラムやデータは図示されていない。
【０１０９】
《情報処理装置の処理手順》
図１５は、本実施形態に係る情報処理装置１４００の処理手順を示すフローチャートである。このフローチャートは、図１４ＢのＣＰＵ２１０がＲＡＭ１４４０を使用して実行し、図１４Ａの機能構成部を実現する。
【０１１０】
設計情報の読み込み（ステップＳ３０１）から局所事後条件情報の生成（ステップＳ３０５）までは、図３と同様の処理を行うので、説明を省く。続く、形式記述の生成（ステップＳ１５０７）と形式記述の書き出し（ステップＳ１５０９）は、図１５で追加された動作である。なお、ステップＳ１５０９は単なる生成したデータの書き出し処理なので、説明を省き、図１６のフローチャートを用いてステップＳ１５０７の動作を詳細に説明する。
【０１１１】
なお、形式記述とは、ソフトウェアの仕様や設計内容を形式手法の記法を用いて表現した情報を指す。ここでは具体的な形式手法としてEvent-Bを用いて説明し、Event-Bの記法による形式記述をＥvent-B記述と呼ぶこととする。Event-B記述は、基本的な集合や定数の集まりからなるコンテキストと、変数と変数に関する制約と変数の値を更新するイベントの集まりからなるマシンと、からなる。コンテキストは他のコンテキストを拡張できる。マシンはコンテキストを参照する。参照されるコンテキストが他のコンテキストを拡張したものであれば、マシンは拡張元のコンテキストも参照することになる。ここでは、コンテキストＣ０に文字列といった基本的な型や定数を記述する。また、コンテキストＣ０を拡張したコンテキストＣにクラス図（４０１）から得られる基本的な型と定数を記述する。そして、コンテキストＣを参照するマシンＭにクラス図（４０１）から得られる変数とアクティビティ図（４０２）から得られるアクションノードの処理内容を記述することとする。
【０１１２】
《形式記述生成処理》
図１６は、本実施形態に係る形式記述生成処理（Ｓ１５０７）の手順を示すフローチャートである。
【０１１３】
まず、情報処理装置１４００は、識別子情報を調べてEvent-Bにおける定数とすべき識別子を抽出して、Event-B記述（Event-Bコンテキスト）を生成する（ステップＳ１６０１）。
【０１１４】
次に、情報処理装置１４００は、定数に関する記述の生成に続いて、識別子情報を調べてEvent-Bにおける変数とすべき識別子を抽出して、Event-B記述（Event-Bマシン）を生成する（ステップＳ１６０３）。
【０１１５】
次に、情報処理装置１４００は、変数に関する記述の生成に続いて、アクティビティ図を調べてEvent-Bにおけるイベントを抽出して、ステップＳ１６０３で生成したEvent-Bマシンに追記する（ステップＳ１６０５）。
【０１１６】
そして、情報処理装置１４００は、イベントに関する記述の生成に続いて、局所事後条件情報を調べてEvent-Bにおける不変条件を抽出して、ステップＳ１６０５で追記されたEvent-Bマシンに不変条件をさらに追記する（ステップＳ１６０７）。
【０１１７】
以下、図１６の各ステップの処理を詳細に説明する。
【０１１８】
（定数に関する記述の生成：Ｓ１６０１）
まず、情報処理装置１４００は、識別子情報を調べてEvent-Bにおける定数とすべき識別子を抽出して、Event-B記述（コンテキスト）を生成する（ステップＳ１６０１）。
【０１１９】
ステップＳ１６０１では、まずコンテキストＣ０を生成し、次にコンテキストＣを生成する。情報処理装置１４００は、識別子情報において既定欄が“true”である行を、コンテキストＣ０に記述する。情報処理装置１４００は、識別子欄と基本型欄の値が同じであれば、コンテキストＣ０のsets節に識別子を記述する。情報処理装置１４００は、識別子欄と基本型欄の値が異なれば、コンテキストＣ０のconstants節に識別子を記述する。情報処理装置１４００は、constants節に記述された識別子については、分類欄が「集合」であれば、識別子が基本型の部分集合であるという論理式「識別子⊆基本型」を記述する。また、情報処理装置１４００は、分類欄が「要素」であれば、識別子が基本型の要素であるという論理式「識別子∈基本型」をaxiom節に記述する。情報処理装置１４００は、さらに静的制約欄に記述があれば、それもaxiom節に記述する。
【０１２０】
（Event-Bコンテキスト）
図１７は、本実施形態に係る形式記述としてのEvent-BコンテキストＣ０（１４４８Ａ）の記述を示す図である。Event-Bコンテキスト１４４８Ａは、Event-Bコンテキスト１４４８ＢおよびEvent-Bマシン１４４９Ｃと関連付けて検索可能に形式記述格納部１４９０に格納される。図１７は、図６の識別子情報において既定欄が“true”である１行目から３行目を元に生成されたコンテキストＣ０を示す。
【０１２１】
また、情報処理装置１４００は、識別子情報において既定欄が“false”であり、かつ識別子欄と基本型欄の値が同じ行を、コンテキストＣに記述する。コンテキストＣのsets節に識別子を記述する。
【０１２２】
（拡張したEvent-Bコンテキス）
図１８は、本実施形態に係る拡張したEvent-BコンテキストＣ（１４４８Ｂ）の記述を示す図である。Event-Bコンテキスト１４４８Ｂは、Event-Bコンテキスト１４４８ＡおよびEvent-Bマシン１４４９Ｃと関連付けて検索可能に形式記述格納部１４９０に格納される。図１８は、図６の識別子情報において既定欄が“false”であり、識別子欄と基本型欄の値がともに「商品型」である４行目を元に生成されたコンテキストＣを示す。コンテキストＣの１行目の記述「extends C0」は、コンテキストＣがコンテキストＣ０を拡張することを示す。
【０１２３】
（変数に関する記述の生成：Ｓ１６０３）
定数に関する記述の生成に続いて、情報処理装置１４００は、識別子情報を調べてEvent-Bにおける変数とすべき識別子を抽出して、Event-B記述（マシン）を生成する（ステップＳ１６０３）。
【０１２４】
情報処理装置１４００は、識別子情報において既定欄が“false”であり、かつ識別子欄と基本型欄の値が異なる行を、マシンＭに記述する。Ｍのvariables節には、識別子を記述する。情報処理装置１４００は、variables節に続くinvariants節には、識別子情報の静的制約欄に記述がなく、かつ分類欄が「集合」であれば、識別子が基本型の部分集合であるという論理式「識別子⊆基本型」を記述する。また、情報処理装置１４００は、識別子情報の静的制約欄に記述がなく、分類欄が「要素」であれば、識別子が基本型の要素であるという論理式「識別子∈基本型」をinvariants節に記述する。一方、静的制約欄に記述があれば、それを記述する。情報処理装置１４００は、invariants節に続く、events節のinitializationイベントには、識別子情報の分類欄が「集合」であれば、識別子の初期値を空集合とする代入式「識別子:=Φ」（記号Φおよび図面の類似表示は空集合を表わす）を記述する。一方、情報処理装置１４００は、分類欄が「要素」であれば、識別子の初期値を基本型から任意に選んだ要素とする代入式「識別子:∈基本型」を記述する。
【０１２５】
（ノード番号および有効範囲の無いEvent-Bマシン）
図１９は、本実施形態に係るノード番号および有効範囲の無い形式記述としてのEvent-Bマシン１４４９Ａの記述を示す図である。Event-Bマシン１４４９Ａは、ＲＡＭ１４４０のEvent-Bマシン１４４９に一時記憶される。なお、図１９で空白のライン番号は、ステップＳ１６０３においては、まだ生成していない記述であり、本実施形態のようにノード番号割り当てによる先行ノードの局所事前条件、あるいは、局所事後条件の有効範囲設定がなければ、図１９の形式記述が生成されるのみである。
【０１２６】
（イベントに関する記述の生成：Ｓ１６０５）
変数に関する記述の生成に続いて、情報処理装置１４００は、アクティビティ図を調べてEvent-Bにおけるイベントを抽出して、ステップＳ１６０３で生成したEvent-Bマシンに追記する（ステップＳ１６０５）。
【０１２７】
（ノード番号追加後のEvent-Bマシン）
図２０は、本実施形態に係るノード番号追加後のEvent-Bマシン１４４９Ｂの記述を示す図である。Event-Bマシン１４４９Ｂは、ＲＡＭ１４４０のEvent-Bマシン１４４９に一時記憶される。なお、図２０で空白のライン番号は、後述のステップＳ１６０７において生成される有効範囲を有する局所事後条件情報の記述領域である。
【０１２８】
まず、情報処理装置１４００は、直前に実行されたノードのノード番号を保持する変数sc（step counter）を導入して、マシンのvariables節にsc２００１を追記する。また、情報処理装置１４００は、invariants節にscが整数であることを示す論理式「sc∈INT」２００２を追記する。そして、情報処理装置１４００は、initializationイベントにscの初期値が“０”であることを示す代入式「sc:=0」２００３を追記する。
【０１２９】
次に、情報処理装置１４００は、開始ノードを起点として制御フローをたどって到達するノードごとに、Event-Bイベント「stepノード番号」２０１１を追記する。また、情報処理装置１４００は、局所事前条件追加処理として、Event-Bイベント「stepノード番号」のEvent-Bガード(Guard)には「sc=当該ノードの直前に実行されたノードのノード番号」２０１２を記述する。さらに、情報処理装置１４００は、Event-Bアクションには「sc:=当該ノードのノード番号」２０１３を記述する。これらのEvent-BガードとEvent-Bアクションの記述によって、アクティビティ図における制御フローのどおりに、各Event-Bイベントが実行されることが保証される。
【０１３０】
さらに、情報処理装置１４００は、当該ノードに記述された論理式を当該ノードに対応するEvent-BイベントのEvent-Bガードに追記し、当該ノードに記述された代入式をEvent-Bアクションに追記する。情報処理装置１４００は、代入式の両辺に同じ変数が出現する場合には、「pre_変数:=変数」という代入式をEvent-Bアクションに追記する。
【０１３１】
なお、本実施形態のようにノード番号割り当てによる先行ノードの局所事前条件、あるいは、局所事後条件の有効範囲設定がなければ、図２０の形式記述のEvent-bマシンには変数scは導入されない。その結果、Event-Bイベントには、「stepノード番号」２０１１も、Event-Bガードの「sc=当該ノードの直前に実行されたノードのノード番号」２０１２も、Event-Bアクションの「sc:=当該ノードのノード番号」２０１３も記述されない。
【０１３２】
（局所事後条件に関する記述の生成：Ｓ１６０７）
イベントに関する記述の生成に続いて、情報処理装置１４００は、局所事後条件情報を調べてEvent-Bにおける不変条件を抽出して、ステップＳ１６０５で追記されたEvent-Bマシンに不変条件を追記する（ステップＳ１６０７）。
【０１３３】
情報処理装置１４００は、局所事後条件情報のうち区分欄が「有効」である行について、終了番号に記述がなければ、論理式「開始番号≦sc ⇒ ( 局所事後条件 )」を、Event-Bマシンのinvariant節に追記する。また、情報処理装置１４００は、終了番号に記述があれば、論理式「開始番号≦sc ∧ sc＜終了番号 ⇒ ( 局所事後条件 )」を、Event-Bマシンのinvariant節に追記する。ここで、⇒は論理の含意（〜ならば）、∧は論理積を表す。なお、上記例では、区分欄が「有効」である行について局所事後条件として記述したが、図１２の他の区分欄が「追加」である行により代用することもできる。
【０１３４】
（有効範囲のある局所事後条件設定後のEvent-Bマシン）
図２１は、本実施形態に係る有効範囲のある局所事後条件設定後のEvent-Bマシン１４４９Ｃの記述を示す図である。Event-Bマシン１４４９Ｃは、Event-Bコンテキスト１４４８ＡおよびEvent-Bコンテキスト１４４８Ｂと関連付けて検索可能に形式記述格納部１４９０に格納される。図２１は、図４のアクティビティ図（４０２）と図１３の局所事後条件情報２４５Ｃを元に生成されたマシンＭを示す。Ｍの１行目の記述「sees C」は、ＭがコンテキストＣを参照することを示す。
【０１３５】
本実施形態によれば、生成した形式記述において、アクティビティ図でのアクションノードの実行順序どおりにEvent-Bイベントを実行できる。また、生成した形式記述において、アクティビティ図の各アクションノードの実行結果をEvent-Bの不変条件にできる。
【０１３６】
［他の実施形態］
以上、実施形態を参照して発明を説明したが、発明は上記実施形態に限定されるものではない。発明の構成や詳細には、本願発明のスコープ内で当業者が理解し得る様々な変更をすることができる。また、それぞれの実施形態に含まれる別々の特徴を如何様に組み合わせたシステムまたは装置も、本発明の範疇に含まれる。
【０１３７】
また、本発明は、複数の機器から構成されるシステムに適用されてもよいし、単体の装置に適用されてもよい。さらに、本発明は、実施形態の機能を実現する情報処理プログラムが、システムあるいは装置に直接あるいは遠隔から供給される場合にも適用可能である。したがって、本発明の機能をコンピュータで実現するために、コンピュータにインストールされるプログラム、あるいはそのプログラムを格納した媒体、そのプログラムをダウンロードさせるＷＷＷ(World Wide Web)サーバも、本発明の範疇に含まれる。特に、少なくとも、上述した実施形態に含まれる処理ステップをコンピュータに実行させるプログラムを格納した非一時的コンピュータ可読媒体（non-transitory computer readable medium）は本発明の範疇に含まれる。
【０１３８】
［実施形態の他の表現］
上記の実施形態の一部または全部は、以下の付記のようにも記載されうるが、以下には限られない。
（付記１）
データの静的な構造および制約を記述したクラス図と、データを逐次的に処理するソフトウェアの処理の流れおよび実行内容を記述したアクティビティ図と、からなる設計情報を読み込む入力処理手段と、
ソフトウェアの設計で用いるデータの型または定数を記述した既定識別子情報を読み込み、前記入力処理手段により読み込まれた前記設計情報および前記既定識別子情報から、形式記述の作成に必要となる定数または変数の名称、型および静的制約からなる識別子情報と、前記アクティビティ図に記述された前記実行内容を実行した結果を示す論理式である局所事後条件および該局所事後条件の有効範囲を示す局所事後条件情報と、を生成する局所事後条件生成手段と、
を備える情報処理装置。
（付記２）
前記局所事後条件生成手段は、
前記アクティビティ図に含まれる各ノードに前記ソフトウェアの処理の流れにしたがって一意のノード番号を割り当てるノード番号割当手段と、
前記アクティビティ図に含まれる各ノードの実行内容と前記ノード番号とに基づいて、前記局所事後条件の有効範囲を生成する有効範囲生成手段と、
を含む付記１に記載の情報処理装置。
（付記３）
前記有効範囲生成手段は、前記局所事後条件において有効範囲を示すノードの開始番号とノードの終了番号が等しい場合に、当該局所事後条件を無効とする付記２に記載の情報処理装置。
（付記４）
前記設計情報、前記識別子情報および前記局所事後条件情報を用いて、前記ソフトウェアの仕様を形式手法の記法で表現した形式記述を生成する形式記述生成手段、をさらに備える付記１乃至３のいずれか１項に記載の情報処理装置。
（付記５）
前記形式記述生成手段は、
前記形式記述に対して、前記アクティビティ図に含まれる先行ノードに割り当てられたノード番号を局所事前条件として追加する局所事前条件追加手段と、
前記形式記述に対して、前記有効範囲を記述した局所事後条件を追加する局所事後条件追加手段と、
を含む付記４に記載の情報処理装置。
（付記６）
前記形式記述生成手段は、Ｅｖｅｎｔ−Ｂの形式手法により形式記述を行ない、
前記局所事前条件追加手段は、Ｅｖｅｎｔ−Ｂマシンにおいて、前記ノード番号を変数として追加して、前記ノード番号のアクションノードのガード(Guard)節として先行ノードのノード番号を記述し、
前記局所事後条件追加手段は、Ｅｖｅｎｔ−Ｂマシンにおいて、前記有効範囲としてのノードの開始番号と終了番号とを含んだ局所事後条件を不変条件(Invariants）節に記述する付記５に記載の情報処理装置。
（付記７）
データの静的な構造および制約を記述したクラス図と、データを逐次的に処理するソフトウェアの処理の流れおよび実行内容を記述したアクティビティ図と、からなる設計情報を読み込む入力処理ステップと、
ソフトウェアの設計で用いるデータの型または定数を記述した既定識別子情報を読み込み、前記入力処理ステップにおいて読み込まれた前記設計情報および前記既定識別子情報から、形式記述の作成に必要となる定数または変数の名称、型および静的制約からなる識別子情報と、前記アクティビティ図に記述された前記実行内容を実行した結果を示す論理式である局所事後条件および該局所事後条件の有効範囲を示す局所事後条件情報と、を生成する局所事後条件生成ステップと、
を含む情報処理方法。
（付記８）
前記設計情報、前記識別子情報および前記局所事後条件情報を用いて、前記ソフトウェアの仕様を形式手法の記法で表現した形式記述を生成する形式記述生成ステップ、をさらに含む付記７に記載の情報処理方法。
（付記９）
データの静的な構造および制約を記述したクラス図と、データを逐次的に処理するソフトウェアの処理の流れおよび実行内容を記述したアクティビティ図と、からなる設計情報を読み込む入力処理ステップと、
ソフトウェアの設計で用いるデータの型または定数を記述した既定識別子情報を読み込み、前記入力処理ステップにおいて読み込まれた前記設計情報および前記既定識別子情報から、形式記述の作成に必要となる定数または変数の名称、型および静的制約からなる識別子情報と、前記アクティビティ図に記述された前記実行内容を実行した結果を示す論理式である局所事後条件および該局所事後条件の有効範囲を示す局所事後条件情報と、を生成する局所事後条件生成ステップと、
をコンピュータに実行させる情報処理プログラム。
（付記１０）
前記設計情報、前記識別子情報および前記局所事後条件情報を用いて、前記ソフトウェアの仕様を形式手法の記法で表現した形式記述を生成する形式記述生成ステップ、をさらにコンピュータに実行させる付記９に記載の情報処理プログラム。
【図１】
2014241051.tif 000003
【図２Ａ】
2014241051.tif 000004
【図２Ｂ】
2014241051.tif 000005
【図３】
2014241051.tif 000006
【図４】
2014241051.tif 000007
【図５】
2014241051.tif 000008
【図６】
2014241051.tif 000009
【図７】
2014241051.tif 000010
【図８】
2014241051.tif 000011
【図９】
2014241051.tif 000012
【図１０】
2014241051.tif 000013
【図１１】
2014241051.tif 000014
【図１２】
2014241051.tif 000015
【図１３】
2014241051.tif 000016
【図１４Ａ】
2014241051.tif 000017
【図１４Ｂ】
2014241051.tif 000018
【図１５】
2014241051.tif 000019
【図１６】
2014241051.tif 000020
【図１７】
2014241051.tif 000021
【図１８】
2014241051.tif 000022
【図１９】
2014241051.tif 000023
【図２０】
2014241051.tif 000024
【図２１】
2014241051.tif 000025