(57)【特許請求の範囲】
【請求項１】
再帰データを構成する要素数を限定せずに該再帰データの構造を表現した情報を含む仕様を読み込み、該再帰データに含まれる要素の数を所定数に限定すると仮定した場合の該再帰データの構造を示す構造限定情報を生成する構造限定情報生成手段と、
前記構造限定情報を、表明を用いた検証を実行可能な記法に変換した構造限定表明を生成する構造限定表明生成手段と、
前記構造限定表明を、検証対象とするプログラムが記述された検証対象ファイルが含む前記再帰データの構造とは関係しない表明と合成し、合成した表明を含む検証用ファイルを生成する検証用ファイル生成手段と、
前記検証用ファイルを解析して、合成した前記表明に基づいて前記プログラムに不具合が存在するか否かを検証する表明検証実行手段とを
備えたことを特徴とするプログラム検証装置。
【請求項２】
構造限定情報生成手段は、再帰データの要素を、０から所定数までの個数にそれぞれ限定した複数の構造限定情報を生成し、
構造限定表明生成手段は、生成した前記複数の構造限定情報を、表明検証実行手段が検証可能な記法に変換した複数の構造限定表明を生成し、
検証用ファイル生成手段は、生成した前記複数の構造限定表明を、検証対象ファイルと合成して、複数の検証用ファイルを生成する
請求項１記載のプログラム検証装置。
【請求項３】
構造限定表明を再帰データの構造を示す情報を含む仕様と同じ記法で表現した構造限定仕様を生成する構造限定仕様生成手段と、
前記構造限定仕様を前記仕様に基づいて不具合が存在するか否かを検証する構造限定仕様検証手段とを備えた
請求項１又は請求項２記載のプログラム検証装置。
【請求項４】
構造限定情報生成手段は、再帰データを構成する要素および要素間の連結構造を示す構造限定情報を生成する
請求項１から請求項３のうちのいずれか１項に記載のプログラム検証装置。
【請求項５】
構造限定表明生成手段は、予め定められた構造を補足する情報に基づいて、構造限定情報を表明検証実行手段が検証可能な記法に変換した構造限定表明を生成する
請求項１から請求項４のうちのいずれか１項に記載のプログラム検証装置。
【請求項６】
プログラム検証装置の構造限定情報生成手段が、再帰データの構造に関する情報を含む仕様を読み込み、該再帰データに含まれる要素の数を所定数に限定すると仮定した場合の該再帰データの構造を示す構造限定情報を生成する構造限定情報生成ステップと、
前記プログラム検証装置の構造限定表明生成手段が、前記構造限定情報を、表明を用いた検証を実行可能な記法に変換した構造限定表明を生成する構造限定表明生成ステップと、
前記プログラム検証装置の検証用ファイル生成手段が、前記構造限定表明を、検証対象とするプログラムが記述された検証対象ファイルが含む前記再帰データの構造とは関係しない表明と合成し、合成した表明を含む検証用ファイルを生成する検証用ファイル生成ステップと、
前記プログラム検証装置の表明検証実行手段が、前記検証用ファイルを解析して、合成した表明に基づいて前記プログラムに不具合が存在するか否かを検証する表明検証実行ステップとを
含むことを特徴とするプログラム検証方法。
【請求項７】
コンピュータに、
再帰データの構造に関する情報を含む仕様を読み込み、該再帰データに含まれる要素の数を所定数に限定すると仮定した場合の該再帰データの構造を示す構造限定情報を生成する構造限定情報生成処理と、
前記構造限定情報を、表明を用いた検証を実行可能な記法に変換した構造限定表明を生成する構造限定表明生成処理と、
前記構造限定表明を、検証対象とするプログラムが記述された検証対象ファイルが含む前記再帰データの構造とは関係しない表明と合成し、合成した表明を含む検証用ファイルを生成する検証用ファイル生成処理と、
前記検証用ファイルを解析して、合成した表明に基づいて前記プログラムに不具合が存在するか否かを検証する表明検証実行処理とを
実行させるためのプログラム検証用プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、表明に基づいてプログラムを静的に検証するためのプログラム検証装置、プログラム検証方法及びプログラム検証方法用プログラムに関する。
【背景技術】
【０００２】
プログラムを静的に解析し、「変数がNULLではない」といった調べたい性質（プロパティ property）が成り立つか否かを調べて、不具合を検出する方法がある。
【０００３】
調べたい性質を表現する一つの考え方として、非特許文献１には「契約による設計」(Design by Contract（米国Eiffel Software, Inc.の登録商標）)が記載されている。この考え方では、まず、ソースコードに、関数の開始時点の状態が満たすべき事前条件と、終了時点の状態が満たすべき事後条件と、関数の実行によっても変わらないデータの不変条件とを表明(Assertion)として記述する。そして、表明に基づいてソースコードが正しく記述されているか否かを、プログラムを実行して動的に、またはプログラムを実行せずに静的に調べる。
【０００４】
なお、プログラムを静的に検証するとは、コンピュータに対象プログラムを実行させずに、不具合の有無を確認することを意味する。例えば、静的解析ツールによって、対象プログラムのソースコードや実行可能なバイナリコードを用いて検証する。
【０００５】
また、プログラムを動的に検証するとは、コンピュータに対象プログラムを実行させて、不具合の有無を確認することを意味する。プログラミング言語によっては、対象プログラムのソースコードを実行可能なバイナリコードに変換することや、ソースコードをそのままインタープリタによって実行することもある。
【０００６】
Java（米国Sun Microsystem, Inc.の登録商標）言語における表明記法の一例が非特許文献２に、C言語における表明記法の一例が非特許文献３に記載されている。これらの記法では、その記法で定めた述語とプログラム中の変数とを用いて、プログラム言語の記法に沿って論理式を記述する。
【０００７】
また、プログラムを静的に解析し、表明に基づいて、不具合を検出する方法について、モデル検査法(model checking)を用いた一例が特許文献１に、定理証明(theorem proving)を用いた一例が非特許文献４に記載されている。また、C言語プログラムをモデル検査するための基本的な技術が特許文献２に、プログラムの静的な解析を行うための技術が特許文献３に記載されている。
【０００８】
モデル検査法とは、システムやソフトウェアの振舞いを表した有限個の「状態(state)」および状態間の遷移(transition)からなる有限状態空間(finite state space)において、調べたい性質（プロパティ property）が成立するか否かを、網羅探索により調べる手法である。とくに、探索の深さを限定した有界モデル検査法(bounded model checking)は、効率的な不具合検出方法として注目されている。プログラム検証への適用では、プログラム中の変数の値の組合せを「状態」として、プログラムを有限状態空間としての制約式Cに変換し、事前条件Preと事後条件Postとを合わせた式Pre∧C∧¬Post（∧は論理和、¬は否定）を満たす変数値の推移を網羅探索により見つけることを試みる。見つかった場合、事前条件が成り立ち、かつプログラムを実行した結果、事後条件違反を起こす不具合があるといえる。
【０００９】
定理証明法とは、基本的な幾つかの推論ルールを用いて、ある論理式の真偽を判定する手法である。プログラム検証への適用では、プログラムの各文を論理式S1,S2,S3,…,Sn-2,Sn-1,Snに変換し、事前条件Postが成立したと仮定した事後状態から、Snを実行すると事後状態に到達するような最弱事前条件を計算する。次いで、Sn-1を実行すると上記の最弱事前条件を満たすような状態に到達するような最弱事前条件を計算し、事後状態から事前状態まで同様にSn-2,Sn-3,…,S2,S1についての最弱事前条件を計算する。そして、「事前条件が成立するならば最弱事前条件が成立する」ならばプログラムに不具合は無く、そうでなければプログラムに不具合があるといえる。ここで、最弱事前条件とは、処理Ｓを実行すると条件Ｑを満たす事後状態に必ず到達するような事前状態が満たすべき、もっとも弱い条件である。
【００１０】
一方、システムやソフトウェアの仕様を形式的に記述する手法の一例が、非特許文献５に記載されている。この手法を用いて、同じ構造を持つ要素同士が繰り返し連結されてできた再帰データについて、例えば、ツリー（二分木）によって記述する場合を想定する。この場合、この手法では、ツリーを構成する要素であるノードがleftとrightとの２つのリンクによりノードを参照できる（構造の制約）、全てのノードがleftまたはrightのリンクを１回以上辿って参照できる要素の集合（推移閉包）に自分自身を含まない（連結の仕方の制約）といった仕様を形式的に記述することができる。さらに、この手法では、利用者が指定した個数のツリーとノードについて、仕様を満たす組合せを提示することができる。
【先行技術文献】
【特許文献】
【００１１】
【特許文献１】特開２００９−２１１５０３号公報（段落０００４、段落００１０）
【特許文献２】特表２００７−５２８０５９号公報
【特許文献３】特開平０９−２８２１７３号公報（段落００２３）
【非特許文献】
【００１２】
【非特許文献１】B. Meyer. Applying "Design by Contract". IEEE Computer, Vol.25, No.10, pages 4051, 1992.
【非特許文献２】G. T. Leavens, E. Poll, C. Clifton, Y. Cheon, C. Ruby, D. Cok, P. Muller, J. Kiniry, P. Chalin, D. M. Zimmerman, and W. Dietl. JML Reference Manual. インターネット<URL:http://www.eecs.ucf.edu/~leavens/JML/jmlrefman/>
【非特許文献３】P. Baudin, J.-C. Filliatre, C. Marche, B. Monate, Y. Moy, and V. Prevosto. ACSL: ANSI/ISO C Specification Language.インターネット<URL:http://frama-c.cea.fr/download/acsl_1.4.pdf>
【非特許文献４】C. Flanagan, K. R. M. Leino, M. Lillibridge, G. Nelson, J. B. Saxe, and R. Stata. Extended Static Checking for Java. In Proc. PLDI'02, pages 234-245, 2002.
【非特許文献５】D. Jackson. Software Abstractions: Logic, Language, and Analysis. The MIT Press, 2006.
【発明の概要】
【発明が解決しようとする課題】
【００１３】
しかしながら、上述したJava言語やC言語の表明記法により、再帰データの構造を表現する表明を記述することは困難である。その理由は、繰り返し回数が決まっていないため、再帰データの要素の数も決まらず、プログラム言語の記法の範囲では論理式を記述できないからである。
【００１４】
また、上述したモデル検査法により、再帰データを扱うプログラムを検証することも困難である。その理由は、繰り返し回数が決まっていないため、再帰データの要素の数も決まらず、プログラムを有限状態空間に変換することができないからである。
【００１５】
詳しく説明すると、再帰データについての構造は、再帰データの１番目の要素の構造を決め、この要素が繰り返しの終端でなければ、２番目の要素の構造を決め、この要素が繰り返しの終端でなければ、３番目の要素の構造を決め、…というように、再帰データの各要素についての構造を決める必要がある。プログラム言語ではＮ番目の要素をＮが不定の場合に表現することは難しい。したがって、繰り返しの回数または要素の数が決まらなければ、再帰データの構造をプログラム言語の記法で表現することができない。その結果、プログラム言語の記法に則って、再帰データの構造を表明として記述することができない。
【００１６】
特許文献１の段落００１０に記載されているように、Kripke構造は、非決定性有限オートマトンであり、状態が有限である必要がある。また、特許文献１の段落０００４に記載されているように、状態は、変数i (i=1〜m）が取り得る値の数の積で決まる。したがって、再帰データでは、値を持つ変数（要素）の数mは有限ではないため、Kripke構造に変換することができない。
【００１７】
本発明の構造限定情報は、特許文献１のKripke構造モデルの状態遷移グラフの初期状態に相当する。本発明によれば、再帰データの要素の数を利用者が指定したN以下に限定し、要素数が0の場合の構造限定情報、要素数が1の場合の構造限定情報・・・要素数がNの場合の構造限定情報を生成し、各構造限定情報を初期状態として特許文献１に記載の検証を可能とすることができる。
【００１８】
また、特許文献３に記載されたループ停止条件および再帰呼び出し停止条件とは、再帰データに循環が無いことを示すものであり、再帰データの要素数が有限であることを示すものではない。したがって、これらの条件を用いて、特許文献１に記載されたKripke構造を作ることはできないため、特許文献１に記載された方法でプログラムを検証することはできない。
【００１９】
また、特許文献３の段落００２３に「停止するための必要条件も常に検出できるわけではない。」と記載されているように、ループ停止条件および再帰呼び出し停止条件は、算出できないことも有る。そのため、この場合には、再帰データの検証ができなくなる。
【００２０】
特許文献２に記載された技術は、C言語プログラムをモデル検査するためのものである。そして、特許文献１に記載された技術は、特許文献２に記載された効果に加えて、表明の検証ができるようにしたものである。
【００２１】
しかし、特許文献１、特許文献２および特許文献３に記載された技術では、要素の個数が不明な再帰データについて表明に基づいて検証を行うことができない。
【００２２】
そこで、本発明は、表明に基づいて再帰データを扱うプログラムを静的に検証することができるプログラム検証装置、プログラム検証方法及びプログラムを提供することを目的とする。
【課題を解決するための手段】
【００２３】
本発明によるプログラム検証装置は、再帰データを構成する要素数を限定せずに再帰データの構造を表現した情報を含む仕様を読み込み、再帰データに含まれる要素の数を所定数に限定すると仮定した場合の再帰データの構造を示す構造限定情報を生成する構造限定情報生成手段と、構造限定情報を、表明を用いた検証を実行可能な記法に変換した構造限定表明を生成する構造限定表明生成手段と、構造限定表明を、検証対象とするプログラムが記述された検証対象ファイルが含む再帰データの構造とは関係しない表明と合成し、合成した表明を含む検証用ファイルを生成する検証用ファイル生成手段と、検証用ファイルを解析して、合成した表明に基づいてプログラムに不具合が存在するか否かを検証する表明検証実行手段とを備えたことを特徴とする。
【００２４】
本発明によるプログラム検証方法は、プログラム検証装置の構造限定情報生成手段が、再帰データの構造に関する情報を含む仕様を読み込み、再帰データに含まれる要素の数を所定数に限定すると仮定した場合の再帰データの構造を示す構造限定情報を生成する構造限定情報生成ステップと、プログラム検証装置の構造限定表明生成手段が、構造限定情報を、表明を用いた検証を実行可能な記法に変換した構造限定表明を生成する構造限定表明生成ステップと、プログラム検証装置の検証用ファイル生成手段が、構造限定表明を、検証対象とするプログラムが記述された検証対象ファイルが含む再帰データの構造とは関係しない表明と合成し、合成した表明を含む検証用ファイルを生成する検証用ファイル生成ステップと、プログラム検証装置の表明検証実行手段が、検証用ファイルを解析して、合成した表明に基づいてプログラムに不具合が存在するか否かを検証する表明検証実行ステップとを含むことを特徴とする。
【００２５】
本発明によるプログラム検証用プログラムは、コンピュータに、再帰データの構造に関する情報を含む仕様を読み込み、再帰データに含まれる要素の数を所定数に限定すると仮定した場合の再帰データの構造を示す構造限定情報を生成する構造限定情報生成処理と、構造限定情報を、表明を用いた検証を実行可能な記法に変換した構造限定表明を生成する構造限定表明生成処理と、構造限定表明を、検証対象とするプログラムが記述された検証対象ファイルが含む再帰データの構造とは関係しない表明と合成し、合成した表明を含む検証用ファイルを生成する検証用ファイル生成処理と、検証用ファイルを解析して、合成した表明に基づいてプログラムに不具合が存在するか否かを検証する表明検証実行処理とを実行させることを特徴とする。
【発明の効果】
【００２６】
本発明によれば、表明に基づいて再帰データを扱うプログラムを静的に検証することができる。
【図面の簡単な説明】
【００２７】
【図１】本発明によるプログラム検証方法の第１の実施形態を適用した情報処理装置の全体構成例を示す概略図である。
【図２】第１の実施形態の全体的な処理の流れの一例を示すフロー図である。
【図３】プログラム検証方法の第２の実施形態を適用した情報処理装置の全体構成例を示す概略図である。
【図４】第２の実施形態の全体的な処理の流れの一例を示すフロー図である。
【図５】再帰データの構造を表現する仕様の具体例を示す説明図である。
【図６】要素の数を限定した再帰データの構造を表現する構造限定情報の具体例を示す説明図である。
【図７】再帰データを扱うプログラムを含む検証の対象である検証対象ファイルの内容の具体例を示す説明図である。
【図８】仕様とプログラムの変数の対応関係とプログラムにしかない変数の値の制約とを記述する構造補足情報の具体例を示す説明図である。
【図９】要素の数を限定した再帰データの構造を、表明検証実行手段が扱える記法で表現する構造限定表明の具体例を示す説明図である。
【図１０】検証対象ファイルの内容に構造限定表明を付与した検証用ファイルの内容の具体例を示す説明図である。
【図１１】構造限定表明を、再帰データの構造を表現する仕様の記法で記した構造限定仕様の具体例を示す説明図である。
【図１２】仕様を満たす再帰データの抽出例を示すブロック図である。
【図１３】変数名の付け直しの一例を示す説明図である。
【図１４】プログラム検証装置の最小の構成例を示すブロック図である。
【発明を実施するための形態】
【００２８】
実施形態１．
以下、本発明の第１の実施形態について図面を参照して説明する。
【００２９】
＜装置構成＞
図１は、本発明によるプログラム検証方法の第１の実施形態を適用した情報処理装置の全体構成例を示す概略図である。情報処理装置１００は、情報処理部１６０とファイル格納部１７０とを含む。情報処理装置１００は、具体的には、プログラムに従って動作するパーソナルコンピュータ等によって実現される。情報処理部１６０は、具体的には、プログラムに従って動作する情報処理装置のＣＰＵによって実現される。ファイル格納部１７０は、具体的には、磁気ディスク装置や光ディスク装置、メモリ等の記憶装置によって実現される。
【００３０】
情報処理部１６０は、制御モジュール１１０と構造限定情報生成モジュール１２０と構造限定表明生成モジュール１３０と検証用ファイル生成モジュール１４０と表明検証実行モジュール１５０とを含む。これらのモジュールのうち、制御モジュール１１０は、利用者による指定要素数や検証対象ファイル、構造補足情報（詳細については後述する）を指定する操作に従って、他のモジュールに図２で示す一連の処理を実行させるように制御する。なお、指定要素数については、予め再帰データの要素数を知っている必要はなく、利用者は任意の数を入力すればよい。
【００３１】
情報処理部１６０が含む各モジュールは、具体的には、情報処理装置が備えるプログラムによって実現される。また、情報処理装置１００は、各モジュールに従って処理を実行する。
【００３２】
構造限定情報生成モジュール１２０は、構造補足情報が示す種類の再帰データに対応する仕様を読み込み、０から指定要素数までの個数ごとに、その個数の要素を含むような再帰データの具体例を検出する機能を備えている。また、構造限定情報生成モジュール１２０は、再帰データを構成する要素と要素間の連結といった構造とを表す情報を含む構造限定情報を生成する機能を備えている。なお、本実施形態では、仕様を読み込む等の表現を用いるが、具体的には、仕様を示すデータを読み込む処理を実行する。
【００３３】
構造限定表明生成モジュール１３０は、構造限定情報生成モジュール１２０が生成した構造限定情報を参照し、構造限定情報を表明検証実行モジュール１５０が検証できる形式に変換した構造限定表明を生成する機能を備えている。
【００３４】
検証用ファイル生成モジュール１４０は、構造限定表明生成モジュール１３０が生成した構造限定表明を検証対象ファイルと合成して、検証用ファイルを生成して出力する機能を備えている。
【００３５】
表明検証実行モジュール１５０は、検証用ファイル生成モジュール１４０が出力した検証用ファイルを解析し、表明に基づいてプログラムの不具合を検出し、検証結果を出力する機能を備えている。
【００３６】
本実施形態では、構造限定情報生成モジュール１２０は、例えば、非特許文献５に記載された技術を利用することによって実現される。また、表明検証モジュール１５０は、例えば、特許文献１または非特許文献２に記載された技術を利用することによって実現される。
【００３７】
＜全体の処理の流れ＞
次に、図１及び図２のフローチャートを参照して、本実施形態の全体の動作について説明する。図２は、第１の実施形態の全体的な処理の流れの一例を示すフロー図である。
【００３８】
プログラムの検証をするために、利用者は情報処理装置１００で所定の情報を入力する操作を行う。すると、制御モジュール１１０は、利用者の操作に従って、指定要素数、検証対象ファイルおよび構造補足情報を入力し、他のモジュールに図２で示す一連の処理（ステップＳ２０１〜Ｓ２０５）を実行させるように制御する。
【００３９】
まず、構造限定情報生成モジュール１２０は、構造補足情報が示す種類の再帰データに対応する仕様を読み込み、０から指定要素数までの個数ごとに、その個数の要素を含むような再帰データの具体例を検出する。すなわち、構造限定情報生成モジュール１２０は、要素数０の再帰データ〜要素数が指定要素数である再帰データをそれぞれ生成する。そして、構造限定情報生成モジュール１２０は、再帰データを構成する要素と要素間の連結といった構造とを表す情報を含む構造限定情報を生成する（ステップＳ２０１）。
【００４０】
＜＜構造限定情報の生成＞＞
ここで、図５、図６、図７、図８および図１２を用いて、構造限定情報の生成処理（ステップＳ２０１）について説明する。
【００４１】
図５は、再帰データの構造を表現する仕様の具体例を示す説明図である。図８は、仕様とプログラムの変数の対応関係とプログラムにしかない変数の値の制約とを記述する構造補足情報の具体例を示す説明図である。
【００４２】
構造限定情報生成モジュール１２０は、構造補足情報８１（図８）から再帰データの種類（構造補足情報８１の２行目BinaryTree）を取得し、ファイル名やモジュール名（図５（ａ）の仕様５１の１行目module BinaryTree_mod）などから、対応する仕様５１および５２（図５（ａ）（ｂ））を特定する。
【００４３】
次いで、構造限定情報生成モジュール１２０は、特定した仕様を読み込み、再帰データ全体については１個の変数を用意し、再帰データを構成する要素については０から指定要素数までの個数ごとに変数を用意し、これらの変数の組合せのうち仕様を満たす組合せを抽出する。
【００４４】
図１２は、仕様を満たす再帰データの抽出例を示すブロック図である。例えば、０から指定要素数までの要素の個数が３の場合、構造限定情報生成モジュール１２０は、図５の仕様で再帰データ全体を現すBinaryTree（仕様５１の４〜６行目）については、１個の変数を用意する（図１２（ａ）のBinaryTree$0）。また、構造限定情報生成モジュール１２０は、再帰データを構成する要素Node（仕様５１の８〜１１１行目）については、３個の変数を用意する（図１２（ａ）のNode$0、Node$1およびNode$2）。
【００４５】
そして、構造限定情報生成モジュール１２０は、これらの組合せについて、ツリーの構造を示す制約（仕様５１の１３〜１９行目 representationInvariant）と、ツリーの構成に余すことなく全要素が使われることを示す制約（仕様５１の２１〜２３行目connected）と、要素の順序の制約（仕様５１の２５〜３０行目 symmetryBreaking）とを満たすものを抽出する。
【００４６】
ツリーの構造を示す制約とは、具体的には、再帰データからrootとして参照される要素からleftまたはrightを０回以上辿って参照できる要素の集合に含まれる全ての要素について、要素からleftまたはrightを１回以上辿って参照できる要素の集合に元の要素自体は含まれず、要素からleftまたはrightを逆に辿った要素は高々１個であり、要素からleftにより参照される要素とrightにより参照される要素とが異なることを示す。
【００４７】
また、ツリーの構成に余すことなく全要素が使われることを示す制約とは、具体的には、再帰データからrootとして参照される要素からleftまたはrightを０回以上辿って参照できる要素の集合は要素の集合に等しいことを示す。
【００４８】
また、要素の順序の制約とは、具体的には、要素のleftとして参照される要素からleftまたはrightを１回以上辿って参照できる要素の集合に含まれる要素は元の要素よりも小さい番号を持ち、要素のrightとして参照される要素からleftまたはrightを１回以上辿って参照できる要素の集合に含まれる要素は元の要素よりも大きい番号を持つ、といったグラフとして同型の組合せを排除することに役立つことを示す。
【００４９】
全要素が使われることを示す制約に合わない組合せとして、例えば、図１２（ｂ）に示すような、Node$2がBinaryTree$0を構成しない組み合わせがある。また、要素の順序間の制約に合わない組合せとして、例えば、図１２（ｃ）に示すような、Node$1のleftに順序が小さいNode$0が連結されているべきだが、順序が大きいNode$2が連結されている組合せがある。
【００５０】
このような全要素が使われることを示す制約に合わない組合せや、要素の順序間の制約に合わない組合せを除き、構造限定情報生成モジュール１２０は、仕様を満たす組合せ５件（図１２（ｄ）参照）を抽出する。
【００５１】
次いで、構造限定情報生成モジュール１２０は、仕様を満たす組合せごとに、再帰データを表す変数と、再帰データを構成する要素を表す変数と、変数間の関係を示す情報とを含む構造限定情報を生成する。
【００５２】
図６は、要素の数を限定した再帰データの構造を表現する構造限定情報の具体例を示す説明図である。例えば、図６において、図６（ｂ）に示す仕様を満たす組合せの一つに対して、構造限定情報６１の３〜５行目には、再帰データを表す変数BinaryTree$0が記述されている。
【００５３】
また、構造限定情報６１の６〜９行目には、再帰データBinaryTree$0からrootという名称で要素Node$1を参照することが記述されている。また、構造限定情報６１の１０〜１４行目には、再帰データを構成する要素を表す変数Node$0、Node$1およびNode$2が記述されている。
【００５４】
また、構造限定情報６１の１５〜１８行目には、要素Node$1からleftという名称で要素Node$0を参照することが記述されている。また、構造限定情報６１の１９〜２２行目には、要素Node$1からrightという名称で要素Node$2を参照することが記述されている。
【００５５】
以上のように、ステップＳ２０１で構造限定情報を生成すると、制御モジュール１１０は、生成した構造限定情報ごとに、構造限定表明の生成処理（ステップＳ２０３）、検証用ファイルの生成処理（ステップＳ２０４）および表明検証の実行処理（ステップＳ２０５）を繰り返すように制御する（ステップＳ２０２）。以下、各処理について具体例を用いて説明する。
【００５６】
＜＜構造限定表明の生成＞＞
構造限定表明の生成処理（ステップＳ２０３）について説明する。構造限定表明生成モジュール１３０は、生成された構造限定情報から、構造補足情報を用いて、仕様の用語をプログラムの用語に変換し、仕様には記述されていない情報を付加して、構造限定表明を生成する（ステップＳ２０３）。
【００５７】
構造補足情報は、利用者が予め定義しておく必要がある。例えば、形式言語Ａｌｌｏｙで記述された仕様５１および５２と、Ｃ言語で記述された図７の検証対象ファイルの内容７１とに対して定義された図８の構造補足情報について説明する。ここでは、構造補足情報８１の５〜９行目は、仕様における用語「root」「Node」「left」「right」「none」を、それぞれプログラムにおける用語「引数の *p」「struct Node *」「l」「r」「NULL」に変換すべきことを示している。
【００５８】
また、構造補足情報８１の１１、１２行目では、それぞれプログラムにおける要素のメンバ変数keyの値が仕様における要素の序数に１を加えて後に２倍した値であること、引数keyの値が１以上７以下であることを付加すべきであることを示している。構造限定表明生成モジュール１３０は、これらの情報を用いて、図６（ｂ）の組合せ６２に対応した構造限定表明９１を生成する。
【００５９】
図９は、要素の数を限定した再帰データの構造を、表明検証実行手段が扱える記法で表現する構造限定表明の具体例を示す説明図である。図９の構造限定表明９１の１から３行目は、仕様におけるroot、root.left、root.rightをプログラムにおける変数*p, (*p)->l, (*p)->rに変換し、__allocated述語で囲むことにより、述語の「引数として与えたプログラム変数に異なるアドレスを割り当てる」ことを示している。
【００６０】
また、構造限定表明９１の４〜７行目は、(*p)->lと(*p)->rとからは、lおよびrが無効なアドレス（NULL）であることを仮定することを示している。
【００６１】
また、構造限定表明９１の７から１０行目は、変数*p, (*p)->l, (*p)->rのメンバ変数keyがそれぞれ４、２、６であると仮定することを示している。また、構造限定表明９１の１１行目は、引数keyの値が０以上７以下であることを示している。
【００６２】
＜＜検証用ファイルの生成＞＞
次に、検証用ファイルの生成処理（ステップＳ２０４）について説明する。検証用ファイル生成モジュール１４０は、生成された構造限定表明を検証対象ファイルと合成して、検証用ファイルを生成する（ステップＳ２０４）。
【００６３】
図１０は、検証対象ファイルの内容に構造限定表明を付与した検証用ファイルの内容の具体例を示す説明図である。例えば、図１０の検証用ファイルの内容１００１は、構造限定表明９１と検証対象ファイルの内容７１とを合成したものであり、２〜１２行目が構造限定表明となっている。
【００６４】
＜＜表明検証の実行＞＞
次に、表明検証の実行処理（ステップＳ２０５）について説明する。表明検証実行モジュール１５０は、生成された検証用ファイルを解析し、表明に基づいてプログラムの不具合を検出し、不具合の有無を検証結果として出力する（ステップＳ２０５）。
【００６５】
以上のように、本実施形態では、再帰データを構成する要素数を限定せずに再帰データの構造を仕様として表現することができる。そのため、利用者が要素数を限定しなくても、再帰データを構成する要素数を限定した表明に基づいて再帰データを扱うプログラムを、モデル検査法または定理証明法などを用いて、静的に検証することができる。
【００６６】
実施形態２．
以下、本発明の第２の実施形態について図面を参照して説明する。
【００６７】
＜装置構成＞
図３は、本発明によるプログラム検証方法の第２の実施形態を適用した情報処理装置の全体構成例を示す概略図である。情報処理装置３００は、情報処理部３６０とファイル格納部３７０とを含む。情報処理装置３００は、具体的には、プログラムに従って動作するパーソナルコンピュータ等によって実現される。情報処理部３６０は、具体的には、プログラムに従って動作する情報処理装置のＣＰＵによって実現される。ファイル格納部３７０は、具体的には、光ディスク装置や磁気ディスク装置、メモリ等の記憶装置によって実現される。
【００６８】
情報処理部３６０は、制御モジュール３１０と構造限定情報生成モジュール３２０と構造限定表明生成モジュール３３０と検証用ファイル生成モジュール３４０と表明検証実行モジュール３５０と構造限定仕様生成モジュール３８０と構造限定仕様検証モジュール３９０とを含む。これらのモジュールのうち、制御モジュール３１０は、利用者による指定要素数、検証対象ファイル、構造補足情報を指定する操作に従って、他のモジュールに図４で示す一連の処理を実行させるように制御する。各モジュールは、具体的には、情報処理装置が備えるプログラムによって実現される。また、情報処理装置は、各モジュールに従って処理を実行する。
【００６９】
モジュール３２０〜３５０については、第１実施形態におけるモジュール１１０〜１５０とそれぞれ同じ役割を持つため、説明を省略する。
【００７０】
構造限定仕様生成モジュール３８０は、構造補足情報が示す仕様における用語とプログラムにおける用語との変換の方法に従って、構造限定表明を変換し、構造限定仕様を生成する機能を備えている。
【００７１】
構造限定仕様検証モジュール３９０は、元の仕様に基づいて生成された構造限定仕様に不具合が存在するか否かを検証する機能を備えている。
【００７２】
本実施形態では、構造限定情報生成モジュール３２０と構造限定仕様検証モジュール３９０とは、例えば、非特許文献５に記載された技術を利用することによって実現される。また、表明検証モジュール１５０は、例えば、特許文献１または非特許文献２に記載された技術を利用することによって実現される。
【００７３】
＜全体の処理の流れ＞
次に、図３及び図４のフローチャートを参照して本実施形態の全体の動作について説明する。図４は、本実施形態の全体的な処理の流れの一例を示すフロー図である。
【００７４】
プログラムの検証をするために、利用者は情報処理装置３００で所定の情報を入力する操作を行う。すると、制御モジュール３１０は、利用者の操作に従って、指定要素数、検証対象ファイルおよび構造補足情報を入力し、他のモジュールに図４で示す一連の処理（ステップＳ４０１〜Ｓ４０９）を実行させるように制御する。
【００７５】
構造限定情報生成モジュール３２０は、構造補足情報が示す種類の再帰データに対応する仕様を読み込み、０から指定要素数までの個数ごとに、その個数の要素を含むような再帰データの具体例を検出する。そして、構造限定情報生成モジュール３２０は、再帰データを構成する要素と要素間の連結といった構造とを表す情報を含む構造限定情報を生成する（ステップＳ４０１）。本ステップの詳細は、第１の実施形態のステップＳ２０１と同様である。
【００７６】
次いで、制御モジュール３１０は、生成された構造限定情報ごとに、構造限定表明の生成処理（ステップＳ４０３）、構造限定仕様の生成処理（ステップＳ４０４）および構造限定仕様の検証処理（ステップＳ４０５）を繰り返すように制御する（ステップＳ４０２）。
【００７７】
構造限定表明の生成処理では、構造限定表明生成モジュール３３０は、生成された構造限定情報から、構造補足情報を用いて、仕様の用語をプログラムの用語に変換し、仕様には記述されていない情報を付加して、構造限定表明を生成する（ステップＳ４０３）。本ステップの詳細は第１の実施形態のステップＳ２０３と同様である。
【００７８】
次いで、構造限定仕様の生成処理では、構造限定仕様生成モジュール３８０は、構造補足情報が示す仕様における用語とプログラムにおける用語との変換の方法に従って、構造限定表明を変換し、構造限定仕様を生成する（ステップＳ４０４）。
【００７９】
図１１は、構造限定表明を、再帰データの構造を表現する仕様の記法で記した構造限定仕様の具体例を示す説明図である。例えば、生成される構造限定仕様１１０１は、構造補足情報８１の２行目の再帰データの種類BinaryTreeに対応する仕様BianryTree_modを２行目で引用している。
【００８０】
また、構造限定仕様１１０１は、構造限定表明９１で用いた述語__allocatedの「引数として与えたプログラム変数に異なるアドレスを割り当てる」ことを表現するために、再帰データの要素Nodeをnodeという名前で参照するアドレスAddressを４〜６行目で定義している。
【００８１】
また、構造限定仕様１１０１は、プログラムにおける変数が指すアドレスと仕様における再帰データの要素との対応関係を述語addressMappingとして８〜１３行目で定義している。
【００８２】
addressMappingを詳しく見ると、構造限定表明９１の１〜３行目に対応して、アドレスと再帰データの要素とを９〜１２行目で対応付けている。また、１３行目では、仕様BianryTree_modの述語show（仕様５２の３２〜３６行目）を介して、制約representationInvariant、connected、symmetryBreakingを参照している。
【００８３】
次いで、構造限定仕様の検証処理では、構造限定仕様検証モジュール３９０は、元の仕様に基づいて生成された構造限定仕様に不具合が存在する（問題がある）か否かを検証する（ステップＳ４０５）。
【００８４】
例えば、構造限定仕様検証モジュール３９０は、構造限定仕様１１０１において、変数の数が３個、ただしBinaryTreeの変数が１個という条件に従って、述語addressMappingを満たすAddress、BinaryTree、Nodeの変数の組合せを検出する。そして、構造限定仕様検証モジュール３９０は、検出した組合せが唯一つであれば、仕様に基づいて構造限定表明には問題がないと判断し、それ以外であれば、問題ありと判断する。
【００８５】
上記の一連の処理が終了すると、制御モジュール３１０は、構造限定表明に問題があれば処理全体を終了し、そうでなければ、構造限定情報に関する繰り返し処理の起点（ステップＳ４０２）に処理を移行する（ステップＳ４０６）。
【００８６】
制御モジュール３１０は、構造限定情報に関する繰り返し処理が終了すれば（ステップＳ４０２）、生成された構造限定表明ごとに、検証用ファイルの生成処理（ステップＳ４０８）および表明検証の実行処理（ステップＳ４０９）を繰り返すように制御する（ステップＳ４０７）。なお、検証用ファイルの生成処理（ステップＳ４０８）および表明検証の実行処理（ステップＳ４０９）については、第１の実施形態のステップＳ２０４、Ｓ２０５と同様であるため、説明を省略する。
【００８７】
以上のように、本実施形態では、再帰データを構成する要素数を限定せずに再帰データの構造を仕様として表現するとともに、仕様とプログラムとにおける用語の変換およびそのチェックをすることができる。そのため、利用者が要素数を限定しなくても、再帰データを構成する要素数を限定した表明に基づいて再帰データを扱うプログラムを、モデル検査法または定理証明法などを用いて、静的に検証することができる。
【００８８】
以下、先行技術との差異について説明する。特許文献１の段落００１０に記載されているように、Kripke構造は、非決定性有限オートマトンであり、状態が有限である必要がある。また、特許文献１の段落０００４に記載されているように、状態は、変数i (i=1〜m）が取り得る値の数の積で決まる。したがって、再帰データでは、値を持つ変数（要素）の数mは有限ではないため、Kripke構造に変換することができない。
【００８９】
本発明における構造限定情報は、特許文献１のKripke構造モデルの状態遷移グラフの初期状態に相当する。本発明によれば、再帰データの要素の数を利用者が指定したN以下に限定し、要素数が0の場合の構造限定情報、要素数が1の場合の構造限定情報・・・要素数がNの場合の構造限定情報を生成する。そして、各構造限定情報を初期状態として特許文献１に記載の検証を可能とすることができる。
【００９０】
また、特許文献２の段落００２１に記載されている変数名の付け直しとは、図１３に示すような関数f1,f2,f3を一つの大きな関数bigにまとめる際に、各関数のローカル変数xの名前が衝突しないように、元の変数にプレフィックスやサフィックスなどを付加して、bigで一意になるようにするものである。したがって、本発明のように、構造限定情報と補足情報とにより構造限定表明を作成することとは異なる。
【００９１】
また、特許文献３に記載されたループ停止条件および再帰呼び出し停止条件とは、再帰データに循環が無いことを示すものであり、再帰データの要素数が有限であることを示すものではない。したがって、これらの条件を用いて、特許文献１に記載されたKripke構造を作ることはできないため、特許文献１に記載された方法でプログラムを検証することはできない。
【００９２】
特許文献３の段落００２３に「停止するための必要条件も常に検出できるわけではない。」と記載されているように、ループ停止条件および再帰呼び出し停止条件は、算出できないことも有る。そのため、この場合には、再帰データの検証ができなくなる。
【００９３】
これらの条件は、本発明の図１の仕様（の一部）に相当する。このため、本発明によれば、ループ停止条件および再帰呼び出し停止条件を含むような仕様を図１にあるように入力として与えることとで、再帰データの検証を可能としている。
【００９４】
次に、本発明によるプログラム検証装置の最小構成について説明する。図１４は、プログラム検証装置の最小の構成例を示すブロック図である。図１４に示すように、プログラム検証装置は、最小の構成要素として、構造限定情報生成手段１と、構造限定表明生成手段２と、検証用ファイル生成手段３と、表明検証実行手段４とを含む。
【００９５】
図１４に示す最小構成のプログラム検証装置では、構造限定情報生成手段１は、再帰データを構成する要素数を限定せずに再帰データの構造を表現した情報を含む仕様を読み込み、再帰データに含まれる要素の数を所定数に限定すると仮定した場合の再帰データの構造を示す構造限定情報を生成する。次いで、構造限定表明生成手段２は、構造限定情報を表明を用いた検証を実行可能な記法に変換した構造限定表明を生成する。
【００９６】
次いで、検証用ファイル生成手段３は、構造限定表明を、検証対象ファイルが含む再帰データの構造とは関係しない表明と合成し、合成した表明を含む検証用ファイルを生成する。次いで、表明検証実行手段４は、検証用ファイルを解析して、合成した表明に基づいてプログラムに不具合が存在するか否かを検証する。
【００９７】
従って、最小構成のプログラム検証装置によれば、表明に基づいて再帰データを扱うプログラムを静的に検証することができる。
【００９８】
なお、本実施形態では、以下の（１）〜（５）に示すようなプログラム検証装置の特徴的構成が示されている。
【００９９】
（１）プログラム検証装置（例えば、情報処理装置１００によって実現される。）は、再帰データを構成する要素数を限定せずに再帰データの構造を表現した情報を含む仕様（例えば、仕様５１）を読み込み、再帰データに含まれる要素の数を所定数に限定すると仮定した場合の再帰データの構造を示す構造限定情報（例えば、構造限定情報６１）を生成する構造限定情報生成手段（例えば、構造限定情報生成モジュール１２０によって実現される。）と、構造限定情報を、表明を用いた検証を実行可能な記法に変換した構造限定表明（例えば、構造限定表明９１）を生成する構造限定表明生成手段（例えば、構造限定表明生成モジュール１３０によって実現される。）と、構造限定表明を、検証対象ファイル（例えば、検証対象ファイルの内容７１）が含む再帰データの構造とは関係しない表明と合成し、合成した表明を含む検証用ファイル（例えば、検証用ファイルの内容１００１に示される）を生成する検証用ファイル生成手段と、検証用ファイルを解析して、合成した表明に基づいてプログラムに不具合が存在するか否かを検証する表明検証実行手段（例えば、表明検証実行モジュール１５０によって実現される。）とを備えたことを特徴とする。
【０１００】
（２）プログラム検証装置において、構造限定情報生成手段は、再帰データの要素を、０から所定数までの個数にそれぞれ限定した複数の構造限定情報を生成し、構造限定表明生成手段は、生成した複数の構造限定情報を、表明検証手段が検証可能な記法に変換した複数の構造限定表明を生成し、検証用ファイル生成手段は、生成した複数の構造限定表明を、検証対象ファイルと合成して、複数の検証用ファイルを生成するように構成されていてもよい。
【０１０１】
（３）プログラム検証装置は、構造限定表明を再帰データの構造を示す情報を含む仕様と同じ記法で表現した構造限定仕様（例えば、構造限定仕様１１０１）を生成する構造限定仕様生成手段（例えば、構造限定仕様生成モジュール３８０によって実現される。）と、構造限定仕様を仕様に基づいて不具合が存在するか否かを検証する構造限定仕様検証手段（例えば、構造限定仕様検証モジュール３９０によって実現される。）とを備えるように構成されていてもよい。
【０１０２】
（４）プログラム検証装置において、構造限定情報生成手段は、再帰データを構成する要素および要素間の連結構造を示す構造限定情報を生成するように構成されていてもよい。
【０１０３】
（５）プログラム検証装置において、構造限定表明生成手段は、予め定められた構造を補足する情報（例えば、構造補足情報８１）に基づいて、構造限定情報を表明検証実行手段が検証可能な記法に変換した構造限定表明を生成するように構成されていてもよい。
【０１０４】
上記の実施形態の一部又は全部は、以下の付記のようにも記載され得るが、以下には限られない。
【０１０５】
（付記１）再帰データを構成する要素数を限定せずに該再帰データの構造を表現した情報を含む仕様を読み込み、該再帰データに含まれる要素の数を所定数に限定すると仮定した場合の該再帰データの構造を示す構造限定情報を生成する構造限定情報生成手段と、前記構造限定情報を、表明を用いた検証を実行可能な記法に変換した構造限定表明を生成する構造限定表明生成手段と、前記構造限定表明を、検証対象ファイルが含む前記再帰データの構造とは関係しない表明と合成し、合成した表明を含む検証用ファイルを生成する検証用ファイル生成手段と、前記検証用ファイルを解析して、合成した前記表明に基づいてプログラムに不具合が存在するか否かを検証する表明検証実行手段とを備えたことを特徴とするプログラム検証装置。
【０１０６】
（付記２）構造限定情報生成手段は、再帰データの要素を、０から所定数までの個数にそれぞれ限定した複数の構造限定情報を生成し、構造限定表明生成手段は、生成した前記複数の構造限定情報を、表明検証実行手段が検証可能な記法に変換した複数の構造限定表明を生成し、検証用ファイル生成手段は、生成した前記複数の構造限定表明を、検証対象ファイルと合成して、複数の検証用ファイルを生成する付記１記載のプログラム検証装置。
【０１０７】
（付記３）構造限定表明を再帰データの構造を示す情報を含む仕様と同じ記法で表現した構造限定仕様を生成する構造限定仕様生成手段と、前記構造限定仕様を前記仕様に基づいて不具合が存在するか否かを検証する構造限定仕様検証手段とを備えた付記１又は付記２記載のプログラム検証装置。
【０１０８】
（付記４）構造限定情報生成手段は、再帰データを構成する要素および要素間の連結構造を示す構造限定情報を生成する付記１から付記３のうちのいずれか記載のプログラム検証装置。
【０１０９】
（付記５）構造限定表明生成手段は、予め定められた構造を補足する情報に基づいて、構造限定情報を表明検証実行手段が検証可能な記法に変換した構造限定表明を生成する付記１から付記４のうちのいずれかに記載のプログラム検証装置。
【０１１０】
（付記６）再帰データの構造に関する情報を含む仕様を読み込み、該再帰データに含まれる要素の数を所定数に限定すると仮定した場合の該再帰データの構造を示す構造限定情報を生成する構造限定情報生成ステップと、前記構造限定情報を、表明を用いた検証を実行可能な記法に変換した構造限定表明を生成する構造限定表明生成ステップと、前記構造限定表明を、検証対象ファイルが含む前記再帰データの構造とは関係しない表明と合成し、合成した表明を含む検証用ファイルを生成する検証用ファイル生成ステップと、前記検証用ファイルを解析して、合成した表明に基づいてプログラムに不具合が存在するか否かを検証する表明検証実行ステップとを含むことを特徴とするプログラム検証方法。
【０１１１】
（付記７）構造限定表明を再帰データの構造を示す情報を含む仕様と同じ記法で表現した構造限定仕様を生成する構造限定仕様生成ステップと、前記構造限定仕様を前記仕様に基づいて不具合が存在するか否かを検証する構造限定仕様検証ステップとを含む付記６記載のプログラム検証方法。
【０１１２】
（付記８）コンピュータに、再帰データの構造に関する情報を含む仕様を読み込み、該再帰データに含まれる要素の数を所定数に限定すると仮定した場合の該再帰データの構造を示す構造限定情報を生成する構造限定情報生成処理と、前記構造限定情報を、表明を用いた検証を実行可能な記法に変換した構造限定表明を生成する構造限定表明生成処理と、前記構造限定表明を、検証対象ファイルが含む前記再帰データの構造とは関係しない表明と合成し、合成した表明を含む検証用ファイルを生成する検証用ファイル生成処理と、前記検証用ファイルを解析して、合成した表明に基づいてプログラムに不具合が存在するか否かを検証する表明検証実行処理とを実行させるためのプログラム検証用プログラム。
【０１１３】
（付記９）コンピュータに、構造限定表明を再帰データの構造を示す情報を含む仕様と同じ記法で表現した構造限定仕様を生成する構造限定仕様生成処理と、前記構造限定仕様を前記仕様に基づいて不具合が存在するか否かを検証する構造限定仕様検証処理とを実行させる付記８記載のプログラム検証用プログラム。
【産業上の利用可能性】
【０１１４】
本発明は、プログラムを検証する用途に適用可能である。
【符号の説明】
【０１１５】
１  構造限定情報生成手段
２  構造限定表明生成手段
３  検証用ファイル生成手段
４  表明検証実行手段
【図１】
0005589528.tif 000002
【図２】
0005589528.tif 000003
【図３】
0005589528.tif 000004
【図４】
0005589528.tif 000005
【図５】
0005589528.tif 000006
【図６】
0005589528.tif 000007
【図７】
0005589528.tif 000008
【図８】
0005589528.tif 000009
【図９】
0005589528.tif 000010
【図１０】
0005589528.tif 000011
【図１１】
0005589528.tif 000012
【図１２】
0005589528.tif 000013
【図１３】
0005589528.tif 000014
【図１４】
0005589528.tif 000015