(57)【要約】【課題】  再帰データを扱うプログラムをモデル検査法により効率的に検証すること。【解決手段】  情報処理装置であって、再帰データに関する再帰表明情報を含む検証対象ソースファイルを解析して再帰表明情報を抽出する構文解析手段と、再帰表明情報から、再帰データの要素数を所定数に限定した限定表明情報を生成する限定表明生成手段と、検証対象ソースファイルにおいて、再帰表明情報を生成された限定表明情報に置換して、モデル検査によるプログラム検証を行なうための検証用ファイルを生成する検証用ファイル生成手段と、を備えることを特徴とする。【選択図】  図１
2011154568.tif 000002
【特許請求の範囲】
【請求項１】
再帰データに関する再帰表明情報を含む検証対象ソースファイルを解析して前記再帰表明情報を抽出する構文解析手段と、
前記再帰表明情報から、前記再帰データの要素数を所定数に限定した限定表明情報を生成する限定表明生成手段と、
前記検証対象ソースファイルにおいて、前記再帰表明情報を、生成された前記限定表明情報に置換して、モデル検査によるプログラム検証を行なうための検証用ファイルを生成する検証用ファイル生成手段と、
を備えることを特徴とする情報処理装置。
【請求項２】
前記限定表明生成手段は、
前記再帰データの要素数を、０から前記所定数までの各要素数に限定した複数の限定表明情報を生成し、
前記検証用ファイル生成手段は、
前記検証対象ソースファイルにおいて、前記再帰表明情報を、生成された前記複数の限定表明情報の各々に置換して、モデル検査によるプログラム検証を行なうための複数の検証用ファイルを生成することを特徴とする請求項１に記載の情報処理装置。
【請求項３】
前記限定表明生成手段は、
前記再帰データの要素数を、０から前記所定数までの各要素数に限定した事前条件と、前記再帰データの構造がどのように変わるのかを示す事後条件とを生成することを特徴とする請求項１又は２に記載の情報処理装置。
【請求項４】
前記再帰表明情報は、推移閉包に関する表明を示す情報であり、前記限定表明生成手段は、前記構文解析手段による構文解析により得たデータ型情報に基づいて、推移閉包の要素の数を０から前記所定数までの限定要素数に限定した表明を生成することを特徴とする請求項１、２又は３に記載の情報処理装置。
【請求項５】
前記検証用ファイル生成手段は、更に、前記検証対象ソースファイルが関数の再帰呼出しを含む場合に、該関数の再帰呼出しを、ダミー関数の呼出しに置換することを特徴とする請求項１乃至４の何れか１項に記載の情報処理装置。
【請求項６】
前記検証用ファイル生成手段は、前記検証対象ソースファイル中の関数が再帰呼出しを行っている場合に、該関数と同じ引数と関数型と表明とを持つダミー関数を作成し、再帰呼出しをダミー関数の呼出しに変更することを特徴とする請求項１乃至５の何れか１項に記載の情報処理装置。
【請求項７】
再帰データに関する再帰表明情報を含む検証対象ソースファイルを解析して前記再帰表明情報を抽出する構文解析ステップと、
前記再帰表明情報から、前記再帰データの要素数を所定数に限定した限定表明情報を生成する限定表明生成ステップと、
前記検証対象ソースファイルにおいて、前記再帰表明情報を、生成された前記限定表明情報に置換して、モデル検査によるプログラム検証を行なうための検証用ファイルを生成する検証用ファイル生成ステップと、
を含むことを特徴とするプログラム検証方法。
【請求項８】
コンピュータに、
再帰データに関する再帰表明情報を含む検証対象ソースファイルを解析して前記再帰表明情報を抽出する構文解析ステップと、
前記再帰表明情報から、前記再帰データの要素数を所定数に限定した限定表明情報を生成する限定表明生成ステップと、
前記検証対象ソースファイルにおいて、前記再帰表明情報を、生成された前記限定表明情報に置換して、モデル検査によるプログラム検証を行なうための検証用ファイルを生成する検証用ファイル生成ステップと、
を実行させることを特徴とするプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、モデル検査手法を用いてプログラムを検証するための技術に関する。
【背景技術】
【０００２】
プログラムを解析し、不具合を検出する方法の一例が特許文献１及び２、並びに非特許文献１及び２に記載されている。また、この種の検出方法の一種として知られているモデル検査手法は、特許文献２及び非特許文献１に開示がある。モデル検査手法とは、システムやソフトウェアの振る舞いを表した有限個の「状態（state）」および状態間の遷移(transition)からなる有限状態空間(limited state space)において、調べたい性質（プロパティ）が成立するか否かを、網羅探索により調べる手法である。とくに、探索の深さを限定した有界モデル検査法は、効率的な不具合検出方法として注目されている。この方法では、プログラム中の変数の値および制御フロー上の位置の組合せを「状態」としてプログラムを有限状態空間に変換して有界モデル検査を適用する。変数の値の組合せと、プログラム中での値の変化とを制御フローに沿って追跡するので、精確な解析を行うことができる。
【０００３】
調べたい性質を表現する一つの考え方に「契約による設計」（Design by Contract）がある（非特許文献２）。この考え方では、ソースコードに、関数の開始時点の状態を示す事前条件と終了時点の状態を示す事後条件と関数の実行により変らない状態を示す不変条件とを表明として記述し、表明に照らしてソースコードが正しく記述されているかを検証する。
【先行技術文献】
【特許文献】
【０００４】
【特許文献１】特開２００８−２１００５９号
【特許文献２】特開２００９−２１１５０３号
【非特許文献】
【０００５】
【非特許文献１】F. Ivancic, I. Shlyakhter, A. Gupta, M. Ganai, V. Kahlon,C.Wang, and Z. Yang. Model Checking C Programs Using F-SOFT. In Proc. ICCD’05, 2005.
【非特許文献２】B. Meyer. Applying ”Design by Contract”. IEEE Computer,Vol.25, No.10, pages 40-51, 1992.
【発明の概要】
【発明が解決しようとする課題】
【０００６】
しかしながら、上述したモデル検査法により、例えば、リストやツリーなど同じ構造を持つ変数同士が繰り返し連結されてできた再帰データを扱うプログラムを、検証するのは困難である。その理由は、繰り返し回数が決まっていないため、再帰データの変数の数も決まらず、プログラムを有限状態空間に変換することができないからである。
【０００７】
詳しく説明すると、再帰データを扱うプログラムは、引数で渡された再帰データの一部分を処理し、残りの部分に関して同じ関数を再帰的に呼出して処理をさせるという再帰関数の再帰呼出しとして記述される。しかし、再帰関数内で定義された変数は、１回目の呼出しにおける変数、２回目の呼出しにおける変数、・・・Ｎ回目の呼出しにおける変数・・・というように呼出し毎に異なる変数として実体化される。このため、再帰呼出しの繰り返し回数が決まらなければ、再帰関数内で定義された変数の数も決まらず、プログラムを有限状態空間に変換することができない。その結果、モデル検査法を適用することができない。
【０００８】
以上を踏まえ、本発明は、上記課題を解決することを目的とする。
【課題を解決するための手段】
【０００９】
上記目的を達成するため、本発明に係る情報処理装置は、
再帰データに関する再帰表明情報を含む検証対象ソースファイルを解析して前記再帰表明情報を抽出する構文解析手段と、
前記再帰表明情報から、前記再帰データの要素数を所定数に限定した限定表明情報を生成する限定表明生成手段と、
前記検証対象ソースファイルにおいて、前記再帰表明情報を、生成された前記限定表明情報に置換して、モデル検査によるプログラム検証を行なうための検証用ファイルを生成する検証用ファイル生成手段と、
を備えることを特徴とする。
【００１０】
上記目的を達成するため、本発明に係るプログラム検証方法は、
再帰データに関する再帰表明情報を含む検証対象ソースファイルを解析して前記再帰表明情報を抽出する構文解析ステップと、
前記再帰表明情報から、前記再帰データの要素数を所定数に限定した限定表明情報を生成する限定表明生成ステップと、
前記検証対象ソースファイルにおいて、前記再帰表明情報を、生成された前記限定表明情報に置換して、モデル検査によるプログラム検証を行なうための検証用ファイルを生成する検証用ファイル生成ステップと、
を含むことを特徴とする。
【００１１】
上記目的を達成するため、本発明に係るプログラムは、
コンピュータに、
再帰データに関する再帰表明情報を含む検証対象ソースファイルを解析して前記再帰表明情報を抽出する構文解析ステップと、
前記再帰表明情報から、前記再帰データの要素数を所定数に限定した限定表明情報を生成する限定表明生成ステップと、
前記検証対象ソースファイルにおいて、前記再帰表明情報を、生成された前記限定表明情報に置換して、モデル検査によるプログラム検証を行なうための検証用ファイルを生成する検証用ファイル生成ステップと、
を実行させることを特徴とする。
【発明の効果】
【００１２】
本発明によれば、再帰データを扱うプログラムをモデル検査法により効率的に検証することができる。
【図面の簡単な説明】
【００１３】
【図１】本発明の実施形態としてのシステムの全体構成を示す概略図である。
【図２】本発明の実施形態としてのシステムの全体的な処理の流れを示す概略図である。
【図３】本発明の実施形態としてのシステムにおける表明処理の流れを示す概略図である。
【図４】本発明の実施形態としてのシステムにおける事前条件及び事後条件の生成処理を示す図である。
【図５】本発明の実施形態としてのシステムにおけるソースコードのデータ型情報及び関数呼出し情報を示す図である。
【図６】本発明の実施形態としてのシステムにおいて、ソースコード中の再帰表明に関する情報を示す図である。
【図７】本発明の実施形態としてのシステムにおいて、推移閉包に関する表明について説明する図である。
【図８】本発明の実施形態としてのシステムにおけるソースコードのデータ型及び関数の具体例を示す図である。
【図９】本発明の実施例としてのシステムにおいて、ソースコード中の再帰表明の例を示す図である。
【図１０】本発明の実施例としてのシステムにおけるソースコードのデータ型情報及び関数呼出し情報の具体例を示す図である。
【図１１】本発明の実施例としてのシステムにおいて、ソースコード中の再帰表明に関する情報の具体例を示す図である。
【図１２】本発明の実施例としてのシステムにおいて、ソースコード中の事前条件の要素数を限定する処理の具体例を示す図である。
【図１３】本発明の実施例としてのシステムにおいて、ソースコード中の事後条件の要素数を限定する処理の具体例を示す図である。
【図１４】本発明の実施例としてのシステムにおいて、ソースコード中の事後条件の要素数を限定する処理の具体例を示す図である。
【図１５】本発明の実施例としてのシステムにおいて、ソースコード中の事後条件の要素数を限定する処理の具体例を示す図である。
【図１６】本発明の実施例としてのシステムにおいて、ソースコードの表明及び呼出し先の置換によって生成される検証用ファイルの具体例を示す図である。
【発明を実施するための形態】
【００１４】
以下に、図面を参照して、本発明の実施の形態について例示的に詳しく説明する。ただし、以下の実施の形態に記載されている構成要素はあくまで例示であり、本発明の技術範囲をそれらのみに限定する趣旨のものではない。
【００１５】
（第１実施形態）
＜装置構成＞
図１は、本発明の第１実施形態としての情報処理装置１００の概略構成を示す図である。情報処理装置１００は、検証対象指定モジュール１１０と構文解析モジュール１２０と限定表明生成モジュール１３０と再帰関数置換モジュール１４０と検証用ファイル出力モジュール１５０と外部ツール実行モジュール１６０とファイル格納部１７０とを含む。これらのモジュールのうち、検証対象指定モジュール１１０は、利用者から検証の対象とするファイルと関数、また再帰データの繰り返し数を限定するための要素数を入力として受け取る。構文解析モジュール１２０は、検証対象として指定された検証対象ソースファイルを、ファイル格納部１７０から読み込み、ソースコードを解析して、検証対象関数に関係するデータ型の情報、関数呼出しの情報、再帰データに関する表明（Assertion）の情報を抽出する。限定表明生成モジュール１３０は、抽出されたデータ型の情報と再帰データに関する表明とに基づいて、指定された所定数に要素数を限定した限定表明（すなわち限定表明情報）を生成する。再帰関数置換モジュール１４０は、抽出された関数呼出しの情報を参照し、指定された関数が再帰関数であった場合には、再帰呼出しを無くし、限定表明を付与されたダミー関数への通常の関数呼出しに変換する。
【００１６】
検証用ファイル出力モジュール１５０は、指定されたソースファイルの内容を、再帰データに関する表明を生成された限定表明に置き換える。また、再帰呼出しがある場合には、「再帰呼出し」を、「限定表明を付与されたダミー関数への呼出し」に置き換えて、モデル検査を行なうための検証用ファイルを生成し、ファイル格納部１７０に格納する。外部ツール実行モジュール１６０は、生成した検証用ファイルを用いて、既存のモデル検査によるプログラム検証モジュール１９０を実行する。
【００１７】
＜全体の検証処理の流れ＞
次に、図１及び図２、図３のフローチャートを参照して本実施の形態の全体の動作について詳細に説明する。検証対象指定モジュール１１０は、利用者からの、検証対象ファイル名、検証対象関数名、要素数の指定を受け付ける（Ｓ２０１）。
【００１８】
構文解析モジュール１２０は、指定された検証対象ファイル名に対応するソースファイルをファイル格納部１７０から読み込み（Ｓ２０２）、ソースコードおよび表明の構文解析を行う（Ｓ２０３）。
【００１９】
＜＜ソースコードおよび表明の構文解析＞＞
ここで、図３、図５、図６、図７を用いてソースコードおよび表明の構文解析（Ｓ２０３）について詳しく説明する。構文解析モジュール１２０は、ソースコードのデータ型について解析し（Ｓ３０１）、その結果をデータ型情報（図５の５０１）として登録する。また、関数の呼出し関係について解析し（Ｓ３０２）、その結果を関数呼出し情報（図５の５０２）として登録する。
【００２０】
次に、構文解析モジュール１２０は、表明について解析を行い（Ｓ３０３）、表明が再帰データに関するものであれば、その種類に応じて再帰表明情報（図６の６０１〜６０６）の登録を行う（Ｓ３０４〜Ｓ３１３）。
【００２１】
ここでまず、ステップＳ３０５で推移閉包に関する表明か否か判断する。図７の７０１に示すように、推移閉包（ＴＣ：Transitive Closure）とは、起点となる要素から推移変数を辿って、終端に達するまでに、到達できる要素からなる集合である。ＴＣは、データ構造が推移閉包であることを表わす識別子である。ソースコードに、推移閉包に関する表明が含まれると判断すれば、推移閉包の識別子である「ＴＣ名」をＴＣのリスト情報（図６の６０１）に登録し（Ｓ３０６）、表明の内容、つまり、起点、推移メンバ及び終端をＴＣ情報（図６の６０２）として登録する。
【００２２】
次に、ステップＳ３０７で、推移閉包の要素の値設定に関する表明（図７の７０２）か否かを判断する。推移閉包の要素の値設定に関する表明であれば、表明の内容を要素の値設定情報（図６の６０３）に登録する（Ｓ３０８）。更に、ステップＳ３０９で、推移閉包の要素の値変更に関する表明（図７の７０３）であれば、表明の内容を要素の値変更情報（図６の６０４）に登録する（Ｓ３１０）。
【００２３】
また、ステップＳ３１１で推移閉包の分割に関する表明（図７の７０４）であれば、分割された推移閉包の識別子とした「ＴＣ１」「ＴＣ２」をＴＣのリスト情報（図６の６０１）に登録し、表明の内容を分割ＴＣ情報（図６の６０５）に登録する（Ｓ３１２）。このとき、「ＴＣ１」と「ＴＣ２」とはそれぞれ別の分割ＴＣ情報として登録し、ＴＣ２についての条件はＴＣ１についての条件を否定したものとして登録する。
【００２４】
それ以外で、推移閉包の結合に関する表明（図７の７０５）であれば、表明の内容をＴＣの結合情報（図６の６０６）に登録する（Ｓ３１３）。このとき、結合対象がＴＣのリスト情報（図６の６０１）に登録済みであれば結合対象のＴＣ区分を「ＴＣ」とし、そうでなければ「要素」とする。
【００２５】
＜＜要素の限定＞＞
図２に戻り、ステップＳ２０３でソースコードと表明の解析が終わると、ステップＳ２０５以下に進んで、限定要素数Ｎを、０からＳ２０１で指定された要素数までインクリメントさせつつ（Ｓ２１９）、限定表明の生成処理（Ｓ２０７〜Ｓ２１７）を複数回繰り返す。具体的には、まず、限定要素数Ｎに０を代入し（Ｓ２０５）、ステップＳ２０７において、Ｎが指定要素数より小さいか否か判定する。Ｎが指定要素数よりも小さければ、ステップＳ２０９に進み、限定表明生成モジュール１３０は、構文解析により得たデータ型情報と再帰表明情報を元に、推移閉包の要素の数を限定要素数Ｎに限定した表明を生成する（Ｓ２０９）。
【００２６】
次に、再帰関数置換モジュール１４０は、関数呼出し情報（図５の５０２）を参照して、指定された検証対象関数が再帰呼出しを行っているか否か判断する（Ｓ２１１）。指定された検証対象関数が再帰呼出しを行っていれば、ステップＳ２１３に進み、検証対象関数と同じ引数と関数型と表明を持つダミー関数を作成し、再帰呼出しをダミー関数の呼出しに変更（置換）する。
【００２７】
ついで、検証用ファイル出力モジュール１５０は、限定表明生成モジュール１３０と再帰関数置換モジュール１４０の処理結果を検証用ファイルとして生成し、ファイル格納部１７０に出力する（Ｓ２１５）。最後に、外部ツール実行モジュール１６０は検証用ファイルを入力として、従来のモデル検査によるプログラム検証モジュール１９０を実行し（Ｓ２１７）、限定表明に照らしてソースコードが正しく記述されていることを検証する。以上の限定表明の生成処理（Ｓ２０７〜Ｓ２１７）を複数回繰り返すことにより、再帰データの要素数を、０から指定要素数（所定数）までの各要素数Ｎに限定した複数の限定表明情報を生成する。
【００２８】
＜＜限定表明の生成処理＞＞
図２のステップＳ２０９で行なわれる限定表明生成モジュール１３０による要素数Ｎの限定表明の生成処理について、図４と図６を用いて詳細に説明する。まず、限定表明生成モジュール１３０は、限定要素数Ｎに応じたデータ構造を表す事前条件を生成する（Ｓ４０１）。すなわち、ＴＣ情報（図６の６０２）を参照して、起点から０〜Ｎ−１回だけ推移メンバを介して到達する要素に未使用のメモリアドレスを割り当てるような事前条件を生成する。そしてさらに、起点からＮ回だけ推移メンバを介して到達する要素には終端を割り当てるような事前条件を生成する。
【００２９】
また、限定表明生成モジュール１３０は、ＴＣ情報と要素値設定情報（図６の６０３）を参照して、起点から０〜Ｎ−１回だけ推移メンバを経て到達できる各要素について、そのメンバの値が条件に合致するような事前条件を生成する（Ｓ４０２）。次に、限定表明生成モジュール１３０は、要素値変更情報（図６の６０３）を参照して、情報が登録されているか否かを判断する（Ｓ４０３）。情報が登録されている場合には、再帰データの構造が変らないことを示す事後条件を生成する（Ｓ４０４）。つまり、要素値変更情報の結果変数から０〜Ｎ−１回だけ推移メンバを介して到達できる各要素が、関数開始時に、ＴＣ情報の起点から０〜Ｎ−１回だけ推移メンバを介して到達できる各要素と等しいことを示す事後条件を生成する。
【００３０】
また、結果変数から推移メンバを介して０回、１回、・・・Ｎ−１回の推移で到達する要素毎に、当該要素のメンバが一致条件と変更条件を満たし、一致条件と変更条件に関与しないメンバの値は変らず、他の要素のメンバの値も変らないという事後条件を生成する（Ｓ４０５〜Ｓ４０７）。
【００３１】
次に、限定表明生成モジュール１３０は、ＴＣ結合情報（図６の６０６）が登録されているか否かを判断する（Ｓ４０８）。ＴＣ結合情報が登録されている場合には、ＴＣ区分が「ＴＣ」である結合対象の要素数の和が、限定要素数Ｎになるような組合せを求める（Ｓ４０９）。例えば、ＴＣ区分が「ＴＣ」である結合対象ＴＣ１とＴＣ２があり、限定要素数が２である場合、ＴＣ１およびＴＣ２の要素数の組として、（２，０）、（１，１）、（０，２）が求められる。限定表明生成モジュール１３０は、この組合せ毎に事後条件の生成を繰り返す（Ｓ４１０〜Ｓ４１３）。
【００３２】
事後条件としては、まずデータ構造についての条件が生成される（Ｓ４１１）。関数開始時点の再帰データをＴ０とし、Ｔ０を分割した再帰データをＴ１およびＴ２とし、再帰データと同じデータ型の要素ｅとを、Ｔ１、ｅ、Ｔ２の順に結合するものとする。ＴＣ結合情報のＴＣ・要素名を元に、ＴＣリスト情報を参照すると、ＴＣ１とＴＣ２に関する分割ＴＣ情報が判り、分割ＴＣ情報の被参照ＴＣ名を元に、ＴＣリスト情報を参照すると、ＴＣ０に関するＴＣ情報が判る。
【００３３】
ＴＣ１およびＴＣ２の組合せが（２，０）の場合、結果変数から推移メンバを介して０〜１回の推移で到達する各要素は、ＴＣ０の起点から推移メンバを介して０回〜１回の推移で到達する各要素に等しくなるような事後条件が生成される。また、結果変数から２回の推移で到達する要素はｅに等しく、結果変数から３回の推移で到達する要素はＴＣ０のＴＣ情報の終端に等しくなるような事後条件が生成される。
【００３４】
ＴＣ１およびＴＣ２の組合せが（１，１）の場合、結果変数から推移メンバを介して０回の推移で到達する要素は、ＴＣ０の起点から推移メンバを介して０回の推移で到達する要素に等しく、結果変数から１回の推移で到達する要素はｅに等しくなるような事後条件が生成される。また、結果変数から２回の推移で到達する要素はＴＣ０の起点から推移メンバを介して１回の推移で到達する要素に等しく、結果変数から３回の推移で到達する要素はＴＣ０のＴＣ情報の終端に等しくなるような事後条件が生成される。
【００３５】
ＴＣ１およびＴＣ２の組合せが（０，２）の場合、結果変数から推移メンバを介して０回の推移で到達する要素はｅに等しくなるような事後条件が生成される。また、結果変数から１〜２回の推移で到達する要素はＴＣ０の起点から推移メンバを介して０〜１回の推移で到達する要素に等しく、結果変数から３回の推移で到達する要素はＴＣ０のＴＣ情報の終端に等しくなるような事後条件が生成される。
【００３６】
データ構造についての事後条件の生成後には、限定表明生成モジュール１３０は、個々の要素の値に関する事後条件を生成する（Ｓ４１２）。
【００３７】
ＴＣ１およびＴＣ２の組合せが（２，０）の場合、結果変数から推移メンバを介して０〜１回の推移で到達する各要素の各メンバが、ＴＣ０の起点から推移メンバを介して０回〜１回の推移で到達する各要素のメンバに等しくなるような事後条件が生成される。
【００３８】
ＴＣ１およびＴＣ２の組合せが（１，１）の場合、結果変数から推移メンバを介して０回の推移で到達する要素の各メンバは、ＴＣ０の起点から推移メンバを介して０回の推移で到達する要素の各メンバに等しくなるような事後条件が生成される。また、結果変数から２回の推移で到達する要素の各メンバはＴＣ０の起点から推移メンバを介して１回の推移で到達する要素の各メンバに等しくなるような事後条件が生成される。
【００３９】
ＴＣ１およびＴＣ２の組合せが（０，２）の場合、結果変数から１〜２回の推移で到達する要素の各メンバはＴＣ０の起点から推移メンバを介して０〜１回の推移で到達する要素の各メンバに等しくなるような事後条件が生成される。
【００４０】
以上のように、本実施の形態では、要素の個数が決まっていない再帰データに関する事前条件などの表明を、要素数を指定数以下に限定した表明に置き換え、また呼出し回数が決まっていない再帰呼出しを通常の関数呼出しに置き換える。これにより、検証対象のプログラムにおける変数の個数を有限個に限定することができ、検証対象のプログラムを有限状態空間に変換することができるため、モデル検査法による網羅的な検証を行うことが可能となる。すなわち、モデル検査法を用いたプログラムの精確な検証において、従来は検証が困難であった要素の個数が不明な再帰データおよび呼出し回数が不明な再帰関数についても検証を行うことができる。言い換えれば、要素数が決まっていない再帰構造を持つデータや呼出し回数が決まっていない再帰的な関数呼出しを持つプログラムの正しさを、ソースファイルに記述された事前条件と事後条件といった表明に照らして、モデル検査法によって検証できる。
【００４１】
＜具体例＞
次に、図８に示すように、再帰のあるデータ型「struct Node」と、このデータ型を扱い、自分自身への再帰呼出しを行う関数「put」を例として、実施形態として上述した検証用ファイル生成の具体例について説明する。検証対象としてのソースコードを図１６の１６０１（行番号１〜１８）に示す。図９は関数 put に関する再帰表明を示したものである。図９において、２行目の @pre は後続の式が事前条件であることを示しており、４行目の @post は後続の式が事後条件であることを示している。
【００４２】
事前条件としての２行目の式 __tc( TC0, p, "next", NULL ) は、引数 p を起点としてメンバ変数 next を介して、next の値が NULL になるまでに到達することができる変数の集合を「TC0」と名付けることを示している。
【００４３】
また、３行目の式 __tc_value( TC0, e, ( e->next == NULL ) ||( e->key < e->next->key ) ) は、集合 TC0 の各要素 e に関して、e のメンバ変数next の値が NULL で無ければ、e のメンバ変数 key の値は、e から next を介した１回の推移で到達する要素の key の値よりも小さいことを示している。
【００４４】
４行目の式 __tc_modify( __return, TC0, e, e->key == k, e->value == v ) は、集合 TC0 にメンバ key が引数 k と同じ値を持つ要素があれば、その要素のメンバ value は引数 v と同じ値に変更し、変更した結果を含む集合の起点を関数の戻り値とすることを示している。
【００４５】
集合 TC0 にメンバ key が引数 k と同じ値を持つ要素が無い場合には、４行目の式は偽と評価されて、５行目の論理和の論理学上の意味に従って、６行目以降の式が評価される。６行目の式 __fresh(e) && e->key == k&& e->value == v は、変数 e に未使用のメモリアドレスを割り当てることと、eのメンバ key および value がそれぞれ引数 k および v と同じ値を持つことを示している。
【００４６】
７行目の式 __tc_split( TC0, TC1, TC2, d, d->key < k ) は集合 TCOにおけるメンバ key が引数 k よりも小さい値を持つ要素の集合を TC1 と名付け、それ以外の要素の集合を TC2 と名付けたｋとを示している。８行目の式 __tc_join( __return, “next", TC1 && e && TC2 ) は、TC1およびTC2内での要素の結合の順番は変えずに、TC1 の各要素と変数 e と TC2 の各要素とをメンバ next により結合し、結合結果としてできた集合の起点を関数の戻り値とすることを示している。
【００４７】
検証対象指定モジュール１１０に、要素数として２、検証対象関数名としてput、検証対象ファイル名として関数putを含むファイルが与えられたとする。
【００４８】
構文解析モジュール１２０は、検証対象のソースファイルを読み込み（図２のステップＳ２０１）、ソースコード（図１６の１６０１）を解析して、データ型 struct Node についてのデータ型情報（図１０の１０１１）と関数 put についての関数呼出し情報（図１０の１０２１）を得る。また、ソースコードに付随した再帰表明（図９。図１６の行５では仔細省略）を解析し、関数 put についての再帰表明情報（図１１の１１１１から１１６１）を得る（図２のステップＳ２０２）。
【００４９】
指定要素数２に対する限定要素数Ｎ＝０、１、２の繰り返し（図２のステップＳ２０５〜Ｓ２１９）において、Ｎ＝２の場合を例に説明する。限定表明生成モジュール１３０は、ＴＣ情報（図１１の１１２１）を参照して、要素の個数が２となるデータ構造を表す事前条件（図１２の行２’）を生成する（図４のステップＳ４０１）。この事前条件は、集合ＴＣ０の起点 p およびnextを介して１回推移した要素のそれぞれに未使用のメモリアドレスを割り当て、２回推移した要素にはＴＣ０の終端であるNULLを割り当てることを示している。
【００５０】
限定表明生成モジュール１３０は、要素値設定情報（図１１の１１３１）を参照し、要素の値についての事前条件（図１２の行３’）を生成する（図４のステップＳ４０２）。この事前条件は、p のメンバ key の値が p から next を介して１回推移した要素の key の値よりも小さいことを示している。２回推移した要素は無効なアドレスの代表値であるNULLであるため、１回推移した要素の key 値と２回推移した要素の key 値との関係は事前条件に含めない。
【００５１】
事後条件については、限定表明生成モジュール１３０は、まず要素値変更情報（図１１の１１４１）を参照して情報があることを確認し（図４のステップＳ４０３）、再帰データの構造がどのように変わるのかを示す事後条件（図１３の行４a’）を生成する（図４のステップＳ４０４）。ここでは、事後条件（図１３の行４a’）は、関数の戻り値を起点とする再帰データの構造が、関数開始時点の引数 p を起点とする構造と同じであることを示している。データ構造に関する事後条件の生成後は、要素の値がどう変更されたかを示す事後条件（図１３の行４b’と４c’）を生成する（図４のステップＳ４０５〜４０７）。図１３の行４b’は戻り値が指す要素に関してメンバ value が引数 v に変り、その他の要素・メンバは変らないことを示している。図１３の行４c’は戻り値からメンバ next を介して推移した要素に関してメンバ value が引数 v に変り、その他の要素・メンバは変らないことを示している。このようにデータ構造が変らない場合の事後条件を生成すると、次に限定表明生成モジュール１３０は、ＴＣ結合情報（図１１の１１６１）を参照して情報があることを確認し（図４のステップＳ４０８）、結合の組合せを計算する（図４のステップＳ４０９）。
【００５２】
ＴＣ結合情報にはＴＣ区分がＴＣである結合対象ＴＣ１とＴＣ２があり、限定要素数Ｎ＝２の制約の下では、ＴＣ１とＴＣ２の要素の数の組合せは（２，０）、（１，１）、（０，２）の３通りである。この３通りについて、限定表明生成モジュール１３０は事後条件の生成を繰り返す（図４のステップＳ４０９〜４１２）。組合せ（２，０）について、データ構造に関する事後条件が図１４の８a’と７a’行である。８a’行は、戻り値およびnext を介した１回目の推移先はＴＣと同じ要素であり、２回目の推移先は未使用のメモリを割り当てられた新たな要素であり、３回目の推移先はＴＣ０の終端NULLであることを示している。７a’行は、関数の開始時点において引数 p と p から１回推移した要素 p->next のそれぞれのメンバ key が k よりも小さい、即ち これら２個の要素がＴＣ１に属していることを表している。
【００５３】
要素の値に関する事後条件は図１４の６a’行である。ここでは、戻り値および next を介した１回目の推移先の各メンバの値はＴＣ０において対応する要素の各メンバと同じ値であり、２回目の推移先のメンバ key および value は引数 k およびvと同じ値であることを示している。組合せ（１，１）についてのデータ構造に関する事後条件は図１４の８b’と７b’行、要素の値に関する事後条件は図１４の６b’行、組合せ（０，２）についてのデータ構造に関する事後条件は図１５の８c’と７c’行、要素の値に関する事後条件は図１５の６c’行であり、組合せ（２，０）と図１４の補足欄に示したような構造と要素の値を示している。再帰関数置換モジュール１４０は、関数呼出し情報（図１０の１０２１）において、関数 put の被参照関数が put 自身であるという再帰呼出しがあることを確認する（図２のステップＳ２０７）。そして、関数 put と戻り値と引数が同じである非再帰関数のダミー関数を生成し、関数 put から put自身への再帰呼出しをダミー関数への通常の関数呼出しに変換する。検証用ファイル出力モジュール１５０は、限定表明生成モジュール１３０と再帰関数置換モジュール１４０による結果を検証用ファイルとして出力する。
【００５４】
図１６において、置換後の検証用ファイル１６０２において、４b’〜４c’行は再帰関数置換モジュールにより生成されたダミー関数であり、１５’行が put自身への再帰呼出しをダミー関数への呼出しに変えた箇所である。また、図１６では４a’行と５’行について図を簡略化するために省略しているが、実際には図１２〜図１４に記した、要素数を限定した表明がここに存在する。
【００５５】
（他の実施形態）
本発明は、上記実施形態の機能を実現する検証プログラムが、システム或いは装置に直接或いは遠隔から供給される場合にも適用可能である。したがって、本発明の機能をコンピュータで実現するために、コンピュータにインストールされるプログラム、或いはそのプログラムを格納した媒体、そのプログラムをダウンロードさせるＷＷＷサーバも、本発明の範疇に含まれる。
【図１】
2011154568.tif 000003
【図２】
2011154568.tif 000004
【図３】
2011154568.tif 000005
【図４】
2011154568.tif 000006
【図５】
2011154568.tif 000007
【図６】
2011154568.tif 000008
【図７】
2011154568.tif 000009
【図８】
2011154568.tif 000010
【図９】
2011154568.tif 000011
【図１０】
2011154568.tif 000012
【図１１】
2011154568.tif 000013
【図１２】
2011154568.tif 000014
【図１３】
2011154568.tif 000015
【図１４】
2011154568.tif 000016
【図１５】
2011154568.tif 000017
【図１６】
2011154568.tif 000018