(57)【要約】【課題】形式手法による仕様であっても、仕様の検証を容易に行う。【解決手段】複数の処理に課される共通の制約を記述した不変条件および処理の内容を処理ごとに記述した処理内容を含む形式仕様記述データを読み込む読込処理部１１と、読込処理部により読み込まれた形式仕様記述データに含まれる処理に基づいて二つの処理を組み合わせることで生成される処理対および形式仕様記述データを用い、各処理対に含まれる二つの処理が連続して実行し得るか否かを判定し、連続して実行し得る場合に、当該処理対に含まれる二つの処理を、先行処理および後続処理として含む処理順序対に選定する判定処理部１２と、判定処理部により選定された処理順序対を用いて有向グラフを生成する生成処理部１３と、を備える。【選択図】図９
2014099042.tif 000002
【特許請求の範囲】
【請求項１】
複数の処理に課される共通の制約を記述した不変条件および前記処理の内容を前記処理ごとに記述した処理内容を含む形式仕様記述データを読み込む読込処理部と、
前記読込処理部により読み込まれた前記形式仕様記述データに含まれる前記処理に基づいて二つの前記処理を組み合わせることで生成される処理対および前記形式仕様記述データを用い、各前記処理対に含まれる二つの前記処理が連続して実行し得るか否かを判定し、連続して実行し得る場合に、当該処理対に含まれる二つの前記処理を、先行処理および後続処理として含む処理順序対に選定する判定処理部と、
前記判定処理部により選定された前記処理順序対を用いて有向グラフを生成する生成処理部と、
を備えることを特徴とする有向グラフ生成装置。
【請求項２】
前記生成処理部は、前記処理順序対に含まれる前記処理のうち、前記後続処理として出現しない前記処理を、開始処理に選定し、当該開始処理を起点にして前記処理順序対に含まれる前記処理をつないでいくことで、前記有向グラフを生成する、
ことを特徴とする請求項１記載の有向グラフ生成装置。
【請求項３】
前記生成処理部により生成された前記有向グラフを図式化して出力する出力処理部を、さらに備える、
ことを特徴とする請求項１または２記載の有向グラフ生成装置。
【請求項４】
前記処理内容は、前記処理の前提条件および前記処理の実行内容を含み、
前記判定処理部は、各前記処理対について、前記不変条件、前記前提条件および前記実行内容を用いた条件式が真になり得るか否かを判定することで、前記処理対に含まれる二つの前記処理内容が連続して実行し得るか否かを判定する、
ことを特徴とする請求項１〜３のいずれか１項に記載の有向グラフ生成装置。
【請求項５】
前記読込処理部は、前記形式仕様記述データに含まれる前記処理のうち、並列に実行する前記処理を特定するための並列処理データをさらに読み込み、
前記生成処理部は、並列に実行する前記処理を識別可能な状態で前記有向グラフを生成する、
ことを特徴とする請求項１〜４のいずれか１項に記載の有向グラフ生成装置。
【請求項６】
前記読込処理部は、前記形式仕様記述データに含まれる前記処理のうち、入れ子構造を形成する入れ子となる前記処理を特定するための入れ子処理データをさらに読み込み、
前記判定処理部は、前記入れ子となる前記処理に対応する前記処理内容を集約し、当該集約後の前記処理内容を生成してから、前記処理対の生成を開始し、前記入れ子となる前記処理に対応する前記処理順序対に含まれる前記後続処理を該当無とする、
ことを特徴とする請求項１〜５のいずれか１項に記載の有向グラフ生成装置。
【請求項７】
複数の処理に課される共通の制約を記述した不変条件および前記処理の内容を前記処理ごとに記述した処理内容を含む形式仕様記述データを読み込む読込処理ステップと、
前記読込処理ステップにおいて読み込まれた前記形式仕様記述データに含まれる前記処理に基づいて二つの前記処理を組み合わせることで生成される処理対および前記形式仕様記述データを用い、各前記処理対に含まれる二つの前記処理が連続して実行し得るか否かを判定し、連続して実行し得る場合に、当該処理対に含まれる二つの前記処理を、先行処理および後続処理として含む処理順序対に選定する判定処理ステップと、
前記判定処理ステップにおいて選定された前記処理順序対を用いて有向グラフを生成する生成処理ステップと、
を含むことを特徴とする有向グラフ生成方法。
【請求項８】
前記生成処理ステップは、前記処理順序対に含まれる前記処理のうち、前記後続処理として出現しない前記処理を、開始処理に選定し、当該開始処理を起点にして前記処理順序対に含まれる前記処理をつないでいくことで、前記有向グラフを生成する、
ことを特徴とする請求項７記載の有向グラフ生成方法。
【請求項９】
前記生成処理ステップにおいて生成された前記有向グラフを図式化して出力する出力処理ステップを、さらに含む、
ことを特徴とする請求項７または８記載の有向グラフ生成方法。
【請求項１０】
前記処理内容は、前記処理の前提条件および前記処理の実行内容を含み、
前記判定処理ステップは、各前記処理対について、前記不変条件、前記前提条件および前記実行内容を用いた条件式が真になり得るか否かを判定することで、前記処理対に含まれる二つの前記処理内容が連続して実行し得るか否かを判定する、
ことを特徴とする請求項７〜９のいずれか１項に記載の有向グラフ生成方法。
【請求項１１】
前記読込処理ステップは、前記形式仕様記述データに含まれる前記処理のうち、並列に実行する前記処理を特定するための並列処理データをさらに読み込み、
前記生成処理ステップは、並列に実行する前記処理を識別可能な状態で前記有向グラフを生成する、
ことを特徴とする請求項７〜１０のいずれか１項に記載の有向グラフ生成方法。
【請求項１２】
前記読込処理ステップは、前記形式仕様記述データに含まれる前記処理のうち、入れ子構造を形成する入れ子となる前記処理を特定するための入れ子処理データをさらに読み込み、
前記判定処理ステップは、前記入れ子となる前記処理に対応する前記処理内容を集約し、当該集約後の前記処理内容を生成してから、前記処理対の生成を開始し、前記入れ子となる前記処理に対応する前記処理順序対に含まれる前記後続処理を該当無とする、
ことを特徴とする請求項７〜１１のいずれか１項に記載の有向グラフ生成方法。
【請求項１３】
コンピュータに、
複数の処理に課される共通の制約を記述した不変条件および前記処理の内容を前記処理ごとに記述した処理内容を含む形式仕様記述データを読み込む読込処理ステップと、
前記読込処理ステップにおいて読み込まれた前記形式仕様記述データに含まれる前記処理に基づいて二つの前記処理を組み合わせることで生成される処理対および前記形式仕様記述データを用い、各前記処理対に含まれる二つの前記処理が連続して実行し得るか否かを判定し、連続して実行し得る場合に、当該処理対に含まれる二つの前記処理を、先行処理および後続処理として含む処理順序対に選定する判定処理ステップと、
前記判定処理ステップにおいて選定された前記処理順序対を用いて有向グラフを生成する生成処理ステップと、
を実行させることを特徴とする有向グラフ生成プログラム。
【請求項１４】
前記生成処理ステップは、前記処理順序対に含まれる前記処理のうち、前記後続処理として出現しない前記処理を、開始処理に選定し、当該開始処理を起点にして前記処理順序対に含まれる前記処理をつないでいくことで、前記有向グラフを生成する、
ことを特徴とする請求項１３記載の有向グラフ生成プログラム。
【請求項１５】
前記生成処理ステップにおいて生成された前記有向グラフを図式化して出力する出力処理ステップを、さらに実行させる、
ことを特徴とする請求項１３または１４記載の有向グラフ生成プログラム。
【請求項１６】
前記処理内容は、前記処理の前提条件および前記処理の実行内容を含み、
前記判定処理ステップは、各前記処理対について、前記不変条件、前記前提条件および前記実行内容を用いた条件式が真になり得るか否かを判定することで、前記処理対に含まれる二つの前記処理内容が連続して実行し得るか否かを判定する、
ことを特徴とする請求項１３〜１５のいずれか１項に記載の有向グラフ生成プログラム。
【請求項１７】
前記読込処理ステップは、前記形式仕様記述データに含まれる前記処理のうち、並列に実行する前記処理を特定するための並列処理データをさらに読み込み、
前記生成処理ステップは、並列に実行する前記処理を識別可能な状態で前記有向グラフを生成する、
ことを特徴とする請求項１３〜１６のいずれか１項に記載の有向グラフ生成プログラム。
【請求項１８】
前記読込処理ステップは、前記形式仕様記述データに含まれる前記処理のうち、入れ子構造を形成する入れ子となる前記処理を特定するための入れ子処理データをさらに読み込み、
前記判定処理ステップは、前記入れ子となる前記処理に対応する前記処理内容を集約し、当該集約後の前記処理内容を生成してから、前記処理対の生成を開始し、前記入れ子となる前記処理に対応する前記処理順序対に含まれる前記後続処理を該当無とする、
ことを特徴とする請求項１３〜１７いずれか１項に記載の有向グラフ生成プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、有向グラフ生成装置、有向グラフ生成方法および有向グラフ生成プログラムに関する。
【背景技術】
【０００２】
システム開発では、ソフトウェアの品質を確保するために、開発中のプログラムを検証する必要がある。しかしながら、プログラムの動作内容を確認するのは容易ではない。下記特許文献１には、プログラムリストを解析し、プログラムの動作をフローチャート等の可視的な情報に変換して表示する技術が記載されている。この技術では、フローチャート等の可視的情報を取得するのが困難なプログラムを検証する場合には、プログラムを実行した時に表示される表示情報を用いて検証用のドキュメントを作成する。
【先行技術文献】
【特許文献】
【０００３】
【特許文献１】特開２０００−１８７５８６号公報
【発明の概要】
【発明が解決しようとする課題】
【０００４】
近年、システム開発に、いわゆる形式手法を採用することが多くなってきている。形式手法とは、数学的な概念に基づき、対象を正確に曖昧さのない形で表現する手法である。具体的には、主に集合と、集合や集合の要素同士の関係とを用いて対象を表現する。そして、複数の集合や関係に対して何らかの操作をした場合に、それらの関係が成り立つまたは成り立たないという言明を論理命題の形で表す。この形式手法では、形式仕様記述言語を用いてシステムの仕様を表現する。このような形式手法では、一般に、処理を記述する際に、処理Ａ、処理Ｂ、処理Ｃ…のように、単に処理内容を記述するだけで、どのような順序で処理を実行するのかまでは記述しない。したがって、上述した特許文献１に記載の技術を用いて、形式手法による仕様を検証しようとしても、プログラムの動作を特定することができないため、検証用のドキュメントを作成することができない。
【０００５】
本発明は、上述した課題を解決するためになされたものであり、形式手法による仕様であっても、仕様の検証を容易に行うことができる有向グラフ生成装置、有向グラフ生成方法および有向グラフ生成プログラムを提供することを目的の一つとする。
【課題を解決するための手段】
【０００６】
本発明の一態様である有向グラフ生成装置は、複数の処理に課される共通の制約を記述した不変条件および前記処理の内容を前記処理ごとに記述した処理内容を含む形式仕様記述データを読み込む読込処理部と、前記読込処理部により読み込まれた前記形式仕様記述データに含まれる前記処理に基づいて二つの前記処理を組み合わせることで生成される処理対および前記形式仕様記述データを用い、各前記処理対に含まれる二つの前記処理が連続して実行し得るか否かを判定し、連続して実行し得る場合に、当該処理対に含まれる二つの前記処理を、先行処理および後続処理として含む処理順序対に選定する判定処理部と、前記判定処理部により選定された前記処理順序対を用いて有向グラフを生成する生成処理部と、を備える。
【０００７】
本発明の一態様である有向グラフ生成方法は、複数の処理に課される共通の制約を記述した不変条件および前記処理の内容を前記処理ごとに記述した処理内容を含む形式仕様記述データを読み込む読込処理ステップと、前記読込処理ステップにおいて読み込まれた前記形式仕様記述データに含まれる前記処理に基づいて二つの前記処理を組み合わせることで生成される処理対および前記形式仕様記述データを用い、各前記処理対に含まれる二つの前記処理が連続して実行し得るか否かを判定し、連続して実行し得る場合に、当該処理対に含まれる二つの前記処理を、先行処理および後続処理として含む処理順序対に選定する判定処理ステップと、前記判定処理ステップにおいて選定された前記処理順序対を用いて有向グラフを生成する生成処理ステップと、を含む。
【０００８】
本発明の一態様である有向グラフ生成プログラムは、コンピュータに、複数の処理に課される共通の制約を記述した不変条件および前記処理の内容を前記処理ごとに記述した処理内容を含む形式仕様記述データを読み込む読込処理ステップと、前記読込処理ステップにおいて読み込まれた前記形式仕様記述データに含まれる前記処理に基づいて二つの前記処理を組み合わせることで生成される処理対および前記形式仕様記述データを用い、各前記処理対に含まれる二つの前記処理が連続して実行し得るか否かを判定し、連続して実行し得る場合に、当該処理対に含まれる二つの前記処理を、先行処理および後続処理として含む処理順序対に選定する判定処理ステップと、前記判定処理ステップにおいて選定された前記処理順序対を用いて有向グラフを生成する生成処理ステップと、を実行させる。
【発明の効果】
【０００９】
本発明によれば、形式手法による仕様であっても、仕様の検証を容易に行うことができる。
【図面の簡単な説明】
【００１０】
【図１】実施形態における有向グラフ生成装置の構成を例示する図である。
【図２】形式仕様記述データに含まれる不変条件および処理内容を例示する図である。（Ａ）は、不変条件を例示するものであり、（Ｂ）〜（Ｅ）は、処理内容を例示するものである。
【図３】条件式（１）を用いて処理対の連続性を判定する際の事例を模式化した図である。
【図４】条件式（１）を用いて処理対の連続性を判定する際の事例を模式化した図である。
【図５】処理順序対を例示する図である。
【図６】有向グラフを例示する図である。
【図７】図６の有向グラフをＵＭＬアクティビティ図で図式化した図である。
【図８】有向グラフを生成し、図式化して出力する際の動作説明するためのフローチャートである。
【図９】本発明に係る有向グラフ生成装置の最小構成を例示する図である。
【図１０】実施形態における有向グラフを例示する図である。
【図１１】変形例における有向グラフを例示する図である。
【図１２】図１１の有向グラフをＵＭＬアクティビティ図で図式化した図である。
【図１３】変形例における形式仕様記述データに含まれる処理内容を例示する図である。
【図１４】変形例における形式仕様記述データに含まれる処理内容を例示する図である。
【図１５】変形例における形式仕様記述データに含まれる処理内容を例示する図である。
【図１６】処理順序対を例示する図である。
【図１７】実施形態における有向グラフを例示する図である。
【図１８】実施形態における有向グラフを例示する図である。
【図１９】変形例における集約後の処理内容を例示する図である。
【図２０】変形例における処理順序対を例示する図である。
【図２１】変形例における上位フローに対応する有向グラフを例示する図である。
【図２２】図２１の有向グラフをＵＭＬアクティビティ図で図式化した図である。
【図２３】変形例における処理順序対を例示する図である。
【図２４】変形例における下フローに対応する有向グラフを例示する図である。
【図２５】図２４の有向グラフをＵＭＬアクティビティ図で図式化した図である。
【発明を実施するための形態】
【００１１】
以下、添付図面を参照して、本発明に係る有向グラフ生成装置、有向グラフ生成方法および有向グラフ生成プログラムの好適な実施形態について説明する。
【００１２】
まず、図１を参照して、実施形態における有向グラフ生成装置の構成について説明する。有向グラフ生成装置１０は、機能的には、例えば、読込処理部１１と、判定処理部１２と、生成処理部１３と、出力処理部１４と、を有する。
【００１３】
ここで、有向グラフ生成装置１０は、物理的には、例えば、ＣＰＵ（Central Processing Unit）と、メモリと、入出力インターフェースとを含む。記憶装置は、例えば、ＣＰＵで処理されるプログラムおよびデータを記憶するＲＯＭ（Read Only Memory）やＨＤＤ（Hard Disk Drive）、主として制御処理のための各種作業領域として使用するＲＡＭ（Random Access Memory）等を含む。これらの要素は、互いにバスを介して接続する。ＣＰＵが、ＲＯＭに記憶されたプログラムを実行し、入出力インターフェースを介して受信されるメッセージや、入力装置から入力されるデータ、ＲＡＭに展開されるデータ等を処理することで、図１に示す有向グラフ生成装置１０の各部の機能を実現する。
【００１４】
読込処理部１１は、形式仕様記述データＤＢ（Data Base）２０から形式仕様記述データを読み込む。形式仕様記述データは、形式手法における形式仕様記述言語を用いてシステムの仕様を表現することで生成される。この形式仕様記述データは、不変条件および処理内容を含む。不変条件は、複数の処理に課される共通の制約を記述したデータである。処理内容は、処理する内容を処理ごとに記述したデータであり、その処理の前提条件および実行内容等をデータとして含む。
【００１５】
図２を参照して、形式仕様記述データに含まれる不変条件および処理内容について具体的に説明する。図２は、例示的に、図書館システムにおける形式仕様記述データを示している。図２（Ａ）は、不変条件を例示するものであり、集合“貸出図書”は、集合“図書”の部分集合であることを不変条件としている。
【００１６】
図２（Ｂ）〜（Ｅ）は、処理内容を例示するものである。図２（Ｂ）に示す処理内容は、“図書登録”という処理に関するデータであり、要素“ｃ”を引数とし、集合“本”は要素“ｃ”を含むという命題と、集合“図書”は要素“ｃ”を含まないという命題とが共に真となる（論理積）ことを前提条件とし、集合“図書”と要素“ｃ”との和を変数“図書”に代入することを実行内容としている。
【００１７】
図２（Ｃ）に示す処理内容は、“図書貸出”という処理に関するデータであり、要素“ｃ”を引数とし、集合“図書”は要素“ｃ”を含むという命題と、集合“貸出図書”は要素“ｃ”を含まないという命題とが共に真となる（論理積）ことを前提条件とし、集合“貸出図書”と要素“ｃ”との和を変数“貸出図書”に代入することを実行内容としている。
【００１８】
図２（Ｄ）に示す処理内容は、“図書返却”という処理に関するデータであり、要素“ｃ”を引数とし、集合“貸出図書”は要素“ｃ”を含むという命題が真となることを前提条件とし、集合“貸出図書”と要素“ｃ”との差を変数“貸出図書”に代入することを実行内容としている。
【００１９】
図２（Ｅ）に示す処理内容は、“図書抹消”という処理に関するデータであり、要素“ｃ”を引数とし、集合“図書”は要素“ｃ”を含むという命題と、集合“貸出図書”は要素“ｃ”を含まないという命題とが共に真となる（論理積）ことを前提条件とし、集合“図書”と要素“ｃ”との差を変数“図書”に代入することを実行内容としている。
【００２０】
なお、本実施形態では、形式仕様記述データＤＢ２０が有向グラフ生成装置１０の外部に設けられている場合について説明するが、形式仕様記述データＤＢ２０が有向グラフ生成装置１０の内部に設けられている場合にも同様にして本発明に適用できる。
【００２１】
図１に示す判定処理部１２は、読込処理部１１により読み込まれた形式仕様記述データに含まれる処理に基づいて二つの処理を組み合わせることで生成される処理対と、形式仕様記述データとを用い、各処理対に含まれる二つの処理が連続して実行し得るか否かを判定する。具体的に、判定処理部１２は、各処理対について、不変条件、前提条件および実行内容を用いた、以下の条件式（１）が真になり得るか否かを判定することで、各処理対に含まれる二つの処理（ｓ、ｔ）が連続して実行し得るか否かを判定する。
【００２２】
Ｉ（ｃ，ｖ）∧Ｇｓ（ｃ，ｖ）∧Ａｓ（ｃ，ｖ，ｖ'）∧Ｉ（ｃ，ｖ'）∧Ｇｔ（ｃ，ｖ'）  …  条件式（１）
【００２３】
ここで、上記条件式（１）のＩ（ｃ，ｖ）およびＩ（ｃ，ｖ'）は、不変条件であり、これらの不変条件は"ｃ"を定数とし、"ｖ"または"ｖ'"を変数とする。"ｖ'"は、処理を実行した後の変数を示す。同様にＧｓ（ｃ，ｖ）は、処理ｓの前提条件であり、Ａｓ（ｃ，ｖ，ｖ'）は、処理ｓの実行内容であり、Ｇｔ（ｃ，ｖ'）は、処理ｔの前提条件である。
【００２４】
判定処理部１２は、読込処理部１１により読み込まれた形式仕様記述データに含まれる処理内容が、例えば図２の（Ｂ）〜（Ｅ）に示す四つの処理内容である場合、この四つの処理内容に基づいて、二つの処理を組み合わせていき、複数の処理対を生成する。判定処理部１２は、各処理対に含まれる二つの処理（ｓ、ｔ）が連続して実行し得るか否かを、順次判定する。以下に、連続して実行し得ない場合と、連続して実行し得る場合について、具体的に説明する。
【００２５】
図３を参照して、図２（Ｂ）の“図書登録”処理ｓと図２（Ｂ）の“図書登録”処理ｔとの処理対を、上記条件式（１）を用いて判定する場合について説明する。
【００２６】
この場合には、図３に示す条件式（１）に含まれる部分式（１１）〜（１５）は成り立つが、部分式（１６）は、以下の理由で成り立たない。それは、部分式（１３）により、集合"図書"と要素"ｃ"との和が、集合"図書'"に代入され、集合"図書'"には要素"ｃ"が含まれることになる。その結果、部分式（１６）における、集合“図書'”は要素“ｃ”を含まないという命題が偽となる。したがって、部分式（１６）が成り立たず、条件式（１）全体としても成り立たないことになる。それゆえ、この場合、判定処理部１２は、“図書登録”処理ｓと“図書登録”処理ｔとの処理対について、二つの処理（ｓ、ｔ）は連続して実行し得ないと判定する。
【００２７】
図４を参照して、図２（Ｂ）の“図書登録”処理ｓと図２（Ｅ）の“図書抹消”処理ｔとの処理対を、条件式（１）を用いて判定する場合について説明する。
【００２８】
この場合には、図４の部分式（１１）〜（１６）の全てが成り立つため、条件式（１）全体が真として成り立つことになる。それゆえ、判定処理部１２は、“図書登録”処理ｓと“図書抹消”処理ｔとの処理対について、二つの処理（ｓ、ｔ）は連続して実行し得ると判定する。
【００２９】
図１に示す判定処理部１２は、処理対に含まれる二つの処理が連続して実行し得る場合に、この処理対に含まれる二つの処理を、先行処理および後続処理として含む処理順序対に選定する。以下に具体的に説明する。
【００３０】
図２（Ｂ）〜（Ｅ）に示す処理内容の全ての組み合わせを処理対にして判定した結果、選定される処理順序対について、図５を参照して説明する。この場合、図５に示すように、"図書登録"処理を先行処理とし、"図書貸出"処理を後続処理とする処理順序対"１"と、"図書登録"処理を先行処理とし、"図書抹消"処理を後続処理とする処理順序対"２"と、"図書貸出"処理を先行処理とし、"図書返却"処理を後続処理する処理順序対"３"と、"図書返却"処理を先行処理とし、"図書貸出"処理を後続処理とする処理順序対"４"と、"図書返却"処理を先行処理とし、"図書抹消"処理を後続処理とする処理順序対"５"と、が選定される。
【００３１】
図１に示す生成処理部１３は、判定処理部１２により選定された処理順序対を用いて有向グラフを生成する。具体的に、生成処理部１３は、処理順序対に含まれる処理のうち、後続処理として出現しない処理を、開始処理に選定し、この開始処理を起点にして処理順序対に含まれる処理をつないでいくことで、有向グラフを生成する。開始処理が複数存在する場合には、開始処理ごとに、有向グラフを生成する。以下に、具体的に説明する。
【００３２】
処理順序対として、例えば図５に示す処理順序対が選定されている場合、後続処理として出現しない処理は、"図書登録"処理となる。したがって、この場合、生成処理部１３は、"図書登録"処理を、開始処理に選定し、この"図書登録"処理を起点にして処理順序対に含まれる処理をつないでいくことで、有向グラフを生成する。図５に示す処理順序対に基づいて生成される有向グラフを、図６に例示する。
【００３３】
図６に例示する有向グラフは、開始処理である"図書登録"処理の後続処理として、"図書抹消"処理と"図書貸出"処理とが存在し、"図書抹消"処理には、後続処理が存在せず、"図書貸出"処理には、後続処理として、"図書返却"処理が存在することを示す。また、"図書返却"処理の後続処理として、この"図書返却"処理の先行処理となる"図書貸出"処理と、"図書抹消"処理とが存在し、この"図書抹消"処理には、後続処理が存在しないことを示す。
【００３４】
出力処理部１４は、生成処理部１３により生成された有向グラフを図式化して出力する。図式化には、例えば、ＵＭＬ（Unified Modeling Language）アクティビティ図や、フローチャートを用いることができる。図６に例示する有向グラフを、ＵＭＬアクティビティ図を用いて図式化した結果を、図７に例示する。出力処理部１４は、図式化した結果を、処理フローとして処理フローＤＢ３０に格納する。なお、出力処理部１４は、図式化した結果を、プリンターに出力して印刷させてもよいし、表示装置に出力して表示させてもよい。
【００３５】
次に、図８を参照して、有向グラフを生成し、図式化して出力する際の動作について説明する。
【００３６】
最初に、読込処理部１１は、形式仕様記述データＤＢ２０から形式仕様記述データを読み込む（ステップＳ１０１）。
【００３７】
続いて、判定処理部１２は、上記ステップＳ１０１で読み込まれた形式仕様記述データに含まれる処理内容を組み合わせて複数の処理対を生成する（ステップＳ１０２）。
【００３８】
続いて、判定処理部１２は、上記ステップＳ１０２で生成した処理対から一つの処理対を選択し、選択した処理対と、上記ステップＳ１０１で読み込まれた形式仕様記述データとを用い、上述した条件式（１）が真になり得るか否かを判定することで、処理対に含まれる二つの処理が連続して実行し得るか否かを判定する（ステップＳ１０３）。この判定がＮＯである場合（ステップＳ１０３；ＮＯ）には、処理を後述するステップＳ１０５に移行する。
【００３９】
一方、上記ステップＳ１０３の判定において、処理対に含まれる二つの処理が連続して実行し得ると判定された場合（ステップＳ１０３；ＹＥＳ）に、判定処理部１２は、この処理対に含まれる二つの処理を処理順序対として選定する（ステップＳ１０４）。
【００４０】
続いて、判定処理部１２は、上記ステップＳ１０２で生成した全ての処理対について、上記ステップＳ１０３の判定処理が終了したか否かを判定する（ステップＳ１０５）。この判定がＮＯである場合（ステップＳ１０５；ＮＯ）には、処理を上述したステップＳ１０３に移行する。
【００４１】
一方、上記ステップＳ１０５の判定において、全ての処理対について処理が終了したと判定された場合（ステップＳ１０５；ＹＥＳ）に、生成処理部１３は、上記ステップＳ１０４で選定された処理順序対に含まれる処理のうち、後続処理として出現しない処理を開始処理として選定する（ステップＳ１０６）。
【００４２】
続いて、生成処理部１３は、上記ステップＳ１０６で選定した開始処理ごとに、その開始処理を起点にして処理順序対に含まれる処理をつないでいくことで、有向グラフを生成する（ステップＳ１０７）。
【００４３】
続いて、出力処理部１４は、上記ステップＳ１０７で生成された有向グラフを図式化して出力する（ステップＳ１０８）。
【００４４】
上述したように、実施形態における有向グラフ生成装置１０によれば、読込処理部が形式仕様記述データを読み込み、判定処理部が、形式仕様記述データに含まれる処理に基づいて生成した処理対および形式仕様記述データを用い、各処理対に含まれる二つの処理が連続して実行し得るか否かを判定し、連続して実行し得る場合に、当該処理対に含まれる二つの処理を、先行処理および後続処理として含む処理順序対に選定し、生成処理部が、選定された処理順序対を用いて有向グラフを生成することができる。
【００４５】
これにより、形式仕様記述データに基づいて、連続して実行し得る処理を処理順序対として選定し、この選定した処理順序対に含まれる先行処理および後続処理に従って、処理を順次つないで有向グラフを生成することができるため、処理の流れを漏れなく正確に把握することが可能となる。それゆえに、形式手法による仕様であっても、仕様の検証を容易に行うことができることが可能となる。
【００４６】
[変形例]
なお、上述した実施形態は、単なる例示に過ぎず、実施形態に明示していない種々の変形や技術の適用を排除するものではない。すなわち、本発明は、その趣旨を逸脱しない範囲で様々な形態に変形して実施することができる。
【００４７】
例えば、上述した実施形態における有向グラフ生成装置１０は、図１に示す各機能を構成要素としているが、本発明に係る有向グラフ生成装置の構成は、これに限定されない。本発明の最小構成について説明する。図９は、本発明に係る有向グラフ生成装置の最小構成を例示する図である。図９に示す有向グラフ生成装置１０Ａは、図１に示す有向グラフ生成装置１０が有する各機能のうち、出力処理部１４を外部に配置して省略したものである。出力処理部１４以外の各機能については、図１に示す有向グラフ生成装置１０の各機能と同じである。
【００４８】
また、上述した実施形態における有向グラフ生成装置１０は、以下の（ｉ）並列処理明示機能と（ｉｉ）入れ子構造明示機能とをオプション機能として追加することができる。
【００４９】
（ｉ）並列処理明示機能
上述した実施形態では、処理が分岐する場合、分岐後の処理が並列に実行されるのかどうかを表現することができない。そこで、並列に実行する処理をユーザが指定することで、並列処理を明示した有向グラフを作成する、並列処理明示機能を追加できることとしてもよい。図１０〜図１２を参照して、具体的に説明する。
【００５０】
例えば、処理Ａの後続処理として処理Ｂと処理Ｅとが存在し、処理Ｂの後続処理として処理Ｃが存在し、処理Ｃおよび処理Ｅの後続処理として処理Ｄが存在する場合、上述した実施形態における有向グラフ生成装置１０は、図１０に示す有向グラフを生成する。この場合、処理Ｂおよび処理Ｃと、処理Ｅとが並列に実行されるのか、いずれか一方の処理が実行されるのかを判別することはできない。
【００５１】
一方、並列処理機能を追加した場合には、ユーザは、有向グラフを生成して図式化する処理を実行させる前に、並列して実行する処理の組み合わせ（並列処理データ）を入力する。その結果、入力した並列して実行する処理の組み合わせの前後に、並列処理の開始および終了を示す図形等が組み込まれた有向グラフが生成され、図式化される。
【００５２】
具体的に、ユーザは、並列して実行する処理の組み合わせとして、例えば、"処理Ｂ、処理Ｃ"、"処理Ｅ"のように入力することができる。この場合、読込処理部１１は、入力された"処理Ｂ、処理Ｃ"、"処理Ｅ"を読み込み、生成処理部１３は、例えば、図１１に示すように、並列に実行する処理（"処理Ｂ、処理Ｃ"と"処理Ｅ"）を識別可能な状態で有向グラフを生成する。また、出力処理部１４は、例えば、図１２に示すように、並列に実行する処理（"処理Ｂ、処理Ｃ"と"処理Ｅ"）を識別可能な状態で有向グラフを図式化する。
【００５３】
（ｉｉ）入れ子構造明示機能
上述した実施形態では、処理が入れ子構造を有する場合、どの処理が上位フローに属し、下位フローに属するのかを表現することができない。そこで、下位フローに属する処理をユーザが指定することで、入れ子構造を明示した有向グラフを作成する、入れ子構造明示機能を追加できることとしてもよい。図１３〜図２５を参照して、具体的に説明する。
【００５４】
以下においては、例示的に、"ｍａｘ（ｘ，ｙ）＋１"を三つの処理に分け、図１３〜図１５にそれぞれ示す三つの処理内容を含む形式仕様記述データが生成されている場合について説明する。
【００５５】
この場合、上述した実施形態における有向グラフ生成装置１０の判定処理部１２は、図１６に示す二つの処理順序対を選択し、生成処理部１３は、図１７および図１８に示す有向グラフを生成することになる。つまり、入れ子構造を有する有向グラフを生成することができない。
【００５６】
一方、入れ子構造明示機能を追加した場合には、ユーザは、有向グラフを生成して図式化する処理を実行させる前に、入れ子となる下位フローに属する処理および下位フローを識別する名称（入れ子処理データ）を入力する。その結果、入力した下位フローを集約した上位フローの有向グラフと、下位フローごとの有向グラフとが生成され、図式化される。
【００５７】
具体的に、ユーザは、下位フローに属する処理として、"ｍａｘ１"，"ｍａｘ２"を入力し、下位フローを識別する名称として、"ｍａｘ"を入力することができる。この場合、読込処理部１１は、入力された"ｍａｘ１"，"ｍａｘ２"と"ｍａｘ"とを読み込み、判定処理部１２は、図１３に示す"ｍａｘ１"の処理内容と、図１４に示す"ｍａｘ２"の処理内容とを集約し、図１９に示す"ｍａｘ"の処理内容を生成してから、実施形態で説明した処理対の生成を開始する。図１９に示す"ｍａｘ"の前提条件は、"ｍａｘ１"の前提条件と"ｍａｘ２"の前提条件との和となり、"ｍａｘ"の実行内容は、"ｍａｘ１"の実行内容と"ｍａｘ２"の実行内容とを、"ｏｒ"で結合したものである。ここで、実行内容を集約する際に、前提条件と実行内容との関係が分岐である場合には、各実行内容を"ｏｒ"で結合し、前提条件と実行内容との関係が直列である場合には、各実行内容を"ａｎｄ"で結合する。
【００５８】
この場合、判定処理部１２は、上位フローの処理順序対として、図２０に示す一つの処理順序対を選定し、下位フローの処理順序対として、図２１に示す二つの処理順序対を選定する。下位フローの処理順序対に含まれる後続処理については該当無（空値）とする。
【００５９】
続いて、生成処理部１３は、図２０に示す処理順序対に基づいて、図２１に示す上位フローに対応する有向グラフを生成し、出力処理部１４は、上位フローに対応する有向グラフを、ＵＭＬアクティビティ図を用いて、図２２に示すように図式化する。
【００６０】
一方、生成処理部１３は、図２３に示す処理順序対に基づいて、図２４に示す下位フローに対応する二つの有向グラフを生成し、出力処理部１４は、下位フローに対応する有向グラフを、ＵＭＬアクティビティ図を用いて、図２５に示すように図式化する。
【００６１】
このように、入れ子構造明示機能を追加することで、入れ子構造を有する処理を識別可能な状態で有向グラフを生成し、その有向グラフを図式化することが可能となる。
【００６２】
上述した実施形態の一部または全部は、以下の付記のようにも記載され得るが、本発明を以下のように限定するものではない。
【００６３】
（付記１）  複数の処理に課される共通の制約を記述した不変条件および前記処理の内容を前記処理ごとに記述した処理内容を含む形式仕様記述データを読み込む読込処理部と、前記読込処理部により読み込まれた前記形式仕様記述データに含まれる前記処理に基づいて二つの前記処理を組み合わせることで生成される処理対および前記形式仕様記述データを用い、各前記処理対に含まれる二つの前記処理が連続して実行し得るか否かを判定し、連続して実行し得る場合に、当該処理対に含まれる二つの前記処理を、先行処理および後続処理として含む処理順序対に選定する判定処理部と、前記判定処理部により選定された前記処理順序対を用いて有向グラフを生成する生成処理部と、を備えることを特徴とする有向グラフ生成装置。
【００６４】
（付記２）  前記生成処理部は、前記処理順序対に含まれる前記処理のうち、前記後続処理として出現しない前記処理を、開始処理に選定し、当該開始処理を起点にして前記処理順序対に含まれる前記処理をつないでいくことで、前記有向グラフを生成する、ことを特徴とする付記１記載の有向グラフ生成装置。
【００６５】
（付記３）  前記生成処理部により生成された前記有向グラフを図式化して出力する出力処理部を、さらに備える、ことを特徴とする付記１または２記載の有向グラフ生成装置。
【００６６】
（付記４）  前記処理内容は、前記処理の前提条件および前記処理の実行内容を含み、前記判定処理部は、各前記処理対について、前記不変条件、前記前提条件および前記実行内容を用いた条件式が真になり得るか否かを判定することで、前記処理対に含まれる二つの前記処理内容が連続して実行し得るか否かを判定する、ことを特徴とする付記１〜３のいずれかに記載の有向グラフ生成装置。
【００６７】
（付記５）  前記読込処理部は、前記形式仕様記述データに含まれる前記処理のうち、並列に実行する前記処理を特定するための並列処理データをさらに読み込み、前記生成処理部は、並列に実行する前記処理を識別可能な状態で前記有向グラフを生成する、ことを特徴とする付記１〜４のいずれかに記載の有向グラフ生成装置。
【００６８】
（付記６）  前記読込処理部は、前記形式仕様記述データに含まれる前記処理のうち、入れ子構造を形成する入れ子となる前記処理を特定するための入れ子処理データをさらに読み込み、前記判定処理部は、前記入れ子となる前記処理に対応する前記処理内容を集約し、当該集約後の前記処理内容を生成してから、前記処理対の生成を開始し、前記入れ子となる前記処理に対応する前記処理順序対に含まれる前記後続処理を該当無とする、ことを特徴とする付記１〜５のいずれかに記載の有向グラフ生成装置。
【００６９】
（付記７）  複数の処理に課される共通の制約を記述した不変条件および前記処理の内容を前記処理ごとに記述した処理内容を含む形式仕様記述データを読み込む読込処理ステップと、前記読込処理ステップにおいて読み込まれた前記形式仕様記述データに含まれる前記処理に基づいて二つの前記処理を組み合わせることで生成される処理対および前記形式仕様記述データを用い、各前記処理対に含まれる二つの前記処理が連続して実行し得るか否かを判定し、連続して実行し得る場合に、当該処理対に含まれる二つの前記処理を、先行処理および後続処理として含む処理順序対に選定する判定処理ステップと、前記判定処理ステップにおいて選定された前記処理順序対を用いて有向グラフを生成する生成処理ステップと、を含むことを特徴とする有向グラフ生成方法。
【００７０】
（付記８）  前記生成処理ステップは、前記処理順序対に含まれる前記処理のうち、前記後続処理として出現しない前記処理を、開始処理に選定し、当該開始処理を起点にして前記処理順序対に含まれる前記処理をつないでいくことで、前記有向グラフを生成する、ことを特徴とする付記７記載の有向グラフ生成方法。
【００７１】
（付記９）  前記生成処理ステップにおいて生成された前記有向グラフを図式化して出力する出力処理ステップを、さらに含む、ことを特徴とする付記７または８記載の有向グラフ生成方法。
【００７２】
（付記１０）  前記処理内容は、前記処理の前提条件および前記処理の実行内容を含み、前記判定処理ステップは、各前記処理対について、前記不変条件、前記前提条件および前記実行内容を用いた条件式が真になり得るか否かを判定することで、前記処理対に含まれる二つの前記処理内容が連続して実行し得るか否かを判定する、ことを特徴とする付記７〜９のいずれかに記載の有向グラフ生成方法。
【００７３】
（付記１１）  前記読込処理ステップは、前記形式仕様記述データに含まれる前記処理のうち、並列に実行する前記処理を特定するための並列処理データをさらに読み込み、前記生成処理ステップは、並列に実行する前記処理を識別可能な状態で前記有向グラフを生成する、ことを特徴とする付記７〜１０のいずれかに記載の有向グラフ生成方法。
【００７４】
（付記１２）  前記読込処理ステップは、前記形式仕様記述データに含まれる前記処理のうち、入れ子構造を形成する入れ子となる前記処理を特定するための入れ子処理データをさらに読み込み、前記判定処理ステップは、前記入れ子となる前記処理に対応する前記処理内容を集約し、当該集約後の前記処理内容を生成してから、前記処理対の生成を開始し、前記入れ子となる前記処理に対応する前記処理順序対に含まれる前記後続処理を該当無とする、ことを特徴とする付記７〜１１のいずれかに記載の有向グラフ生成方法。
【００７５】
（付記１３）  コンピュータに、複数の処理に課される共通の制約を記述した不変条件および前記処理の内容を前記処理ごとに記述した処理内容を含む形式仕様記述データを読み込む読込処理ステップと、前記読込処理ステップにおいて読み込まれた前記形式仕様記述データに含まれる前記処理に基づいて二つの前記処理を組み合わせることで生成される処理対および前記形式仕様記述データを用い、各前記処理対に含まれる二つの前記処理が連続して実行し得るか否かを判定し、連続して実行し得る場合に、当該処理対に含まれる二つの前記処理を、先行処理および後続処理として含む処理順序対に選定する判定処理ステップと、前記判定処理ステップにおいて選定された前記処理順序対を用いて有向グラフを生成する生成処理ステップと、を実行させることを特徴とする有向グラフ生成プログラム。
【００７６】
（付記１４）  前記生成処理ステップは、前記処理順序対に含まれる前記処理のうち、前記後続処理として出現しない前記処理を、開始処理に選定し、当該開始処理を起点にして前記処理順序対に含まれる前記処理をつないでいくことで、前記有向グラフを生成する、ことを特徴とする付記１３記載の有向グラフ生成プログラム。
【００７７】
（付記１５）  前記生成処理ステップにおいて生成された前記有向グラフを図式化して出力する出力処理ステップを、さらに実行させる、ことを特徴とする付記１３または１４記載の有向グラフ生成プログラム。
【００７８】
（付記１６）  前記処理内容は、前記処理の前提条件および前記処理の実行内容を含み、前記判定処理ステップは、各前記処理対について、前記不変条件、前記前提条件および前記実行内容を用いた条件式が真になり得るか否かを判定することで、前記処理対に含まれる二つの前記処理内容が連続して実行し得るか否かを判定する、ことを特徴とする付記１３〜１５のいずれかに記載の有向グラフ生成プログラム。
【００７９】
（付記１７）  前記読込処理ステップは、前記形式仕様記述データに含まれる前記処理のうち、並列に実行する前記処理を特定するための並列処理データをさらに読み込み、前記生成処理ステップは、並列に実行する前記処理を識別可能な状態で前記有向グラフを生成する、ことを特徴とする付記１３〜１６のいずれかに記載の有向グラフ生成プログラム。
【００８０】
（付記１８）  前記読込処理ステップは、前記形式仕様記述データに含まれる前記処理のうち、入れ子構造を形成する入れ子となる前記処理を特定するための入れ子処理データをさらに読み込み、前記判定処理ステップは、前記入れ子となる前記処理に対応する前記処理内容を集約し、当該集約後の前記処理内容を生成してから、前記処理対の生成を開始し、前記入れ子となる前記処理に対応する前記処理順序対に含まれる前記後続処理を該当無とする、ことを特徴とする付記１３〜１７いずれかに記載の有向グラフ生成プログラム。
【符号の説明】
【００８１】
１０、１０Ａ…有向グラフ生成装置
１１…読込処理部
１２…判定処理部
１３…生成処理部
１４…出力処理部
２０…形式仕様記述データＤＢ
３０…処理フローＤＢ
【図１】
2014099042.tif 000003
【図２】
2014099042.tif 000004
【図３】
2014099042.tif 000005
【図４】
2014099042.tif 000006
【図６】
2014099042.tif 000007
【図７】
2014099042.tif 000008
【図８】
2014099042.tif 000009
【図９】
2014099042.tif 000010
【図１０】
2014099042.tif 000011
【図１１】
2014099042.tif 000012
【図１２】
2014099042.tif 000013
【図１３】
2014099042.tif 000014
【図１４】
2014099042.tif 000015
【図１５】
2014099042.tif 000016
【図１６】
2014099042.tif 000017
【図１７】
2014099042.tif 000018
【図１８】
2014099042.tif 000019
【図１９】
2014099042.tif 000020
【図２０】
2014099042.tif 000021
【図２１】
2014099042.tif 000022
【図２２】
2014099042.tif 000023
【図２３】
2014099042.tif 000024
【図２４】
2014099042.tif 000025
【図２５】
2014099042.tif 000026
【図５】
2014099042.tif 000027