(57)【要約】【課題】検証したいプログラムが使っているモジュールについて、そのモジュールの外部公開関数の定義が提供されていない場合でも、生成されるスタブモジュールを用いることにより、該モジュールの関数を呼び出すプログラムを静的に検証できること。【解決手段】モジュール外部仕様解析部は、関数宣言及びアサーションが記されたモジュール外部仕様を読み込む。関数宣言解析部は、モジュール外部仕様に記された関数宣言の解析を行い、その解析の結果を表す関数解析情報を生成する。アサーション解析部は、モジュール外部仕様に記されたアサーションの解析を行い、その解析の結果を表すアサーション解析情報を生成する。スタブモジュール生成部は、関数解析情報とアサーション解析情報とに基づいて、スロット定義とスタブ関数定義とを表すスタブモジュールを生成する。【選択図】図１
2010079525.tif 000002
【特許請求の範囲】
【請求項１】
関数宣言及びアサーションが記されたモジュール外部仕様を読み込むモジュール外部仕様解析部と、
前記モジュール外部仕様に記された前記関数宣言の解析を行い、その解析の結果を表す関数解析情報を生成する関数宣言解析部と、
前記モジュール外部仕様に記された前記アサーションの解析を行い、その解析の結果を表すアサーション解析情報を生成するアサーション解析部と、
前記関数解析情報と前記アサーション解析情報とに基づいて、スロット定義とスタブ関数定義とを表すスタブモジュールを生成するスタブモジュール生成部と、
を具備するプログラム検証支援装置。
【請求項２】
前記関数解析情報は、関数名と関数型とを対応付ける関数情報と、前記関数名と序数と引数名と引数型とを対応付ける引数情報と、を含み、
請求項１に記載のプログラム検証支援装置。
【請求項３】
前記スタブモジュールは、前記スロット定義を表すスロット定義部と、前記スタブ関数定義を表すスタブ関数定義部と、を含み、
前記スタブモジュール生成部は、
照会関数ごとに、
前記関数情報と前記引数情報とを参照して照会関数に引数があるか否かを判定し、
引数がない場合、戻り値スロットを前記スロット定義部として設定し、
引数がある場合、引数スロット配列、戻り値スロット配列を前記スロット定義部として設定し、
前記関数情報の関数ごとに、
前記アサーションと前記関数情報とを前記スタブ関数定義部として設定し、
その関数が照会関数である場合、前記引数情報に対応した引数スロットの値を調べ、引数値の組と引数スロットの値の組が合致する戻り値スロットの値を取得して戻り値に設定し、
その関数が照会関数ではない場合、事前変数の定義を出力し、依存されるアサーションを優先して、スロットへ引数の値と事前変数の値の組を設定する、
請求項２に記載のプログラム検証支援装置。
【請求項４】
前記アサーション解析情報は、アサーション情報と、事前変数情報と、照会関数情報と、アサーション依存情報と、を含み、
前記アサーション解析部は、
前記モジュール外部仕様に記された複数の前記アサーションの各々について、
前記アサーションの解析の結果として、前記アサーションを識別するＩＤと、前記アサーションが制約する関数を表す前記関数名と、前記アサーションが事前条件・事後条件・不変条件のいずれであるかを表す制約区分と、前記アサーションの元の制約式と、を前記アサーション情報に設定し、
前記元の制約式を整形するための整形ルールに従って整形後の制約式を生成し、前記アサーション情報に設定し、
前記整形後の制約式における関数実行前の式を前記事前変数情報に設定し、前記関数実行前の式を事前変数に置換し、
同じ関数を制約する前記アサーション情報について、
前記元の制約式に出現する照会関数を前記照会関数情報に設定し、
対象となるアサーション情報が他のアサーション情報に依存するか否かを調べ、依存する場合、依存されるアサーション情報の前記ＩＤを依存ＩＤとして前記対象となるアサーション情報に設定し、
前記整形後の制約式が設定されている前記アサーション情報について、
前記関数名と前記依存ＩＤと前記ＩＤとを対応付ける情報を前記アサーション依存情報に設定する、
請求項２に記載のプログラム検証支援装置。
【請求項５】
前記スタブモジュールは、前記スロット定義を表すスロット定義部と、前記スタブ関数定義を表すスタブ関数定義部と、を含み、
前記スタブモジュール生成部は、
前記照会関数情報の照会関数ごとに、
前記関数情報と前記引数情報とを参照して照会関数に引数があるか否かを判定し、
引数がない場合、戻り値スロットを前記スロット定義部として設定し、
引数がある場合、引数スロット配列、戻り値スロット配列を前記スロット定義部として設定し、
前記関数情報の関数ごとに、
前記アサーションと前記関数情報とを前記スタブ関数定義部として設定し、
その関数が前記照会関数情報の照会関数に設定されているか否かを判定し、
その関数が照会関数である場合、前記引数情報に対応した引数スロットの値を調べ、引数値の組と引数スロットの値の組が合致する戻り値スロットの値を取得して戻り値に設定し、
その関数が照会関数ではない場合、前記事前変数情報ごとに事前変数の定義を出力し、前記アサーション依存情報において依存されるアサーションを優先して、スロットへ引数の値と事前変数の値の組を設定する、
請求項４に記載のプログラム検証支援装置。
【請求項６】
前記スタブモジュールは、検証ツール固有部を更に含み、
前記スタブモジュール生成部は、
検証ツールが対象とするプログラミング言語に依存した定数・変数・関数の宣言や定義を前記検証ツール固有部に設定する、
請求項３又は５に記載のプログラム検証支援装置。
【請求項７】
前記モジュール外部仕様が格納された記憶装置と、
前記モジュール外部仕様解析部は、
実行指示に応じて、前記記憶装置から前記モジュール外部仕様を読み込む、
請求項１〜６のいずれかに記載のプログラム検証支援装置。
【請求項８】
関数宣言及びアサーションが記されたモジュール外部仕様を読み込むステップと、
前記モジュール外部仕様に記された前記関数宣言の解析を行い、その解析の結果を表す関数解析情報を生成するステップと、
前記モジュール外部仕様に記された前記アサーションの解析を行い、その解析の結果を表すアサーション解析情報を生成するステップと、
前記関数解析情報と前記アサーション解析情報とに基づいて、スロット定義とスタブ関数定義とを表すスタブモジュールを生成するステップと、
を具備するプログラム検証支援方法。
【請求項９】
前記関数解析情報は、関数名と関数型とを対応付ける関数情報と、前記関数名と序数と引数名と引数型とを対応付ける引数情報と、を含み、
請求項８に記載のプログラム検証支援方法。
【請求項１０】
前記スタブモジュールは、前記スロット定義を表すスロット定義部と、前記スタブ関数定義を表すスタブ関数定義部と、を含み、
前記スタブモジュールを生成するステップは、
照会関数ごとに、
前記関数情報と前記引数情報とを参照して照会関数に引数があるか否かを判定するステップと、
引数がない場合、戻り値スロットを前記スロット定義部として設定するステップと、
引数がある場合、引数スロット配列、戻り値スロット配列を前記スロット定義部として設定するステップと、
前記関数情報の関数ごとに、
前記アサーションと前記関数情報とを前記スタブ関数定義部として設定するステップと、
その関数が照会関数である場合、前記引数情報に対応した引数スロットの値を調べ、引数値の組と引数スロットの値の組が合致する戻り値スロットの値を取得して戻り値に設定するステップと、
その関数が照会関数ではない場合、事前変数の定義を出力し、依存されるアサーションを優先して、スロットへ引数の値と事前変数の値の組を設定するステップと、
を含む請求項９に記載のプログラム検証支援方法。
【請求項１１】
前記アサーション解析情報は、アサーション情報と、事前変数情報と、照会関数情報と、アサーション依存情報と、を含み、
前記アサーション解析情報を生成するステップは、
前記モジュール外部仕様に記された複数の前記アサーションの各々について、
前記アサーションの解析の結果として、前記アサーションを識別するＩＤと、前記アサーションが制約する関数を表す前記関数名と、前記アサーションが事前条件・事後条件・不変条件のいずれであるかを表す制約区分と、前記アサーションの元の制約式と、を前記アサーション情報に設定するステップと、
前記元の制約式を整形するための整形ルールに従って整形後の制約式を生成し、前記アサーション情報に設定するステップと、
前記整形後の制約式における関数実行前の式を前記事前変数情報に設定し、前記関数実行前の式を事前変数に置換するステップと、
同じ関数を制約する前記アサーション情報について、
前記元の制約式に出現する照会関数を前記照会関数情報に設定するステップと、
対象となるアサーション情報が他のアサーション情報に依存するか否かを調べ、依存する場合、依存されるアサーション情報の前記ＩＤを依存ＩＤとして前記対象となるアサーション情報に設定するステップと、
前記整形後の制約式が設定されている前記アサーション情報について、
前記関数名と前記依存ＩＤと前記ＩＤとを対応付ける情報を前記アサーション依存情報に設定するステップと、
を含む請求項９に記載のプログラム検証支援方法。
【請求項１２】
前記スタブモジュールは、前記スロット定義を表すスロット定義部と、前記スタブ関数定義を表すスタブ関数定義部と、を含み、
前記スタブモジュールを生成するステップは、
前記照会関数情報の照会関数ごとに、
前記関数情報と前記引数情報とを参照して照会関数に引数があるか否かを判定するステップと、
引数がない場合、戻り値スロットを前記スロット定義部として設定するステップと、
引数がある場合、引数スロット配列、戻り値スロット配列を前記スロット定義部として設定するステップと、
前記関数情報の関数ごとに、
前記アサーションと前記関数情報とを前記スタブ関数定義部として設定するステップと、
その関数が前記照会関数情報の照会関数に設定されているか否かを判定するステップと、
その関数が照会関数である場合、前記引数情報に対応した引数スロットの値を調べ、引数値の組と引数スロットの値の組が合致する戻り値スロットの値を取得して戻り値に設定するステップと、
その関数が照会関数ではない場合、前記事前変数情報ごとに事前変数の定義を出力し、前記アサーション依存情報において依存されるアサーションを優先して、スロットへ引数の値と事前変数の値の組を設定するステップと、
を含む請求項１１に記載のプログラム検証支援方法。
【請求項１３】
前記スタブモジュールは、検証ツール固有部を更に含み、
前記スタブモジュールを生成するステップは、
検証ツールが対象とするプログラミング言語に依存した定数・変数・関数の宣言や定義を前記検証ツール固有部に設定するステップ、
を更に含む請求項１０又は１２に記載のプログラム検証支援方法。
【請求項１４】
記憶装置には、前記モジュール外部仕様が格納され、
前記モジュール外部仕様を読み込むステップは、
実行指示に応じて、前記記憶装置から前記モジュール外部仕様を読み込むステップ、
を含む請求項８〜１３のいずれかに記載のプログラム検証支援方法。
【請求項１５】
請求項８〜１４のいずれかに記載のプログラム検証支援方法の各ステップをコンピュータに実行させるコンピュータプログラムであるプログラム検証支援プログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本発明は、静的なプログラムを検証するプログラム検証支援装置、プログラム検証支援方法、及び、プログラム検証支援プログラムに関する。
【背景技術】
【０００２】
アサーションを用いてプログラムの品質を確保する方法が、非特許文献１に記載されている。この非特許文献１の著者は、記述した方法を実現するための言語及びコンパイラＥｉｆｆｅｌを実装・商品化している。この方法では、関数の実行前に満足されるべき条件である事前条件と、関数が実行後に満足すべき条件である事後条件と、モジュール内の全ての関数の実行前に満足されるべきであり、かつ実行後に満足すべき条件である不変条件とを、モジュールが外部に公開している変数、照会関数（副作用のない関数、モジュールの状態を変更することなく状態を照会可能とする関数）及び関数の引数と戻り値を用いた論理式で表現する。一般に、このような事前条件・事後条件・不変条件などプログラムのある時点で成立すべき条件の記述をアサーション（表明）と呼ぶ。
【０００３】
アサーションはモジュールや関数を制約するものである。図９Ａ、Ｂは、スタックについてのアサーションをソースコードのコメントとして記述した例である。図９Ａ、Ｂでは、非特許文献１のＥｉｆｆｅｌ言語の記法ではなく、一般に普及しているＣ言語の表記を用いている。スタックは先入れ後出し方式のキューであり、関数ｐｕｓｈによりアイテムをキューのトップに追加し、関数ｐｏｐによってアイテムをキューのトップから取り除く。また、副作用のない関数として、スタック内の指定位置に登録されたアイテムを返す関数ｐｅｅｋや、スタックにその時登録されているアイテム数を返す関数ｃｏｕｎｔが用いられる。図９Ａ、Ｂの4行目の「ｃｏｕｎｔ（）＝＝￥ｏｌｄ（ｃｏｕｎｔ（）＋１）」は、関数ｐｏｐの実行後にスタックのアイテム数が実行前のアイテム数よりも１だけ増えることを表し、５行目の「ｉｔｅｍ＝＝ｐｅｅｋ（ｃｏｕｎｔ（）−１）」は、関数ｐｏｐの実行後にスタックのアイテム数より１だけ少ない位置にあるアイテムは、関数ｐｏｐの引数として与えたアイテムに等しいことを表している。
【０００４】
ソフトウェア開発者は、このようなアサーションをモジュールや関数の外部仕様として定め、これに適合するようにソースコードを記述する。ソースコードがアサーションに適合していることは、プログラム検証ツールによって調べることができる。
【０００５】
例えば、Ｃａｄｕｃｅｕｓ（Ｃ言語向け）やＥＳＣ／Ｊａｖａ（登録商標）２（Ｊａｖａ（登録商標）言語向け）などの検証ツールは、ソースコードを静的解析して、事後条件から逆にソースコード（関数定義中の実行文）を辿り、定理証明手法によって関数の実行後に事後条件を満たすような関数の入り口における条件（最弱事前条件）を計算する。その結果、ソフトウェア開発者が定義した事前条件が満たされると最弱事前条件も必ず満たされるのであれば、ソースコードがアサーションに適合していると判断する。
【０００６】
ＣＢＭＣ（Ｃ言語向け）などの検証ツールは、ソースコードを解析し、実行箇所と変数の値の組合せを状態とする有限状態遷移モデルを作成し、モデル検査手法によって事前条件を満たす状態から遷移可能な状態を網羅的に探索する。その結果、関数の実行終了時の状態において事後条件が満たされていれば、ソースコードがアサーションに適合していると判断する。
【０００７】
【非特許文献１】バートランド・メイヤー（Ｂｅｒｔｒａｎｄ  Ｍｅｙｅｒ）．オブジェクト指向入門  第２版  原則・コンセプト．（翔泳社  ２００７）
【発明の開示】
【発明が解決しようとする課題】
【０００８】
しかし、これらの従来技術を、ソフトウェア開発に適用するには、次の問題があった。
【０００９】
定理証明やモデル検査に基づく静的なプログラム検証ツールでは、関数定義を元に最弱事前条件の計算や有限状態遷移モデルの作成を行うことにより検証している。このため、モジュールの外部公開関数の定義が与えられていない場合に、該モジュールの関数を呼び出すプログラムの検証ができない。
【００１０】
本発明の課題は、以上の問題点を解決するプログラム検証支援装置、プログラム検証支援方法、及び、プログラム検証支援プログラムを提供することにある。
【課題を解決するための手段】
【００１１】
本発明のプログラム検証支援装置は、モジュール外部仕様解析部と、関数宣言解析部と、アサーション解析部と、スタブモジュール生成部と、を具備している。モジュール外部仕様解析部は、関数宣言及びアサーションが記されたモジュール外部仕様を読み込む。関数宣言解析部は、モジュール外部仕様に記された関数宣言の解析を行い、その解析の結果を表す関数解析情報を生成する。アサーション解析部は、モジュール外部仕様に記されたアサーションの解析を行い、その解析の結果を表すアサーション解析情報を生成する。スタブモジュール生成部は、関数解析情報とアサーション解析情報とに基づいて、スロット定義とスタブ関数定義とを表すスタブモジュールを生成する。
【発明の効果】
【００１２】
本発明のプログラム検証支援装置によれば、検証したいプログラムが使っているモジュールについて、そのモジュールの外部公開関数の定義が提供されていない場合でも、生成されるスタブモジュールを用いることにより、該モジュールの関数を呼び出すプログラムを静的に検証できる。
【発明を実施するための最良の形態】
【００１３】
以下に添付図面を参照して、本発明の実施形態によるプログラム検証支援装置について詳細に説明する。
【００１４】
図１は、本発明の実施形態によるプログラム検証支援装置の構成を示している。そのプログラム検証支援装置は、コンピュータであり、入出力装置１と、処理装置２と、記憶装置３と、を具備している。入出力装置１は、入力装置と出力装置とを含み、入力装置としてはキーボードやポインティングデバイスが例示され、出力装置としてはディスプレイが例示される。処理装置２としては、ＣＰＵが例示され、記憶装置３としては、ハードディスクやメモリ等が例示される。
【００１５】
記憶装置３には、処理装置２に実行させるためのコンピュータプログラムであるプログラム検証支援プログラムが格納されている。処理装置２は、上記コンピュータが起動するときなどにプログラム検証支援プログラムを記憶装置３から読み取って実行する。そのプログラム検証支援プログラムは、制御部４と、モジュール外部仕様解析部５と、関数宣言解析部６と、アサーション解析部７と、スタブモジュール生成部８と、を含んでいる。
【００１６】
記憶装置３には、関数宣言及びアサーションが記されたモジュール外部仕様９が格納されている。また、記憶装置３には、モジュール外部仕様９を基に生成されるスタブモジュール１０が格納される。
【００１７】
図２は、本発明の実施形態によるプログラム検証支援装置の動作として、プログラム検証支援方法を示すフローチャートである。
【００１８】
まず、制御部４は、入出力装置１からの実行指示に応じて、モジュール外部仕様解析部５に処理実行指示を行う。モジュール外部仕様解析部５は、処理実行指示に応じて、記憶装置３からモジュール外部仕様９を読み込む（図２のステップＳ２０１）。このとき、モジュール外部仕様解析部５は、関数宣言解析部６に関数解析情報生成指示を行い、アサーション解析部７にアサーション解析情報生成指示を行う。
【００１９】
関数宣言解析部６は、関数解析情報生成指示に応じて、モジュール外部仕様９に記された関数宣言の解析を行い、その解析の結果として、関数解析情報３０（図３参照）を生成する（図２のステップＳ２０２）。
【００２０】
アサーション解析部７は、アサーション解析情報生成指示に応じて、モジュール外部仕様９に記されたアサーションの解析を行い、その解析の結果として、アサーション解析情報４０（図４参照）を生成する（図２のステップＳ２０３）。
【００２１】
次に、制御部４は、スタブモジュール生成部８にスタブモジュール生成指示を行う。スタブモジュール生成部８は、スタブモジュール生成指示に応じて、関数解析情報３０とアサーション解析情報４０とに基づいて、スロット定義とスタブ関数定義とを表すスタブモジュール１０を生成する（図２のステップＳ２０４）。
【００２２】
図３は、関数解析情報３０を示している。関数解析情報３０は、関数情報３１と、引数情報３２と、を含んでいる。
【００２３】
関数情報３１は、関数名と関数型とを対応付ける情報である。例えば、関数情報３１は、関数名“ｐｕｓｈ”と関数型“ｖｏｉｄ＠”とを対応付ける。関数情報３１は、関数名“ｐｏｐ”と関数型“ｖｏｉｄ＊＠”とを対応付ける。関数情報３１は、関数名“ｐｅｅｋ”と関数型“ｖｏｉｄ＊＠”とを対応付ける。関数情報３１は、関数名“ｃｏｕｎｔ”と関数型“ｕｎｓｉｇｎｅｄ  ｉｎｔ＠”とを対応付ける。ここで、関数型の＠は関数名が挿入される位置を示している。
【００２４】
引数情報３２は、関数名と序数と引数名と引数型とを対応付ける情報である。例えば、引数情報３２は、関数名“ｐｕｓｈ”と序数“１”と引数名“ｉｔｅｍ”と引数型“ｖｏｉｄ＊＠”とを対応付ける。引数情報３２は、関数名“ｐｅｅｋ”と序数“１”と引数名“ｉｎｄｅｘ”と引数型“ｕｎｓｉｇｎｅｄ  ｉｎｔ＠”とを対応付ける。ここで、引数型の＠は引数名が挿入される位置を示している。
【００２５】
図４は、アサーション解析情報４０を示している。アサーション解析情報４０は、アサーション情報４１と、事前変数情報４２と、照会関数情報４３と、アサーション依存情報４４と、整形ルール４５と、を含んでいる。
【００２６】
アサーション情報４１は、アサーションの解析の結果として、アサーションを識別するＩＤと、アサーションに依存するアサーションを識別する依存ＩＤと、アサーションが制約する関数を表す関数名と、アサーションが事前条件・事後条件・不変条件のいずれであるかを表す制約区分と、アサーションの元の制約式と、アサーションの整形後の制約式とを対応付ける情報である。例えば、アサーション情報４１は、ＩＤ“１”と、関数名“ｐｕｓｈ”と、制約区分“事前”と、元の制約式“ｉｔｅｍ＝ＮＵＬＬ”とを対応付ける。アサーション情報４１は、ＩＤ“２”と、関数名“ｐｕｓｈ”と、制約区分“事後”と、元の制約式“ｃｏｕｎｔ（）＝＝￥ｏｌｄ（ｃｏｕｎｔ（）＋１）”と、整形後の制約式“ｃｏｕｎｔ（）＝＝＿＿ｏｌｄ＿１”とを対応付ける。アサーション情報４１は、ＩＤ“３”と、依存ＩＤ“２”と、関数名“ｐｕｓｈ”と、制約区分“事後”と、元の制約式“ｉｔｅｍ＝ｐｅｅｋ（ｃｏｕｎｔ（）−１）”と、整形後の制約式“ｐｅｅｋ（ｃｏｕｎｔ（）−１）＝＝ｉｔｅｍ”とを対応付ける。アサーション情報４１は、ＩＤ“４”と、関数名“ｐｏｐ”と、制約区分“事前”と、元の制約式“０＜ｃｏｕｎｔ（）”とを対応付ける。アサーション情報４１は、ＩＤ“５”と、依存ＩＤ“６”と、関数名“ｐｏｐ”と、制約区分“事後”と、元の制約式“ｐｅｅｋ（ｃｏｕｎｔ（））＝＝￥ｒｅｓｕｌｔ”と、整形後の制約式“￥ｒｅｓｕｌｔ＝＝ｐｅｅｋ（ｃｏｕｎｔ（））”とを対応付ける。アサーション情報４１は、ＩＤ“６”と、関数名“ｐｏｐ”と、制約区分“事後”と、元の制約式“￥ｏｌｄ（ｃｏｕｎｔ（））＝＝ｃｏｕｎｔ（）＋１”と、整形後の制約式“ｃｏｕｎｔ（）＝＝＿＿ｏｌｄ＿２−１”とを対応付ける。アサーション情報４１は、ＩＤ“７”と、関数名“ｐｅｅｋ”と、制約区分“事前”と、元の制約式“ｉｎｄｅｘ＜ｃｏｕｎｔ（）”とを対応付ける。アサーション情報４１は、ＩＤ“８”と、関数名“ｐｅｅｋ”と、制約区分“事後”と、元の制約式“￥ｒｅｓｕｌｔ＝＝ＮＵＬＬ”とを対応付ける。
【００２７】
事前変数情報４２は、スタブモジュール１０において関数実行前の式の値を一時的に保持するための事前変数を管理し、関数（関数名）と参照ＩＤと事前変数名と事前変数型と事前変数値とを対応付ける情報である。例えば、事前変数情報４２は、関数“ｐｕｓｈ”と参照ＩＤ“２”と事前変数名“＿＿ｏｌｄ＿１”と事前変数型“ｕｎｓｉｇｎｅｄ  ｉｎｔ＠”と事前変数値“ｃｏｕｎｔ（）＋１”とを対応付ける。更に、事前変数情報４２は、関数“ｐｏｐ”と参照ＩＤ“６”と事前変数名“＿＿ｏｌｄ＿２”と事前変数型“ｕｎｓｉｇｎｅｄ  ｉｎｔ＠”と事前変数値“ｃｏｕｎｔ（）”とを対応付ける。ここで、事前変数型の＠は事前変数名が挿入される位置を示している。
【００２８】
照会関数情報４３は、照会関数名を表す情報である。例えば、照会関数情報４３は、照会関数名“ｐｅｅｋ”を表している。更に、照会関数情報４３は、照会関数名“ｃｏｕｎｔ”を表している。
【００２９】
アサーション依存情報４４は、アサーション情報の関数（関数名）と依存ＩＤとＩＤとを対応付ける情報である。ここで、アサーション情報は事後条件のみとする。例えば、アサーション依存情報４４は、関数“ｐｕｓｈ”と依存ＩＤ“２”とＩＤ“３”とを対応付ける。更に、アサーション依存情報４４は、関数“ｐｏｐ”と依存ＩＤ“６”とＩＤ“５”とを対応付ける。更に、アサーション依存情報４４は、関数“ｐｅｅｋ”とＩＤ“８”とを対応付ける。
【００３０】
整形ルール４５は、ＩＤと、元の制約式を整形後の制約式に整形するためのルールと、を対応付ける情報である。例えば、整形ルール４５は、ＩＤ“Ｆ１”と、ルール“等値演算子（左辺と右辺が等しい）を持つ事後条件のみを整形する。”と、を対応付ける。更に、整形ルール４５は、ＩＤ“Ｆ２”と、ルール“関数実行前の式は等値演算子の右辺に移す。”と、を対応付ける。更に、整形ルール４５は、ＩＤ“Ｆ３”と、ルール“戻り値は等値演算子の左辺に移す。このとき、戻り値以外を右辺に移す。”と、を対応付ける。更に、整形ルール４５は、ＩＤ“Ｆ４”と、ルール“照会関数は等値演算子の左辺に移す。このとき、照会関数以外を右辺に移す。”と、を対応付ける。ここで、ＩＤ“Ｆ１”、“Ｆ２”、“Ｆ３”、“Ｆ４”はこの順に優先される。
【００３１】
図６は、図１のスタブモジュール１０として、スタブモジュール６０を示している。スタブモジュール６０は、検証ツール固有部６１と、上記のスロット定義を表すスロット定義部６２と、上記のスタブ関数定義を表すスタブ関数定義部６３と、を含んでいる。
【００３２】
アサーションを解析する処理（ステップＳ２０３）については、図４と図５を参照して、より詳細に説明する。図５は、図２のアサーションを解析する処理（ステップＳ２０３）を示すフローチャートである。
【００３３】
モジュール外部仕様９には複数のアサーションが記されているものとする。まず、アサーション解析部７は、モジュール外部仕様９に記された複数のアサーションの各々について処理を繰り返す（図５のステップＳ５１〜Ｓ５５）。そこで、アサーションの解析の結果として、アサーションを識別するＩＤと、アサーションが制約する関数を表す関数名と、アサーションが事前条件・事後条件・不変条件のいずれであるかを表す制約区分と、アサーションの元の制約式と、をアサーション情報４１に設定する（図５のステップＳ５２）。次に、整形ルール４５に従って元の制約式を変換して整形後の制約式を生成し、アサーション情報４１に設定する（図５のステップＳ５３）。整形後の制約式における関数実行前の式を事前変数情報４２に設定し、代わりに整形後の制約式の関数実行前の式を事前変数に置換する（図５のステップＳ５４）。
【００３４】
次に、アサーション解析部７は、同じ関数を制約するアサーション情報４１（選択アサーション情報４１）について処理を繰り返す（図５のステップＳ５６〜Ｓ５９）。そこで、上記選択アサーション情報４１の元の制約式に出現する照会関数を照会関数情報４３に設定する（図５のステップＳ５７）。次に、アサーション依存判定ルール１１１（図１１参照）に従って、選択アサーション情報４１のうちの、対象となるアサーション情報４１が他のアサーション情報４１に依存するか否かを調べ、依存する場合、依存されるアサーション情報４１のＩＤを依存ＩＤとして上記対象となるアサーション情報４１に設定する（図５のステップＳ５８）。
【００３５】
最後に、アサーション解析部７は、整形後の制約式が設定されているアサーション情報４１について、関数名と依存ＩＤとＩＤとを対応付ける情報をアサーション依存情報４４に設定する（図５のステップＳ６０）。
【００３６】
スタブモジュールを生成する処理（ステップＳ２０４）については、図３、４、６、７Ａ、７Ｂ、８を参照して、より詳細に説明する。図７Ａは、戻り値スロット７１の例を示している。図７Ｂは、引数スロット配列、戻り値スロット配列７２の例を示している。図８は、図２のスタブモジュールを生成する処理（ステップＳ２０４）を示すフローチャートである。
【００３７】
スタブモジュール生成部８は、ファイルやメモリ上の構造体など検証ツールが処理できる形式でスタブモジュール６０を生成する。まず、検証ツールが対象とするプログラミング言語に依存した定数・変数・関数の宣言や定義を検証ツール固有部６１に設定する（図８のステップＳ８０１）。
【００３８】
次に、スタブモジュール生成部８は、照会関数情報４３の照会関数ごとに、関数情報３１と引数情報３２とを参照して照会関数に引数があるかを判定する。引数がない場合、戻り値スロット７１をスロット定義部６２として設定する。引数がある場合、引数スロット配列、戻り値スロット配列７２をスロット定義部６２として設定する（図８のステップＳ８０２）。
【００３９】
スタブモジュール生成部８は、関数情報３１の関数ごとに処理を繰り返す（図８のステップＳ８０３〜Ｓ８１１）。そこで、アサーション情報４１と関数情報３１と引数情報３２とを用いて、アサーションと関数情報３１とをスタブ関数定義部６３として設定する（図８のステップＳ８０４）。その関数が照会関数情報４３の照会関数に設定されているか否かを判定する（図８のステップＳ８０５）。
【００４０】
その関数が照会関数である場合（ステップＳ８０５−ＹＥＳ）、スタブモジュール生成部８は、引数情報３２に対応した引数スロットの値を調べ、引数値の組と引数スロットの値の組が合致する戻り値スロットの値を取得して戻り値に設定し（図８のステップＳ８０６）、関数について上記の処理を繰り返す場合、復帰処理（図８のステップ８０７）としてステップＳ８０３を実行し、上記の処理を繰り返さない場合、ステップＳ８１１の実行として処理を終了する。
【００４１】
その関数が照会関数ではない場合（ステップＳ８０５−ＮＯ）、事前変数情報４２ごとに事前変数の定義を設定し（図８のステップＳ８０８）、アサーション依存情報４４において依存されるアサーションを優先して、スロットへ引数の値と事前変数の値の組を設定し（図８のステップＳ８０９）、関数について上記の処理を繰り返す場合、復帰処理（図８のステップＳ８１０）としてステップＳ８０３を実行し、上記の処理を繰り返さない場合、ステップＳ８１１の実行として処理を終了する。
【００４２】
次に、手続き型言語であるＣのソースコードの具体例を交えて、本実施形態の動作を詳しく説明する。図９Ａは、モジュール外部仕様９の例９１を示し、図９Ｂは、アサーション記法の例９２を示している。図１１は、アサーション依存判定ルール１１１の例を示している。図１２Ａ、１２Ｂは、図６のスタブモジュール６０として、スタブモジュール１２０の例を示している。
【００４３】
モジュール外部仕様９（例９１）では、アサーション記法（例９２）に従って、複数の事前・事後条件などがコメントに記された後に関数宣言が続くという構造が繰り返し記述されている。モジュール外部仕様解析部５は、このモジュール外部仕様９を読み込み（図２のステップＳ２０１）、関数宣言解析部６は、関数宣言の解析において、関数情報３１と引数情報３２を得る（図２のステップＳ２０２）。
【００４４】
アサーション解析部７は、アサーションの解析（図２のステップＳ２０３、図５の全ステップ）において、モジュール外部仕様のアサーションを対象として（図５のステップＳ５１〜Ｓ５５）、モジュール外部仕様９（例９１）のアサーションをアサーション記法（例９２）の予約語＠ｐｒｅなどと後続の制約式に分けて、アサーション情報４１のＩＤ、関数、制約区分、元の制約式を設定する（図５のステップＳ５２）。制約式の整形（図５のステップＳ５３）では、整形ルール４５のＩＤとＦ１のルールにより、等値演算子を含む事後条件（アサーション情報４１におけるＩＤが２・３・５・６の行）が整形対象となる。ＩＤが２のアサーション情報４１については、ＩＤがＦ１以外の整形ルールには合致しないので、元の制約式「ｃｏｕｎｔ（）＝＝￥ｏｌｄ（ｃｏｕｎｔ（）＋１）」をそのまま整形後の制約式とする（注意：後で変更が入る）。ＩＤが３のアサーション情報４１については、ＩＤがＦ４のルールによって元の制約式「ｉｔｅｍ＝＝ｐｅｅｋ（ｃｏｕｎｔ（）−１）」の右辺の照会関数「ｐｅｅｋ」を左辺に移して整形後の制約式「ｐｅｅｋ（ｃｏｕｎｔ（）−１）＝＝ｉｔｅｍ」を得る。ＩＤが５のアサーション情報４１については、ＩＤがＦ３のルールによって元の制約式「ｐｅｅｋ（ｃｏｕｎｔ（））＝＝￥ｒｅｓｕｌｔ」の右辺の戻り値「￥ｒｅｓｕｌｔ」を左辺に移して整形後の制約式「￥ｒｅｓｕｌｔ＝＝ｐｅｅｋ（ｃｏｕｎｔ（））」を得る。ＩＤが６のアサーション情報４１については、ＩＤがＦ２のルールによって元の制約式「￥ｏｌｄ（ｃｏｕｎｔ（））＝＝ｃｏｕｎｔ（）＋１」の左辺の関数実行前の式「￥ｏｌｄ（ｃｏｕｎｔ（））」を右辺に移して「ｃｏｕｎｔ（）＋１＝＝￥ｏｌｄ（ｃｏｕｎｔ（））」を得て、ＩＤがＦ４のルールによって左辺を照会関数「ｃｏｕｎｔ（）」のみとするために他を右辺に移して整形後の制約式「ｃｏｕｎｔ（）＝＝￥ｏｌｄ（ｃｏｕｎｔ（））−１」を得る（注意：すぐ後で変更が入る）。事前変数への置換（図５のステップＳ５４）では、ＩＤが２と６のアサーション情報４１については整形後の制約式に関数実行前の式「￥ｏｌｄ（
式 ）」を含むので、これに対応した事前変数情報４２を設定し、ＩＤが２の整形後の制約式「ｃｏｕｎｔ（）＝＝￥ｏｌｄ（ｃｏｕｎｔ（）＋１）」を「ｃｏｕｎｔ（）＝＝＿＿ｏｌｄ＿１」とし、ＩＤが６の整形後の制約式「ｃｏｕｎｔ（）＝＝￥ｏｌｄ（ｃｏｕｎｔ（））−１」を「ｃｏｕｎｔ（）＝＝＿＿ｏｌｄ＿２−１」とする。
【００４５】
アサーション解析部７は、アサーション情報４１を対象として（図５のステップＳ５６〜Ｓ５９）、元の制約式に出現する関数「ｃｏｕｎｔ」「ｐｅｅｋ」を照会関数情報４３に設定する（図５のステップＳ５７）。
【００４６】
図１１に示されるように、アサーション依存判定ルール１１１では、以下の条件が全て成立するとき、アサーションＡはアサーションＢに依存するものとする。
・アサーションＡとアサーションＢは同じ関数を制約する。
・アサーションＡは等値演算子を持ち、照会関数Ａを持ち、その引数に照会関数Ｂがある。
・アサーションＢは等値演算子を持ち、その左辺には照会関数Ｙがある。
【００４７】
アサーション解析部７は、アサーション依存判定ルール１１１により、整形後の制約式についてＩＤが３のアサーションについては左辺の「ｐｅｅｋ」の引数に「ｃｏｕｎｔ」が出現するので、同じ関数ｐｕｓｈを制約するアサーションのうち整形後の制約式の左辺に「ｃｏｕｎｔ」だけを持つＩＤが２のアサーションに依存するものと判定して依存ＩＤに２を設定する。ＩＤが５のアサーションについては整形後の制約式の右辺に「ｐｅｅｋ」と「ｃｏｕｎｔ」が出現するので、同じ関数ｐｏｐを制約するアサーションのうち整形後の制約式の左辺に「ｃｏｕｎｔ」だけを持つＩＤが６のアサーションに依存するものと判定して依存ＩＤに６を設定する（図５のステップＳ５８）。
【００４８】
アサーション解析部７は、アサーション情報の関数ｐｕｓｈに関して、依存ＩＤが設定されておらず制約区分が事後であるＩＤが２のアサーションをつなぎ、次に依存ＩＤが設定されているＩＤが３のアサーションを既につながれているＩＤが２のアサーションにつなぐといった処理を繰り返すことにより、アサーション依存情報４４を得ることができる（図５のステップＳ６０）。
【００４９】
スタブモジュール生成部８は、スタブモジュールの生成（図２のステップＳ２０４、図８の全ステップ）において、図１２Ａ、Ｂに示されるようなスタブモジュール１２０（図６のスタブモジュール６０と同じ）を生成する。まずＣ言語で一般に使用するＮＵＬＬ定数を宣言したヘッダファイルを参照するための「＃ｉｎｃｌｕｄｅ＜ｓｔｄｉｏ．ｈ＞」や照会関数についてＣ言語では必要となる関数のプロトタイプ宣言を検証ツール固有部１２１（図６の検証ツール固有部６１と同じ）として設定する（図８のステップＳ８０１）。
【００５０】
スタブモジュール生成部８は、スロット定義部１２２（図６のスロット定義部６２と同じ）については、照会関数情報４３の照会関数ごとに、まず照会関数ｐｅｅｋについて関数情報３１と引数情報３２とを参照して引数が有ると判定し、引数ｉｎｄｅｘに対するスロット「ｕｎｓｉｇｎｅｄ  ｉｎｔ＿＿ｐｅｅｋ＿＿ｉｎｄｅｘ［ＭＡＸＳＩＺＥ］」と戻り値に対するスロット「ｖｏｉｄ＊＿＿ｐｅｅｋ＿＿ｒｅｓｕｌｔ［ＭＡＸＳＩＺＥ］」を設定する。一方、照会関数ｃｏｕｎｔは引数が無いので、戻り値に対するスロット「ｕｎｓｉｇｎｅｄ  ｉｎｔ＿＿ｃｏｕｎｔ＿＿ｒｅｓｕｌｔ」だけを設定する（図８のステップＳ８０２）。
【００５１】
スタブモジュール生成部８は、スタブ関数定義部１２３（図６のスタブ関数定義部６３と同じ）について（図８のステップＳ８０４）、関数情報３１の関数ごとに処理を繰り返す（図８のステップＳ８０３〜Ｓ８１１）。
【００５２】
スタブモジュール生成部８は、１番目の関数ｐｕｓｈについては照会関数情報４３に設定されていないので照会関数ではないと判定する（図８のステップＳ８０５−ＮＯ）。この場合、関数ｐｕｓｈについての各事前変数４２の定義「ｕｎｓｉｇｎｅｄ  ｉｎｔ＿＿ｏｌｄ＿１＝ｃｏｕｎｔ（）＋１；」を設定する（図８のステップＳ８０８）。次に、アサーション依存情報４４に設定された順序で、まずＩＤが２のアサーションについて、等値を示す整形後の制約式「ｃｏｕｎｔ（）＝＝＿＿ｏｌｄ＿１」に基づいてスロットへの引数値などを設定し、次にＩＤが３のアサーションについて、等値を示す整形後の制約式「ｐｅｅｋ（ｃｏｕｎｔ（）−１）＝＝ｉｔｅｍ」に基づいてスロットへの引数値などを設定する（図８のステップＳ８０９）。次に、復帰処理を実行する（図８のステップＳ８１０）。２番目の関数ｐｏｐも同様である。
【００５３】
スタブモジュール生成部８は、３番目の関数ｐｅｅｋは照会関数情報４３に設定されているので照会関数であると判定する（図８のステップＳ８０５−ＹＥＳ）。この場合、引数の値の組と一致する引数スロットがあれば対応する戻り値スロットから値を取得し（図８のステップＳ８０６）、復帰処理を実行する（図８のステップＳ８０７）。４番目の関数ｃｏｕｎｔは引数がないので、戻り値スロットの値を戻り値に設定し（図８のステップＳ８０６）、復帰処理を実行する（図８のステップＳ８０７）。
【００５４】
図１０は、プログラム側で、関数ｐｕｓｈを２回呼び出す処理１０１、１０２を実行してから、関数ｐｏｐを２回呼び出す処理１０３、１０４を実行する場合に、スタブモジュールのスロットがどのように更新されるかを示したものである。スタックの一般的な実装では、ｐｏｐが呼ばれるとスタックから最上位のアイテム（図１０ではスロットの下の方が最上位）を削除し、そのアイテムを戻り値として返すが、生成されたスタブモジュールではアイテムが削除されずにスロットに残っていることが判る。一方で、戻り値はｐｏｐに期待されるとおりの値を返す。このようにスタブモジュールは内部の実装は本来のモジュールとは異なるが、引数や戻り値などの外部仕様はアサーションに記述された内容に関しては本来のモジュールと同様に振舞う。
【００５５】
以上は、手続き型言語Ｃの例に基づく説明であるが、オブジェクト指向言語であるＪａｖａ（登録商標）やＣ＋＋であれば、Ｊａｖａ（登録商標）やＣ＋＋のクラスをＣのファイルにＪａｖａ（登録商標）やＣ＋＋のメソッドをＣの関数に置き換えれば、上述の実施形態に適用することができる。
【００５６】
［効果］
本発明の実施形態によるプログラム検証支援装置によれば、検証したいプログラムが使っているモジュール（１つ１以上の関数を含み、且つ、状態を有する）について、そのモジュールの外部公開関数の定義が提供されていない場合でも、生成されるスタブモジュール１０、６０、１２０を用いることにより、該モジュールの関数を呼び出すプログラムを静的に検証できる。
【００５７】
例えば、モジュールが状態を持つ場合、そのモジュールの外部公開関数には、モジュールの状態を問い合わせる関数（照会関数）と状態を更新する関数とがある。本発明では、照会関数については、関数宣言に基づいて、モジュールの状態を表す値を保持する変数（スロット）の変数定義（スロット定義部６２、１２２）と、スロットを検索して状態を表す値を返す関数定義（スタブ関数定義部６３、１２３）を生成する。他の外部公開関数については、関数宣言とアサーションに基づいて、スロットの更新・照会関数の呼び出し・戻り値の設定などを行う関数定義（スタブ関数定義部６３、１２３）を生成する。これらの生成された変数定義や関数定義のまとまり（スタブモジュール１０、６０、１２０）を、外部公開関数の定義が与えられていないモジュールの代わりに用いれば、このモジュールの関数を呼び出すプログラムを従来の静的プログラム検証ツールによって検証できるようになる。
【００５８】
また、本発明の実施形態によるプログラム検証支援装置によれば、上述の具体例のように、該モジュールの動作環境を準備せずともソースコードとアサーションだけを入力として静的に検証できるので、実際にプログラムを動作させて検証を行うテストよりも早い時点で検証を行えるようになる。
【図面の簡単な説明】
【００５９】
【図１】図１は、本発明の実施形態によるプログラム検証支援装置の構成を示している。
【図２】図２は、本発明の実施形態によるプログラム検証支援装置の動作として、プログラム検証支援方法を示すフローチャートである。
【図３】図３は、関数解析情報３０を示している。
【図４】図４は、アサーション解析情報４０を示している。
【図５】図５は、図２のアサーションを解析する処理（ステップＳ２０３）を示すフローチャートである。
【図６】図６は、図１のスタブモジュール１０として、スタブモジュール６０を示している。
【図７Ａ】図７Ａは、戻り値スロット７１の例を示している。
【図７Ｂ】図７Ｂは、引数スロット配列、戻り値スロット配列７２の例を示している。
【図８】図８は、図２のスタブモジュールを生成する処理（ステップＳ２０４）を示すフローチャートである。
【図９Ａ】図９Ａは、モジュール外部仕様９の例９１を示している。
【図９Ｂ】図９Ｂは、アサーション記法の例９２を示している。
【図１０】図１０は、プログラム側で、関数ｐｕｓｈを２回呼び出す処理１０１、１０２を実行してから、関数ｐｏｐを２回呼び出す処理１０３、１０４を実行する場合に、スタブモジュールのスロットがどのように更新されるかを示したものである。
【図１１】図１１は、アサーション依存判定ルール１１１の例を示している。
【図１２Ａ】図１２Ａは、図６のスタブモジュール６０として、スタブモジュール１２０の例を示している。
【図１２Ｂ】図１２Ｂは、図６のスタブモジュール６０として、スタブモジュール１２０の例を示している。
【符号の説明】
【００６０】
１    入出力装置、
２    処理装置、
３    記憶装置、
４    制御部、
５    モジュール外部仕様解析部、
６    関数宣言解析部、
７    アサーション解析部、
８    スタブモジュール生成部、
９    モジュール外部仕様、
１０    スタブモジュール、
３０    関数解析情報、
３１    関数情報、
３２    引数情報、
４０    アサーション解析情報、
４１    アサーション情報、
４２    事前変数情報、
４３    照会関数情報、
４４    アサーション依存情報、
４５    整形ルール、
６０    スタブモジュール、
６１    検証ツール固有部、
６２    スロット定義部、
６３    スタブ関数定義部、
７１    戻り値スロット、
７２    引数スロット配列、戻り値スロット配列、
９１    モジュール外部仕様９の例、
９２    アサーション記法の例、
１０１    処理、
１０２    処理、
１０３    処理、
１０４    処理、
１１１    アサーション依存判定ルール、
１２１    検証ツール固有部、
１２２    スロット定義部、
１２３    スタブ関数定義部、
【図１】
2010079525.tif 000003
【図２】
2010079525.tif 000004
【図３】
2010079525.tif 000005
【図４】
2010079525.tif 000006
【図５】
2010079525.tif 000007
【図６】
2010079525.tif 000008
【図７Ａ】
2010079525.tif 000009
【図７Ｂ】
2010079525.tif 000010
【図８】
2010079525.tif 000011
【図９Ａ】
2010079525.tif 000012
【図９Ｂ】
2010079525.tif 000013
【図１０】
2010079525.tif 000014
【図１１】
2010079525.tif 000015
【図１２Ａ】
2010079525.tif 000016
【図１２Ｂ】
2010079525.tif 000017