(57)【要約】【課題】ループ処理を有界にした上で、ループ後の処理に係る不具合を検出し得るようにする情報処理装置、情報処理方法、及び情報処理プログラムを提供する。【解決手段】検査対象プログラムの入力を受ける入力モジュール１１１と、検査対象プログラムから、該検査対象プログラムに含まれるループの繰返し演算数を閾値以下とするための有界プログラムを生成するループ有界化モジュール１１３とを備える。ループ有界化モジュール１１３は、ループ処理以降で参照される変数にループ内で値が設定されるか否かに応じて、検査対象プログラム内のループ後の処理を行う有界プログラムとするか否かを変える。【選択図】図１
2013065258.tif 000002
【特許請求の範囲】
【請求項１】
検査対象プログラムの入力を受ける入力手段と、
前記検査対象プログラムから、該検査対象プログラムに含まれるループによる繰返し演算数を閾値以下とするための有界プログラムを生成する生成手段と
を備え、
前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える、
情報処理装置。
【請求項２】
前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定される場合には、前記検査対象プログラム内の前記ループ後の処理を行わない有界プログラムを生成し、前記ループ以降で参照される変数に前記ループ内で値が設定されない場合には、前記閾値回の繰返し演算後、前記検査対象プログラム内の前記ループ処理後の処理を行う有界プログラムを生成する、
請求項１記載の情報処理装置。
【請求項３】
前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定される場合には、前記閾値回の繰返し演算後に強制終了し、前記ループ以降で参照される変数に前記ループ内で値が設定されない場合には、前記閾値回の繰返し演算後、前記検査対象プログラム内の前記ループ後の処理へ移る有界プログラムを生成する、
請求項１又は請求項２に記載の情報処理装置。
【請求項４】
前記検査対象プログラムが生成した有界プログラムを用いて、有界モデル検査を行う検査手段をさらに備える、
請求項１乃至請求項３のいずれか１項に記載の情報処理装置。
【請求項５】
記憶媒体から、検査対象プログラムを読込む入力ステップと、
前記検査対象プログラムから、該検査対象プログラムに含まれるループによる繰返し演算数を閾値以下とするための有界プログラムを生成する生成ステップと、
を備え、
前記生成ステップは、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える、
情報処理方法。
【請求項６】
コンピュータに情報処理方法を実行させる情報処理プログラムであって、当該情報処理方法は、
記憶媒体から、検査対象プログラムを読込む入力ステップと、
前記検査対象プログラムから、該検査対象プログラムに含まれるループの繰返し演算数を閾値以下とするための有界プログラムを生成する生成ステップと、
を備え、
前記生成ステップは、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える、
情報処理プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明に係るいくつかの態様は、情報処理装置、情報処理方法及び情報処理プログラムに関する。
【背景技術】
【０００２】
従来から、検査対象のプログラムが、検査したい性質（以下、プロパティ；ｐｒｏｐｅｒｔｙともいう）を満たすか否かをモデル検査法（ｍｏｄｅｌ  ｃｈｅｃｋｉｎｇ  ｍｅｔｈｏｄ）を用いて、当該検査対象プログラムを実行せずに（静的に）調べる方法がある。この検査は、ソフトウェアモデル検査（ｓｏｆｔｗａｒｅ  ｍｏｄｅｌ  ｃｈｅｃｋｉｎｇ）又はモダンモデル検査（ｍｏｄｅｒｎ  ｍｏｄｅｌ  ｃｈｅｃｋｉｎｇ）と呼ばれている。
【０００３】
このソフトウェアモデル検査で用いられる検査法の中でも、有界モデル検査法（ｂｏｕｎｄｅｄ  ｍｏｄｅｌ  ｃｈｅｃｋｉｎｇ  ｍｅｔｈｏｄ）は、探索する深さを限定することで探索範囲を有界にして有限状態遷移空間を効率的に探索する手法である。有界モデル検査法を用いたソフトウェアモデル検査については、例えば、非特許文献１に記載されている。
【先行技術文献】
【非特許文献】
【０００４】
【非特許文献１】Ｅｄｍｕｎｄ  Ｃｌａｒｋｅ他２名、“Ｂｅｈａｖｉｏｒａｌ  Ｃｏｎｓｉｓｔｅｎｃｙ  ｏｆ  Ｃ  ａｎｄ  Ｖｅｒｉｌｏｇ  Ｐｒｏｇｒａｍｓ  Ｕｓｉｎｇ  Ｂｏｕｎｄｅｄ  Ｍｏｄｅｌ  Ｃｈｅｃｋｉｎｇ”、Ｐｒｏｃｅｅｄｉｎｇｓ  Ｏｆ  ＤＡＣ２００３、ｐ．３６８−ｐ．３７１
【発明の概要】
【発明が解決しようとする課題】
【０００５】
しかしながら、非特許文献１記載のソフトウェアモデル検査では、ループ内の処理を所定回数まで実行した後、ループ後の処理を探索しない場合があるという課題があった。
【０００６】
本発明のいくつかの態様は前述の課題に鑑みてなされたものであり、ループ処理を有界にした上で、ループ後の処理に係る不具合を検出し得るようにする情報処理装置、情報処理方法、及び情報処理プログラムを提供することを目的の１つとする。
【課題を解決するための手段】
【０００７】
本発明に係る情報処理装置は、検査対象プログラムの入力を受ける入力手段と、前記検査対象プログラムから、該検査対象プログラムに含まれるループの繰返し演算数を閾値以下とするための有界プログラムを生成する生成手段とを備え、前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える。
【０００８】
本発明に係る情報処理方法は、記憶媒体から、検査対象プログラムを読込む入力ステップと、前記検査対象プログラムから、該検査対象プログラムに含まれるループの繰返し演算数を閾値以下とするための有界プログラムを生成する生成ステップと、を備え、前記生成ステップは、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える。
【０００９】
本発明に係る情報処理プログラムは、コンピュータに情報処理方法を実行させる情報処理プログラムであって、当該情報処理方法は、記憶媒体から、検査対象プログラムを読込む入力ステップと、前記検査対象プログラムから、該検査対象プログラムに含まれるループの繰返し演算数を閾値以下とするための有界プログラムを生成する生成ステップと、を備え、前記生成ステップは、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える。
【発明の効果】
【００１０】
本発明によれば、ループ処理を有界にした上で、ループ後の処理に係る不具合を検出し得るようにする情報処理装置、情報処理方法、及び情報処理プログラムを提供することができる。
【図面の簡単な説明】
【００１１】
【図１】本発明の第１実施形態における情報処理装置の概略構成を示す機能ブロック図である。
【図２】図１に示した情報処理装置が検査の対象とすることのできるプログラムの具体例を示す図である。
【図３】図１に示した情報処理装置がループ有界化処理を行うための変換ルールの例を示す図である。
【図４】図２に示した検査対象プログラムから第１のループ有界化処理により生成した有界プログラムの具体例を示す図である。
【図５】図１に示した情報処理装置がループ有界化処理を行うための変換ルールの例を示す図である。
【図６】図２に示した検査対象プログラムから第１のループ有界化処理により生成した有界プログラムの具体例を示す図である。
【図７】図１に示した情報処理装置が検査の対象とすることのできるプログラムの具体例を示す図である。
【図８】図２に示した検査対象プログラムから第２のループ有界化処理により生成した有界プログラムの具体例を示す図である。
【図９】図２に示した検査対象プログラムから第２のループ有界化処理により生成した有界プログラムの具体例を示す図である。
【図１０】図１に示した情報処理装置の処理の流れを示すフローチャートである。
【図１１】ループ位置情報の具体例を示す図である。
【図１２】データ依存関係の具体例を示す図である。
【図１３】本発明の第２実施形態における情報処理装置の概略構成を示す機能ブロック図である。
【図１４】図１３に示した情報処理装置の処理の流れを示すフローチャートである。
【発明を実施するための形態】
【００１２】
以下に本発明の実施の形態を説明する。以下の説明及び参照する図面の記載において、同一又は類似の構成には、それぞれ同一又は類似の符号が付されている。
【００１３】
（第１実施形態）
図１乃至図１２は、本発明の第１実施形態を説明するための図である。図１は、第１実施形態における情報処理装置の概略構成を説明するための機能ブロック図である。
【００１４】
図１に記載の情報処理装置１００は、検査対象プログラムに含まれるループを有界化した有界プログラムを生成することにより、当該検査対象プログラムに対して好適に有界モデル検査を行い得るようにする装置である。
【００１５】
情報処理装置１００は、例えばＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）等の演算装置で実装される情報処理部１１０と、例えばＨＤＤ（Ｈａｒｄ  Ｄｉｓｋ  Ｄｒｉｖｅ）やメモリ等の記憶媒体で実装されるファイル格納部１２０とを含む。情報処理部１１０は、入力モジュール１１１と、ループ有界化モジュール１１３と、出力モジュール１１５とを含む。尚、これらのモジュールはソフトウェアで実装されていてもハードウェアで実装されていても良い。すなわち、情報処理部１１０上の処理は、すべてコンピュータに実行させるプログラムにより実現されうる。
入力モジュール１１１は、ファイル格納部１２０から検査対象プログラムを読込むことで、検査対象プログラムの入力を受けるモジュールである。
【００１６】
ループ有界化モジュール１１３は、ファイル格納部１２０から読込んだ検査対象プログラムに対し、ループ処理を有界化する。以下、検査対象プログラムに対してループ処理を有界化することで生成されるプログラムを有界プログラムと呼ぶ。
【００１７】
ここで、ループ有界化モジュール１１３は、ループ内の変数の参照関係に応じて、２つの有界化処理が可能である。以下では、これらの２つの有界化処理を、第１のループ有界化処理及び第２のループ有界化処理と呼ぶ。第１のループ有界化処理及び第２のループ有界化処理については、後に詳述する。
出力モジュール１１５は、ループ有界化モジュール１１３が生成した有界プログラムをファイル格納部１２０へ出力するモジュールである。
【００１８】
尚、以下では有界モデル検査の対象プログラムはＣ言語で記載されているものとして説明を進めるが、本発明の適用はＣ言語で記載されたプログラムに限られるものではない。
【００１９】
また、以下では、ループ処理についてｗｈｉｌｅ文を用いているプログラムを例に説明するが、本発明の適用はｗｈｉｌｅ文を用いたループ処理には限られない。例えば、ｆｏｒ文、ｄｏ文、ｇｏｔｏ文を用いたループ処理は、実行前後の変数の値が同じであるという意味で等価なｗｈｉｌｅ文に変換することができるものであるため、このようなループ処理にも本発明は適用可能である。
【００２０】
以下では、ループ終了直後にラベルｗｈｉｌｅＭ＿ｂｒｅａｋ（Ｍは対象関数内のループに割り振った１から始まる連番）が設定されているものとするが、これに限られるものではない。
【００２１】
更に、以下では、検査対象プログラムに関して、ループ処理のコードを固定回数（任意に指定可能な閾値回数）だけ展開する変換（以下、「ループ展開」とも呼ぶ）、あるいはループ処理に繰返し回数を表すメタ変数やその値を調べるコード（命令文）を挿入する変換（以下、「ループ強制終了」とも呼ぶ）を、ソースコードに対して行う例について説明するが、本発明が適用される検査対象プログラムは、ソースコードには限られない。例えば、ソースコードを解析して得られる抽象構文木や制御フローグラフ、若しくは、ソースコードをコンパイルして得られる中間コードやバイナリコードに適用しても良い。
以下、有界モデル検査について説明する。
【００２２】
検査対象のプログラムが検査したい性質（プロパティ；ｐｒｏｐｅｒｔｙ）を満たすか否かを、モデル検査法（ｍｏｄｅｌ  ｃｈｅｃｋｉｎｇ  ｍｅｔｈｏｄ）を用いて静的に（すなわち、プログラムを実行せずに）調べる方法がある。この方法は、ソフトウェアモデル検査（ｓｏｆｔｗａｒｅ  ｍｏｄｅｌ  ｃｈｅｃｋｉｎｇ）又はモダンモデル検査（ｍｏｄｅｒｎ  ｍｏｄｅｌ  ｃｈｅｃｋｉｎｇ）と呼ばれている。モデル検査法とは、検査対象のシステムやソフトウェア（以下、システムやソフトウェアを総称してプログラムと呼ぶことがある）を有限状態遷移システム（ｆｉｎｉｔｅ  ｓｔａｔｅ  ｔｒａｎｓｉｔｉｏｎ  ｓｙｓｔｅｍ）として表し、同システム上の有限状態空間（ｆｉｎｉｔｅ  ｓｔａｔｅ  ｓｐａｃｅ）を網羅探索することにより、時相論理（ｔｅｍｐｏｒａｌ  ｌｏｇｉｃ）で表現されたプロパティが成立するか否かを調べる手法である。
【００２３】
モデル検査法では、プロパティが成立しない場合には、プロパティへの反例（ｃｏｕｎｔｅｒ−ｅｘａｍｐｌｅ）として、初期状態からプロパティが成立しない状態への状態遷移列（パス情報）が出力される。
【００２４】
特に、有界モデル検査法（ｂｏｕｎｄｅｄ  ｍｏｄｅｌ  ｃｈｅｃｋｉｎｇ  ｍｅｔｈｏｄ）は、探索する深さを限定して（すなわち、探索範囲を有界にして）有限状態遷移空間を効率的に探索する手法であり、不具合の検出に有効であると考えられている。有界モデル検査法を用いたソフトウェアモデル検査では、検査対象プログラムに出現する全ての変数に関して、各変数の値の組合せの１つ１つが状態として取り扱われる。
【００２５】
以下、有界モデル検査法をプログラムの静的検査へ適用した例を説明する。有界モデル検査法により、Ｃ∧¬Ｐ（“∧”は論理積、“¬”は否定）を満たす変数値の遷移（パス情報）を検出することを試みる。ここで、検査対象プログラムに表れる各変数の値の遷移は制約式Ｃ（有限状態遷移システム）として、検査対象プログラムが正しい状態にあることは論理式Ｐ（プロパティ）として表現されている。
【００２６】
検出されたパス情報は、検査対象プログラムが正しく動作すること（Ｃ⇒Ｐ（“⇒”は論理の含意））への反例である（Ｃ∧¬Ｐ＝¬（Ｃ⇒Ｐ））。反例として示されたパス情報に沿って検査対象プログラムを実行すると、検査対象プログラムが正しい状態にないという不具合が発生する。
【００２７】
一般に、プログラムの状態及び遷移は無数にあり得るため、プログラムを有界な（探索の深さを限定した）有限状態遷移システムに変換する際には、過小近似（ｕｎｄｅｒ−ａｐｐｒｏｘｉｍａｔｉｏｎ）が必要となる。プログラム上の表現のうち、特にループは定められた探索の深さを超えやすい。よって、ループを有界化する処理が必要となる。
以下、第１のループ有界化処理について、図２に示すソースファイル２００ａを検査対象プログラムとしてループ展開を行う場合を例に説明する。
【００２８】
第１のループ有界化処理では、図３のルールａとｂとを用いて、ループを、ユーザが指定した固定回数（以下、ＮＭＡＸ回とする）だけ展開する。より具体的には、０≦ｎ＜ＮＭＡＸであるｎ回目のループ内の処理についてはルールａを、ｎ＝ＮＭＡＸであるｎ回目のループ内の処理についてはルールｂを用いて展開する。
【００２９】
ルールｂのａｓｓｅｒｔ文において、ａｓｓｅｒｔ（！ｅ）の式“！ｅ”が偽（すなわちｅが真）の場合、有限モデル検査ツールは、式！ｅに対する反例を出力してその状態以降の探索は行わない。ここで、“！”はＣやＪａｖａ（登録商標）等のプログラミング言語における否定の単項演算子である。
【００３０】
ルールｂの式ｅは、元のループの制御式なので、！ｅへの反例は、ｅが真であること、すなわちループをＮＭＡＸ回展開した後で、制御式が真になり得ることを示す。換言すると、この反例は、元のループがＮＭＡＸを超える回数の繰返しを含んでいること、すなわちＮＭＡＸを越える繰返し部分で起きる不具合を有限モデル検査ツールが見過ごし得ることを示している。以下、ルールｂのａｓｓｅｒｔ文をループ展開表明と呼ぶ。
【００３１】
図４のソースファイル４００ａは、図２で示したソースファイル２００ａを検査対象プログラムとし、ＮＭＡＸを２としてループを展開した有界プログラムの例である。
【００３２】
尚、ここまではループ展開によりループを有界化する場合を説明したが、ループボディの固定回数の実行後にループの処理を強制終了するように有界プログラムを生成する変換処理（ループ強制終了）も可能である。図５のルールｃは、このループ強制終了の際に用いる変換ルールを示す。
【００３３】
ルールｃでは、検査対象プログラムには存在しないメタ変数＿ｎＭを導入する。＿ｎＭはループの実行回数を示すメタ変数であり、初期値は０を取り、ループボディの先頭で１ずつ値が加算されるようになっている。ルールｃでは、この＿ｎＭがＮＭＡＸを超えると、図３のルールｂと同様のループ展開表明としてａｓｓｅｒｔ（！ｅ）が呼び出されるようになっている。
【００３４】
図６のソースファイル４００ｂは、図２に示したソースファイル２００ａを検査対象プログラムとして、ＮＭＡＸを２としてループを強制終了するように変換（生成）された有界プログラムの例である。
【００３５】
このように、第１のループ有界化処理では、ルールａ及びｂ、又はルールｃを用いて、検査対象プログラムに含まれるループを有界化することができる。しかしながら、第１のループ有界化処理によりループを有界にする方式（ループ有界化法）には、ループ内の処理を固定回数（ＮＭＡＸ）まで実行した後の処理が、有界モデル検査ツールにより検査されないという課題がある。この点、以下に説明する。
【００３６】
ソースファイル２００ａは、変数ｘに１を設定し（第１２行）、変数ｉとａに関係するループ処理を１０２４回繰返し（第１３行〜第１７行）、当該ループ処理終了後にｘが０であることを検査するようにａｓｓｅｒｔ文で指示している（第１９行）。
【００３７】
実際にソースファイル２００ａを実行すると、第１９行ではｘの値は１となるのでａｓｓｅｒｔ文の式ｘ＝＝０は偽となり、結果、ａｓｓｅｒｔ違反の警告が出力されて停止する。
【００３８】
一方、第１のループ有界化処理により有界化された有界プログラムである図４のソースファイル４００ａや図６のソースファイル４００ｂを有界モデル検査によって検査すると、ループボディ（元のソースファイル２００ａが含むループ内の処理）を固定回数（ここでは２回）繰り返してからループ展開表明が偽となるため（ソースファイル４００ａの第１４＿３行、及びソースファイル４００ｂの第１４ｃ行）、ここでａｓｓｅｒｔ違反の警告が出力されて停止する。これにより、ループ後の処理（第１９行）は探索されないので、ｘ＝＝０のａｓｓｅｒｔ違反は見過ごされることとなる。
【００３９】
つまり、有界モデル検査法を用いた検索対象プログラムの検査において、第１のループ有界化処理によってプログラムを有界な有限状態空間に収めるためにループを固定回数のループボディの処理の繰返しに変換すると、固定回数が本来の繰返し回数（図２のソースファイル２００ａの例では１０２４回）未満である場合には、それ以降の処理に対する検査が行われないこととなってしまう。ルールａ及びｂを用いた、ループボディを固定回数だけ展開して繰返しを限定するループ展開の方式であっても、ルールｃを用いた、ループボディに繰返し回数を表すメタ変数を挿入し、メタ変数の値と固定回数とを比較して繰返しを限定するようなループ強制終了の方式であっても、この課題は発生する。
【００４０】
そこで、ループ有界化モジュール１１３は、状況に応じてループ後の処理も探索できるように有界化を行う機能（第２のループ有界化処理）を有する。以下、図２に示すソースファイル２００ａを検査対象プログラムとして、第２のループ有界化処理を行う場合を例に説明する。
【００４１】
第２のループ有界化処理によるループ展開では、図３のルールａとルールｂ’とを用いて、ループを、ユーザが指定した固定回数であるＮＭＡＸ回だけ展開する。より具体的には、０≦ｎ＜ＮＭＡＸであるようなｎ回目までのループ内の処理についてはルールａを、ｎ＝ＮＭＡＸであるｎ回目のループ内の処理についてはルールｂ’を用いてループを展開する。
【００４２】
図８のソースファイル４００ｃは、ソースファイル２００ａを検査対象プログラムとし、ＮＭＡＸを２として第２のループ有界化処理を行った結果である有界プログラムの例を示す。
【００４３】
第１のループ有界化処理では、ＮＭＡＸ回目のループ内の処理がルールｂによって、図４の１４＿３行目のようにａｓｓｅｒｔを用いた表明（ループ展開表明、第１４＿３行）に変換されていた。これにより、変換結果であるソースファイル４００ａは、ａｓｓｅｒｔに指定された式が偽となる場合にはループの後に続く処理には制御が移らない、すなわち、ループの後に続く処理（第１９行）が有界モデル検査法で探索されないものとなっていた。
【００４４】
一方、第２のループ有界化処理では、ＮＭＡＸ回目のループ内の処理は、ルールｂ’によって、ループ後に続くラベルｗｈｉｌｅ１＿ｂｒｅａｋに制御を移すｇｏｔｏ文（第１４＿３行）に変換される（図８のソースファイル４００ｃ）。
これにより、第２のループ有界化処理を用いた有界プログラムは、ループ後の処理も有界モデル検査法で探索可能となる。
【００４５】
尚、ここまではループ展開によりループを有界化する場合を説明してきたが、第２のループ有界化処理でも第１のループ有界化処理と同様に、ループを強制終了するように変換することも可能である。図５のルールｃ’にその変換ルールを示す。
【００４６】
ルールｃ’でも、ルールｃと同様に、検査対象プログラムには存在しないメタ変数＿ｎＭが導入される。＿ｎＭはループの実行回数を示すメタ変数であり、初期値は０を取り、ループボディの先頭で１ずつ値が加算される。ルールｃ’では、この＿ｎＭがＮＭＡＸを超えると、図３のルールｂ’と同様に、ループ後に続くラベルｗｈｉｌｅＭ＿ｂｒｅａｋに制御を移すｇｏｔｏ文を呼び出す。
【００４７】
図９のソースファイル４００ｄは、第２のループ有界化処理において、ソースファイル２００ａを検査対象プログラムとし、ＮＭＡＸを２としてループ強制終了により変換した結果である有界プログラムの例である。
【００４８】
第１のループ有界化処理では、ルールｃを用いていたので、ＮＭＡＸ回目のループの処理が図６の第１４ｃ行のようにａｓｓｅｒｔを用いた表明（ループ展開表明）に変換されていた。これにより、変換結果であるソースファイル４００ｂは、ａｓｓｅｒｔに指定された式が偽となる場合には、ループの後に続く処理に制御が移らない、すなわち、ループの後に続く処理（第１９行）が有界モデル検査法で探索されないものとなっていた。
【００４９】
一方、第２のループ有界化処理では、ルールｃ’によって、ＮＭＡＸ回目のループの処理がループ後に続くラベルｗｈｉｌｅ１＿ｂｒｅａｋ（１８行）に制御を移すｇｏｔｏ文（１４ｃ行）に変換される（図９のソースファイル４００ｄ）。
【００５０】
以上のように、ループ展開の場合であっても、ループ強制終了の場合であっても、第２のループ有界化処理により有界プログラムを生成すれば、有界モデル検査ツールがループより後の処理も探索できるようになる。
【００５１】
しかしながら、すべての場合に第２のループ有界化処理を適用して、一律でループ後の処理も探索することとしてしまうと、誤警告が生じるという新たな課題が発生する。以下、その課題を説明する。
【００５２】
例えば、図７のソースファイル２００ｂに記載の検査対象プログラムを実際に動かすと、ループ（第１４行〜第１７行）を１０２４回繰返し、変数ｉの値が１０２４となってループを終了する。よってループ後の処理（第１９行）での表明ｉ＝＝１０２４は真となり、表明違反を起こさない。
【００５３】
一方、ループ（第１４行〜第１７行）を２回のみ繰り返した後、ループ後の処理（第１９行）を強制的に探索するようにループ有界化を行うと、有界プログラムは、図４のソースファイル４００ａで第１９行が“ａｓｓｅｒｔ（ｉ＝＝１０２４）”に置換されたものとなる。これを実行すると、第１９行において変数ｉの値は２となるので、表明ｉ＝＝１０２４は偽となる。よって、表明違反の警告が出力されることとなる。上述の通り、本来の検査対象プログラムでは表明違反は起きないので、この警告は誤り（誤警告）である。
【００５４】
誤警告が発生した原因は、繰返し回数を限定したループ内で値が参照される変数（図７の例ではｉ）をループ後の処理で参照することにより、当該変数が本来のループ終了時とは異なる値を得てしまったことである。
【００５５】
このような誤警告を防ぐために、ループ有界化モジュール１１３は、ループ後の処理で値が参照される変数に対し、その変数の値がループ内で設定されたか否かを調べた上で、第１のループ有界化処理を行うか、若しくはループ後の処理も探索する第２のループ有界化処理を行うかを判別する。これにより、誤警告を防ぎつつ、ループ後の処理も探索することができるようになる。
以下、図１０のフローチャートを参照しながら、情報処理装置１００の処理の流れを説明する。
【００５６】
まず情報処理部１１０は、ユーザから、有界モデル検査の対象である検査対象プログラムと、検査対象関数との指定を受付け、これに伴い、入力モジュール１１１、ループ有界化モジュール１１３、及び出力モジュール１１５を用いて一連の処理を実行する。以下、特に記載しない場合には、検査対象プログラムとして図２に示すソースファイル２００ａが指定されたものとして説明を行う。
【００５７】
入力モジュール１１１は、ファイル格納部１２０から検査対象プログラムを読込む（Ｓ５０１）。ループ有界化モジュール１１３は、まず、読込まれた検査対象プログラムの関数毎に、ループの開始位置と終了位置とを含むループ位置情報を抽出する（Ｓ５０３）。
【００５８】
図１１は、ループ有界化モジュール１１３が抽出したループ位置情報の例である。図１１の例では、ループを含む関数の名前と、ソースファイル等の検査対象プログラムを格納するもの（格納体）の名前、格納体上でのループの開始位置と終了位置（格納体がソースファイルの場合、開始位置及び終了位置は、行番号となる）がそれぞれ対応づけて管理されている。例えば、図１１の１行目（見出し行は除く）は、関数ｆｏｏに含まれるループが、ソースファイルＦｏｏ．ｃにおいて、第１４行から始まり第１７行で終わることを示す。
【００５９】
続いてループ有界化モジュール１１３は、検査対象プログラムの関数毎に、変数に値が設定される位置と、その値を参照する位置との組であるデータ依存関係を抽出する（Ｓ５０５）。
【００６０】
図１２は、ループ有界化モジュール１１３が抽出したループ位置情報の例である。図１２の例では、変数が現れる関数の名前と、変数の名前と、ソースファイル等の検索対象プログラムを格納するもの（格納体）の名前と、格納体上で変数に値を設定する位置（定義位置）と、その変数の値を参照する位置（参照位置）とが対応付けて管理されている。
【００６１】
例えば、図１２の１行目（見出し行は除く）は、関数ｆｏｏに現れる変数ｘにソースファイルＦｏｏ．ｃの第１２行で値が設定され（図２のソースファイル２００ａにおける第１２行の“ｘ＝１”）、第１９行でその値が参照される（ソースファイル２００ａの第１９行の“ｘ＝＝０”）ことを示す。
【００６２】
次に、ループ有界化モジュール１１３は、検査対象関数に含まれるループをループ位置情報から抽出し（Ｓ５０７）、ループ毎に、ループボディの処理（ループ内の処理）の繰返しを固定回数までとする有界化を行う（Ｓ５１１〜Ｓ５２１）。
最後に、ループ有界化モジュール１１３は、ループが有界化されたプログラム（有界プログラム）を出力する（Ｓ５２３）。
【００６３】
以下、ループ毎の有界化の処理（Ｓ５１１〜Ｓ５２１）を詳しく説明する。ループ有界化モジュール１１３は、検査対象関数に現れる変数のうち、「処理中のループの終了位置＜変数の参照位置」である変数を、データ依存関係から抽出する（Ｓ５１１）。ループ有界化モジュール１１３は、抽出した変数毎に（Ｓ５１３）、変数の定義位置とループの開始位置／終了位置とを比較し（Ｓ５１５及びＳ５１７）、変数の定義位置がループ内にあれば（Ｓ５１７がＮｏ（比較結果が偽））、ループの後の処理に制御を移さないように第１のループ有界化処理を用いてループを有界化する（Ｓ５１９）。より具体的には、ループ展開によりループを有界化するのであれば図３のルールａ、ｂを、ループの強制終了によりループを有界化するのであれば図５のルールｃを用いてループを有界化する。
【００６４】
変数の定義位置がループ内になければ（Ｓ５１５またはＳ５１７がＹｅｓ（比較結果が真））、第１のループ有界化処理とは異なり、ループの後の処理に制御を移すように第２のループ有界化処理を用いてループを有界化する（Ｓ５２１）。より具体的には、ループ展開によりループを有界化するのであれば図３のルールａ、ｂ’を、ループの強制終了によりループを有界化するのであれば図５のルールｃ’を用いてループを有界化する。
【００６５】
以下、具体例を用いて、ループをループボディの繰返しに展開する処理を説明する。検査対象プログラムであるソースファイル２００ａのループ（第１４行〜第１７行）は、まず図３のルールａを用いて有界プログラム（図８のソースファイル４００ｃ）の１回目のループボディ（第１４＿１行、第１５＿１行、第１６＿１行、及び第１７＿１行）、２回目のループボディ（第１４＿２行、第１５＿２行、第１６＿２行、及び第１７＿２行）に展開される。次に、図３のルールｂ’を用いて、ループの後に続くラベルｗｈｉｌｅ１＿ｂｒｅａｋに制御を移すｇｏｔｏ文（第１４＿３行）に変換される。これにより、ループの後に続く処理が有界モデル検査で探索可能となる。
【００６６】
ここで、もしルールｂを用いた場合（すなわち、第１のループ有界化処理を用いた場合）には、図４のソースファイル４００ｂの第１４＿３行のように、ａｓｓｅｒｔを用いた表明に変換されるので、ａｓｓｅｒｔに指定された式が偽となる場合、ループの後に続く処理には制御が移らない。つまり、すなわちループの後に続く処理が有界モデル検査で探索されないこととなってしまう。
【００６７】
しかしながら、図２のソースファイル２００ａを検査対象プログラムとする場合には、図１１で示したループの終了位置（第１７行）よりも後の位置で値が参照される変数は、図１２を参照すると、ｘ（第１９行で参照）のみであることがわかる。
【００６８】
変数ｘは、ループ開始前に値が設定され（第１２行）、ループ終了（第１７行）後に値が参照されている（第１９行）。よって、変数ｘの定義位置とループの開始位置の比較で比較結果が真（Ｓ５１５のＹｅｓ）となるので、ループ有界化モジュール１１３の処理はＳ５１３に戻る。この例において調べるべき変数はｘのみであったので、ループ有界化モジュール１１３は、Ｓ５１３からＳ５２１に処理を進める。Ｓ５２１において、ループ有界化モジュール１１３は、検査対象プログラムであるソースファイル２００ａを、第２のループ有界化処理により、有界プログラムであるソースファイル４００ｃへと変換する。
このように変換された有界プログラムを出力することにより（Ｓ５２３）、有界モデル検査ツールがループよりも後の処理を探索できるようになる。
【００６９】
（第２実施形態）
以下、図１３及び図１４を参照しながら本発明の第２実施形態を説明する。図１３及び図１４は、本発明の第２実施形態を説明するための図である。尚、第１実施形態と同様の構成及び動作を行う構成には第１実施形態と同じ符号を付すと共に、説明を省略する。また、構成以外にも、有限モデル検査の説明や、情報処理装置１００が入力とすることのできる検査対象プログラム等の、第１実施形態と同様の前提等については、説明を省略している。
図１３は、第２実施形態に係る情報処理装置１００の概略構成を示す機能ブロック図である。
【００７０】
本実施形態に係る情報処理装置１００は、例えばＣＰＵ（Ｃｅｎｔｒａｌ  Ｐｒｏｃｅｓｓｉｎｇ  Ｕｎｉｔ）等の演算装置である情報処理部１１０と、例えば記憶媒体等であるファイル格納部１２０とを有する。この点、第１の実施形態と同様である。
【００７１】
ここで、情報処理部１１０が、入力モジュール１１１、ループ有界化モジュール１１３、及び出力モジュール１１５に加えて、有界モデル検査モジュール１１７を更に有する点が第１実施形態と異なる。尚、これらのモジュールはソフトウェアで実装されていてもハードウェアで実装されていても良い。すなわち、情報処理部１１０上の処理は、すべてコンピュータに実行させるプログラムにより実現されうる。
【００７２】
情報処理部１１０は、入力モジュール１１１と、ループ有界化モジュール１１３と、出力モジュール１１５と、有界モデル検査モジュール１１７とに、図１４に示すＳ６０１乃至Ｓ６０５の処理を実行させる。
以下、図１４のフローチャートを参照しながら、本実施形態に係る情報処理装置１００の処理の流れを詳細に説明する。
【００７３】
情報処理部１１０は、利用者（ユーザ）から検査対象プログラムと検査対象関数との指定を受付け、入力モジュール１１１と、ループ有界化モジュール１１３と、出力モジュール１１５と、有界モデル検査モジュール１１７とに図１４に示す一連の処理を実行させる。
【００７４】
入力モジュール１１１は、検査対象プログラムをファイル格納部１２０から読込む（Ｓ６０１）。そしてループ有界化モジュール１１３は、ループボディの処理の繰返しが固定回数に制限された有界プログラムに変換し、生成した有界プログラムを出力する（Ｓ６０３）。ここで、有界プログラムへの変換処理（Ｓ６０３）の詳細は、第１実施形態の図１０の処理と同様である。
【００７５】
有界モデル検査モジュール１１７は、有界プログラムを入力として、プログラムを有界名有限状態遷移システムに変換し、同システム上の有限状態空間を決められた範囲内で網羅探索して、プログラムの正しさを示す性質（プロパティ）を表現した論理式が成立するか否かを調べる（Ｓ６０５）。出力モジュール１１５は、当該有界モデル検査モジュール１１７による検査結果をファイル格納部１２０へと出力する（Ｓ６０７）。
【００７６】
有界モデル検査モジュール１１７は、決められた時間内に網羅探索が終わった場合、検査結果として不具合の有無を示す。もし不具合があった場合には、有界モデル検査モジュール１１７は、初期状態からプロパティが成立しない状態までの変数値の遷移列（パス情報）も併せて示す。他方、決められた網羅探索が終わらなかった場合には、有界モデル検査モジュール１１７は不具合の有無を示すことができない。
【００７７】
（第１及び第２実施形態の効果）
有界モデル検査法を用いたプログラムの検査では、プログラムを有界名有限状態空間に収めるために、ループを固定回数の繰返しに変換する。第１のループ有界化処理のみを用いる場合には、固定回数を超えるループボディの繰返しに続く処理にプログラム実行の制御が移らないように有界プログラムを生成するため、ループに続く処理が有界モデル検査の探索対象外となってしまう。換言すると、ループに続く処理で生じる不具合を有界モデル検査で見逃す場合があった。
【００７８】
第１及び第２実施形態に示す手法によれば、ループの後に続く処理で値が参照される変数について、その値がループ内で設定されていない場合であれば、固定回数を超えるループボディの繰返しに続く処理にもプログラム実行の制御が移るように変換されるので、ループに続く処理も有界モデル検査による探索対象となる。よって、このような場合に、ループに続く処理で生じる不具合を有界モデル検査で示すことができるようになる。
【００７９】
（付記事項）
なお、前述の各実施形態の構成は、組み合わせたり或いは一部の構成部分を入れ替えたりしてもよい。また、本発明の構成は前述の実施形態のみに限定されるものではなく、本発明の要旨を逸脱しない範囲内において種々変更を加えてもよい。
尚、前述の各実施形態の一部又は全部は、以下の付記のようにも記載されうるが、以下には限られない。
【００８０】
（付記１）
検査対象プログラムの入力を受ける入力手段と、前記検査対象プログラムから、該検査対象プログラムに含まれるループによる繰返し演算数を閾値以下とするための有界プログラムを生成する生成手段とを備え、前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える、情報処理装置。
【００８１】
（付記２）
前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定される場合には、前記検査対象プログラム内の前記ループ後の処理を行わない有界プログラムを生成し、前記ループ以降で参照される変数に前記ループ内で値が設定されない場合には、前記閾値回の繰返し演算後、前記検査対象プログラム内の前記ループ処理後の処理を行う有界プログラムを生成する、付記１記載の情報処理装置。
【００８２】
（付記３）
前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定される場合には、前記閾値回の繰返し演算後に強制終了し、前記ループ以降で参照される変数に前記ループ内で値が設定されない場合には、前記閾値回の繰返し演算後、前記検査対象プログラム内の前記ループ後の処理へ移る有界プログラムを生成する、付記１又は付記２に記載の情報処理装置。
【００８３】
（付記４）
前記検査対象プログラムが生成した有界プログラムを用いて、有界モデル検査を行う検査手段をさらに備える、付記１乃至付記３のいずれか１項に記載の情報処理装置。
【００８４】
（付記５）
記憶媒体から、検査対象プログラムを読込む入力ステップと、前記検査対象プログラムから、該検査対象プログラムに含まれるループによる繰返し演算数を閾値以下とするための有界プログラムを生成する生成ステップと、を備え、前記生成ステップは、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える、情報処理方法。
【００８５】
（付記６）
コンピュータに情報処理方法を実行させる情報処理プログラムであって、当該情報処理方法は、記憶媒体から、検査対象プログラムを読込む入力ステップと、前記検査対象プログラムから、該検査対象プログラムに含まれるループの繰返し演算数を閾値以下とするための有界プログラムを生成する生成ステップと、を備え、前記生成ステップは、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える、情報処理プログラム。
【符号の説明】
【００８６】
１００・・・情報処理装置、１１０・・・情報処理部、１１１・・・入力モジュール、１１３・・・ループ有界化モジュール、１１５・・・出力モジュール、１２０・・・ファイル格納部
【図１】
2013065258.tif 000003
【図２】
2013065258.tif 000004
【図３】
2013065258.tif 000005
【図４】
2013065258.tif 000006
【図５】
2013065258.tif 000007
【図６】
2013065258.tif 000008
【図７】
2013065258.tif 000009
【図８】
2013065258.tif 000010
【図９】
2013065258.tif 000011
【図１０】
2013065258.tif 000012
【図１１】
2013065258.tif 000013
【図１２】
2013065258.tif 000014
【図１３】
2013065258.tif 000015
【図１４】
2013065258.tif 000016