検査対象プログラムの入力を受ける入力手段と、前記検査対象プログラムから、該検査対象プログラムに含まれるループによる繰返し演算数を閾値以下とするための有界プログラムを生成する生成手段とを備え、前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える、情報処理装置。前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定される場合には、前記検査対象プログラム内の前記ループ後の処理を行わない有界プログラムを生成し、前記ループ以降で参照される変数に前記ループ内で値が設定されない場合には、前記閾値回の繰返し演算後、前記検査対象プログラム内の前記ループ処理後の処理を行う有界プログラムを生成する、請求項1記載の情報処理装置。前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定される場合には、前記閾値回の繰返し演算後に強制終了し、前記ループ以降で参照される変数に前記ループ内で値が設定されない場合には、前記閾値回の繰返し演算後、前記検査対象プログラム内の前記ループ後の処理へ移る有界プログラムを生成する、請求項1又は請求項2に記載の情報処理装置。前記検査対象プログラムが生成した有界プログラムを用いて、有界モデル検査を行う検査手段をさらに備える、請求項1乃至請求項3のいずれか1項に記載の情報処理装置。記憶媒体から、検査対象プログラムを読込む入力ステップと、前記検査対象プログラムから、該検査対象プログラムに含まれるループによる繰返し演算数を閾値以下とするための有界プログラムを生成する生成ステップと、を備え、前記生成ステップは、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える、情報処理方法。コンピュータに情報処理方法を実行させる情報処理プログラムであって、当該情報処理方法は、記憶媒体から、検査対象プログラムを読込む入力ステップと、前記検査対象プログラムから、該検査対象プログラムに含まれるループの繰返し演算数を閾値以下とするための有界プログラムを生成する生成ステップと、を備え、前記生成ステップは、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える、情報処理プログラム。しかしながら、非特許文献1記載のソフトウェアモデル検査では、ループ内の処理を所定回数まで実行した後、ループ後の処理を探索しない場合があるという課題があった。本発明のいくつかの態様は前述の課題に鑑みてなされたものであり、ループ処理を有界にした上で、ループ後の処理に係る不具合を検出し得るようにする情報処理装置、情報処理方法、及び情報処理プログラムを提供することを目的の1つとする。本発明に係る情報処理装置は、検査対象プログラムの入力を受ける入力手段と、前記検査対象プログラムから、該検査対象プログラムに含まれるループの繰返し演算数を閾値以下とするための有界プログラムを生成する生成手段とを備え、前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える。本発明に係る情報処理方法は、記憶媒体から、検査対象プログラムを読込む入力ステップと、前記検査対象プログラムから、該検査対象プログラムに含まれるループの繰返し演算数を閾値以下とするための有界プログラムを生成する生成ステップと、を備え、前記生成ステップは、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える。本発明に係る情報処理プログラムは、コンピュータに情報処理方法を実行させる情報処理プログラムであって、当該情報処理方法は、記憶媒体から、検査対象プログラムを読込む入力ステップと、前記検査対象プログラムから、該検査対象プログラムに含まれるループの繰返し演算数を閾値以下とするための有界プログラムを生成する生成ステップと、を備え、前記生成ステップは、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える。本発明によれば、ループ処理を有界にした上で、ループ後の処理に係る不具合を検出し得るようにする情報処理装置、情報処理方法、及び情報処理プログラムを提供することができる。以下に本発明の実施の形態を説明する。以下の説明及び参照する図面の記載において、同一又は類似の構成には、それぞれ同一又は類似の符号が付されている。第1実施形態図1乃至図12は、本発明の第1実施形態を説明するための図である。図1は、第1実施形態における情報処理装置の概略構成を説明するための機能ブロック図である。図1に記載の情報処理装置100は、検査対象プログラムに含まれるループを有界化した有界プログラムを生成することにより、当該検査対象プログラムに対して好適に有界モデル検査を行い得るようにする装置である。情報処理装置100は、例えばCPUCentralProcessingUnit等の演算装置で実装される情報処理部110と、例えばHDDHardDiskDriveやメモリ等の記憶媒体で実装されるファイル格納部120とを含む。情報処理部110は、入力モジュール111と、ループ有界化モジュール113と、出力モジュール115とを含む。尚、これらのモジュールはソフトウェアで実装されていてもハードウェアで実装されていても良い。すなわち、情報処理部110上の処理は、すべてコンピュータに実行させるプログラムにより実現されうる。入力モジュール111は、ファイル格納部120から検査対象プログラムを読込むことで、検査対象プログラムの入力を受けるモジュールである。ループ有界化モジュール113は、ファイル格納部120から読込んだ検査対象プログラムに対し、ループ処理を有界化する。以下、検査対象プログラムに対してループ処理を有界化することで生成されるプログラムを有界プログラムと呼ぶ。ここで、ループ有界化モジュール113は、ループ内の変数の参照関係に応じて、2つの有界化処理が可能である。以下では、これらの2つの有界化処理を、第1のループ有界化処理及び第2のループ有界化処理と呼ぶ。第1のループ有界化処理及び第2のループ有界化処理については、後に詳述する。出力モジュール115は、ループ有界化モジュール113が生成した有界プログラムをファイル格納部120へ出力するモジュールである。尚、以下では有界モデル検査の対象プログラムはC言語で記載されているものとして説明を進めるが、本発明の適用はC言語で記載されたプログラムに限られるものではない。また、以下では、ループ処理についてwhile文を用いているプログラムを例に説明するが、本発明の適用はwhile文を用いたループ処理には限られない。例えば、for文、do文、goto文を用いたループ処理は、実行前後の変数の値が同じであるという意味で等価なwhile文に変換することができるものであるため、このようなループ処理にも本発明は適用可能である。以下では、ループ終了直後にラベルwhileM_breakMは対象関数内のループに割り振った1から始まる連番が設定されているものとするが、これに限られるものではない。更に、以下では、検査対象プログラムに関して、ループ処理のコードを固定回数任意に指定可能な閾値回数だけ展開する変換以下、ループ展開とも呼ぶ、あるいはループ処理に繰返し回数を表すメタ変数やその値を調べるコード命令文を挿入する変換以下、ループ強制終了とも呼ぶを、ソースコードに対して行う例について説明するが、本発明が適用される検査対象プログラムは、ソースコードには限られない。例えば、ソースコードを解析して得られる抽象構文木や制御フローグラフ、若しくは、ソースコードをコンパイルして得られる中間コードやバイナリコードに適用しても良い。以下、有界モデル検査について説明する。検査対象のプログラムが検査したい性質プロパティ;propertyを満たすか否かを、モデル検査法modelcheckingmethodを用いて静的にすなわち、プログラムを実行せずに調べる方法がある。この方法は、ソフトウェアモデル検査softwaremodelchecking又はモダンモデル検査modernmodelcheckingと呼ばれている。モデル検査法とは、検査対象のシステムやソフトウェア以下、システムやソフトウェアを総称してプログラムと呼ぶことがあるを有限状態遷移システムfinitestatetransitionsystemとして表し、同システム上の有限状態空間finitestatespaceを網羅探索することにより、時相論理temporallogicで表現されたプロパティが成立するか否かを調べる手法である。モデル検査法では、プロパティが成立しない場合には、プロパティへの反例counter-exampleとして、初期状態からプロパティが成立しない状態への状態遷移列パス情報が出力される。特に、有界モデル検査法boundedmodelcheckingmethodは、探索する深さを限定してすなわち、探索範囲を有界にして有限状態遷移空間を効率的に探索する手法であり、不具合の検出に有効であると考えられている。有界モデル検査法を用いたソフトウェアモデル検査では、検査対象プログラムに出現する全ての変数に関して、各変数の値の組合せの1つ1つが状態として取り扱われる。以下、有界モデル検査法をプログラムの静的検査へ適用した例を説明する。有界モデル検査法により、C∧¬P∧は論理積、¬は否定を満たす変数値の遷移パス情報を検出することを試みる。ここで、検査対象プログラムに表れる各変数の値の遷移は制約式C有限状態遷移システムとして、検査対象プログラムが正しい状態にあることは論理式Pプロパティとして表現されている。検出されたパス情報は、検査対象プログラムが正しく動作することC⇒P⇒は論理の含意への反例であるC∧¬P=¬C⇒P。反例として示されたパス情報に沿って検査対象プログラムを実行すると、検査対象プログラムが正しい状態にないという不具合が発生する。一般に、プログラムの状態及び遷移は無数にあり得るため、プログラムを有界な探索の深さを限定した有限状態遷移システムに変換する際には、過小近似under-approximationが必要となる。プログラム上の表現のうち、特にループは定められた探索の深さを超えやすい。よって、ループを有界化する処理が必要となる。以下、第1のループ有界化処理について、図2に示すソースファイル200aを検査対象プログラムとしてループ展開を行う場合を例に説明する。第1のループ有界化処理では、図3のルールaとbとを用いて、ループを、ユーザが指定した固定回数以下、NMAX回とするだけ展開する。より具体的には、0≦n<NMAXであるn回目のループ内の処理についてはルールaを、n=NMAXであるn回目のループ内の処理についてはルールbを用いて展開する。ルールbのassert文において、asserteの式eが偽すなわちeが真の場合、有限モデル検査ツールは、式eに対する反例を出力してその状態以降の探索は行わない。ここで、はCやJava登録商標等のプログラミング言語における否定の単項演算子である。ルールbの式eは、元のループの制御式なので、eへの反例は、eが真であること、すなわちループをNMAX回展開した後で、制御式が真になり得ることを示す。換言すると、この反例は、元のループがNMAXを超える回数の繰返しを含んでいること、すなわちNMAXを越える繰返し部分で起きる不具合を有限モデル検査ツールが見過ごし得ることを示している。以下、ルールbのassert文をループ展開表明と呼ぶ。図4のソースファイル400aは、図2で示したソースファイル200aを検査対象プログラムとし、NMAXを2としてループを展開した有界プログラムの例である。尚、ここまではループ展開によりループを有界化する場合を説明したが、ループボディの固定回数の実行後にループの処理を強制終了するように有界プログラムを生成する変換処理ループ強制終了も可能である。図5のルールcは、このループ強制終了の際に用いる変換ルールを示す。ルールcでは、検査対象プログラムには存在しないメタ変数_nMを導入する。_nMはループの実行回数を示すメタ変数であり、初期値は0を取り、ループボディの先頭で1ずつ値が加算されるようになっている。ルールcでは、この_nMがNMAXを超えると、図3のルールbと同様のループ展開表明としてasserteが呼び出されるようになっている。図6のソースファイル400bは、図2に示したソースファイル200aを検査対象プログラムとして、NMAXを2としてループを強制終了するように変換生成された有界プログラムの例である。このように、第1のループ有界化処理では、ルールa及びb、又はルールcを用いて、検査対象プログラムに含まれるループを有界化することができる。しかしながら、第1のループ有界化処理によりループを有界にする方式ループ有界化法には、ループ内の処理を固定回数NMAXまで実行した後の処理が、有界モデル検査ツールにより検査されないという課題がある。この点、以下に説明する。ソースファイル200aは、変数xに1を設定し第12行、変数iとaに関係するループ処理を1024回繰返し第13行~第17行、当該ループ処理終了後にxが0であることを検査するようにassert文で指示している第19行。実際にソースファイル200aを実行すると、第19行ではxの値は1となるのでassert文の式x==0は偽となり、結果、assert違反の警告が出力されて停止する。一方、第1のループ有界化処理により有界化された有界プログラムである図4のソースファイル400aや図6のソースファイル400bを有界モデル検査によって検査すると、ループボディ元のソースファイル200aが含むループ内の処理を固定回数ここでは2回繰り返してからループ展開表明が偽となるためソースファイル400aの第14_3行、及びソースファイル400bの第14c行、ここでassert違反の警告が出力されて停止する。これにより、ループ後の処理第19行は探索されないので、x==0のassert違反は見過ごされることとなる。つまり、有界モデル検査法を用いた検索対象プログラムの検査において、第1のループ有界化処理によってプログラムを有界な有限状態空間に収めるためにループを固定回数のループボディの処理の繰返しに変換すると、固定回数が本来の繰返し回数図2のソースファイル200aの例では1024回未満である場合には、それ以降の処理に対する検査が行われないこととなってしまう。ルールa及びbを用いた、ループボディを固定回数だけ展開して繰返しを限定するループ展開の方式であっても、ルールcを用いた、ループボディに繰返し回数を表すメタ変数を挿入し、メタ変数の値と固定回数とを比較して繰返しを限定するようなループ強制終了の方式であっても、この課題は発生する。そこで、ループ有界化モジュール113は、状況に応じてループ後の処理も探索できるように有界化を行う機能第2のループ有界化処理を有する。以下、図2に示すソースファイル200aを検査対象プログラムとして、第2のループ有界化処理を行う場合を例に説明する。第2のループ有界化処理によるループ展開では、図3のルールaとルールb’とを用いて、ループを、ユーザが指定した固定回数であるNMAX回だけ展開する。より具体的には、0≦n<NMAXであるようなn回目までのループ内の処理についてはルールaを、n=NMAXであるn回目のループ内の処理についてはルールb’を用いてループを展開する。図8のソースファイル400cは、ソースファイル200aを検査対象プログラムとし、NMAXを2として第2のループ有界化処理を行った結果である有界プログラムの例を示す。第1のループ有界化処理では、NMAX回目のループ内の処理がルールbによって、図4の14_3行目のようにassertを用いた表明ループ展開表明、第14_3行に変換されていた。これにより、変換結果であるソースファイル400aは、assertに指定された式が偽となる場合にはループの後に続く処理には制御が移らない、すなわち、ループの後に続く処理第19行が有界モデル検査法で探索されないものとなっていた。一方、第2のループ有界化処理では、NMAX回目のループ内の処理は、ルールb’によって、ループ後に続くラベルwhile1_breakに制御を移すgoto文第14_3行に変換される図8のソースファイル400c。これにより、第2のループ有界化処理を用いた有界プログラムは、ループ後の処理も有界モデル検査法で探索可能となる。尚、ここまではループ展開によりループを有界化する場合を説明してきたが、第2のループ有界化処理でも第1のループ有界化処理と同様に、ループを強制終了するように変換することも可能である。図5のルールc’にその変換ルールを示す。ルールc’でも、ルールcと同様に、検査対象プログラムには存在しないメタ変数_nMが導入される。_nMはループの実行回数を示すメタ変数であり、初期値は0を取り、ループボディの先頭で1ずつ値が加算される。ルールc’では、この_nMがNMAXを超えると、図3のルールb’と同様に、ループ後に続くラベルwhileM_breakに制御を移すgoto文を呼び出す。図9のソースファイル400dは、第2のループ有界化処理において、ソースファイル200aを検査対象プログラムとし、NMAXを2としてループ強制終了により変換した結果である有界プログラムの例である。第1のループ有界化処理では、ルールcを用いていたので、NMAX回目のループの処理が図6の第14c行のようにassertを用いた表明ループ展開表明に変換されていた。これにより、変換結果であるソースファイル400bは、assertに指定された式が偽となる場合には、ループの後に続く処理に制御が移らない、すなわち、ループの後に続く処理第19行が有界モデル検査法で探索されないものとなっていた。一方、第2のループ有界化処理では、ルールc’によって、NMAX回目のループの処理がループ後に続くラベルwhile1_break18行に制御を移すgoto文14c行に変換される図9のソースファイル400d。以上のように、ループ展開の場合であっても、ループ強制終了の場合であっても、第2のループ有界化処理により有界プログラムを生成すれば、有界モデル検査ツールがループより後の処理も探索できるようになる。しかしながら、すべての場合に第2のループ有界化処理を適用して、一律でループ後の処理も探索することとしてしまうと、誤警告が生じるという新たな課題が発生する。以下、その課題を説明する。例えば、図7のソースファイル200bに記載の検査対象プログラムを実際に動かすと、ループ第14行~第17行を1024回繰返し、変数iの値が1024となってループを終了する。よってループ後の処理第19行での表明i==1024は真となり、表明違反を起こさない。一方、ループ第14行~第17行を2回のみ繰り返した後、ループ後の処理第19行を強制的に探索するようにループ有界化を行うと、有界プログラムは、図4のソースファイル400aで第19行がasserti==1024に置換されたものとなる。これを実行すると、第19行において変数iの値は2となるので、表明i==1024は偽となる。よって、表明違反の警告が出力されることとなる。上述の通り、本来の検査対象プログラムでは表明違反は起きないので、この警告は誤り誤警告である。誤警告が発生した原因は、繰返し回数を限定したループ内で値が参照される変数図7の例ではiをループ後の処理で参照することにより、当該変数が本来のループ終了時とは異なる値を得てしまったことである。このような誤警告を防ぐために、ループ有界化モジュール113は、ループ後の処理で値が参照される変数に対し、その変数の値がループ内で設定されたか否かを調べた上で、第1のループ有界化処理を行うか、若しくはループ後の処理も探索する第2のループ有界化処理を行うかを判別する。これにより、誤警告を防ぎつつ、ループ後の処理も探索することができるようになる。以下、図10のフローチャートを参照しながら、情報処理装置100の処理の流れを説明する。まず情報処理部110は、ユーザから、有界モデル検査の対象である検査対象プログラムと、検査対象関数との指定を受付け、これに伴い、入力モジュール111、ループ有界化モジュール113、及び出力モジュール115を用いて一連の処理を実行する。以下、特に記載しない場合には、検査対象プログラムとして図2に示すソースファイル200aが指定されたものとして説明を行う。入力モジュール111は、ファイル格納部120から検査対象プログラムを読込むS501。ループ有界化モジュール113は、まず、読込まれた検査対象プログラムの関数毎に、ループの開始位置と終了位置とを含むループ位置情報を抽出するS503。図11は、ループ有界化モジュール113が抽出したループ位置情報の例である。図11の例では、ループを含む関数の名前と、ソースファイル等の検査対象プログラムを格納するもの格納体の名前、格納体上でのループの開始位置と終了位置格納体がソースファイルの場合、開始位置及び終了位置は、行番号となるがそれぞれ対応づけて管理されている。例えば、図11の1行目見出し行は除くは、関数fooに含まれるループが、ソースファイルFoo.cにおいて、第14行から始まり第17行で終わることを示す。続いてループ有界化モジュール113は、検査対象プログラムの関数毎に、変数に値が設定される位置と、その値を参照する位置との組であるデータ依存関係を抽出するS505。図12は、ループ有界化モジュール113が抽出したループ位置情報の例である。図12の例では、変数が現れる関数の名前と、変数の名前と、ソースファイル等の検索対象プログラムを格納するもの格納体の名前と、格納体上で変数に値を設定する位置定義位置と、その変数の値を参照する位置参照位置とが対応付けて管理されている。例えば、図12の1行目見出し行は除くは、関数fooに現れる変数xにソースファイルFoo.cの第12行で値が設定され図2のソースファイル200aにおける第12行のx=1、第19行でその値が参照されるソースファイル200aの第19行のx==0ことを示す。次に、ループ有界化モジュール113は、検査対象関数に含まれるループをループ位置情報から抽出しS507、ループ毎に、ループボディの処理ループ内の処理の繰返しを固定回数までとする有界化を行うS511~S521。最後に、ループ有界化モジュール113は、ループが有界化されたプログラム有界プログラムを出力するS523。以下、ループ毎の有界化の処理S511~S521を詳しく説明する。ループ有界化モジュール113は、検査対象関数に現れる変数のうち、処理中のループの終了位置<変数の参照位置である変数を、データ依存関係から抽出するS511。ループ有界化モジュール113は、抽出した変数毎にS513、変数の定義位置とループの開始位置/終了位置とを比較しS515及びS517、変数の定義位置がループ内にあればS517がNo比較結果が偽、ループの後の処理に制御を移さないように第1のループ有界化処理を用いてループを有界化するS519。より具体的には、ループ展開によりループを有界化するのであれば図3のルールa、bを、ループの強制終了によりループを有界化するのであれば図5のルールcを用いてループを有界化する。変数の定義位置がループ内になければS515またはS517がYes比較結果が真、第1のループ有界化処理とは異なり、ループの後の処理に制御を移すように第2のループ有界化処理を用いてループを有界化するS521。より具体的には、ループ展開によりループを有界化するのであれば図3のルールa、b’を、ループの強制終了によりループを有界化するのであれば図5のルールc’を用いてループを有界化する。以下、具体例を用いて、ループをループボディの繰返しに展開する処理を説明する。検査対象プログラムであるソースファイル200aのループ第14行~第17行は、まず図3のルールaを用いて有界プログラム図8のソースファイル400cの1回目のループボディ第14_1行、第15_1行、第16_1行、及び第17_1行、2回目のループボディ第14_2行、第15_2行、第16_2行、及び第17_2行に展開される。次に、図3のルールb’を用いて、ループの後に続くラベルwhile1_breakに制御を移すgoto文第14_3行に変換される。これにより、ループの後に続く処理が有界モデル検査で探索可能となる。ここで、もしルールbを用いた場合すなわち、第1のループ有界化処理を用いた場合には、図4のソースファイル400bの第14_3行のように、assertを用いた表明に変換されるので、assertに指定された式が偽となる場合、ループの後に続く処理には制御が移らない。つまり、すなわちループの後に続く処理が有界モデル検査で探索されないこととなってしまう。しかしながら、図2のソースファイル200aを検査対象プログラムとする場合には、図11で示したループの終了位置第17行よりも後の位置で値が参照される変数は、図12を参照すると、x第19行で参照のみであることがわかる。変数xは、ループ開始前に値が設定され第12行、ループ終了第17行後に値が参照されている第19行。よって、変数xの定義位置とループの開始位置の比較で比較結果が真S515のYesとなるので、ループ有界化モジュール113の処理はS513に戻る。この例において調べるべき変数はxのみであったので、ループ有界化モジュール113は、S513からS521に処理を進める。S521において、ループ有界化モジュール113は、検査対象プログラムであるソースファイル200aを、第2のループ有界化処理により、有界プログラムであるソースファイル400cへと変換する。このように変換された有界プログラムを出力することによりS523、有界モデル検査ツールがループよりも後の処理を探索できるようになる。第2実施形態以下、図13及び図14を参照しながら本発明の第2実施形態を説明する。図13及び図14は、本発明の第2実施形態を説明するための図である。尚、第1実施形態と同様の構成及び動作を行う構成には第1実施形態と同じ符号を付すと共に、説明を省略する。また、構成以外にも、有限モデル検査の説明や、情報処理装置100が入力とすることのできる検査対象プログラム等の、第1実施形態と同様の前提等については、説明を省略している。図13は、第2実施形態に係る情報処理装置100の概略構成を示す機能ブロック図である。本実施形態に係る情報処理装置100は、例えばCPUCentralProcessingUnit等の演算装置である情報処理部110と、例えば記憶媒体等であるファイル格納部120とを有する。この点、第1の実施形態と同様である。ここで、情報処理部110が、入力モジュール111、ループ有界化モジュール113、及び出力モジュール115に加えて、有界モデル検査モジュール117を更に有する点が第1実施形態と異なる。尚、これらのモジュールはソフトウェアで実装されていてもハードウェアで実装されていても良い。すなわち、情報処理部110上の処理は、すべてコンピュータに実行させるプログラムにより実現されうる。情報処理部110は、入力モジュール111と、ループ有界化モジュール113と、出力モジュール115と、有界モデル検査モジュール117とに、図14に示すS601乃至S605の処理を実行させる。以下、図14のフローチャートを参照しながら、本実施形態に係る情報処理装置100の処理の流れを詳細に説明する。情報処理部110は、利用者ユーザから検査対象プログラムと検査対象関数との指定を受付け、入力モジュール111と、ループ有界化モジュール113と、出力モジュール115と、有界モデル検査モジュール117とに図14に示す一連の処理を実行させる。入力モジュール111は、検査対象プログラムをファイル格納部120から読込むS601。そしてループ有界化モジュール113は、ループボディの処理の繰返しが固定回数に制限された有界プログラムに変換し、生成した有界プログラムを出力するS603。ここで、有界プログラムへの変換処理S603の詳細は、第1実施形態の図10の処理と同様である。有界モデル検査モジュール117は、有界プログラムを入力として、プログラムを有界名有限状態遷移システムに変換し、同システム上の有限状態空間を決められた範囲内で網羅探索して、プログラムの正しさを示す性質プロパティを表現した論理式が成立するか否かを調べるS605。出力モジュール115は、当該有界モデル検査モジュール117による検査結果をファイル格納部120へと出力するS607。有界モデル検査モジュール117は、決められた時間内に網羅探索が終わった場合、検査結果として不具合の有無を示す。もし不具合があった場合には、有界モデル検査モジュール117は、初期状態からプロパティが成立しない状態までの変数値の遷移列パス情報も併せて示す。他方、決められた網羅探索が終わらなかった場合には、有界モデル検査モジュール117は不具合の有無を示すことができない。第1及び第2実施形態の効果有界モデル検査法を用いたプログラムの検査では、プログラムを有界名有限状態空間に収めるために、ループを固定回数の繰返しに変換する。第1のループ有界化処理のみを用いる場合には、固定回数を超えるループボディの繰返しに続く処理にプログラム実行の制御が移らないように有界プログラムを生成するため、ループに続く処理が有界モデル検査の探索対象外となってしまう。換言すると、ループに続く処理で生じる不具合を有界モデル検査で見逃す場合があった。第1及び第2実施形態に示す手法によれば、ループの後に続く処理で値が参照される変数について、その値がループ内で設定されていない場合であれば、固定回数を超えるループボディの繰返しに続く処理にもプログラム実行の制御が移るように変換されるので、ループに続く処理も有界モデル検査による探索対象となる。よって、このような場合に、ループに続く処理で生じる不具合を有界モデル検査で示すことができるようになる。付記事項なお、前述の各実施形態の構成は、組み合わせたり或いは一部の構成部分を入れ替えたりしてもよい。また、本発明の構成は前述の実施形態のみに限定されるものではなく、本発明の要旨を逸脱しない範囲内において種々変更を加えてもよい。尚、前述の各実施形態の一部又は全部は、以下の付記のようにも記載されうるが、以下には限られない。付記1検査対象プログラムの入力を受ける入力手段と、前記検査対象プログラムから、該検査対象プログラムに含まれるループによる繰返し演算数を閾値以下とするための有界プログラムを生成する生成手段とを備え、前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える、情報処理装置。付記2前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定される場合には、前記検査対象プログラム内の前記ループ後の処理を行わない有界プログラムを生成し、前記ループ以降で参照される変数に前記ループ内で値が設定されない場合には、前記閾値回の繰返し演算後、前記検査対象プログラム内の前記ループ処理後の処理を行う有界プログラムを生成する、付記1記載の情報処理装置。付記3前記生成手段は、前記ループ以降で参照される変数に前記ループ内で値が設定される場合には、前記閾値回の繰返し演算後に強制終了し、前記ループ以降で参照される変数に前記ループ内で値が設定されない場合には、前記閾値回の繰返し演算後、前記検査対象プログラム内の前記ループ後の処理へ移る有界プログラムを生成する、付記1又は付記2に記載の情報処理装置。付記4前記検査対象プログラムが生成した有界プログラムを用いて、有界モデル検査を行う検査手段をさらに備える、付記1乃至付記3のいずれか1項に記載の情報処理装置。付記5記憶媒体から、検査対象プログラムを読込む入力ステップと、前記検査対象プログラムから、該検査対象プログラムに含まれるループによる繰返し演算数を閾値以下とするための有界プログラムを生成する生成ステップと、を備え、前記生成ステップは、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える、情報処理方法。付記6コンピュータに情報処理方法を実行させる情報処理プログラムであって、当該情報処理方法は、記憶媒体から、検査対象プログラムを読込む入力ステップと、前記検査対象プログラムから、該検査対象プログラムに含まれるループの繰返し演算数を閾値以下とするための有界プログラムを生成する生成ステップと、を備え、前記生成ステップは、前記ループ以降で参照される変数に前記ループ内で値が設定されるか否かに応じて、前記検査対象プログラム内の前記ループ後の処理を行う有界プログラムとするか否かを変える、情報処理プログラム。