(57)【特許請求の範囲】
【請求項１】
ソースコードのモデル検査のために前記ソースコードにおいてループ抽象化を行うシステムであって、
プロセッサに結合されるコンテキスト拡張モジュールであって、
抽象化のための前記ソースコードを受信し、
前記ソースコードの中の原ループを決定し、前記原ループは制御ステートメント及びループボディを含み、前記原ループは前記制御ステートメントに基づいて前記ループボディを反復して実行させ、
前記原ループにおける出力変数及び前記原ループに関係付けられるブロックの数を識別し、前記出力変数は入出力変数及び純出力変数を含み、前記入出力変数は前記原ループにおいて読み込まれ且つ修正される変数を示し、前記ブロックの数は、少なくとも１つの出力変数が計算される無条件に実行されるステートメントセットのカウントを示すコンテキスト拡張モジュールと、
前記プロセッサに結合され、前記原ループに対応する抽象化ループを生成するループ抽象化モジュールであって、前記抽象化ループを生成するために、前記ループ抽象化モジュールは、
前記出力変数の第１のサブセットにおける各出力変数の加速割り当てのための修正式を追加し、前記修正式は前記ループ本体の前に追加され、
前記制御ステートメントを有界制御ステートメントと置換し、前記有界制御ステートメントは前記ブロックの数及び前記出力変数の第２のサブセットのカウントに基づく上限を有し、
前記モデル検査のための抽象化ソースコードを生成するために前記原ループを前記抽象化ループと置換するように更に構成されループ抽象化モジュールと
を備える、システム。
【請求項２】
前記純出力変数は前記原ループにおいて読み込まれずに修正される変数を示し、前記出力変数の第１のサブセットは前記入出力変数に対応し、前記出力変数の第２のサブセットは純出力変数に対応する、請求項１に記載のソースコードにおいてループ抽象化を行うシステム。
【請求項３】
前記有界制御ステートメントにおける前記上限は、少なくとも１つの出力変数が計算される無条件に実行されるステートメントセットの数及び純出力変数の数に基づいて計算される決定性の境界値である、請求項２に記載のソースコードにおいてループ抽象化を行うシステム。
【請求項４】
前記ループ抽象化モジュールは、
アサーションステートメントが前記原ループの内側に配置されていることを決定し、
前記抽象化ループを生成するために帰納法を適用するように構成される、請求項１に記載のソースコードにおいてループ抽象化を行うシステム。
【請求項５】
非再帰出力変数の加速割り当てのために、前記ループ抽象化モジュールは、前記非再帰変数の初期値、前記非再帰変数に対する初期化式の数、及び前記初期化式の初期化値の関数として前記非再帰出力変数の値を定式化するように更に構成される、請求項１に記載のソースコードにおいてループ抽象化を行うシステム。
【請求項６】
自己再帰出力変数の加速割り当てのために、前記ループ抽象化モジュールは、複数のパラメータの中で、前記自己再帰出力変数の初期値、前記自己再帰出力変数を修正する計算の数、及び前記原ループにおける前記計算の実行の回数の関数として前記自己再帰出力変数の値を定式化するように更に構成される、請求項１に記載のソースコードにおいてループ抽象化を行うシステム。
【請求項７】
前記プロセッサに結合され、前記抽象化ループに対するエラーメッセージを生成するモデルチェッカー
を更に備え、前記エラーメッセージは前記抽象化ループのモデル検査中のエラーの発生に対応し、
前記コンテキスト拡張モジュールは拡張コンテキストで前記抽象化ループを再生するように構成され、前記拡張コンテキストは前記原ループを実行させる前記原ループの外側の実行ステートメントを含む、請求項１に記載のソースコードにおいてループ抽象化を行うシステム。
【請求項８】
ソースコードのモデル検査のために前記ソースコードにおいてループを抽象化する、コンピュータによって実装される方法であって、
抽象化のための前記ソースコードを受信するステップと、
前記ソースコードの中の原ループを決定するステップであって、前記原ループは制御ステートメント及びループボディを含み、前記原ループは前記制御ステートメントに基づいて前記ループボディを反復して実行させるステップと、
前記原ループにおける出力変数及び前記原ループに関係付けられるブロックの数を識別するステップであって、前記出力変数は入出力変数及び純出力変数を含み、前記入出力変数は前記原ループにおいて読み込まれ且つ修正される変数を示し、前記ブロックの数は、少なくとも１つの出力変数が計算される無条件に実行されるステートメントセットのカウントを示すステップと、
前記原ループに対応する抽象化ループを生成するステップであって、前記抽象化ループを生成することは、
前記出力変数の第１のサブセットにおける各出力変数に対する加速割り当てのための修正式を追加ことであって、前記修正式は前記ループ本体の前に追加されること、及び
前記制御ステートメントを有界制御ステートメントと置換することであって、前記有界制御ステートメントは前記ブロックの数及び前記出力変数の第２のサブセットのカウントに基づく上限を有すること
を含むステップと、
前記モデル検査のための抽象化ソースコードを生成するために前記原ループを前記抽象化ループと置換するステップと
を含む、方法。
【請求項９】
前記純出力変数は前記原ループにおいて読み込まれずに修正される変数を示し、前記出力変数の第１のサブセットは前記入出力変数に対応し、前記出力変数の第２のサブセットは前記純出力変数に対応する、請求項８に記載の方法。
【請求項１０】
前記有界制御ステートメントにおける前記上限は、少なくとも１つの出力変数が計算される無条件に実行されるステートメントセットの数及び純出力変数の数に基づいて計算される決定性の境界値である、請求項９に記載の方法。
【請求項１１】
前記抽象化ループを生成することは、
アサーションステートメントが前記原ループの内側に配置されていることを決定すること、及び
前記抽象化ループを生成するために帰納法を適用すること
を含む、請求項８に記載の方法。
【請求項１２】
非再帰出力変数の加速割り当ては、前記非再帰変数の初期値、前記非再帰変数に対する初期化式の数、及び前記初期化式の初期化値の関数として前記非再帰出力変数の値を定式化することを含み、前記非再帰出力変数は定数の関数である、請求項８に記載の方法。
【請求項１３】
自己再帰出力変数の加速割り当ては、複数のパラメータの中で、前記自己再帰出力変数の初期値、前記自己再帰出力変数を修正する計算の数、及び前記原ループにおける前記計算の実行の回数の関数として前記自己再帰出力変数の値を定式化することを含み、前記自己再帰出力変数は定数及び前記自己再帰出力変数の関数である、請求項８に記載の方法。
【請求項１４】
モデルチェッカーから前記抽象化ループに対するエラーメッセージを受信するステップであって、前記エラーメッセージは前記抽象化ループのモデル検査中のエラーの発生に対応するステップと、
拡張コンテキストで前記抽象化ループを再生するステップであって、前記拡張コンテキストは前記原ループを実行させる前記原ループの外側の実行ステートメントを含むステップと
を更に含む、請求項８に記載の方法。
【請求項１５】
前記抽象化ループを生成することは、最も内側のネスト化ループから開始して前記原ループにおける各ネスト化ループに対して前記抽象化ループを生成することを含む、請求項８に記載の方法。
【請求項１６】
ソースコードのモデル検査のために前記ソースコードにおけるループを抽象化する方法を実行するためのコンピュータプログラムを有する一時的でないコンピュータ可読媒体であって、前記方法は、
抽象化のための前記ソースコードを受信するステップと、
前記ソースコードの中の原ループを決定するステップであって、前記原ループは制御ステートメント及びループボディを含み、前記原ループは前記制御ステートメントに基づいて前記ループボディを反復して実行させるステップと、
前記原ループにおける出力変数及び前記原ループに関係付けられるブロックの数を識別するステップであって、前記出力変数は入出力変数及び純出力変数を含み、前記入出力変数は前記原ループにおいて読み込まれ且つ修正される変数を示し、前記純出力変数は前記原ループにおいて読み込まれずに修正される変数を示し、前記ブロックの数は、少なくとも１つの出力変数が計算される無条件に実行されるステートメントセットのカウントを示すステップと、
前記原ループに対応する抽象化ループを生成するステップであって、前記抽象化ループを生成することは、
前記出力変数の第１のサブセットにおける各出力変数に対する加速割り当てのための修正式を追加することであって、前記修正式は前記ループ本体の前に追加すること、及び
前記制御ステートメントを有界制御ステートメントと置換することであって、前記有界制御ステートメントは前記ブロックの数及び前記出力変数の第２のサブセットのカウントに基づく上限を有すること
を含むステップと、
前記モデル検査のための抽象化ソースコードを生成するために前記原ループを前記抽象化ループと置換するステップと
を含む、一時的でないコンピュータ可読媒体。
【請求項１７】
前記抽象化ループを生成することは、
アサーションステートメントが前記原ループの内側に配置されていることを決定すること、及び
前記抽象化ループを生成するために帰納法を適用すること
を含む、請求項１６に記載の一時的でないコンピュータ可読媒体。
【請求項１８】
定数の関数である非再帰出力変数の加速割り当ては、前記非再帰変数の初期値、前記非再帰変数に対する初期化式の数、及び前記初期化式の初期化値の関数として前記非再帰出力変数の値を定式化することを含み、前記非再帰変数は定数の関数である、請求項１６に記載の一時的でないコンピュータ可読媒体。
【請求項１９】
自己再帰出力変数の加速割り当ては、複数のパラメータの中で、前記自己再帰出力変数の初期値、前記自己再帰出力変数を修正する計算の数、及び前記原ループにおける前記計算の実行の回数の関数として前記自己再帰出力変数の値を定式化することを含み、前記自己再帰出力変数は定数及び前記自己再帰出力変数の関数である、請求項１６に記載の一時的でないコンピュータ可読媒体。
【請求項２０】
モデルチェッカーから前記抽象化ループに対するエラーメッセージを受信するステップであって、前記エラーメッセージは前記抽象化ループのモデル検査中のエラーの発生に対応するステップと、
拡張コンテキストで前記抽象化ループを再生するステップであって、前記拡張コンテキストは前記原ループを実行させる前記原ループの外側の実行ステートメントを含むステップと
を更に含む、請求項１６に記載の一時的でないコンピュータ可読媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
本願の主題は、モデル検査のためのデータ抽象化、特に、排他的ではないが、モデル検査のためのコンピュータプログラムにおけるループ抽象化に関する。
【背景技術】
【０００２】
コンピュータプログラムは、コンピュータ及びラップトップ等のコンピュータ装置において特定のタスクを行うようにプログラミング言語で記述されたコードのシーケンスである。単にプログラムとも呼ばれるコンピュータプログラムは、通常、特定のタスクを行うために実行される１つ以上の実行ステートメントを含む。ステートメントは、一般に、プログラムの実行が最初のステートメントの実行から開始して最後のステートメントの実行で終了する逐次的形式で提供される。しかしながら、複雑なプログラムにおいて、ステートメントはループの形式で提供されてもよく、ループ終了条件に達するまで特定のステートメントのセットが所与のシーケンスで反復して実行される。このような場合、最後の連続的ステートメントの実行により、終了条件が達成されたかどうかが初めて決定される。終了条件が達成されない場合、最初のステートメントから開始する所与のシーケンスが再び実行されるが、そうでない場合、プログラムにおけるループは終了する。更に、ループは、特定のループ境界（loop bound）に対して実行されるように構成されてもよい。ループ境界は、ループを実行する必要がある最大回数として理解されてもよい。
【図面の簡単な説明】
【０００３】
詳細な説明は、（複数の）添付の図面を参照して記載される。（複数の）図面において、参照番号の一番左の数字が参照番号が最初に現れる図面を識別する。同様の特徴及び構成要素を参照するために、（複数の）図面を通じて同じ番号が用いられる。例示として、（複数の）添付の図面を参照して、本願の主題の実装に従うシステム及び／又は方法の幾つかの実装が次に記載される。
【図１】本願の主題の実装に従って、ループ抽象化システムを実装するネットワーク環境を示す。
【図２】本願の主題の実装に従って、ソースコードにおいてループ抽象化システムを実装する方法を示す。
【発明を実施するための形態】
【０００４】
ループを有するプログラムの実行中に、無限ループ又は大きなループ境界を有するループの場合にエラーに遭遇することがある。一般に、エラーの無いプログラムの実行を確実にするために、プログラムは、例えば、コンピュータ装置のプログラムアナライザ又はモデルチェッカーにより、エラーについて最初に検査される。モデルチェッカーは、プログラムを分析して、プログラムの実行により発生し得る様々なエラーを検査するように構成される。しかしながら、非決定性の境界、即ち、無限又は大きなループ境界を有するループにおいて、モデルチェッカーは、小さな上限を特定して、その上限に従ってループを展開する。更に、モデルチェッカーはこのような境界を特定するのに十分な知性に欠けることがあるので、上限を特定することは、モデルチェッカーにとって時間がかかると共に困難なタスクであり得る。従って、不適切な、即ち、必要とされるより小さな境界を提供することは、有界モデルチェッカーにループ展開アサーションエラー等の結果を引き起こし得る。更に、小さな境界及び大きな境界のどちらの場合にも、モデルチェッカーは、「メモリ不足（out of memory）」エラーを引き起こし得る。従って、有界モデルチェッカーを用いて無限又は大きな境界を有するループを検証することは実現不可能であるかもしれない。
【０００５】
他の従来技術は、モデル検査及び検証のためのループ抽象化（loop abstraction）を含む。このようなアプローチの１つは、ループが通過する推移の数に基づくループ抽象化に関する。しかしながら、推移の数に基づくループの抽象化は、推移の数が正確に決定されず、無限ループに対して効果的ではないため、モデル検査の効率に影響し得る。
【０００６】
ループ抽象化の別の従来技術は、所与のループを二度展開することに関する。最初に、所与のループがｎ回展開され、その後、展開中にループボディで更新された全ての変数が初期化される。その後、ループはｍ回展開される。しかしながら、この技術の使用は、ループ展開中に更新された全ての変数がループ展開の反復ごとに初期化されず、後続の展開に影響するので複雑な条件を有する所定のループの検証には有益ではないかもしれない。更に、ｍの値は、設定可能なパラメータであり、効率性に関して評価されない。従って、モデルチェッカーは、メモリ不足を起こし、又はループ展開アサーションエラーを起こし得る。
【０００７】
更に別の従来技術は、検証のための述語抽象化（predicate abstraction）を含む。述語抽象化は、典型的には、具象データに対する述語を介して具象データタイプを抽象データタイプにマッピングすることに関する。しかしながら、大きなプログラムに対する述語抽象化の使用は、技術に関連する計算コストのため実行不可能であり得る。
【０００８】
従って、非決定性の境界を有するループを備えたコンピュータプログラムの検証の過程で、メモリ又は処理エラーの無い非決定性の境界を備えたループを抽象化するための効率的且つより時間のかからない機構に対する必要性が存在する。
【０００９】
本願の主題の実装によれば、ソースコードのモデル検査のためにソースコードにおけるループを抽象化するシステム及び方法が求められる。ソースコードは、プログラミング言語で記述されるコンピュータプログラムとして理解されてもよい。システム及び方法は、様々なコンピュータ装置において実装され得る。コンピュータ装置は、限定されないが、デスクトップコンピュータ、ハンドヘルド装置、ラップトップ又は他のポータブルコンピュータ等を含む。１つの実装では、ループ抽象化を実装するシステム及び方法は、限定されないが、Ｃ，Ｃ＋＋，ＶＣ＋＋，Ｃ＃等を含むプログラミング言語を用いて記述されるプログラムにおけるループ抽象化及びその後のモデル検査のために提供されてもよい。
【００１０】
１つの実装において、抽象化のために受信されるソースコードは、ループボディ及び制御ステートメントを有する原ループ（original loop）を決定するために分析されてもよい。更に、出力変数及び原ループに関係付けられるブロックの数も識別される。更に、原ループに対応する抽象化ループが生成されてもよい。このために、出力変数の第１のサブセットにおける各出力変数の加速割り当て（accelerated assignment）のための修正式が、ループボディの前に追加される。更に、ループ制御ステートメント（loop control statement）は、ループ制御ステートメントを含む有界制御ステートメント（bounded control statement）に置換されてもよい。更に、第２のサブセットの出力変数のカウントが、有界制御ステートメントに対して考慮されてもよい。方法は、モデル検査のための抽象化ソースコードを生成するために原ループを抽象化ループと更に置換する。ここで、出力変数の第１のサブセットは入出力変数（IO）に対応し、出力変数の第２のサブセットは純出力変数に対応する。
【００１１】
原ループにおける制御ステートメントは、原ループに対する終了条件として理解されてもよい。原ループは、ループ実行中に、読み込まれ、使用され、又は修正され得る複数の変数を含み得る。ループ変数は、入力変数、純出力変数、及び入出力（IO）変数として更に分類されてもよい。入力変数は、読み取り専用の、即ち原ループに入力を提供するだけの変数であり、従ってループ実行中に修正されない。他方で、純出力変数は、ループ実行中にのみ修正され且つループ外でも使用される変数である。IO変数は、入力を提供するために使用され且つループ実行中に修正される変数である。
【００１２】
１つの実装では、Ｃプログラム等のコンピュータプログラムにおけるループが抽象化される。コンピュータプログラムにおけるループを抽象化するために、「a」と呼ばれる、検証される各プロパティが決定され、アサーションとしてモデル化されてもよい。更に、コンピュータプログラムは、プロパティ「a」に関してスライスされ、低減されスライスされたコンピュータプログラムがプロパティ「a」の検査のために使用される。更に、反復コンテキスト拡張モジュールが、コンピュータプログラムのプロパティ「a」を検証する。検証プロセスにおいて、アサーション（assertion）「a」がある関数「f」が、コンピュータプログラムの分析のために開始コンテキストとして選択される。更に、関数「f」からの大きな未知の境界を有するループが抽象化されて、抽象化コンピュータプログラムがモデルチェッカーを用いて分析される。モデルチェッカーが、コンピュータプログラムのプロパティ「a」を安全であると報告する場合、コンピュータプログラムにおいてプロパティ「a」が安全であると確実に結論を下すことができる。モデルチェッカーがコンピュータプログラムのプロパティ「a」を安全でないと報告する場合、コンテキストは「f」を呼ぶ関数に拡張される。モデルチェッカー報告プロセスは、コンピュータプログラムのプロパティ「a」が安全であると証明され、又はモデルチェッカーが拡張せず、又はコンピュータプログラムのプロパティ「a」がトップレベル関数において安全でないと証明されるまで繰り返される。
【００１３】
更に、本願のループ抽象化プロセスは、アサーションがコンピュータプログラムのループボディの外側にある場合に大きな又は未知の境界を有するループを変形するためにループ置換を用い、アサーションがコンピュータプログラムのループボディの中にある場合に帰納法（induction）を用いる。また、コンピュータプログラムのネスト化ループが、最も内側のループボディから開始して、コンピュータプログラムのループボディの最も外側に進行して抽象化される。ある実装によれば、アサーションがループボディの内側又は外側に存在するかどうかを決定するためにフラグが使用され得る。
【００１４】
更に、何れの変換でも、各IO変数が、抽象化ループの始めに非決定性の値をそれに割り当てることによって抽象化される。IO変数は、最初に読み込まれてそれからループボディの一部のパスに沿って修正される変数である。線形再帰方程式に関与する変数に関して、それに対する非決定性の割り当ては、その割り当ての非決定数の反復に対する閉形式の加速（closed form acceleration）である。また、１つより多くの再帰変数が相互依存性を有する場合に、相互再帰も同様に取り扱われる。
【００１５】
従って、本願の主題のシステム及び方法は、プログラムにおけるループ抽象化プロセスの実装を容易にする。原ループは、ループが固定回数だけ実行されることを確実にする小さな既知の境界を有する別のループに置換され、それによってメモリリソース、処理リソース、及び時間消費に関係付けられるコスト並びに無限の又は大きなループ境界を有するループの実行により引き起こされるメモリオーバーフロー又はループ展開アサーションエラー等のエラーを減らす。更に、コンピュータプログラムは、追加の実行と共に元のコンピュータプログラムの全ての実行を許可する別のコンピュータプログラムへと抽象化されてもよい。このような抽象化コンピュータプログラムは、元のコンピュータプログラムの過大近似（over-approximation）と呼ばれてもよい。従って、コンピュータプログラムのプロパティが抽象化されたコンピュータプログラムにおいて有効であれば、元のコンピュータプログラムにおいても維持されるであろう。更に、アサーションがコンピュータプログラムにおいて安全である場合であって、ループ抽象化プロセスの後、モデルチェッカーが安全となるアサーションを返す場合、元のコンピュータプログラムは、そのアサーションに関して安全である。
【００１６】
本願の主題のこうした及び他の利点が、以下の図面と併せてより詳細に記載される。プログラムにおけるループ抽象化に関して記載されたシステム及び方法の態様が異なるコンピュータシステム、環境及び／又は構成において実装され得るが、実装は以下の（複数の）例示的なシステムに照らして記載されている。
【００１７】
図１は、本願の主題の実装に従って、プログラミング言語で記述されたプログラムにおいてループ抽象化を実装するループ抽象化システム１０２の例示的な構成要素を示す。ループ抽象化システム１０２は、コンピュータ装置１２８において実装されてもよい。コンピュータ装置１２８の例示は、限定されないが、メインフレームコンピュータ、ワークステーション、パーソナルコンピュータ、デスクトップコンピュータ、ミニコンピュータ、サーバ、マルチプロセッサシステム、ラップトップ、ＰＤＡ（personal digital assistant）、スマートフォン及び携帯電話等のセルラ通信装置等を含む。コンピュータ装置１２８を使用して実装されるループ抽象化システム１０２は、１つ以上の（複数の）プロセッサ１０４、（複数の）IOインターフェース１０６、及びプロセッサ１０４に結合されるメモリ１０８を含む。プロセッサ１０４は、単一のプロセッシングユニット又は多数のユニットであり得る。プロセッサ１０４は、１つ以上のマイクロプロセッサ、マイクロコンピュータ、マイクロコントローラ、ＤＳＰ（digital signal processor）、ＣＰＵ（central processing unit）、状態機械、論理回路、及び／又は動作命令に基づいて信号を操作する任意の装置として実装されてもよい。複数の機能の中でも特に、プロセッサ１０４は、メモリ１０８に記憶されたデータ及びコンピュータ可読命令をフェッチして実行するように構成される。
【００１８】
「（複数の）プロセッサ」と名付けられた任意の機能ブロックを含む、図示の様々な要素の機能が、適切なソフトウェアに関連してソフトウェアを実行することが可能なハードウェアと共に専用ハードウェアの使用により提供されてもよい。プロセッサにより提供される場合、機能は、単一の専用プロセッサにより、単一の共有プロセッサにより、又は一部が共有され得る複数の個別プロセッサにより提供され得る。更に、用語「プロセッサ」の明示的な使用は、ソフトウェアを実行することが可能なハードウェアへの排他的な言及と解釈されるべきではなく、限定されないが、ＤＳＰハードウェア、ネットワークプロセッサ、ＡＳＩＣ（application specific integrated circuit）、ＦＰＧＡ（field programmable gate array）、ソフトウェアを記憶するためのＲＯＭ（read only memory）、ＲＡＭ（random access memory）、及び不揮発性記憶装置を潜在的に含んでもよい。また、従来の及び／又はカスタマイズされた他のハードウェアが含まれてもよい。
【００１９】
IOインターフェース１０６は、様々なソフトウェア及びハードウェアインターフェース、例えば、キーボード、マウス、外部メモリ、及びプリンタ等の（複数の）周辺機器に対するインターフェースを含んでもよい。更に、IOインターフェース１０６は、コンピュータ装置がパーソナルコンピュータ及びラップトップ等の他のコンピュータ装置と通信することを可能にしてもよい。
【００２０】
メモリ１０８は、例えば、ＳＲＡＭ（static random access memory）及びＤＲＡＭ（dynamic random access memory）等の揮発性メモリ、及び／又はＲＯＭ（read only memory）、ＥＰＲＯＭ（erasable programmable ROM）、フラッシュメモリ、ハードディスク、光学ディスク、及び磁気テープ等の不揮発性メモリを含む、当技術分野で周知の任意のコンピュータ可読媒体を含んでもよい。また、メモリ１０８は、（複数の）モジュール１１０及びデータ１２０も含む。
【００２１】
（複数の）モジュール１１０は、ルーチン、プログラム、オブジェクト、コンポーネント、データ構造等を含み、特定のタスクを実行し又は特定の抽象データタイプを実装する。（複数の）モジュール１１０は、コンテキスト拡張モジュール１１２、ループ抽象化モジュール１１４、モデルチェッカーモジュール１１６及び（複数の）他のモジュール１１８を更に含む。（複数の）他のモジュール１１８は、コンピュータ装置のアプリケーション及び機能を補完するプログラム又は符号化命令を含んでもよい。
【００２２】
他方で、特に、データ１２０は、１つ以上の（複数の）モジュール１１０により処理され、受信され、生成されるデータを記憶するためのリポジトリとして機能する。データ１２０は、例えば、原ループデータ１２２、抽象化データ１２４、及び他のデータ１２６を含む。他のデータ１２６は、（複数の）他のモジュール１１８における１つ以上のモジュールの実行の結果として生成されるデータを含む。
【００２３】
１つの実装では、コンピュータ装置は、プログラムとも呼ばれるソースコードに含まれるループを抽象化するように構成される。このため、プログラムは、コンテキスト拡張モジュール１１２によって最初に受信される。１つの実装では、コンテキスト拡張モジュール１１２は、コンピュータ装置の内部のコンパイルモジュール（図示せず）からプログラムを受信してもよい。別の実装では、コンテキスト拡張モジュール１１２は、コンピュータ装置の外部のコンパイルモジュール（図示せず）からプログラムを受信してもよい。
【００２４】
プログラムを受信すると、コンテキスト拡張モジュール１１２は、原ループデータ１２２にプログラムを保存して、ループ抽象化が行われ得る原ループを識別するためにプログラムの構文を分析する。原ループは、原ループボディ及び原ループステートメントを含んでもよい。原ループステートメントは、ループを開始するために提供されるプログラム内のステートメントとして定義されてもよい。原ループステートメントは、制御ステートメントとも呼ばれる。典型的には、原ループステートメントは、特に、原ループに対する終了条件を含む。例えば、“for”ループにおいて、“for loop”を定義する最初のステートメント“(for I =0; i<10; i++)”が、原ループステートメントと呼ばれてもよい。更に、原ループボディは、ループ実行中に実行されるループ変数を含む１つ以上のステートメントのセットとして定義されてもよい。例えば、コンピュータ装置１０２により受信されるプログラムの以前の例では、コンテキスト拡張モジュール１１２は、抽象化が遂行される関数呼び出しコンテキストを選択し、それをループ抽象化モジュール１１４に渡すことができ、これは原ループを抽象化して抽象化ループをモデルチェッカー１１６に渡すことができる。更に、コンテキスト拡張モジュール１１２は、アサーションが後で検討される該当コンテキストを用いて検証することができない場合にコンテキストの拡張に関与してもよい。
【００２５】
１つの実装では、ループ抽象化モジュール１１４は、抽象化ソースコードを生成するために原ループを抽象化ループで置換するように構成される。１つの実装では、ループ抽象化モジュール１１４は、所与のコンテキストに存在するループを抽象化することにより抽象化コンピュータプログラムを生成してもよい。ループ抽象化モジュール１１４は、解析のための関数を入力として受け取ってもよく、コンテキスト拡張モジュール１１２から原ループに存在する出力変数及び関数呼び出しコンテキストを取得してもよい。抽象化ループを生成するために、ループ抽象化モジュール１１４は、出力変数のサブセットにおける各出力変数の加速割り当てに関する修正式を追加することができる。修正式は、ループボディの前に追加され得る。更に、ループ抽象化モジュール１１４は、有界制御ステートメントで原ループにおける制御ステートメントを置換し得る。有界制御ステートメントは、ブロックの数又は純出力変数の数に基づいて計算された小さな既知の上限を含み得る。更に、ループ抽象化モジュール１１４は、モデル検査のための抽象化ソースコードを生成するために原ループを抽象化ループと更に置換し得る。ここで、加速割り当ては、テストされている反復よりも大きな反復に対応する値を有する抽象化出力変数で出力変数を置換することを示す。更に、非再帰、自己再帰等である変数に基づいて、加速割り当ては、後述のように変化してもよい。また、他の実装では、当技術分野で周知の方法が加速割り当てのために用いられてもよい。
【００２６】
例えば、原ループが以下に示されており、これは原ループの過大近似である抽象化ループへと変形される。以下に、例示的なループ抽象化プロセス（LA）が説明される。
【００２７】
ケース１：検証されるプロパティがループの内側にある
【００２８】
【表１】
0005923636.tif 000002
【００２９】
ケース２：検証されるプロパティがループの外側にある
【００３０】
【表２】
0005923636.tif 000003
【００３１】
ここで、例１．１‐１．４において、
ｃ  −  ループ条件（loop condition）である。
Loop_body  −  入力ループボディである。
b  −  出力変数の一意のセットを修正するループボディにおけるブロックの数である。ここで、ブロックの数は、無条件に実行されるステートメントセットのカウントを示してもよい。例えば、
while(c) {
If(c1){
Stmt1; //modifying s1
}
If(c2) {
Stmt1; //modifying s2
}
While(c4) { // nested loop
Stmt3; //modifying s3
}
Stmt4; //modifying s4
}
ここで、ブロックの数は４つであり、各ブロックがｉｆ条件ステートメントに関係付けられ、一つのブロックが内側ループ（ネスト化ループ）を有し、１つのブロックが外側ループを有している。
出力変数は、ループ内で読み込まれ且つ修正されるか、又はループボディで修正され且つループ後に使用される変数である。
IO  −  一部のパスに沿って最初に読み込まれてからループボディで修正される変数のセットである。
abstract(IO)  −  ループのIO変数を過大近似する割り当てのセットである。（それ自体を再帰的に用いる）再帰変数に関して、その変数の再帰関係が取得できる場合に、この割り当ては抽象化再帰関係である。その変数の再帰関係が取得できない場合、abstract(IO)は、それに対する非決定的に選択された値の割り当てを示す。IO変数が再帰的でない場合、その変数が任意のループ反復内で達成できる可能な値の１つが、それに対して割り当てられ、又は非決定的に選択される値がそれに対して割り当てられる。
r  −  ループの全ての出力変数の値範囲を制約する条件である。
a  −  ループボディにおける各ブロックが実行された回数について条件を生成することにより出力変数の値を制約する条件である。
min(b. po)  −  ブロックの数及び原ループの純出力変数の最小である。純出力変数がない場合、min(b,po)は１を返す。
【００３２】
例１．１は、原入力ループを含み、例１．２は、入力プロパティのアサーションがループボディに存在する場合のループの対応する抽象化を含む。例１．３は、原入力ループボディを含み、例１．４は、アサーションがループボディに存在しない場合の抽象化を含む。従って、ループ抽象化、抽象化再帰及び帰納法は、アサーションがループボディの中に存在する場合にプロパティを証明するために適用され、アサーションがループボディに存在しない場合、ループ抽象化及び抽象化再帰のみがループを抽象化するために適用される更に、ループ抽象化モジュールは、アサーションを生成して、アサーションがループボディの中又は外に存在するかどうかを決定してもよい。ここで、アサーションがループボディの中に存在する場合、フラグが帰納法のために設定される。
【００３３】
更に、こうして取得された抽象化ループを有するコンピュータプログラムは、ループ抽象化モジュール１１４によって抽象化データ１２４に保存されてもよい。更に、抽象化ループを有するプログラムは、エラーに関して分析されるようにモデルチェッカーモジュール１１６に提供されてもよい。抽象化ループを有するプログラムをモデルチェッカーモジュール１１６に提供することは、分析のために抽象化ループを有する抽象化プログラム及び入力関数を促進するのに役立つと共に、コンピュータプログラムの入力アサーション又はプロパティが安全かどうかを検査する。安全であればプロセスは停止され、そうでなければトレースを生成する。
【００３４】
本願の主題は“while loop”及び“for loop”を参照して定義されているが、ループ抽象化を実装するコンピュータ装置１０２は、当業者には理解されるように、ほとんど修正／変更をしなくても、他のタイプのループにおけるループ抽象化のために使用され得ることが理解されるであろう。
【００３５】
本願の主題はｃ言語で使用されるループを参照して定義されているが、ループ抽象化を実装するコンピュータ装置は、ほとんど修正をしなくても、他のプログラミング言語を用いて記述されたプログラムにおけるループ抽象化のために使用され得ることが理解されるであろう。
【００３６】
更に、図２は、コンピュータプログラムのモデル検査のためのループの抽象化の例示的な方法２００を示す。方法２００において、ブロック２０２では、ソースコード又はコンピュータプログラムが、抽象化のためにコンテキスト拡張モジュール１１２によって受信されてもよい。更に、ブロック２０４では、制御ステートメントを有する原ループ及び原ループに関するループボディが、コンテキスト拡張モジュール１１２によって決定されてもよい。更に、ブロック２０６では、原ループに関係付けられるブロックの数及び出力変数が、コンテキスト拡張モジュール１１２によって決定されてもよい。ここで、出力変数は、純出力変数及び入出力変数の両方を含む。次に、ブロック２０８では、原ループに対応する抽象化ループが、ループ抽象化モジュール１１４によって生成されてもよい。生成された抽象化ループは、少なくとも、出力変数のサブセットにおける各出力変数に対する加速割り当てのための修正式を追加することに基づいてもよい。ここで、修正式は、ループボディの前に追加される。更に、制御ステートメントを有界制御ステートメントと置換する。ここで、有界制御ステートメントは、ブロックの数に基づく上限を含む。
【００３７】
ブロック２１０では、ソースコードにおける原ループは、ループ抽象化モジュール１１４によって、ブロック２０８で生成された抽象化ループにより置換されてもよい。方法２００は、例示を用いて以下に更に詳細に記載される。
【００３８】
例えば、ループ抽象化プロセスにおいて、ループ置換が、大きな又は未知の境界を有するがアサーションを含まない、「L」と呼ばれ得る各ループを、ループのボディにおけるブロックの数又は純出力変数の数により決定される小さな有限数の反復を有する、別のループL0によって置換する。各ブロックに対応して補助変数が導入され、そのブロックの反復の数を表す。ループＬにおける全ての出力変数が、置換されたループL0において抽象化され又は加速される。アサーションがループボディ内にあるループに対して帰納法が用いられる。ループはそのボディの３つのコピーにより置換される。１つはベースケースのためであり、２つ目はkth反復に対応し、３つ目は帰納法のための(k+1)th反復のためである。アサーション「a」が第１の反復の最後に違反されなければ、それはループボディのベースケースに対して維持される。kth反復のためのコピーの開始時に、全ての出力変数が抽象化又は加速される。kth反復の終了時に、検証されるプロパティは、帰納法の仮定として維持されると推定される。(k+1)th反復は、再び置換された内部ループ及びアサートを有する原ループボディを有する。その後、ループ抽象化プロセスが、コンピュータプログラムのループボディの開始時に、非決定性の又は加速された又は抽象化された値を全ての出力変数に割り当てる。従って、ループ抽象化プロセスの適用後に生成されたプログラムコードは、原コードの妥当な過大近似である。
【００３９】
更に、抽象化加速関係と呼ばれ得る、異なるタイプの再帰関係、及び抽象化関係が、非再帰、自己再帰、及び他のIO変数に対して生成され得る。これらの値は以下の通りである。
【００４０】
加速割り当て  例１:非再帰IO変数、iは、以下のような関数における一部の条件下でのみ修正される変数である。
i=γ、即ち、初期化式である。ここで、γは、定数又は入力変数を示してもよい。
ikの加速された値は、以下であってもよい：
【００４１】
【数１】
0005923636.tif 000004
【００４２】
i0は、実行前のiの初期値であり、
rはiの初期化式の数であり、
【００４３】
【数２】
0005923636.tif 000005
【００４４】
は、iの初期化式に対応する。
【００４５】
加速割り当て  例２:自己再帰IO変数、iは、以下のような関数における一部の条件下で修正される変数である。
i = i + β、即ち、自己再帰式である。
βは、定数又は入力である。
加速された値は、以下であってもよい：
【００４６】
【数３】
0005923636.tif 000006
【００４７】
ikは、k反復後の変数iの値であり、
i0は、iの初期値であり、
eは、iを修正する式の数であり、
k1, k2,……keは、各式が原ループで実行された回数の抽象化である。
従って、以下である：
【００４８】
【数４】
0005923636.tif 000007
【００４９】
加速割り当て  例３:ループボディにおいて、一部のパスに沿って、変数oがo = o+c1の形の式で修正され、何らかの他のパスに沿って、o = c2の形の式で初期化される。ここで、℃1及びc2は、所与のループに関する定数又は入力（ループ内で修正されない変数）である。okがk反復後のoの値であるとすると、以下である：
ok= o0 +k1 * c1 || c2 +k2* c1
ここで、o0はoの初期値であり、
k1,k2は初期化前及び最後の初期化後に対応する式が実行された回数であり、
この式は、o = ciの形のループにおいてより多くの式に拡張され得る。
【００５０】
加速割り当て  例４:ループボディにおいて、一部のパスに沿って、変数oがo = o+c1の形の式で修正され、他の一部のパスに沿って、o = ioの形の式で初期化される。ここで、c1は定数であり、ioはIO変数である。okがk反復後のoの値であるとすると、以下である：
ok= o0*k0 + p1*c1 + p2*c2+ …+pe*ce+ k1*io1_0 + k2*io2_0 + …+ kd*iodv_0 + q1*io1_0 + q2*io2_0 + …+ qd*iodb_0
ここで、o0はoの初期値であり、ループの実際の実行中にokが初期化されるかどうかによってk0は0又は1のいずれかである。ciは、okの定義で使用される定数であり、eはこのような式の数である。dvは、okの値が推移的に依存するがそれと相互に再帰的ではない変数の数である。ioi_0は、こうした変数の初期値である。dbは、oの値が推移的に依存する定数又は入力の数であり、ioj_0は、対応する変数である。ki,qi 及びpiは、非決定的に割り当てられる値である。
【００５１】
加速割り当て  例５:変数io1及びio2がio1 = io1 + io2 + c及びio2 = io1 +c2 の形の式でループボディにおける一部のパスに沿って(条件付で)修正される場合を検討する。ここで、io1,io2はIO変数であり、c1,c2は定数式である。ここで、io1及びio2 は互いに依存しており、それ故に、これは相互再帰関係である。
io1kがk反復後のio1の値であるとすると、以下である。
io1k = k1*io1_0 + k2*io2_0 + …+ kd*iod_0 + p1*c1+ p2*c2 + …+pe*ce
ここで、dは、io1が(それ自身を含む)推移的依存性を有する変数の数であり、
eは、io1が推移的依存性を有する定数又は入力変数の数であり、
定数ki,piは、非決定的に割り当てられる値であり、
iod_0は、IO変数iodの初期値を表し、
c1,c2,….,ceは、 io1が推移的依存性を有する定数又は入力である。
【００５２】
加速割り当て  例６:配列が所与のループボディの中で修正される実装において、システムは、ループボディの外の配列要素の全ての実装に対して、全ての配列要素に対する非決定性の値を生成する。
【００５３】
加速割り当て  例７：ポインタがループボディの中で修正される実装では、システムは、ポインタによって指示される全てのメモリ位置を決定し、変数に関する抽象化と同様に、メモリ位置の抽象化を生成する。しかしながら、ループボディにおける任意のポインタに対する情報へのメモリ位置が解決できない場合、全ての出力変数に対する非決定性の割り当てが生成されてもよい。
【００５４】
１つの実装では、ネスト化されたループに関して、抽象化は最も内側のループから開始する。内側のループの抽象化は、外側のループの抽象化で囲まれる。
【００５５】
【表３】
0005923636.tif 000008
【００５６】
例６、例７に示されたループのネスト化構造がこのループの抽象化を示す場合を検討する。第１に、内側ループ、それから外側ループが、ループ抽象化モジュール１１４を用いて抽象化される。外側ループを抽象化しつつ、内側ループがその抽象化により置換される。ここで、abstract inner(IO)が内側ループのIO変数の抽象化であり、abstract touter(IO)が外側ループのIO変数の抽象化である（これは内側ループのIO変数も含む）。
【００５７】
詳細な例：
以下の例示は、例示的なプロセスを示すために提供される。コンピュータプログラムのプロパティ検証が以下に提供される。検証の一部はプロパティのモデル検査を含んでいる。モデルチェッカーツールは、ループの未知の又は大きな境界を有する複雑なループのためプロパティを検証することができなかった。
【００５８】
以下は、ループ抽象化を示す例示である。
1. j=0,p=0,l=0,st=0;
2. last=nondet(); //nondet() returns a signed random value
3. max=unondet(); //unondet() returns an unsigned random value
4. while (1)
5. {
6.   st = 1;
7.   for (l=0; l< max ; l++)
8.   {
9. 
10.     if (l==last )
11.                     st = 0;
12.   }
13.   if(st == 0 && l == last +1)
14.     j+=3; p+=3;
15.   else if (st ==1)
16.   {
17.     j++;
18.     p++;
19.   }
20.   else {
21.     j+=2;
22.     p+=2;
23.   }
24.   if (l == last && st == 0)
25.                     j = j+1;
26.     assert(j==p && max == l) ;
27.   }
例Ａ−原コードの部分
【００５９】
1. l0 = l;
2. for(t=0;t<1&&l<max;t++){
3.   k1 = nondet();
4.   assume(k1>=0);
5.   l = l0 +k1;
6.   assume(l < max);
7.   if (l==last )
8.     st = 0;
9.   l++;
10. }
11. assume(!(l < max));
例Ｂ−抽象化ループ(iloop_absbody)
【００６０】
1. j=0,p=0,l=0,st=0;
2. last=nondet(); max=nondet();
/* Base Case */
3. st = 1;
<iloop_absbody>
4. if(st == 0 && l == last +1)
5.   {
6.                     j+=3; p+=3;
7.   }
8.   if (st ==1) {
9.   j++;
10     p++;
11   }
12   else {
13     j+=2;
14     p+=2;
15   }
16   if (l == last && st == 0)
17   j = j+1;
18   assert(j==p && l == max) ;
19 
/* kth iteration*/
20 for (t1 =0,l0 = l,j0 = j,p0 = p; t1<1 ; t1++) {
21   k1 = nondet(); k = nondet(); k2 = nondet(); k3 = nondet(); k4 = nondet(); k5 = nondet(); j = j0 + k2 + 2*k3 + 3*k5 + k4 ; p = p0 + k2 + 2*k3 + 3*k5;
22   l = l0 + k1;
23   __CPROVER_assume( k>=1 && k1>=0 && k2 >= 0 && k3>=0 && k4 >=0 && k5 >=0 );
24   __CPROVER_assume( k == k2+k3+k5 && k4 <= k);
25   st = 1;
26   // Abstraction of inner loop only recurrence
27   for(t=0;t<2 && l<max ;t++) {
28   k1 = nondet();
29   __CPROVER_assume(k1>=0);
30   l = l0 +k1;
31   __CPROVER_assume(l < max);
32   if (l==last )
33                     st = 0;
34   l++;
35   }
36 _  _CPROVER_assume(!(l < max));
37   // Inner loop abstraction ended
38   if(st == 0 && l == last +1)
39   {
40                     j+=3; p+=3;
41   }
42   else if (st ==1)
43   {
44     j++;
45     p++;
46   }
47   else {
48     j+=2;
49     p+=2;
50   }
51   if (l == last && st == 0)
52                     j = j+1;
53   __CPROVER_assume(j==p && l == max) ;
54   }
/*(k+1)th Loop iteration*/
55.  st = 1;
56.  <iloop_absbody>
57   if(st == 0 && l == last +1)
58   {
59                     j+=3; p+=3;
60   }
61   else if (st ==1)
62   {
63     j++;
64     p++;
65   }
66   else {
67     j+=2;
68     p+=2;
69   }
70   if (l == last && st == 0)
71                     j = j+1;
72   assert(j==p && l == max) ;
例Ｃ−抽象化コード
【００６１】
この技術は、例Ａに示された例示的なＣコードに関して説明される。これは、ネスト化ループ及びアサーション及び対応する抽象化コードを有する原Ｃコードを示す。assertが内側forループ（例Ａの７〜１２行）の外側にあるので、これは、例Ｂの例示で示されたループ置換を用いて抽象化される。ループは、２つのブロックを有するので２つの反復を有する別のループにより置換される。内側ループは、再帰方程式l + +の一部である１つのIO変数lを有する。従って、それは非決定性の方程式l = l + k1を用いて加速される。ここで、k1には、原ループが取った反復の数を示す非決定性の値が割り当てられる。内側ループ抽象化ボディは、抽象化されたコードの例Ｃにおいて< iloop_absbody >と呼ばれる。
【００６２】
対象のプロパティ、例Ａの２６行におけるアサーションは、外側ループの中にあり、それ故に、帰納が外側ループに適用される。例Ｃにおけるコードの３〜２０行は、assertが帰納法のためにベースケースの最後に維持されるかどうかを検査する。帰納的ステップが２０〜−５４行でコード化されており、ここで、ループはk回実行されたものと推定される。外側ループは、IO変数、l,j およびpを有しており、これらはｋ番目の反復の最後に加速された値l = l0 + k1; j = j0+k2+2*k3+k4+3*k5及びp = p0+k2+2*k3+3*k5をそれぞれ与えられる。k2,k3,k4及びk5は、４２行における「else if」構文、４７行における「else」、５１行における「if」及び３８行における「if」のボディがk反復の最後に実行される回数である。j0およびp0は、それぞれj及びpの初期値である。５３行は、プロパティがk反復の最後に維持されるという推定をコード化している。５５‐７２行は、assertを含む（k + 1）番目の反復をコード化している。
【００６３】
抽象化コードはモデルチェッカーによって上手く検証され、例えば、モデルチェッカーはこの場合は有界モデルチェッカーであってもよい。抽象化コードにおいて、変数j及びpの状態空間は、具象コードにおけるそれのスーパーセットであり、それを妥当な過大近似にする。ループ抽象化プロセスは、このコードを検証するために、３つの変換、即ち、抽象化、加速及び帰納法を全て用いる。対照的に、市販のツール（利用可能なモデルチェッカー、市販の静的解析ツール）はいずれも原コードを検証することができなかった。
【００６４】
プログラムにおけるループ抽象化のための実装が構文的特徴及び／又は方法に固有の言語で記載されているが、添付の請求項は必ずしも記載された特定の特徴又は方法に限定されないことが理解されるべきである。むしろ、特定の特徴及び方法は、ループ抽象化のための例示的な実装として開示されている。
【図１】
0005923636.tif 000009
【図２】
0005923636.tif 000010