JP6802109B2 - ソフトウェア仕様分析装置、及びソフトウェア仕様分析方法 - Google Patents

Description

本発明は、ソフトウェア仕様分析装置、及びソフトウェア仕様分析方法に関する。

特許文献１には、「分析対象のプログラムから、繰り返し制御変数を変化させて特定のケースを探索して当該特定のケースにおいて特定の処理を実施するというパターンに合致する繰り返しブロックを抽出し、分析対象のプログラムにおいて、抽出された繰り返しブロック及び当該繰り返しブロックの直後のブロックを、真の場合に特定の処理を実施し且つ偽の場合に直後のブロックの処理を実施し且つ当該真偽に関する述語関数を含む二分岐構造に置換し、二分岐構造に含まれる述語関数について論理制約を生成しておき、変換処理後のプログラムのシンボリック実行時に、上記述語関数を処理していることを検出すると、当該述語関数に対応付けられている論理制約から、述語関数の出現位置におけるパスコンディションを生成してシンボリック実行部の管理データに追加登録する」と記載されている。

特開２０１１−１９１９８５号公報 C.L.リュー 著、成嶋弘／秋山仁 訳、コンピュータサイエンスのための離散数学入門、マグロウヒルブック株式会社、1986年

特許文献１は、「シンボリック実行では、条件分岐においてその充足可能な全ての実行パスを自動的に発生させて、プログラムの網羅的な実行を可能としている。しかし、その網羅性ゆえに組み合せ爆発を起こす可能性があり、特に実装言語特有のアルゴリズムによりシンボリック実行上では本来必要としない組み合せを多く生成してしまい、無駄な探索を繰り返してしまう」との課題に対し、上記の仕組みにより上記課題の解決を図っている。

しかし特許文献１では、配列から特定のデータを検索するためのループ文をそれと等価な条件分岐文に置換しており、配列から特定のデータを検索するためのループ文以外のループ文を含むソースコードからルールを抽出する場合には適用することができない。

本発明はこうした背景に鑑みてなされたものであり、ソフトウェアの仕様分析の効率化に寄与するソフトウェア仕様分析装置、及びソフトウェア仕様分析方法を提供することを目的としている。

上記目的を達成するための本発明の一つは、ソフトウェアの仕様を分析する装置であって、分析対象のソフトウェアを実現するプログラムのソースコードを記憶する記憶部と、前記ソースコードに含まれているループ文の記述を特定するループ文特定部と、特定した前記ループ文以外の前記ソースコードの記述について記号実行を行うことにより、前記ソースコードのパス条件及びパス実行結果を含む情報であるループ外パス情報を、前記ループ文の実行前における変数の値と前記ループ文の実行後における変数の値とを用いて生成するループ外記号実行部と、特定した前記ループ文について記号実行を行うことにより、前記ソースコードに含まれている各変数について、前記ループ文をｎ−１回実行した後に
おける当該変数の値と、前記ループ文をｎ回実行した後における当該変数の値との関係を示す情報である汎化ループ内パス情報を生成する、ループ内記号実行部と、ループを特定回数実行した場合における前記ソースコードのパスに関する情報である特化ループ内パス情報を生成するループ内パス特化部と、前記ループ内パス特化部が生成した前記特化ループ内パス情報のうち、任意回数だけループを実行した場合における変数の値を含む第１の特化ループ内パス情報を取得し、前記第１の特化ループ内パス情報に前記汎化ループ内パス情報を適用することにより、前記第１の特化ループ内パス情報よりもループ回数が１つ大きい第２の特化ループ内パス情報を生成し、前記第２の特化ループ内パス情報と前記ループ外パス情報とに基づき、前記ソフトウェアの仕様を表すルールを含む情報であるルール情報を生成するルール生成部、を備える。

その他、本願が開示する課題、及びその解決方法は、発明を実施するための形態の欄、及び図面により明らかにされる。

本発明によれば、ソフトウェアの仕様の分析を効率よく行うことができる。

第１実施形態の仕様分析装置の機能ブロック図である。 仕様分析装置の実現に用いるハードウェアの例である。 ソースコードの例である。 ループ外パス探索木の例である。 ループ外記号実行情報の例である。 ループ外記号実行情報の例である。 ループ外パス情報の例である。 ループ内パス探索木の例である。 ループ内記号実行処理を説明するフローチャートである。 ループ内記号実行情報の例である。 汎化ループ内パス情報の例である。 ループ内パス特化処理を説明するフローチャートである。 （ａ）、（ｂ）はループ回数が0回の特化ループ内パス情報の例である。 ループ回数が1回の特化ループ内パス情報の例である。 ルール生成処理を説明するフローチャートである。 ループ回数が0回の場合のルールの例である。 ループ回数が1回の場合のルールの例である。 ループの上限回数が1回に指定されている場合のルールの例である。 第２実施形態の仕様分析装置の機能ブロック図である。 ソースコードの例である。 ループ外パス探索木の例である。 ループ外記号実行情報の例である。 ループ外記号実行情報の例である。 ループ外パス情報の例である。 ループ内パス探索木の例である。 ループ内記号実行情報の例である。 汎化ループ内パス情報の例である。 一般項化ループ内パス情報の例である。 一般項化ルール情報の例である。 一般項化ルール表示画面の例である。 ループ上限回数の指定画面の例である。

以下、図面を参照しつつ実施形態について説明する。尚、以下の説明において、同一の又は類似する構成について同一の符号を付して重複した説明を省略することがある。

［第１実施形態］
図１に第１実施形態として説明するソフトウェア仕様分析装置（以下、仕様分析装置１００と称する。）の機能ブロック図を示している。仕様分析装置１００は、分析対象となるソフトウェアを実現しているプログラムのソースコード１５１について記号実行を行うことにより、上記ソフトウェアの仕様に関する情報（以下、ルール情報１５７とも称する。）を生成する。

記号実行では、ソースコードのパラメータに渡される引数をシンボル値で表し、そのシンボル値に対してソースコードの処理を実行する。その際、ソースコードの実行パスごとに、シンボル値がどのような値であればそのパスを実行するかを示す情報（以下、パス条件とも称する。）を取得する。またそのパスを実行した結果、最終的に各変数が保持する値（以下、パス実行結果とも称する。）を取得する。尚、シンボル値はパス実行結果にも現れる可能性がある。パス条件とパス実行結果の組合せは、当該パスが実行される条件と当該パスが実行された場合の結果を示し、IF-THENのルール形式で表すことができる。こ
のようなIF-THEN関係はルールとも称される。ソースコード１５１の全てのパスを探索し
て生成したルールの集合は、そのソースコードの仕様に相当する。

ここでソースコードがループ処理に関する記述（例えば、ソースコードがＣ言語で記述されている場合、while文、do文、for文等の記述ブロック。以下、ループ処理に関する記述ブロックをループ文と称する。）を含んでいる場合を考える。ソースコードがループ文を含んでいる場合、記号実行では、ループ文を１回も実行しないパス、ループ文を１回だけ実行するパス、ループ文を２回だけ実行するパスというように、ループ文の実行回数ごとにパスを生成することになる。例えば、最大でループ文を４回実行する可能性がある場合、ループ文の実行回数が０回のときのパス、１回のときのパス、２回のときのパス、３回のときのパス、４回のときのパスという、合計５つのパスを生成することになる。ここでさらに、ループ文のループ条件が引数に依存する場合を考える。上述のとおり、記号実行ではパラメータに渡される引数をシンボル値で表すため、ループ条件が引数に依存する場合、ループ条件にシンボル値が現れる。このシンボル値は実際の値を持たず、シンボル値を含むループ条件の成立／不成立を決定することができない可能性があり、ループ文を最大で何回実行する可能性があるかについても決定することができない。

このようにループ文の最大実行回数を決定することができないと、探索するパスの数が無限となり、記号実行の処理を終了することができない。この問題を回避する方法としては、例えば、ループ文の上限回数を予め設定しておき、ループ回数が上限回数を超えた時点でループから脱出する方法がある。この方法によれば、探索するパス数を有限に止めることができる。

しかし例えば、ループの上限回数がL回に設定されていた場合、L回のループを実行した場合のパスを探索する際は、ループ文に対してL回の記号実行を繰り返し行う必要がある
。そのため、例えば、ループ文のステップ数が大きい場合、記号実行により多くのリソースが消費されてしまい、また仕様を表すルールを取得するまでの時間も長くなる。

また上限回数が実際のループの最大実行回数よりも小さい場合、ルールの抽出漏れが生じる。例えば、実際の最大実行回数が５回のループ文に対して上限回数を３回に設定して記号実行を行った場合、ループ文の実行回数４回の場合のルールと、５回の場合についてはルールを抽出することができない。

以上の理由から、対象のソースコードがループ文を含む場合、ユーザはルールの抽出漏れの有無を判断する必要がある。そしてルールの抽出漏れがあると判断した場合、ユーザはループの上限回数を増加して再度記号実行を行うことになる。このように、ループ文を含むソースコードからルールを抽出する場合、上限回数を変更して複数回の記号実行を行わねばならず、ユーザは煩雑な作業を強いられる。本実施形態の仕様分析装置１００は、ソフトウェアの仕様を記号実行により分析する際に生じるこうした課題を解決するものである。

図１に示すように、仕様分析装置１００は、情報記憶部１１０、ループ文特定部１１１、ループ外記号実行部１１２、ループ内記号実行部１１３、ループ内パス特化部１１４、ルール生成部１１５、及び入出力処理部１１６を備える。仕様分析装置１００は、これらの機能以外に、例えば、オペレーティングシステム、デバイスドライバ、ＤＢＭＳ（DataBase Management System）等を備えていてもよい。

図２に仕様分析装置１００の実現に用いるハードウェア（情報処理装置５０）の一例を示す。情報処理装置５０は、プロセッサ５１、主記憶装置５２、補助記憶装置５３、入力装置５４、出力装置５５、及び通信装置５６の各構成を備える。これらはバス等の通信手段を介して互いに通信可能に接続されている。尚、情報処理装置５０の全部又は一部を、例えば、クラウドシステムにおけるクラウドサーバ等の仮想的な資源を用いて実現してもよい。

プロセッサ５１は、例えば、ＣＰＵ（Central Processing Unit）、ＭＰＵ（Micro Processing Unit）、ＧＰＵ（Graphics Processing Unit）、ＤＳＰ（Digital Signal Processor）等を用いて構成されている。プロセッサ５１が、主記憶装置５２に格納されているプログラムを読み出して実行することにより、仕様分析装置１００の全部又は一部の機能が実現される。主記憶装置５２は、例えば、ＲＯＭ（Read Only Memory）、ＲＡＭ（Random Access Memory）、不揮発性半導体メモリ（ＮＶＲＡＭ（Non Volatile RAM））等であり、プログラムやデータを記憶する。

仕様分析装置１００が備える上記の各機能は、例えば、プロセッサ５１が、主記憶装置５２や補助記憶装置５３に格納されているプログラムを読み出して実行することにより実現される。またこれらの機能は、例えば、仕様分析装置１００が備えるハードウェア（ＦＰＧＡ（Field-Programmable Gate Array）、ＡＳＩＣ（Application Specific Integrated Circuit）等）によって実現される。

補助記憶装置５３は、例えば、ハードディスクドライブ、ＳＳＤ（Solid State Drive
）、光学式記憶装置（ＣＤ（Compact Disc）、ＤＶＤ(Digital Versatile Disc)等）、ストレージシステム、ＩＣカード、ＳＤメモリカードや光学式記録媒体等の記録媒体に対するデータの読取／書込装置等である。補助記憶装置５３に格納されているプログラムやデータは主記憶装置５２に随時ロードされる。補助記憶装置５３は、例えば、ネットワークストレージのように仕様分析装置１００とは独立した構成としてもよい。

入力装置５４は、外部からのデータの入力を受け付けるインタフェースであり、例えば、記録媒体（不揮発性メモリ、光学式記録媒体、磁気記録媒体、光磁気記録媒体等）からのデータの読取装置、キーボード、マウス、タッチパネル等である。尚、例えば、仕様分析装置１００が、通信装置５６を介して他の装置からデータの入力を受け付ける構成としてもよい。

出力装置５５は、処理経過や処理結果等のデータや情報を外部に提供するユーザインタ
フェースであり、例えば、画面表示装置（液晶ディスプレイ（Liquid Crystal Display）、プロジェクタ、グラフィックカード等）、印字装置、記録媒体へのデータの記録装置等である。尚、例えば、仕様分析装置１００が、処理経過や処理結果等のデータを通信装置５６を介して他の装置に提供する構成としてもよい。

通信装置５６は、他の装置や素子との間の通信を実現する、有線方式又は無線方式の通信インタフェースであり、例えば、ＮＩＣ（Network Interface Card）、無線通信モジュール等である。

図１に戻り、前述した機能のうち、情報記憶部１１０は、ソースコード１５１、ループ外記号実行情報１５２、ループ外パス情報１５３、ループ内記号実行情報１５４、汎化ループ内パス情報１５５、特化ループ内パス情報１５６、及びルール情報１５７を記憶する。情報記憶部１１０は、これらの情報を、例えば、ファイルシステムやＤＢＭＳによって管理する。

ループ文特定部１１１は、ソースコード１５１の記述からループ文を特定（抽出）する。仕様分析装置１００は、例えば、入力装置５４や通信装置５６を介して、ユーザや他の情報処理システム等からソースコード１５１を取得する。

ループ外記号実行部１１２は、ソースコード１５１の、ループ文特定部１１１が特定したループ文以外の記述（以下、ループ外記述とも称する。）について記号実行を行うことにより、ループ外パス情報１５３を生成する。ループ外記号実行部１１２は、記号実行を行う際に利用する各種の情報をループ外記号実行情報１５２として管理し、上記記号実行に際してループ外記号実行情報１５２を適宜参照する。ループ外記号実行情報１５２及びループ外パス情報１５３の詳細については後述する。

ループ内記号実行部１１３は、ループ文特定部１１１が特定したループ文（以下、ループ内記述とも称する。）について記号実行を行うことにより汎化ループ内パス情報１５５を生成する。ループ内記号実行部１１３は、記号実行を行う際に利用する各種の情報をループ内記号実行情報１５４として管理し、上記記号実行に際しループ内記号実行情報１５４を適宜参照する。ループ内記号実行情報１５４及び汎化ループ内パス情報１５５の詳細については後述する。

ループ内パス特化部１１４は、汎化ループ内パス情報１５５をルール生成部１１５からの指示に基づきインスタンス化することにより特化ループ内パス情報１５６を生成する。尚、新たな特化ループ内パス情報１５６の生成に際し、ループ内パス特化部１１４が、既に生成済みの特化ループ内パス情報１５６を利用することがある。特化ループ内パス情報１５６の詳細については後述する。

ルール生成部１１５は、仕様分析装置１００が備える各機能（情報記憶部１１０、ループ外記号実行部１１２、ループ内記号実行部１１３、及びループ内パス特化部１１４）を統括的に制御する。ルール生成部１１５は、例えば、入力装置５４や通信装置５６を介してユーザ等から受け付けた、ループの上限回数（以下、ループ上限回数とも称する。）に基づき、ループ内パス特化部１１４の実行を制御する。またルール生成部１１５は、例えば、ループ外パス情報１５３及び特化ループ内パス情報１５６に基づきルール情報１５７を生成する。

入出力処理部１１６は、情報の受け付けや情報の提示を行うユーザインタフェースを提供する。入出力処理部１１６は、例えば、入力装置５４や通信装置５６を介してループ上限回数等の情報の指定を受け付ける。また入出力処理部１１６は、例えば、ルール生成部
１１５が生成したルール情報１５７を出力装置５５や通信装置５６に出力する。尚、入出力処理部１１６は、例えば、ループ文ごとにループ上限回数の指定を受け付ける。また入出力処理部１１６は、例えば、ソースコード１５１に含まれている全てのループ文について一括指定によりループ上限回数の指定を受け付ける。また入出力処理部１１６は、ユーザからループ上限回数の入力を受け付ける際にソースコード１５１を取得してこれを出力装置５５に表示する。

続いて、図３に示すソースコード１５１を例として、仕様分析装置１００の具体的な動作について説明する。尚、ソースコード１５１はＣ言語で記述されており、ループ文３０１を含むものとする。

ループ文特定部１１１は、ソースコード１５１からループ文３０１を特定する。ループ外記号実行部１１２は、ソースコード１５１のループ文３０１以外の記述（ループ外記述）を対象として記号実行を行う。ループ内記号実行部１１３は、ソースコード１５１のループ文３０１の記述（ループ内記述）を対象として記号実行を行う。

図４は、ループ外記号実行部１１２が、ループ外記述の記号実行に際して図３に示すソースコード１５１に基づき生成する探索木（以下、ループ外パス探索木４００と称する。）である。ループ外記号実行部１１２は、ループ外パス探索木４００を利用してループ外記号実行情報１５２を生成する。同図に示すように、ループ外パス探索木４００は、夫々「N0」〜「N7」の識別子（以下、ノード名と称する。）が付与された８つのノードを有する。

上記８つのノードのうち、ノード名が「N0」のノードは図３のソースコード１５１の１行目の記述に対応し、ソースコード１５１の開始点を意味する「START」という手続きを
含む。またノード名が「N1」のノードは、図３に示すソースコード１５１の２行目の記述に対応し、「z=0」という手続きを含む。またノード名が「N2」のノードは、図３に示す
ソースコード１５１の３〜１０行目の記述、即ちループ文３０１に対応する。このようにループ外記号実行部１１２は、ループ文３０１の記述についてはブラックボックスとして取り扱う。

ノード名が「N3」のノードは、図３に示すソースコード１５１の１１行目に対応する。当該行には条件分岐の記述「if (x % 2 == 0) {」が記述されており、ループ外記号実行
部１１２は、当該行を分岐点として、条件が「True」の場合と「False」の場合の２通り
のパスを探索する。尚、以下の説明において、これら２つのパスの夫々に識別子（以下、パス名と称する。）として「P1」，「P2」を付与する。

図５及び図６は、図４のループ外パス探索木４００に基づきループ外記号実行部１１２が生成するループ外記号実行情報１５２である。このうち図５に示すループ外記号実行情報１５２は、パス名が「P1」のパスに対応し、一方、図６に示すループ外記号実行情報１５２は、パス名が「P2」のパスに対応する。これらの図に示すように、ループ外記号実行情報１５２は、ノード名１５２１、行番号１５２２、パス条件１５２３、ループ前変数状態１５２４、及び変数状態１５２５の各項目を含む一つ以上のレコードで構成されている。ループ外記号実行情報１５２のレコードの一つはループ外パス探索木のノードの一つに対応している。

上記項目のうち、ノード名１５２１には、ノード名が設定される。行番号１５２２には、当該ノードに対応する、図３に示すソースコード１５１の行番号が設定される。

パス条件１５２３には、当該ノードに到達するための条件（以下、パス条件とも称する
。）が設定される。ここで図５はソースコード１５１の１１行目で「True」側のパス「P1」を探索することを選択した場合に対応するので、ノード名が「N3」のノードのパス条件１５２３には１１行目の分岐条件が「True」となるための条件「AL_x % 2 == 0」が設定
されている。一方、図６はソースコード１５１の１１行目で「False」側のパス「P2」を
探索することを選択した場合に対応するので、ノード名が「N3」のノードのパス条件１５２３には１１行目の分岐条件が「False」となるための条件「!(AL_x % 2 == 0)」が設定
されている。

ループ前変数状態１５２４には、ループ文３０１の実行前の各変数の値（以下、ループ前変数状態とも称する。）が設定される。本例の場合、ノード名が「N2」のノードではループ文３０１の実行前の変数「x」、「y」、「z」の値を保持している。図５又は図６に
示す「BL_x」，「BL_y」，BL_y」は、夫々、ループ文３０１の実行前の変数「x」，「ｙ
」，「ｚ」の値を表すシンボル値である（「BL」は「Before Loop」の略）。「BL_x==X」は、ループ文３０１の実行前の変数「x」の値がシンボル値「X」であることを、「BL_y==Y」は、ループ文３０１の実行前の変数「y」の値がシンボル値「Y」であることを、「BL_z==0」は、ループ文３０１の実行前の変数「z」の値が「0」であることを示す。

変数状態１５２５には、上記各ノードの夫々における変数の値（以下、変数状態とも称する。）が設定される。例えば、ノード名が「N0」のノードでは、変数「x」、「y」の値はそれぞれ「X」、「Y」である。尚、「X」、「Y」は、それぞれ、パラメータ変数「x」
、「y」に渡される引数を表すシンボル値である。

ノード名が「N2」のノードでは、ループ文３０１を実行した結果として、変数「x」に
「AL_x」を代入している。ここで「AL_x」は、ループ文実行後の変数「x」の値を表すシ
ンボル値である（「AL」は「After Loop」の略）。前述したように、ループ外記号実行部１１２はループ文３０１をブラックボックスとして取り扱うため、ループ文３０１の実行結果として上記のように新たなシンボル値を変数に代入している。

図７は、ループ外記号実行部１１２が生成するループ外パス情報１５３である。ループ外パス情報１５３は、パス名１５３１、パス終端ノード１５３２、パス条件１５３３、ループ前変数状態１５３４、及び変数状態１５３５の各項目からなる一つ以上のレコードで構成されている。ループ外パス情報１５３の１つのレコードは一つのパスに対応している。

上記項目のうち、パス名１５３１には、当該パスのパス名が設定される。パス終端ノード１５３２には、当該パスの終端ノードのノード名が設定される。図４に示すループ外パス探索木の場合はノード名が「N5」、「N7」のノードが終端ノードとなる。

パス条件１５３３には、終端ノードに到達した時点におけるパス条件が設定される。ループ前変数状態１５３４には、上記終端ノードに到達した時点におけるループ前変数状態が設定される。変数状態１５３５には、上記終端ノードに到達した時点における各変数の値（変数状態）が設定される。

図８は、ループ内記号実行部１１３が、ループ文３０１の記述（以下、ループ内記述とも称する。）について記号実行を行うに際して生成する探索木（以下、ループ内パス探索木８００と称する。）である。ループ内記号実行部１１３は、ループ内パス探索木８００を利用してループ外記号実行情報１５２を生成する。同図に示すように、ループ内パス探索木８００は、夫々「M0」〜「M8」のノード名が付与された９つのノードを有する。

上記９つのノードのうち、ノード名が「M0」のノードは図３に示すソースコード１５１
の３行目の記述に対応し、ソースコード１５１の開始点を意味する「START」という手続
きを含む。またノード名が「M1」のノードは、図３に示すソースコード１５１の３行目の記述に対応し、「while (z < y) {」という条件（以下、ループ条件とも称する。）の記
述を含む。

ノード名が「M2」のノードは、ソースコード１５１の４行目に対応する。またノード名
が「M5」及び「M8」のノードは、ループ文３０１から脱出した後のノードを表し、ノード名が「M5」のノードは３行目のループ条件「z % 3 == 0」が「True」となる場合のパスの終端ノードに、ノード名が「M8」のノードは３行目のループ条件「z % 3 == 0」が「False」となるパスの終端ノードに、夫々対応する。尚、以下の説明において、これら２つの
パスの夫々にパス名として「Q1」，「Q2」を付与する。

図９は、ループ内記号実行部１１３が行う、ループ内記述の記号実行に関する処理（以下、ループ内記号実行処理Ｓ９００と称する。）を説明するフローチャートである。以下、同図とともにループ内記号実行処理Ｓ９００について説明する。以下において、符号の前に付した「Ｓ」の文字は処理ステップを意味する。

まずループ内記号実行部１１３は、ループ文特定部１１１が特定したループ内記述（図３の例ではループ文３０１）を取得する（Ｓ９１１）。

続いて、ループ内記号実行部１１３は、ループ内記述の記号実行の開始に先立ち、当該ループの実行前の変数の値（以下、初項とも称する。）を生成（記憶、設定）し、ループ内記号実行情報１５４の内容（後述する初項１５４３）を更新する。本例では、ループ内記号実行部１１３は、変数xに対する初項を「x_0」とし、ループ実行前の変数「x」の値「BL_x」を生成する（Ｓ９１２）。

続いて、ループ内記号実行部１１３は、ループ内記述についてパスの探索を行い、ループ内記号実行情報１５４の内容（後述するパス条件１５４４及び変数状態１５４５）を更新する（Ｓ９１３）。上記パスの探索に際し、ループ内記号実行部１１３は、n-1回のル
ープの実行後の変数の値を用いてn回のループの実行時の変数の値を生成する。例えば、
図３のループ文３０１の３行目の記述について記号実行を行う場合、ループ内記号実行部１１３は、ループ条件「z < y」に基づき、n-1回のループの実行後の変数の値「z_n-1」及び「y_n-1」を用いて「z_n-1 < y_n-1」（但し、n>0。以下省略））というパス条件を生成する。同様に５行目の記述について記号実行を行う場合、ループ内記号実行部１１３は、n
回のループの実行時の変数「x_n」の値を、ループをn-1回実行後の変数の値を用いて「x_n=x_n-1*2+2」と表す。

続いて、ループ内記号実行部１１３は、ループ内記述についてパスの探索を進めた結果、ループ内記述の末端に到達したか否かを判定する（Ｓ９１４）。例えば、図３のループ文３０１の１０行目の記述はループ内記述の末端に相当する。ループ内記号実行部１１３がループ内記述の末端に到達したと判定した場合（Ｓ９１４：ＹＥＳ）、処理はＳ９１５に進む。ループ内記号実行部１１３がループ内記述の末端に到達していないと判定した場合（Ｓ９１４：ＮＯ）、処理はＳ９１３に戻る。

Ｓ９１５では、ループ内記号実行部１１３は、ループ内記述におけるループ条件の否定に相当する条件をパス条件に追加する。ここでループ条件の否定は、n回のループ実行後
の変数の値を用いて生成する。例えば、図３のループ文３０１におけるループ条件「z_n < y_n)」の否定は「!(z_n < y_n)」となる（但しn≧0。以下省略。）。尚、以下の説明に
おいて、Ｓ９１５で追加した条件式のことを汎化脱出条件式と称する。

続いて、ループ内記号実行部１１３は、Ｓ９１３におけるパスの探索の過程で生成したパス条件及び変数状態に基づき汎化ループ内パス情報１５５を生成する（Ｓ９１６）。具体的には、ループ内記号実行部１１３は、まずＳ９１５の時点におけるノード名、初項、パス条件、及び変数状態を取得する。そしてループ内記号実行部１１３は、取得した変数状態に基づき、取得したパス条件に現れるn-1回のループ実行後の変数の値を、n回のループ実行後の変数の値を用いた式に置き換える。例えば、図３のソースコード１５１のループ文３０１について生成したパス条件「z_n-1 < y_n-1」は、ノード名が「M5」のノードに
おける変数状態「y_n=y_n-1」及び「z_n=z_n-1+1」に基づき「z_n-1 < y_n」というパス条件に
変換する。ループ内記号実行部１１３は、こうして生成したパス条件に加え、ループ内記号実行情報１５４から取得したノード名１５４１、初項１５４３、及び変数状態１５４５を汎化ループ内パス情報１５５として記憶する。

続いて、ループ内記号実行部１１３は、ループ文に含まれている全てのパスを探索済みか否かを判定する（Ｓ９１７）。ループ内記号実行部１１３が全てのパスを探索済みであると判定した場合（Ｓ９１７：ＹＥＳ）、ループ内記号実行処理Ｓ９００は終了する。一方、ループ内記号実行部１１３が全てのパスを探索済みでない（未探索のパスがある）と判定した場合（Ｓ９１７：ＮＯ）、処理はＳ９１８に進む。

Ｓ９１８では、ループ内記号実行部１１３は、未探索のパスを探索すべくＳ９１３からの処理を開始する。

図１０に図３のループ文３０１に基づくループ内記号実行情報１５４を示す。同図に示すように、ループ内記号実行情報１５４は、ノード名１５４１、行番号１５４２、初項１５４３、パス条件１５４４、及び変数状態１５４５の各項目を含む１つ以上のレコードで構成されている。ループ内記号実行情報１５４のレコードの一つはノードの一つに対応している。

上記項目のうち、ノード名１５４１には、ノード名が設定される。行番号１５４２には、当該ノードに対応するソースコード１５１の行番号が設定される。初項１５４３には、前述した初項が設定される。パス条件１５４４には当該ノードの前述したパス条件が設定される。前述したように、パス条件はループをn-1回実行後の変数の値を用いて表される
。変数状態１５４５には当該ノードにおける前述した変数状態が設定される。前述したように、ループn回実行時の変数状態はループn-1回実行後の変数状態を用いて表される。

図１１に図３のループ文３０１に基づき生成される汎化ループ内パス情報１５５を示す。同図に示すように、汎化ループ内パス情報１５５は、パス名１５５１、パス終端ノード１５５２、初項１５５３、パス条件１５５４、及び変数状態１５５５の各項目を有する一つ以上のレコードで構成されている。汎化ループ内パス情報１５５のレコードの一つはパス（以下、汎化ループ内パスとも称する。）の一つに対応している。

上記項目のうち、パス名１５５１には、当該パスのパス名が設定される。パス終端ノード１５５２には、パスの終端のノードが設定される。初項１５５３には、初項が設定される。パス条件１５５４には、パス条件が設定される。変数状態１５５５には、変数状態が設定される。

図１２は、ループ内パス特化部１１４が行う処理（以下、ループ内パス特化処理Ｓ１２００と称する。）を説明するフローチャートである。以下、同図とともにループ内パス特化処理Ｓ１２００について説明する。

まずループ内パス特化部１１４は、汎化ループ内パス情報１５５を取得する（Ｓ１２１
１）。続いて、ループ内パス特化部１１４は、特化ループ内パス情報１５６を参照し、ループ回数が0回の特化ループ内パス情報を生成済みか否かを判定する（Ｓ１２１２）。ル
ープ内パス特化部１１４がループ回数0回の特化ループ内パス情報を生成済みと判定した
場合（Ｓ１２１２：ＹＥＳ）、処理はＳ１２１５に進む。ループ内パス特化部１１４がループ回数が0回の特化ループ内パス情報が生成済みでない（未生成である）と判定した場
合（Ｓ１２１２：ＮＯ）、処理はＳ１２１３に進む。

ループ内パス特化部１１４は、Ｓ１２１１で取得した汎化ループ内パス情報１５５に基づき、ループ回数が0回の特化ループ内パス情報１５６を生成する（Ｓ１２１３）。

図１３（ａ）に、図１１の汎化ループ内パス情報１５５に基づきループ内パス特化部１１４が生成する、ループ回数が0回の特化ループ内パス情報１５６を示す。同図に示すよ
うに、特化ループ内パス情報１５６は、パス名１５６１、パス終端ノード１５６２、初項１５６３、パス条件１５６４、及び変数状態１５６５の各項目を含む一つ以上のレコードで構成されている。特化ループ内パス情報１５６のレコードの一つは一つのパス（以下、特化ループ内パスとも称する。）に対応している。ループ内パス特化部１１４は、上記ループ回数が0回の特化ループ内パスを汎化ループ内パスごとに１つ生成する。

上記項目のうち、パス終端ノード１５６２及び初項１５６３は、汎化ループ内パス情報１５５におけるパス終端ノード１５５２及び初項１５５３を継承する。パス条件１５６４及び変数状態１５６５については、以下に示すように、ループ内パス特化部１１４がパス条件１５５４及び初項１５５３に基づき生成する。

まずループ内パス特化部１１４は、汎化ループ内パス情報１５５のパス条件１５５４をループ回数0回でインスタンス化する。具体的には、ループ内パス特化部１１４は、パス
条件１５５４に現れる、n回のループを実行した後の変数の値に対してn=0を代入する。尚、n=0であるので、ループ内パス特化部１１４は、パス条件１５５４を構成する論理式の
うち「n > 0」という条件付きの論理式は使用せず、前述した汎化脱出条件式のみを使用
する。例えば、図１１の汎化ループ内パス情報１５５のパス名１５５１が「Q1」のパスの場合、ループ内パス特化部１１４は、「(z_n -1) < y_n」と「(z_n -1) % 3 == 0」の各式については「n > 0」という条件付きであるのでこれらは使用せず、汎化脱出条件式である
「!(z_n< y_n)」においてn=0とすることにより取得される「!(z₀ < y₀)」というパス条件を使用する。尚、以下の説明において、このように汎化脱出条件式をインスタンス化して得られる条件式のことを特化脱出条件式と称する。

続いて、ループ内パス特化部１１４は、変数状態１５６５を生成する。ここでループ回数が0回のとき変数状態１５６５は初項１５６３と一致し、また初項１５６３はループ実
行前の変数の値に相当する。そこでループ内パス特化部１１４は、0回のループを実行し
た後の変数の値を、初項として保持しているループ実行前の変数の値で表す。例えば、図１１に示す汎化ループ内パス情報１５５のパス名１５５１が「Q1」のパスの場合、0回の
ループを実行した後の変数の値「x_0」は初項１５５３の式「x₀=BL_x」より「x₀=BL_x」と表す。

図１２に戻り、続いて、ループ内パス特化部１１４は、Ｓ１２１３で生成したパス条件に現れる初項をループ実行前の変数の値を含む式に置換する（Ｓ１２１４）。例えば、図１１に示す汎化ループ内パス情報１５５の「Q1」の場合、ループ内パス特化部１１４は、パス条件「!(z₀< y₀)」を、初項１５５３の式「z₀=BL_z」及び「y₀=BL_y」に基づき「!(BL_z < BL_y)」と表す。

図１３（ｂ）に、図１３（ａ）のループ回数が0回の特化ループ内パス情報１５６につ
いて上記置換を行った後の特化ループ内パス情報１５６を示す。

図１２に戻り、続いて、ループ内パス特化部１１４は、生成済みの特化ループ内パス情報１５６のうちループ回数が最大のものを取得する（Ｓ１２１５）。尚、以下の説明において、ここのときに取得した特化ループ内パス情報１５６のループ回数をK-1回とする。

続いて、ループ内パス特化部１１４は、取得した特化ループ内パス情報（ループ回数はK-1回であるものとする。）と、Ｓ１２１１で取得した汎化ループ内パス情報１５５との
組み合わせに基づき、ループ回数がK回の特化ループ内パス情報１５６を生成する（Ｓ１
２１６）。尚、例えば、ループ回数がK-1回の特化ループ内パス情報１５６が２つ、汎化
ループ内パス情報１５５が２つである場合、ループ内パス特化部１１４は、ループ回数がK回の特化ループ内パス情報１５６を４つ生成する。

まずループ内パス特化部１１４は、変数状態１５６５を生成するため、汎化ループ内パス情報１５５に含まれるn及びn-1を、K及びK-1にインスタンス化する。さらにループ内パス特化部１１４は、ループ回数がK-1回の特化ループ内パス情報１５６の変数状態に基づ
き、ループをK-1回実行後の変数の値を、ループ実行前の変数の値を含む式に置換する。

例えば、図１１の汎化ループ内パス情報１５５のパス名が「Q1」のパスの変数状態「x_n=x_n-1 * 2 + 2」から、ループ回数が1回の特化ループ内パス情報を生成する場合、ループ内パス特化部１１４は、まず「x_n=x_n-1 * 2 + 2」を「x₁=x₀ * 2 + 2」とインスタンス化する。さらにループ内パス特化部１１４は、ループ回数が0回の特化ループ内パス情報１
５６におけるパス名が「Q1」の変数状態「x₀=BL_x」に基づき、「x₁=BL_x* 2 + 2」を生
成する。またループ内パス特化部１１４は、以上と同様の方法で「y₁=BL_y」及び「z₁=BL_z + 1」を生成する。

続いて、パス条件１５６４を生成するため、ループ内パス特化部１１４は、Ｓ１２１５で取得した特化ループ内パス情報１５６のパス条件１５６４から、前述した特化脱出条件式を除外する。例えば、ループ回数が0回の特化ループ内パス情報１５６におけるパス名
が「Q1」のパスの場合、ループ内パス特化部１１４は、特化脱出条件式「!(BL_z < BL_y)」を除外する。尚、以下において、特化脱出条件式を除外した後に残る式を脱出式除外式と称する。

続いて、ループ内パス特化部１１４は、汎化ループ内パスのパス条件をループ回数K回
でインスタンス化する。例えば、汎化ループ内パス情報１５５の「Q1」のパス条件を、ループ回数1回でインスタンス化する場合、ループ内パス特化部１１４は、「(z_n -1) < y_n && (z_n -1) % 3 == 0 && !(z_n < y_n)」のnに1を代入することで、「(z₁-1) < y₁ && (z₁ -1) % 3 == 0 && !(z₁< y₁)」を得る。さらにループ内パス特化部１１４は、特化ループ
内パス情報の変数状態に基づき、ループをK回実行後の変数の値を、ループ実行前の変数
の値を含む式に置換する。上記の例の場合、ループ内パス特化部１１４は、「y₁=BL_y」
及び「z₁=BL_z+ 1」に基づき、「(z₁ -1) < y₁&& (z₁ -1) % 3 == 0 && !(z₁ < y₁)」か
ら「((BL_z + 1) -1) < BL_y && ((BL_z+ 1) -1) % 3 == 0 && !((BL_z + 1) < BL_y)」
を生成する。そしてループ内パス特化部１１４は、生成した上記式を、上記脱出式除外式に論理積結合する。

図１４にループ回数が1回の特化ループ内パス情報１５６の例を示す。同図において、
パス名１５６１における「Q1-Q1」は、特化ループ内パス情報１５６のパス名１５６１が
「Q1」のパスと、汎化ループ内パス情報１５５のパス名１５５１が「Q1」のパスとに基づき生成したパスであることを示す。パス終端ノード１５６２は、生成元の汎化ループ内パス情報１５５のパス終端ノード１５５２を継承する。初項１５６３は、生成元の特化ルー
プ内パス情報１５６の初項１５６３を継承する。変数状態１５６５は、汎化ループ内パス情報１５５の変数状態１５５５と特化ループ内パス情報１５６の変数状態１５６５とに基づき、前述した方法で生成する。またパス条件１５６４は、特化ループ内パス情報１５６のパス条件１５６４、汎化ループ内パス情報１５５のパス条件１５５４、及び特化ループ内パス情報１５６の変数状態１５６５に基づき生成する。

図１５は、以上に説明した各機能（情報記憶部１１０、ループ外記号実行部１１２、ループ内記号実行部１１３、及びループ内パス特化部１１４）を利用して、ルール生成部１１５がルール情報を生成する処理（以下、ルール生成処理Ｓ１５００と称する。）を説明するフローチャートである。以下、同図とともにルール生成処理Ｓ１５００について説明する。

まずルール生成部１１５は、入力装置５４や通信装置５６を介して、ループ上限回数を取得する（Ｓ１５１１）。

続いて、ルール生成部１１５は、ルール情報１５７を参照し、取得したループ上限回数に対応するルールを生成済みか否かを判定する（Ｓ１５１２）。ルール生成部１１５が上限回数に対応するルールを生成済みであると判定した場合（Ｓ１５１２：ＹＥＳ）、ルール生成処理Ｓ１５００は終了する。ルール生成部１１５が上限回数に対応するルールを未生成であると判定した場合（Ｓ１５１２：ＮＯ）、処理はＳ１５１３に進む。

Ｓ１５１３では、ルール生成部１１５は、ループ内パス特化部１１４を制御してループ内パス特化処理Ｓ１２００を実行することにより、既に生成済みのループ回数がK-1回の
特化ループ内パス情報１５６に基づき、ループ回数がK回の特化ループ内パス情報１５６
を生成する。

続いて、ルール生成部１１５は、ループ外パス情報１５３を取得する（Ｓ１５１４）。続いて、ルール生成部１１５は、Ｓ１５１３で生成したループ回数がK回の特化ループ内
パス情報１５６と、Ｓ１５１４で取得したループ外パス情報１５３との組み合わせに基づき、ループ回数がK回のルールを生成する（Ｓ１５１５）。例えば、ルール生成部１１５
は、ループ回数がK回の特化ループ内パス情報１５６の特化ループ内パスが４つ、かつ、
取得したループ外パス情報１５３のループ外パスが２つである場合、ループ回数がK回の
ルールを８つ生成する。

まずルール生成部１１５は、特化ループ内パス情報１５６のパス条件１５６４とループ外パス情報１５３のパス条件１５３３とを論理積で結合することにより、ルールのパス条件を生成する。そしてルール生成部１１５は、生成したルールのパス条件に現れるループを実行した後の変数の値を表すシンボル値を、ループを実行する前の変数の値を表すシンボル値を含む式に置換する。さらにルール生成部１１５は、ループ外パス情報１５３のループ前変数状態１５３４に基づき、ループ実行前の変数の値を表すシンボル値を、当該変数が実際に保持している値に置換する。

例えば、図７に示すループ外パス情報１５３のパス名１５３１が「P1」のパスと、図１３（ｂ）に示すループ回数が0回の特化ループ内パス情報１５６のパス名１５６１が「Q1
」のパスとからパス条件を生成する場合は次のようになる。まず、ルール生成部１１５は、パス名１５３１が「P1」のパスのパス条件１５３３は「AL_x % 2 == 0」、ループ回数
が0回の特化ループ内パス情報１５６のパス条件１５６４は「!(BL_z < BL_y)」であるこ
とから、これらを論理積結合することにより「AL_x % 2 == 0 && !(BL_z < BL_y)」を生
成する。ここで上記式に現れるループ実行後の変数の値「AL_x」は「x₀」に一致することに注目する。また上記「x₀」の値は、上記特化ループ内パス情報１５６の変数状態１５６
５から「x₀=BL_x」である。そこでルール生成部１１５は、「AL_x」を「BL_x」に置換す
ることにより「BL_x % 2 == 0 && !(BL_z < BL_y)」を生成する。またループ外パス情報
１５３のループ前変数状態１５３４より「BL_x == X」、「BL_y == Y」、「BL_z == 0」
であるので、これらに基づき、ルール生成部１１５は、パス条件「X % 2 == 0 && !(0 < Y)」を生成する。

続いて、ルール生成部１１５は、ループ外パス情報１５３の変数状態１５３５と、特化ループ内パス情報１５６の変数状態１５６５とに基づき、パス実行結果を生成する。具体的には、ルール生成部１１５は、ループ外パス情報１５３の変数状態１５３５に現れるループ実行後の変数の値を表すシンボル値を、ループ実行前の変数の値を表すシンボル値に置換する。即ち、ルール生成部１１５は、ループ外パス情報１５３のループ前変数状態１５３４に基づき、ループを実行する前の変数の値を表すシンボル値を、当該変数が実際に保持している値に置換する。

例えば、ルール生成部１１５が、ループ外パス情報１５３のパス名１５３１が「P1」のパスと、ループ回数が0回の特化ループ内パス情報１５６のパス名１５６１が「Q1」のパ
スとに基づきパス実行結果を生成する場合は次のようになる。まずループ外パス情報１５３の変数状態１５３５は「x=AL_x」、特化ループ内パス情報１５６の変数状態１５６５は「x₀=BL_x」である。また前述したように「AL_x」は「x₀」に一致するので「x=BL_x」が
得られる。そしてルール生成部１１５は、ループ外パス情報１５３のループ前変数状態１５３４に基づき「x=X」を得る。同様の方法により、ルール生成部１１５は、「y=Y」及び「z=X」を得る。ここで例えば、ソースコード１５１において戻り値として返す変数の値
のみをルールのパス実行結果として採用するものとした場合、ルール生成部１１５は、図３に示したソースコード１５１の１６行目の記述に基づき、変数zの値を表す「z=X」をパス実行結果とする。

続いて、ルール生成部１１５は、生成した複数のルールに重複がある場合、重複するルールを削除する。また生成したルールのパス条件の充足可能性を確認し、充足不能と判明した場合はそのルールを削除する（Ｓ１５１６）。尚、論理式の充足可能性を確認する方法として例えば推論規則を用いる方法があるが、充足可能性を確認する方法は必ずしも限定されない。

図１６は、ループ外パス情報１５３とループ回数が0回の特化ループ内パス情報１５６
に基づきルール生成部１１５が生成する、ループ回数が0回の場合のルール情報１５７の
例である。同図に示すように、ルール情報１５７は、パス名１５７１、パス条件１５７２、及びパス実行結果１５７３の３つの項目を有する一つ以上のレコードで構成されている。

パス名１５７１には、生成元を特定する情報が設定される。例えば、「P1-Q1」は、当
該ルールが、ループ外パス情報１５３の「P1」と、ループ回数0回の特化ループ内パス情
報１５６の「Q1」に基づき生成されたことを示す。パス条件１５７２、及びパス実行結果１５７３には、前述した方法で生成された値が設定される。尚、本例では「P1-Q2」と「P1-Q1」のレコードの内容が重複しており、この場合、ルール生成部１１５は一方（例えば「P1-Q2」）を前述したＳ１５１６にて削除する。同様に「P2-Q2」も「P2-Q1」と重複し
ているため、ルール生成部１１５は一方をＳ１５１６の処理で削除する。

図１７は、ループ外パス情報１５３とループ回数1回の特化ループ内パス情報１５６に
基づきルール生成部１１５が生成する、ループ回数が1回の場合のルール情報１５７の例
である。同図に示すように、このルール情報１５７は、パス名１５７１、パス条件１５７２、及びパス実行結果１５７３の３つの項目を有する一つ以上のレコードで構成されてい
る。

パス名１５７１には、生成元を特定する情報が設定される。例えば、パス名「P1-Q1-Q1」は、当該ルールが、ループ外パス情報１５３の「P1」と、ループ回数1回の特化ループ
内パス情報１５６の「Q1-Q1」に基づき生成されたことを示す。パス条件１５７２及びパ
ス実行結果１５７３には、前述した方法で生成された値が設定される。尚、本例では、「P1-Q2-Q1」、「P1-Q2-Q2」、「P2-Q2-Q1」、及び「P2-Q2-Q2」のレコードは、夫々「P1-Q1-Q1」、「P1-Q1-Q2」、「P2-Q1-Q1」、及び「P2-Q1-Q2」のレコードと重複するため、ルール生成部１１５は一方をＳ１５１６の処理で削除する。また「P1-Q1-Q2」、「P2-Q1-Q1」、及び「P2-Q1-Q2」についてはパス条件１７１３が充足不能であるため、ルール生成部１１５はこれらをＳ１５１６の処理で削除する。

図１８はループの上限回数が1回に指定されている場合のルール情報１５７の例である
。前述したように入出力処理部１１６は上限回数の指定をユーザから受け付ける。そして、ルール生成部１１５を実行することにより、ループ回数が0回、1回、・・・K-1回、K回の夫々の場合についてルール情報１５７を生成する。入出力処理部１１６は、ルール情報１５７からループ回数が0回からK回の場合のルールを取得し、出力装置５５に出力（表示）する。同図に示す、ループ上限回数が1回の場合のルール情報１５７は、パス名１５７
１、パス条件１５７２、及びパス実行結果１５７３の各項目を含む３つのレコードで構成されている。尚、パス名１５７１に設定されているルール「P1-Q1」、「P2-Q1」、及び「P1-Q1-Q1」は、図１６に示したルール情報１５７及び図１７に示したルール情報１５７から、図１５のＳ１５１６の処理にて「P1-Q2」、「P2-Q2」、「P1-Q2-Q1」、「P1-Q2-Q2」、「P2-Q2-Q1」、「P2-Q2-Q2」、「P1-Q1-Q2」、「P2-Q1-Q1」、及び「P2-Q1-Q2」を削除し、削除後に残ったルールを集約した結果である。

尚、ループ上限回数が1回の場合のルール情報１５７を得るためにはルール情報１５７
を生成する必要があるが、既にループ上限回数を1回に設定して記号実行を行う前にルー
プ上限回数を0回に設定して記号実行を行っていた場合等、既にルール情報１５７が生成
済みである場合には改めてルール情報１５７を生成する必要がない。そのため、ルール生成部１１５は、予めループ上限回数0回の場合のルールがルール情報１５７に格納されて
いるかを確認し、上記ルールが格納されていない場合にのみルール情報１５７を生成すればよい。

以上に説明したように、仕様分析装置１００は、ループ文を含むソースコードからルールを再生するにあたり、ループ文に対するパス実行結果を、ループをn-1回実行後の変数
の値とループをn回実行後の変数の値の関係式として記憶する。そのため、例えば、ルー
プ回数がK-1回の場合のルールが再生済みである場合、上記関係式と上記ループ回数がK-1回の場合のルールを生成する過程で生成したパスの情報に基づき、記号実行を行うことなく、簡単な代入処理や論理演算処理によってループ回数がK回の場合のルールを生成する
ことができる。即ち、一度の記号実行で生成した上記関係式を再帰的に用いることで、記号実行を繰り返し行うことなく、簡単な代入処理及び論理演算処理で、任意のループ回数におけるルールを生成することができる。そのため、記号実行にかかる計算機のリソースの消費を抑えることができるとともに、ルールを取得するまでに要する時間を短縮することができる。

また仕様分析装置１００は、記号実行によって生成したルールを記憶するため、ループ上限回数を変更して複数回の記号実行を行う場合の処理量を削減することができる。例えば、ループ上限回数をL回にして記号実行を行った場合にはループ回数が0回からL回まで
の夫々に対応するルールが生成されて記憶され、例えば、その後にループ上限回数をL+1
回に変更して再度記号実行を行う場合は、ループ回数がL+1回の場合のルールのみを新規
に生成し、ループ回数0回からL回までのルールに追加すればよく、記号実行にかかる計算機のリソースの消費を抑えることができ、ルールを取得するまでに要する時間を短縮することができる。

このように本実施形態の仕様分析装置１００によれば、任意のループ文を含むソースコードについての記号実行を効率よく行うことができる。
［第２実施形態］

図１９は第２実施形態として説明する仕様分析装置１００の機能ブロック図である。第２実施形態の仕様分析装置１００も第１実施形態の仕様分析装置１００と同様のハードウェアによって実現される。

第２実施形態の仕様分析装置１００は、第１実施形態の仕様分析装置１００と同等の機能を備え、ループ内パス一般項化部１２１及び一般項化ルール生成部１２２の各機能をさらに備える。また第２実施形態の仕様分析装置１００の情報記憶部１１０は、第１実施形態の情報記憶部１１０と同様の情報を記憶するとともに、さらに一般項化ループ内パス情報１６１及び一般項化ルール情報１６２を記憶する。

ループ内パス一般項化部１２１は、汎化ループ内パス情報１５５を一般項化することにより一般項化ループ内パス情報１６１を生成する。一般項化ルール生成部１２２は、ループ外パス情報１５３及び一般項化ループ内パス情報１６１に基づき一般項で表現されたルールを生成し、生成したルールを一般項化ルール情報１６２として記憶する。

入出力処理部１１６は、一般項化ルール情報１６２を出力装置５５に出力（表示）する。また、入出力処理部１１６は、一般項化ルール情報１６２を、入力装置５４や通信装置５６を介して取得したループ上限回数にインスタンス化して出力（表示）する。

続いて、図２０に示すソースコード１５１を例として、第２実施形態の仕様分析装置１００の具体的な動作について説明する。同図に示すように、ソースコード１５１はＣ言語で記述されており、ループ文３０２を含む。

図２１は、ループ外記号実行部１１２が、ループ外記述の記号実行に際して図２０に示すソースコード１５１に基づき生成する探索木（以下、ループ外パス探索木２１００と称する。）である。ループ外記号実行部１１２は、ループ外パス探索木２１００を利用してループ外記号実行情報１５２を生成する。同図に示すように、ループ外パス探索木２１００は、夫々「N0」〜「N7」のノード名が付与された８つのノードを有する。

上記８つのノードのうち、ノード名が「N0」のノードは図２１のソースコード１５１の１行目の記述に対応し、ソースコード１５１の開始点を意味する「START」という手続き
を含む。またノード名が「N1」のノードは、図２１に示すソースコード１５１の２行目の記述に対応し、「z=0」という手続きを含む。またノード名が「N2」のノードは、図２１
に示すソースコード１５１の３〜６行目の記述、即ちループ文３０２に対応している。ノード名が「N3」のノードは、図２１に示すソースコード１５１の７行目に対応している。当該行には「if (x % 2 == 0) {」という条件分岐の記述がされており、ループ外記号実
行部１１２は、当該行を分岐点として、条件が「True」の場合と「False」の場合の２通
りのパスを探索する。尚、以下の説明において、これら２つのパスの夫々にパス名として「P1」，「P2」を付与する。

図２２及び図２３は、図２１のループ外パス探索木２１００に基づきループ外記号実行部１１２が生成するループ外記号実行情報１５２である。このうち図２２に示すループ外
記号実行情報１５２は、パス名が「P1」のパスに対応し、一方、図２３に示すループ外記号実行情報１５２は、パス名が「P2」のパスに対応する。

図２４は、ループ外記号実行部１１２が生成するループ外パス情報１５３である。パス終端ノード１５３２には、当該パスの終端ノードのノード名が設定される。図４に示すループ外パス探索木の場合はノード名が「N5」、「N7」のノードが終端ノードとなる。

図２５は、ループ内記号実行部１１３が、ループ文３０２について記号実行を行う際に生成する探索木（以下、ループ内パス探索木２５００と称する。）である。ループ内記号実行部１１３は、ループ内パス探索木２５００を利用してループ外記号実行情報１５２を生成する。同図に示すように、ループ内パス探索木２５００は、夫々「M0」〜「M4」のノード名が付与された５つのノードを有する。

上記５つのノードのうち、ノード名が「M0」のノードは図２０に示すソースコード１５１の３行目の記述に対応し、ソースコード１５１の開始点を意味する「START」という手
続きを含む。またノード名が「M1」のノードは、図２０に示すソースコード１５１の３行目の記述に対応し、「while ( (3 * z) < x ) {」という条件（以下、ループ条件と称す
る。）の記述を含む。またノード名が「M2」のノードは、図２０に示すソースコード１５１の４行目に対応している。またノード名が「M3」のノードは、図２０に示すソースコード１５１の５行目に対応している。またノード名が「M4」のノードはパスの終端ノードに対応している。尚、以下の説明において、上記パスのパス名として「Q1」を付与する。

図２６は、図２０のループ文３０２に基づき生成されるループ内記号実行情報１５４である。同図に示すループ内記号実行情報１５４は、ループ内記号実行部１１３により第１実施形態と同様の方法で生成される。

図２７は図２０のループ文３０２に基づき生成される汎化ループ内パス情報１５５である。同図に示す汎化ループ内パス情報１５５は、ループ内記号実行部１１３により第１実施形態と同様の方法で生成される。

図２８は、汎化ループ内パス情報１５５に基づきループ内パス一般項化部１２１が生成する一般項化ループ内パス情報１６１である。同図に示すように、一般項化ループ内パス情報１６１は、パス名１６１１、パス終端ノード１６１２、初項１６１３、パス条件１６１４、及び一般項１６１５の各項目を有する一つ以上のレコードで構成されている。ループ内パス一般項化部１２１は、汎化ループ内パス情報１５５の変数状態１５５５を漸化式とみなしてその一般項を求める。尚、漸化式からその一般項を求める方法としては、例えば、非特許文献１の第１０章に記載されている方法がある。

図２９は、ループ外パス情報１５３及び一般項化ループ内パス情報１６１に基づき一般項化ルール生成部１２２が生成する一般項化ルール情報１６２である。一般項化ルール生成部１２２は、一般項化ループ内パス情報１６１とループ外パス情報１５３とを組合せることにより一般項化ルール情報１６２を生成する。本例の場合、一般項化ルール生成部１２２は２つの一般項化ルールを生成する。

まず一般項化ルール生成部１２２は、ループ外パス情報１５３のパス条件１５３３に基づき一般項化ルール情報１６２のパス条件１６２２を生成する。一般項化ルール生成部１２２は、ループ外パス情報１５３のパス条件１５３３に現れるループ実行後の変数の値を表すシンボル値を、ループ実行前の変数の値を表すシンボル値を含む式に置換する。さらに、一般項化ルール生成部１２２は、ループ前変数状態１５３４に基づき、上記ループ実行前の変数の値を表すシンボル値を、当該変数が実際に保持する値に置換する。

例えば、ループ外パス情報１５３のパス名１５３１が「P1」のパスと、一般項化ループ内パス情報１６１のパス名１６１１が「Q1」のパスに基づきパス条件を生成する場合を考える。図２４に示すように、ループ外パス情報１５３のパス条件１５３３は「AL_x % 2 == 0」である。ここで、パス条件１５３３におけるループ実行後の変数の値「AL_x」は図
２８の一般項化ループ内パス情報１６１の一般項１６１５の「x_n」に一致することに注目する。そして上記「x_n」の値は、一般項１６１５より「x_n=x₀+2*n」であること、及び初
項１６１３より「x₀=BL_x」であることから、一般項化ルール生成部１２２は、上記パス
条件１５３３を「(BL_x + 2*n) % 2 == 0」に変換する。またループ前変数状態１５３４
より「BL_x == X」であるため、これに基づき一般項化ルール生成部１２２は「(X + 2*n)
% 2 == 0」を生成する。

続いて、一般項化ルール生成部１２２は、ループ外パス情報１５３の変数状態１５３５と、一般項化ループ内パス情報１６１の一般項１６１５から、一般項化ルール情報１６２のパス実行結果１６２３を生成する。具体的には、一般項化ルール生成部１２２は、ループ外パス情報１５３の変数状態１５３５に現れるループ実行後の変数の値を表すシンボル値を、ループ実行前の変数の値を表すシンボル値に置換する。さらに一般項化ルール生成部１２２は、ループ外パス情報１５３のループ前変数状態１５３４に基づき、上記ループ実行前の変数の値を表すシンボル値を、当該変数が実際に保持する値に置換する。

例えば、ループ外パス情報１５３のパス名１５３１が「P1」のパスと、一般項化ループ内パス情報１６１のパス名１６１１が「Q1」パスとに基づき一般項化ルール情報１６２のパス実行結果１６２３を生成する場合を考える。ここでループ外パス情報１５３の変数状態１５３５は「x=AL_x」、一般項化ループ内パス情報１６１の一般項１６１５は「x_n=x₀+2*n」である。上述のとおり「AL_x」は「x_n」に一致すること、及び初項１６１３より「x₀=BL_x」であることから、一般項化ルール生成部１２２は「x=BL_x + 2*n」を得る。そして、一般項化ルール生成部１２２は、ループ外パス情報１５３のループ前変数状態１５３４に基づき「x=X + 2*n」を得る。同様の方法により「z=X + 2*n」が得られる。ここで図２０に示したソースコード１５１において戻り値として返す変数の値のみ、ルールのパス実行結果として採用するものとすれば、一般項化ルール生成部１２２は、ソースコード１５１の１２行目に基づき、変数zの値を表す「z=X + 2*n」をパス実行結果として採用する。

続いて、一般項化ルール生成部１２２は、汎化ループ内パス情報１５５のパス条件１５５４に基づき、一般項化ルール情報１６２におけるループ回数nの制約条件１６２４を生
成する。まず一般項化ルール生成部１２２は、パス条件１５５４に含まれるループの実行回数がn回における変数の値を、一般項化ループ内パス情報１６１の一般項１６１５に置
換する。さらに一般項化ルール生成部１２２は、一般項化ループ内パス情報１６１の初項１６１３及びループ外パス情報１５３のループ前変数状態１５３４に基づき、シンボル値の置換を行う。

例えば、一般項化ルール生成部１２２が、ループ外パス情報１５３のパス名１５３１が「P1」のパスと、一般項化ループ内パス情報１６１のパス名１６１１が「Q1」のパスとに基づき、一般項化ルール情報１６２におけるループ回数nの制約条件１６２４を生成する
場合を考える。まず一般項化ルール生成部１２２は、一般項化ループ内パス情報１６１のパス条件１６１４の式「3 * (z_n -1) < x_n - 2(但しn>0) && !(3 * z_n < x_n) (但しn≧0)」を、一般項１６１５に基づき、「3 * ((z₀ + n) -1) < (x₀ + 2*n) - 2 (但しn>0) && !(3 * (z₀ + n) < (x₀ + 2*n)) (但しn≧0)」に変換する。そして一般項化ルール生成部
１２２は、初項１６１３に基づき、上記式を3 * ((BL_z + n) -1) < (BL_x + 2*n) - 2 (但しn>0) && !(3 * (BL_z + n) < (BL_x + 2*n)) (但しn≧0)」に変換する。さらに一般
項化ルール生成部１２２は、ループ前変数状態１５３４に基づき、上式を「3 * (n -1) <
X + 2*n - 2 (但しn>0) && !(3 * n < X + 2*n) (但しn≧0)」に変換する。

図３０は、入出力処理部１１６が、一般項化ルール情報１６２に基づき出力装置５５に出力する、一般項化ルールを表示する画面の例（以下、一般項化ルール表示画面３０００と称する。）である。

入出力処理部１１６は、同画面に設けられているループ上限回数の入力受付欄３０１０を介して、ユーザからループ上限回数の入力を受け付ける。また入出力処理部１１６は、同画面に設けられているルール展開実行ボタン３０１２が押下されると、一般項化ルール情報１６２に含まれるループ回数を表す変数nに0から上記ループ上限回数までの値を順次代入してその結果を取得する。

例えば、一般項化ルール情報１６２に対して、ユーザがループ上限回数の入力受付欄３０１１に1を入力し、ルール展開実行ボタン３０１２を押下した場合、入出力処理部１１
６は、まず一般項化ルール情報１６２の「P1-Q1」及び「P2-Q1」のnに0を代入することで、展開後ルール表示欄３０１３における「P1-Q1-0」及び「P2-Q1-0」の内容（一般項で表現されたルールを具体化した情報）を生成する。次に入出力処理部１１６は、「P1-Q1」
及び「P2-Q1」のnに1を代入することで、展開後ルール表示欄３０１３における「P1-Q1-1」及び「P2-Q1-1」の内容（一般項で表現されたルールを具体化した情報）を生成する。

一般項化ルール情報１６２におけるループ回数nの制約条件１６２４は、展開後ルール
表示欄３０１３における制約条件３０１４に基づき生成される。入出力処理部１１６は、パス条件３０１５に基づき制約条件３０１４の論理積について充足可能性を判定し、充足不能の場合には、そのルールを非表示あるいは強調表示（太枠表示、グレーアウト等）などとする。本例では「P1-Q1-1」が太枠表示されている。

このように第２実施形態の仕様分析装置１００は、汎化ループ内パス情報を表現した漸化式の一般項を求めることにより、ループ文をn回実行した場合における変数の値と上記nを含む式との関係式である一般項化ループ内パス情報１６１を生成し、一般項化ループ内パス情報１６１とループ外パス情報１５３とに基づき、一般項で表現されたルールである一般項化ルール情報を生成するので、ユーザが利用しやすい形でソフトウェアの仕様（ルール）に関する情報を提供することができる。

ところで、本発明は上記の実施形態に限定されるものではなく、その要旨を逸脱しない範囲で種々変更可能であることはいうまでもない。例えば、上記の実施形態は本発明を分かりやすく説明するために詳細に説明したものであり、必ずしも説明した全ての構成を備えるものに限定されるものではない。また上記実施形態の構成の一部について、他の構成の追加・削除・置換をすることが可能である。

例えば、任意のKについて、ループ回数がK-1回の場合のルールとループ回数がK回の場
合のルールとを比較した場合、例えば、係数の値が規則的に増加もしくは減少する等、ルールの間に一定の規則性を見いだせることがある。またその場合、ループの実行回数が実際の（予め想定されている）ループの最大実行回数を超えた場合に上記規則性の逸脱が見られることがある。そこで、例えば、ルール生成部１１５が、ループ回数0回の場合のル
ール、1回の場合のルール、・・・K-1回の場合のルール、K回の場合のルール、K+1回の場合のルール、・・・と継続的にルールを監視し、上記規則性の逸脱を検知した場合に自動的にユーザに警告等の情報を出力するようにする。これによりユーザは実際のループの最大実行回数を容易かつ精度よく把握することができる。尚、上記規則性を検出する方法としては、例えば、上記ルールを構成している数字や演算子に関する情報を抽出し、それら
の情報を機械学習のアルゴリズムを活用して分類するという方法がある。

また例えば、ソースコードに複数のループ文が含まれている場合、仕様分析装置１００が、ループ文ごとにループ上限回数の指定を受け付け、ループ文ごとに、情報記憶部１１０が記憶している特化ループ内パス情報１５６のうちループ回数が最大のものを取得し、ループ文ごとに、取得した特化ループ内パス情報１５６に汎化ループ内パス情報１５５を再帰的に適用することによりループの上限回数までの特化ループ内パス情報１５６を生成するようにしてもよい。

図３１は、入出力処理部１１６が出力装置５５に出力（表示）するループ上限回数の指定画面３１００の例である。ループ上限回数の指定画面３１００は、ソースコード表示欄３１１１と、ループ上限回数登録欄３１１２とを含む。ループ上限回数登録欄３１１２は、ループ文位置特定結果３１１３、ループ上限回数入力受付部３１１４、ループ上限回数一括入力受付部３１１５、ループ上限回数一括設定ボタン３１１６、ループ文抽出ボタン３１１７、及びループ上限回数登録ボタン３１１８を含む。

まず入出力処理部１１６は、ソースコードを取得し、ソースコード表示欄３１１１に表示する。ユーザがループ文抽出ボタン３１１７を押下すると、入出力処理部１１６は、上記ソースコードを参照し、ループ文の位置を特定する。本実施例では、ループ文３１５１及び３１５２の夫々の開始行及び終了行を特定する。そして、入出力処理部１１６は、上記ループ文３１５１及び３１５２の開始行及び終了行を、ループ文位置特定結果３１１３に表示する。

ユーザは、ループ文位置特定結果３１１３に示されている各ループ文のループ上限回数を、夫々に対応するループ上限回数入力受付部３１１４に入力する。またユーザは、ループ上限回数一括入力受付部３１１５に全ループ文に適用するループ上限回数を入力し、ループ上限回数一括設定ボタン３１１６を押下することで、ループ上限回数入力受付部３１１４に同じ値を（各ループ文に同じ上限回数を）一括設定することもできる。

以上のようにしてループ上限回数を入力した後、ユーザがループ上限回数登録ボタン３１１８を押下すると、入出力処理部１１６は、各ループ文に対するループ上限回数を取得する。

また上記の各構成、機能部、処理部、処理手段等は、それらの一部または全部を、例えば、集積回路で設計する等によりハードウェアで実現してもよい。また上記の各構成、機能等は、プロセッサがそれぞれの機能を実現するプログラムを解釈し、実行することによりソフトウェアで実現してもよい。各機能を実現するプログラム、テーブル、ファイル等の情報は、メモリやハードディスク、ＳＳＤ（Solid State Drive）等の記録装置、また
はＩＣカード、ＳＤカード、ＤＶＤ等の記録媒体に置くことができる。

また上記の各図において、制御線や情報線は説明上必要と考えられるものを示しており、必ずしも実装上の全ての制御線や情報線を示しているとは限らない。例えば、実際にはほとんど全ての構成が相互に接続されていると考えてもよい。

また以上に説明した仕様分析装置１００の各種機能部、各種処理部、各種データベースの配置形態は一例に過ぎない。各種機能部、各種処理部、各種データベースの配置形態は、仕様分析装置１００が備えるハードウェアやソフトウェアの性能、処理効率、通信効率等の観点から最適な配置形態に変更し得る。

また前述したデータベースの構成（スキーマ（Schema）等）は、リソースの効率的な利
用、処理効率向上、アクセス効率向上、検索効率向上等の観点から柔軟に変更し得る。

１００ 仕様分析装置、１１０ 情報記憶部、１１１ ループ文特定部、１１２ ループ外記号実行部、１１３ ループ内記号実行部、１１４ ループ内パス特化部、１１５ ルール生成部、１１６ 入出力処理部１１６ 入出力処理部、１２１ ループ内パス一般項化部、１２２ 一般項化ルール生成部、１５１ ソースコード、１５２ ループ外記号実行情報、１５３ ループ外パス情報、１５４ ループ内記号実行情報、１５５ 汎化ループ内パス情報、１５６ ループ外パス情報、１５７ ルール情報、１６１ 一般項化ループ内パス情報、１６２ 一般項化ルール情報、３０１ ループ文、３０２ ループ文、４００ ループ外パス探索木、
８００ ループ内パス探索木、３０００ 一般項化ルール表示画面、Ｓ１２００ ループ内パス特化処理、Ｓ１５００ ルール生成処理

Claims (10)

1. ソフトウェアの仕様を分析する装置であって、
   分析対象のソフトウェアを実現するプログラムのソースコードを記憶する記憶部と、
   前記ソースコードに含まれているループ文の記述を特定するループ文特定部と、
   特定した前記ループ文以外の前記ソースコードの記述について記号実行を行うことにより、前記ソースコードのパス条件及びパス実行結果を含む情報であるループ外パス情報を、前記ループ文の実行前における変数の値と前記ループ文の実行後における変数の値とを用いて生成するループ外記号実行部と、
   特定した前記ループ文について記号実行を行うことにより、前記ソースコードに含まれている各変数について、前記ループ文をｎ−１回実行した後における当該変数の値と、前記ループ文をｎ回実行した後における当該変数の値との関係を示す情報である汎化ループ内パス情報を生成する、ループ内記号実行部と、
   ループを特定回数実行した場合における前記ソースコードのパスに関する情報である特化ループ内パス情報を生成するループ内パス特化部と、
   前記ループ内パス特化部が生成した前記特化ループ内パス情報のうち、任意回数だけループを実行した場合における変数の値を含む第１の特化ループ内パス情報を取得し、前記第１の特化ループ内パス情報に前記汎化ループ内パス情報を適用することにより、前記第１の特化ループ内パス情報よりもループ回数が１つ大きい第２の特化ループ内パス情報を生成し、前記第２の特化ループ内パス情報と前記ループ外パス情報とに基づき、前記ソフトウェアの仕様を表すルールを含む情報であるルール情報を生成するルール生成部、
   を備える、ソフトウェア仕様分析装置。
2. 請求項１に記載のソフトウェア仕様分析装置であって、
   前記ループ内パス特化部が生成した前記特化ループ内パス情報を記憶する記憶部を備え、
   前記ルール生成部は、ループの上限回数の指定を受け付け、前記記憶部が記憶している前記特化ループ内パス情報のうちループ回数が最大のものを取得し、取得した前記特化ループ内パス情報に前記汎化ループ内パス情報を再帰的に適用することにより前記ループ上限回数までの前記特化ループ内パス情報を生成し、生成した前記特化ループ内パス情報と前記ループ外パス情報とを用いて前記ルールを生成する、
   ソフトウェア仕様分析装置。
3. 請求項１に記載のソフトウェア仕様分析装置であって、
   前記ルール生成部は、前記ソースコードに含まれているループ文ごとにループの上限回数の指定を受け付け、前記ループ文ごとに、前記記憶部が記憶している前記特化ループ内パス情報のうちループ回数が最大のものを取得し、前記ループ文ごとに、取得した前記特化ループ内パス情報に前記汎化ループ内パス情報を再帰的に適用することにより前記ループの上限回数までの前記特化ループ内パス情報を生成する、
   ソフトウェア仕様分析装置。
4. 請求項１に記載のソフトウェア仕様分析装置であって、
   前記汎化ループ内パス情報を表現した漸化式の一般項を求めることにより、前記ループ文をn回実行した場合における前記変数の値と、前記nを含む式との関係式である一般項化ループ内パス情報を生成するループ内パス一般項化部と、
   前記一般項化ループ内パス情報と前記ループ外パス情報とに基づき、一般項で表現されたルールである一般項化ルール情報を生成する、一般項化ルール生成部と、
   をさらに備える、ソフトウェア仕様分析装置。
5. 請求項４に記載のソフトウェア仕様分析装置であって、
   前記ループ文の実行回数の指定を受け付け、受け付けた前記実行回数を前記一般項化ルール情報に代入することにより、前記一般項で表現されたルールを具体化した情報を出力する出力処理部を備える、
   ソフトウェア仕様分析装置。
6. 情報処理装置が、
   分析対象のソフトウェアを実現するプログラムのソースコードを記憶するステップ、
   前記ソースコードに含まれているループ文の記述を特定するステップ、
   特定した前記ループ文以外の前記ソースコードの記述について記号実行を行うことにより、前記ソースコードのパス条件及びパス実行結果を含む情報であるループ外パス情報を、前記ループ文の実行前における変数の値と前記ループ文の実行後における変数の値とを用いて生成するステップ、
   特定した前記ループ文について記号実行を行うことにより、前記ソースコードに含まれている各変数について、前記ループ文をｎ−１回実行した後における当該変数の値と、前記ループ文をｎ回実行した後における当該変数の値との関係を示す情報である汎化ループ内パス情報を生成するステップ、
   ループを特定回数実行した場合における前記ソースコードのパスに関する情報である特化ループ内パス情報を生成するステップ、
   生成した前記特化ループ内パス情報のうち、任意回数だけループを実行した場合における変数の値を含む第１の特化ループ内パス情報を取得し、前記第１の特化ループ内パス情報に前記汎化ループ内パス情報を適用することにより、前記第１の特化ループ内パス情報よりもループ回数が１つ大きい第２の特化ループ内パス情報を生成し、前記第２の特化ループ内パス情報と前記ループ外パス情報とに基づき、前記ソフトウェアの仕様を表すルールを含む情報であるルール情報を生成するステップ、
   を実行する、ソフトウェア仕様分析方法。
7. 請求項６に記載のソフトウェア仕様分析方法であって、
   前記情報処理装置が、
   生成した前記特化ループ内パス情報を記憶するステップ、
   ループの上限回数の指定を受け付け、記憶している前記特化ループ内パス情報のうちループ回数が最大のものを取得し、取得した前記特化ループ内パス情報に前記汎化ループ内パス情報を再帰的に適用することにより前記ループ上限回数までの前記特化ループ内パス情報を生成し、生成した前記特化ループ内パス情報と前記ループ外パス情報とを用いて前記ルールを生成するステップ、
   をさらに実行する、ソフトウェア仕様分析方法。
8. 請求項６に記載のソフトウェア仕様分析方法であって、
   前記情報処理装置が、前記ソースコードに含まれているループ文ごとにループの上限回数の指定を受け付け、前記ループ文ごとに、記憶している前記特化ループ内パス情報のうちループ回数が最大のものを取得し、前記ループ文ごとに、取得した前記特化ループ内パス情報に前記汎化ループ内パス情報を再帰的に適用することにより前記ループの上限回数までの前記特化ループ内パス情報を生成するステップ、
   をさらに実行する、ソフトウェア仕様分析方法。
9. 請求項６に記載のソフトウェア仕様分析方法であって、
   前記情報処理装置が、
   前記汎化ループ内パス情報を表現した漸化式の一般項を求めることにより、前記ループ文をn回実行した場合における前記変数の値と、前記nを含む式との関係式である一般項化ループ内パス情報を生成するステップ、
   前記一般項化ループ内パス情報と前記ループ外パス情報とに基づき、一般項で表現され
   たルールである一般項化ルール情報を生成するステップ、
   をさらに実行する、ソフトウェア仕様分析方法。
10. 請求項９に記載のソフトウェア仕様分析方法であって、
    前記情報処理装置が、前記ループ文の実行回数の指定を受け付け、受け付けた前記実行回数を前記一般項化ルール情報に代入することにより、前記一般項で表現されたルールを具体化した情報を出力するステップ、
    をさらに実行する、ソフトウェア仕様分析方法。
    
    
    
    

Images