(57)【特許請求の範囲】
【請求項１】
ソフトウェアをテストする方法であって、
ソフトウェアプログラムのミックスされたシンボリック実行及び抽象化実行（ミックス実行）の間、前記ソフトウェアプログラムのソフトウェア関数の戻り値のシンボリック値を生成することであって、前記ソフトウェア関数の１つ又は２つ以上のパスは前記戻り値を含み、前記ミックス実行はシンボリック値、及び戻り値が抽象化の範囲内であるように抽象化された抽象化値と、ソフトウェア関数の１つ又は２つ以上の変数の制約とを保持することと、
前記ミックス実行の間、前記シンボリック値の抽象化を、前記抽象化を充足する１つ又は２つ以上のパスの前記戻り値に基づいて派生することであって、前記抽象化は前記シンボリック値を制約することと、
前記ミックス実行の間、前記シンボリック実行の間に探索される１つ又は２つ以上のパスの数が前記抽象化により制約されるように、前記抽象化により制約された前記シンボリック値に基づいて戻り値に対応するソフトウェア関数の１つ又は２つ以上のパスを探索することと、
を含み、
前記パスは、条件命令文、割り当て命令文、方程式、ソフトウェアのコードのライン、ソフトウェアのコードのラインのブロック、及びソフトウェア内部の命令文の少なくとも１つから形成される、方法。
【請求項２】
前記ソフトウェア関数の制御フローに基づいて前記抽象化を修正する、ことを更に含む、請求項１に記載の方法。
【請求項３】
前記制御フローは、データ処理命令、分岐、分岐結合点及びループの１つ又は２つ以上を含む１つ又は２つ以上の命令を含む、請求項２に記載の方法。
【請求項４】
前提が前記シンボリック値を制約するように、前記抽象化に基づいて前記ソフトウェアプログラムの前記シンボリック値の前記前提を生成することと、
前記前提により制約させた前記シンボリック値、及び前記ソフトウェア関数に基づいて宣言関数を生成することと、
前記宣言関数を実行することによって、前記戻り値に対応する前記ソフトウェア関数の１つ又は２つ以上のパスを探索することであって、前記宣言関数の実行は、前記シンボリック実行が前記ソフトウェアプログラムのパスの終端に到達するまで遅延させることと、を更に含む、請求項１に記載の方法。
【請求項５】
前記シンボリック実行の間、前記ソフトウェア関数を前記前提及び前記宣言関数に置き換えることを更に含む、請求項４に記載の方法。
【請求項６】
前記宣言関数を生成することは、前記前提により制約され且つ前記宣言関数を生成する追加引数として前記シンボリック値を加えることによって、前記ソフトウェア関数を拡張することを含む、請求項４に記載の方法。
【請求項７】
前記宣言関数を生成することは、前記宣言関数を生成する他の追加引数として前記ソフトウェア関数に対応するオブジェクトを加えることによって、前記ソフトウェア関数を拡張することを含む、請求項６に記載の方法。
【請求項８】
前記宣言関数を生成することは、前記ソフトウェア関数の戻り命令文をテスト条件が偽のときに関連するパスを終了するテスト命令文に置き換えることを含む、請求項４に記載の方法。
【請求項９】
双方が１つ又は２つ以上の同一の変数にアクセスする宣言関数に基づいて前記宣言関数を他の宣言関数と共に呼び出すことを更に含む、請求項４に記載の方法。
【請求項１０】
１つ又は２つ以上の同一の変数にアクセスする宣言関数に基づいて前記宣言関数を順序付けし且つスケジューリングすることを更に含む、請求項４に記載の方法。
【請求項１１】
前記抽象化は、前記戻り値がブール値であるときのシンボリック述語及び前記シンボリック値の境界を示す区間の１つ又は２つ以上である、請求項１に記載の方法。
【請求項１２】
ソフトウェアをテストする動作をシステムに実行させるプログラムであって、
ソフトウェアプログラムのミックスされたシンボリック実行及び抽象化実行（ミックス実行）の間、前記ソフトウェアプログラムのソフトウェア関数の戻り値のシンボリック値を生成することであって、前記ソフトウェア関数の１つ又は２つ以上のパスは前記戻り値を含み、前記ミックス実行はシンボリック値、及び戻り値が抽象化の範囲内であるように抽象化された抽象化値と、ソフトウェア関数の１つ又は２つ以上の変数の制約とを保持することと、
前記ミックス実行の間、前記シンボリック値の抽象化を、前記抽象化を充足する１つ又は２つ以上のパスの前記戻り値に基づいて派生することであって、前記抽象化は前記シンボリック値を制約することと、
前記ミックス実行の間、前記シンボリック実行の間に探索される１つ又は２つ以上のパスの数が前記抽象化により制約されるように、前記抽象化により制約されたシンボリック値に基づいて戻り値に対応するソフトウェア関数の１つ又は２つ以上のパスを探索することと、
を含み、
前記パスは、条件命令文、割り当て命令文、方程式、ソフトウェアのコードのライン、ソフトウェアのコードのラインのブロック、及びソフトウェア内部の命令文の少なくとも１つから形成される、プログラム。
【請求項１３】
前記動作は、前記ソフトウェア関数の制御フローに基づいて前記抽象化を修正する、ことを更に含む、請求項１２に記載のプログラム。
【請求項１４】
前記動作は、
前提が前記シンボリック値を制約するように、前記抽象化に基づいて前記ソフトウェアプログラムの前記シンボリック値の前記前提を生成することと、
前記前提により制約させた前記シンボリック値、及び前記ソフトウェア関数に基づいて宣言関数を生成することと、
前記宣言関数を実行することによって、前記戻り値に対応する前記ソフトウェア関数の１つ又は２つ以上のパスを探索することであって、前記宣言関数の実行は、前記シンボリック実行が前記ソフトウェアプログラムのパスの終端に到達するまで遅延させることと、を更に含む、請求項１２に記載のプログラム。
【請求項１５】
前記動作は、前記シンボリック実行の間、前記ソフトウェア関数を前記前提及び前記宣言関数に置き換えることを更に含む、請求項１４に記載のプログラム。
【請求項１６】
前記宣言関数を生成することは、前記前提により制約され且つ前記宣言関数を生成する追加引数として前記シンボリック値を加えることによって、前記ソフトウェア関数を拡張することを含む、請求項１４に記載のプログラム。
【請求項１７】
前記宣言関数を生成することは、前記宣言関数を生成する他の追加引数として前記ソフトウェア関数に対応するオブジェクトを加えることによって、前記ソフトウェア関数を拡張することを含む、請求項１６に記載のプログラム。
【請求項１８】
前記宣言関数を生成することは、前記ソフトウェア関数の戻り命令文をテスト条件が偽のときに関連するパスを終了するテスト命令文に置き換えることを含む、請求項１４に記載のプログラム。
【請求項１９】
前記動作は、１つ又は２つ以上の同一の変数にアクセスする宣言関数に基づいて前記宣言関数を順序付けし且つスケジューリングすることを更に含む、請求項１４に記載のプログラム。
【請求項２０】
前記抽象化は、前記戻り値がブール値であるときのシンボリック述語及び前記シンボリック値の境界を示す区間の１つ又は２つ以上である、請求項１２に記載のプログラム。
【発明の詳細な説明】
【技術分野】
【０００１】
本明細書に記載の実施形態は、自動抽象化を包含するシンボリック実行に関する。
【背景技術】
【０００２】
ソフトウェアの認証又は検証のようなソフトウェアのテストは、インフォメーションテクノロジ（information technology、ＩＴ）組織に普及したものである。例えば、ソフトウェアが１つ又は２つ以上のクライアントコンピュータシステムで実行されるデスクトップアプリケーションであるか、又は１つ又は２つのサーバコンピュータシステムで実行されるウェブアプリケーションであるかにかかわらず、ソフトウェアの品質を検証することは多くの場合で重要である。ソフトウェアのいくつかの形式のエラーは、ユーザを苛立たせ、不便を感じさせるだけであるが、他の形式のエラーは、データの損失及び金銭上の損失のような他の問題を引き起こす可能性がある。
【０００３】
シンボリック実行（symbolic execution、記号実行）を使用して、ソフトウェアのテスト入力を生成することによって、ソフトウェアをテストし且つ検証してもよい。しかしながら、シンボリック実行は、比較的簡単なソフトウェアでさえも、いくつかのソフトウェアの状態爆発問題（state explosion problem）に遭遇するおそれがある。状態爆発問題は、シンボリック実行が、対応するテスト入力を生成するために時間を浪費し及び／又は資源を消費するおそれがある。いくつかの例では、状態爆発が要する処理量は、テスト入力の生成において非常に大きくなるおそれがある。
【発明の概要】
【発明が解決しようとする課題】
【０００４】
本明細書の主題は、多くの課題を解決する実施形態、又は上述の課題のような環境においてのみ作動する実施形態に限定されるものではない。むしろ、この背景技術は、本明細書で説明される実施形態が実施できる技術領域の一例を説明するためにのみ提供されるものである。
【課題を解決するための手段】
【０００５】
実施形態の一態様に従うと、ソフトウェアテスト方法は、ソフトウェアプログラムのミックスされたシンボリック（symbolic）実行及び抽象化（abstraction）実行（ミックス実行）の間、ソフトウェアプログラムのソフトウェア関数の戻り値のシンボリック値を生成することを含んでもよい。ソフトウェア関数の１つ又は２つ以上のパスは、戻り値を含んでもよい。加えて、ミックス実行は、シンボリック値、抽象化値及びソフトウェア関数の１つ又は２つ以上の変数の制約（constraints）を保持（maintain）してもよい。また、方法は、ミックス実行の間、シンボリック値の抽象化を派生（deriving）することを含んでもよい。抽象化は、抽象化を充足する１つ又は２つ以上のパスの戻り値に基づいて派生されてもよい。加えて、抽象化は、シンボリック値を制約してもよい。さらに、方法は、ミックス実行の間、抽象化により制約されるように、シンボリック実行の間に探索される１つ又は２つ以上のパスの数が抽象化により制約されるように、シンボリック値に基づいて戻り値に対応するソフトウェア関数の１つ又は２つ以上のパスを探索することを含んでもよい。
【０００６】
実施形態の目的及び利点は、少なくとも特許請求の範囲で具体的に挙げられた構成要素、特徴及び組み合わせによって理解及び達成されることになるであろう。
【０００７】
上述の全般的な説明及び以下の詳細な説明は、典型的且つ説明的なものであり、特許請求の範囲に記載される発明を限定するものではないことが理解されるであろう。
【図面の簡単な説明】
【０００８】
【図１Ａ】ソフトウェアをテストように構成されたシステムの一例を示す図である。
【図１Ｂ】図１Ａに示すテストモジュールを含んでもよい電子デバイスの一例を示す図である。
【図２】遅延シンボリック実行を実行するために使用されるフローの一例を示すフローチャートである。
【図３】抽象化の派生方法の一例のフローチャートである。
【図４】ソフトウェア関数に基づく宣言関数を生成する方法の一例のフローチャートである。
【図５】ソフトウェアのテスト方法の一例のフローチャートである。
【発明を実施するための形態】
【０００９】
例示的な実施形態は、添付図面を使用して更に具体的且つ詳細に記載且つ説明されることになる。
【００１０】
本明細書に記載されるいくつかの実施形態は、ソフトウェアをテストする方法及びそのシステムに関する。いくつかの実施形態において、ソフトウェアをテストするために、ソフトウェアは象徴的、すなわちシンボリックに実行されてもよい。シンボリック実行は、シンボリック形式の数学的方程式及び数式を操作するためにコンピュータのようなマシンを使用して、シンボリック計算から派生するフォーマルなソフトウェア検証技術である。ソフトウェアのテストに適用されるときに、シンボリック実行は、ソフトウェアのソースコードにエラーが発生する場合及び／又はソフトウェアのソースコードにエラーが発生するときを解析して、コード状態が特定の入力及び出力にどのような影響を与えるかを予測し、且つソフトウェア内部のパスのトラバースを検討するために使用されてもよい。
【００１１】
シンボリック実行を使用してソフトウェアをテストするために、シンボリック値は、入力として振る舞うソフトウェアの変数のために生成される。次いで、シンボリック値は、数字、文字列、及び真／偽などのソフトウェアの具体的な入力値に置き換えられてもよい。このような変数を操作するために使用される動作は、シンボリック公式及びシンボリック値を具体的な値の代わりに操作可能なように、動作のシンボリック版に置き換えられてもよい。次いで、ソフトウェアが実行されてもよい。ここで、シンボリック公式及びシンボリック値を解いてもよく、テストケースは、シンボリック公式の解に基づいて、ソフトウェアのために生成されてもよい。
【００１２】
テストされるソフトウェアは、条件命令文、割り当て命令文、方程式、ソフトウェアのコードの他のライン、ソフトウェアのコードのラインのブロック、及び／又はソフトウェア内部の複数の命令文のような１つ又は２つ以上のソフトウェアの命令文から形成される複数のパスを含んでもよい。シンボリック公式は、ソフトウェアに含まれる種々の決定点において生成されてもよいソフトウェアの種々のパスから派生されてもよい。決定点は、入力変数の１つ又は２つ以上の値に基づいて何れのパスが取ってもよいかを示してもよい。このように、入力変数のそれぞれの種々の可能値の数が増加するに従って、典型的なシンボリックエグゼキュータ（symbolic executor）が検索してもよいパスの数は指数的に増加してもよい。これから、比較的少ない数の決定点でさえも、非常に大きな数のパスをもたらす可能性があり、パス爆発問題（path explosion problem、状態爆発問題（state explosion problem）とも称される）をもたらす可能性がある。パス爆発問題は、爆発する可能性があるパスの数が非常に大きな時間浪費、実行困難性及び資源を消費する可能性があるので、従来のシンボリック実行をより大きなプログラムに拡大することは容易ではない。
【００１３】
本明細書に記載される少なくとも１つの実施形態に従って以下に詳細に説明されるように、シンボリック実行は、パス爆発問題が発生する可能性を低減するように、シンボリックエグゼキュータが爆発させるパスの数を低減するために修正されてもよい。例えば、ソフトウェアプログラムのシンボリック実行の間に爆発する可能性があるソフトウェア関数の１つ又は２つ以上のパスは、戻り値を含んでもよい。ソフトウェアプログラムのシンボリック実行の間、戻り値のシンボリック値は、生成されてもよい。加えて、シンボリック値の抽象化は、シンボリック実行の間、ソフトウェアプログラムから派生されてもよい。抽象化は、シンボリック実行の間に爆発するパスの数が抽象化の制約により限定できるように、シンボリック値を制約してもよい。さらに、抽象化は、戻り値が抽象化を充足するように、すなわち戻り値が抽象化の範囲内であるように、１つ又は２つ以上のパスの戻り値に基づいて派生されてもよい。次いで、ソフトウェア関数は、シンボリック実行の間、シンボリック値の前提（assumption）及び宣言関数と置き換えられてもよい。前提は、前提がシンボリック値を制約するように、抽象化に基づいて生成されてもよい。宣言関数は、前提により制約されたシンボリック値に基づいて生成されてもよく、ソフトウェア関数に基づいて生成されてもよい。
【００１４】
次いで、戻り値に対応するソフトウェア関数のパスは、宣言関数を実行することにより検索されてもよい。宣言関数が、前提により制約されたシンボリック値に基づき且つソフトウェア関数に基づくものであるので、宣言関数の実行により検索されるパスは、抽象化を充足するパスに限定することができる。一方、従来のシンボリック実行では、シンボリック値は制約されなくてもよいので、いくつかの不必要なパス（抽象化を充足しない戻り値を有するパスなど）が検索されて、パス爆発問題をもたらすおそれがある。本明細書に記載されるように、爆発するパスの数を低減するシンボリック実行は、「遅延シンボリック実行（lazy symbolic execution）」と称されてもよい。
【００１５】
本発明の実施形態は、添付図面を参照して説明されることになる。
【００１６】
図１Ａは、本明細書に記載される少なくとも１つの実施形態に従って配置され、ソフトウェアをテストするように構成された一例のシステム１００を示す図である。システム１００は、ソフトウェアプログラムのコードアンダーテスト（code under test）１０４に関するシンボリック実行を実行して、ソフトウェアプログラムのテスト結果１０８を生成するように構成されるテストモジュール１０６を含んでもよい。コードアンダーテスト１０４は、例えばソフトウェアプログラム、ソフトウェアプログラムのコード、ライブラリ、アプリケーション、スクリプト、又は処理デバイスが実行するための他の論理又は命令などの電子データを含んでもよい。いくつかの実施形態では、コードアンダーテスト１０４は、ソフトウェアプログラムのコンプリート・インスタンス（complete instance）を含んでもよい。これらの実施形態又は他の実施形態では、コードアンダーテスト１０４は、ソフトウェアプログラムの一部を含んでもよい。コードアンダーテスト１０４は、特に、Ｊａｖａ（登録商標）、Ｃ、Ｃ＋＋、Ｐｅａｒｌ、Ｓｃｈｅｍｅ又はＰｙｔｈｏｎのような適当な形式のコンピュータ言語で書き込まれてもよい。
【００１７】
コードアンダーテスト１０４は、いくつかのソフトウェアモジュールで構造化されたソフトウェアプログラムの一部を含んでもよい。ソフトウェアモジュールは、ソフトウェアモジュールの特定の機能を実行するコードを含んでもよい。特定の機能を実行するコードは、ソフトウェア関数と称されてもよい。
【００１８】
テストモジュール１０６は、コードアンダーテスト１０４に対して遅延シンボリック実行を実行するように構成されてもよい。遅延シンボリック実行の間、テストモジュール１０６は、コードアンダーテスト１０４の可能なパスを決定するように構成されてもよい。可能なパスは、制約の組を包含し又は生み出してもよく、テストモジュール１０６は、制約を解く試みを実行するように構成されてもよい。制約が互いの前後関係で解くことができるとき、対応するパスは、充足可能であると決定できる。制約が互いの前後関係で解くことができないとき、対応するパスは、充足可能でないと決定できる。このような決定に基づいて、コードアンダーテスト１０４の特定のパスに対応する部分を充足できる部分、エラーを含む部分、又は充足可能性に関して不明な部分として識別してもよい。
【００１９】
テストモジュール１０６が実行する遅延シンボリック実行は、解かれてもよい制約の数を低減できるように、検索されてもよいパスの数を低減してもよい。したがって、遅延シンボリック実行は、コードアンダーテスト１０４の充足性の決定に含まれる処理の量を低減することができる。いくつかの実施形態では、テストモジュール１０６は、図２、３、４及び５のそれぞれに対応して以下に詳細に説明されるフロー２００並びに方法３００、４００及び５００に従って遅延シンボリック実行を実行してもよい。
【００２０】
いくつかの実施形態において、テストモジュール１０６は、コードアンダーテスト１０４をテストすることにより、テスト結果１０８を生成してもよい。テスト結果１０８は、コードアンダーテスト１０４の一部が充足可能であるか又は充足可能でないかを決定することを示してもよい。これらの実施形態又は他の実施形態では、テストモジュール１０６は、制約が充足可能であるときに、１つ又は２つ以上の組の制約に対して１つ又は２つ以上の解を生成してもよい。いくつかの実施形態において、一組の制約を解くことは、組に含まれる全ての制約を充足する１つ又は２つ以上の解を見出す試みを実行することを含んでもよい。これらの実施形態のいくつかでは、テストモジュール１０６は、テスト結果１０８を有する解を含んでもよい。いくつかの実施形態では、解を使用して、コードアンダーテスト１０４をテストしてもよい。
【００２１】
図１Ｂは、本明細書に記載される少なくとも１つの実施形態に従って、テストモジュール１０６を含んでもよい一例の電子デバイス１０２を示す図である。電子デバイス１０２は、テストモジュール１０６を使用してコードアンダーテスト１０４をテストするように構成された適当な装置、機器又はデバイスを含んでもよい。電子デバイス１０２は、メモリ１１２に通信可能に結合されたプロセッサ１１０を含んでもよい。いくつかの実施形態において、テストモジュール１０６は、プロセッサ１１０が実行するためにメモリ１１２に常駐する論理又は命令に統合されてもよい。
【００２２】
プロセッサ１１０は、適切な特定用途のコンピュータ及び汎用のコンピュータ、若しくは種々のコンピュータハードウェア又はソフトウェアを含むコンピュータエンティティ又は処理装置を含んでもよく、コンピュータが読み取り可能な適切な媒体に格納された命令を実行するように構成されてもよい。例えば、プロセッサ１１０は、マイクロプロセッサ、マイクロコントローラ、デジタル信号処理（ＤＳＰ）、特定用途向け集積回路（ＡＳＩＣ）、フィールドプログラマブルゲートアレイ（ＦＰＧＡ）又はプログラムの命令を解釈及び／又は実行する及び／又はデータを処理するように構成された他のデジタル回路又はアナログ回路を含んでもよい。図１Ｂには単一のプロセッサとして記載されているものの、プロセッサ１１０はいくつもの操作を実行するように構成されたいくつものプロセッサを含んでもよい。いくつかの実施形態では、プロセッサ１１０は、プログラム命令を解釈及び／又は実行し及び／又はメモリ１１２に記憶されたデータを処理してもよい。
【００２３】
メモリ１１２は、コンピュータ実行可能な命令又はデータ構造を格納して運搬又は所有するコンピュータ読み取り可能な媒体を含んでもよい。コンピュータ読み取り可能な媒体は、汎用コンピュータ又は特定用途コンピュータによりアクセスできる入手可能な媒体であってもよい。限定されない例示では、コンピュータが読み取り可能な媒体は、ランダムアクセスメモリ（ＲＡＭ）、リードオンリメモリ（ＲＯＭ）、電気的に消去可能なプログラマブルリードオンリメモリ（ＥＥＰＲＯＭ）、コンパクトディスクリードオンリメモリ（ＣＤ−ＲＯＭ）又は他の光学ディスク記憶装置、磁気ディスク記憶装置又は他の磁気記憶デバイス、フラッシュメモリデバイス（固体メモリデバイス等）又は所望のプログラムコードをコンピュータが実行可能な命令又はデータ構造で運搬又は格納するために使用され、汎用コンピュータ又は特定用途コンピュータによりアクセス可能な他の記憶媒体又は一時的でないコンピュータ読み取り可能な記憶媒体であってもよい。また、上述の機器を組み合わせたものは、コンピュータ読み取り可能な媒体に含まれてもよい。例えば、コンピュータ読み取り可能な命令は、プロセッサ１１０が特定の関数又は一群の関数を実行する命令及びデータを含んでもよい。
【００２４】
テストモジュール１０６は、プロセッサ１１０が遅延シンボリック実行を実行するように構成された命令及びデータを含んでもよい。このように、電子デバイス１０２は、テストモジュール１０６と協働して、コードアンダーテスト１０４をテストするために、遅延シンボリック実行を実行してもよい。上述のように、テストモジュール１０６は、従来のシンボリック実行と比較して、遅延シンボリック実行の間に検索されるパスの数を低減することができるように構成されてもよい。
【００２５】
図２は、本明細書に記載される少なくとも１つの実施形態に従う遅延シンボリック実行の実行に使用してもよい一例のフロー２００のフローチャートである。フロー２００は、適当なシステム、機器又はデバイスで実行されてもよい。例えば、図１Ｂの電子デバイス１０２のテストモジュール１０６は、フロー２００に関連する動作の１つ又は２つ以上を実行してもよい。個別のブロックとして説明されるものの、種々のブロックは、所望の実装に依存して、付加的なブロックに分割されてもよく、より少ないブロックに組み合わされてもよく、削除されてもよい。
【００２６】
フロー２００は、図１Ａのコードアンダーテスト１０４のようなコードアンダーテストとして動作してもよいソフトウェアプログラムの１つ又は２つ以上の部分のシンボリック実行の間に実行されてもよい。フロー２００は、実行されるシンボリック実行が遅延シンボリック実行であるように構成されてもよい。フロー２００は、ソフトウェアプログラムに含まれる１つ又は２つ以上のソフトウェア関数に対して一連の動作を実行するように構成されてもよい。説明のために、フロー２００は、同時又は異なるタイミングで何れかの数のソフトウェア関数に提供されてもよいとの了解の下で、ソフトウェア関数２０２に対して記載される。説明される実施形態では、フロー２００の動作は、抽象化フェーズ２０４、宣言実装フェーズ２１０及び実行フェーズ２１４において実行されてもよい。
【００２７】
抽象化フェーズ２０４は、抽象化派生２０６、及び前提生成２０８を有してもよい。抽象化派生２０６は、遅延シンボリック実行の間に検索されるソフトウェア関数２０２のパスを制約するために抽象化を使用するように、ソフトウェア関数２０２の１つ又は２つ以上のシンボリック値を制約してもよい抽象化を派生するように構成されてもよい。
【００２８】
いくつかの実施形態では、抽象化派生２０６の間、ソフトウェア関数２０２の１つ又は２つ以上の変数及び値のそれぞれは、ソフトウェア関数２０２のシンボリック実行の間に、シンボリック値及び関連する抽象化を与えられてもよい。与えられるシンボリック値及び関連する抽象化の１つ又は２つ以上は、ソフトウェア関数２０２に含まれてもよい戻り値のためであってもよい。
【００２９】
抽象化は、関連するシンボリック値の値が何であるかに対する制約又は制限であってもよい。いくつかの例では、抽象化は、関連するシンボリック値の範囲に関する境界であってもよい区間（interval）であってもよい。他の例では、区間がシンボリック値を制約するために適切でないようなときでは、抽象化は、シンボリック値を制限してもよいシンボリック述語（symbolic predicate）であってもよい。ここで、シンボリック述語は、「ｐ」が真の場合に「ｑ」もまた真であることを示す形式「ｐ⇒ｑ」であってもよい。また、区間又はシンボリック述語としての抽象化の例は、以下に含まれる。
【００３０】
遅延シンボリック実行の抽象化派生２０６の間、ソフトウェア関数２０２の制御フローは、抽象化値を通って、抽象化値の派生及びリファイン（refine）のために使用される。制御フローは、ソフトウェア関数２０２の種々の命令に対する種々の型の処理動作を生成してもよい１つ又は２つ以上の命令を含んでもよい。抽象化のリファインは、ソフトウェア関数２０２の種々の命令に関連してもよい種々の型の処理動作に基づくものであってもよい。例えば、命令は、データ処理命令、分岐点（branch point）、分岐結合点（branch merge point）及び／又はジャンプ（jump）に関連してもよい。加えて、ソフトウェア関数２０２の１つ又は２つ以上のパスの戻り値の抽象化は、戻り値が抽象化を規定することを補助するために使用されてもよいように、制御フロー及び戻り値から派生されてもよい。このように、抽象化は、戻り値が充足するように、すなわち戻り値が抽象化の範囲にあるように戻り値に基づくものであってもよい。抽象化派生２０６に関する更なる詳細は、図３を参照して以下に説明される。
【００３１】
抽象化フェーズ２０４は、前提生成２０８もまた含む。前提生成２０８は、抽象化派生２０６と同時に実行されてもよく、抽象化派生２０６の後に実行されてもよい。前提生成２０８の間、前提は、ソフトウェア関数２０２の戻り値に関連するシンボリック値のために生成されてもよい。前提は、戻り値の可能値（potential value）の範囲の前提であってもよく、戻り値及び関連するシンボリック値に対応する抽象化から生成されてもよい。前提生成２０８に対する更なる詳細は、図３を参照して更に説明される。
【００３２】
図３を参照して更に詳細に説明されるように、抽象化フェーズ２０４は、ソフトウェア関数２０２の変数のシンボリック値及び関連する抽象化値を保持して、ミックスされたシンボリック実行及び抽象化実行（以下、ミックス実行とも称する）を実行してもよい。例えば、ソフトウェア関数２０２の変数「ｖ」について、抽象化フェーズ２０４は、変数「ｖ」に対応してもよいシンボリック値「ｖs」及び抽象化値「ｖa」の双方を派生し且つ更新してもよい。加えて、抽象化フェーズ２０４の間、「ｖs」及び「ｖa」の制約は保持されてもよく、「ｖs」及び「ｖa」の制約を使用して抽象化的実行を制御してもよい。例えば、シンボリック値「ｖs」を使用して分岐実現可能性（branch feasibility）を決定してもよく、抽象化値「ｖa」を使用してループの終端を決定してもよい。
【００３３】
抽象化フェーズ２０４に続いて、フローは、宣言実装フェーズ２１０に進んでもよい。宣言実装フェーズ２１０の間、宣言関数（declarative function、ＤＦ）は、宣言関数生成２１２を介してソフトウェア関数２０２のために生成されてもよい。宣言関数生成２１２は、ソフトウェア関数に基づいて宣言関数を生成してもよく、前提生成２０８の間に生成された前提により制約されてもよい戻り値に関連するシンボリック値に基づいて宣言関数を生成してもよい。例えば、宣言関数は、宣言関数がソフトウェア関数の変更であるように、ソフトウェア関数２０２の追加引数（extra argument）として戻り値に関連するシンボリック値を追加することで、ソフトウェア関数２０２を拡張することによって、生成されてもよい。これらの実施形態又は他の実施形態では、ソフトウェア関数２０２に対応するオブジェクトは、オブジェクトが宣言関数に含まれるソフトウェア関数の付加的な拡張になるように、他の引数として宣言関数に加えられてもよい。宣言関数生成２１２に対する更なる詳細は、図４を参照して更に説明される。
【００３４】
フロー２００の遅延シンボリック実行は、抽象化フェーズ２０４及び宣言実装フェーズ２１０に続いて、実行フェーズ２１４に進んでもよい。いくつかの実施形態において、実行フェーズ２１４は、抽象化実行２１６及び宣言関数実行２２０を含んでもよい。
【００３５】
いくつかの実施形態では、実行フェーズ２１４は、宣言関数スケジューリング２１８を更に含んでもよい。抽象化実行２１６は、前提生成２０８の間に生成されてもよい１つ又は２つ以上の前提を実行することを含んでもよい。抽象化実行２１６において実行される前提は、ソフトウェア関数２０２に関連してもよく、異なるソフトウェア関数に関連してもよい。いくつかの実施形態では、抽象化実行２１６は、抽象化に関連する関数が呼び出されたときに、関連する抽象化を実行してもよい。抽象化実行２１６が対応する関数のパスの終端に到達すると、フロー２００は、宣言関数実行２２０に進んでもよい。
【００３６】
宣言関数実行２２０は、宣言関数生成２１２の間に生成された１つ又は２つ以上の宣言関数を実行することを含んでもよい。宣言関数実行２２０で実行される宣言関数は、ソフトウェア関数２０２に関連してもよく、他のソフトウェア関数に関連してもよい。こうして、関数の主部（関連する宣言関数に含まれてもよい）は、抽象化実行のパスの終端において実行されるように遅延されてもよい。前提及び宣言関数の実行は、ソフトウェア関数２０２を含むソフトウェアプログラムのテスト結果２２２を生成するために使用されてもよい。いくつかの実施形態では、テスト結果２２２は、図１Ａを参照して説明されるテスト結果１０８に類似していてもよい。
【００３７】
前提及び宣言関数の実行は、ソフトウェア関数２０２又は他のソフトウェア関数の実行の代わりに実行されてもよい。上述のように、前提及び宣言関数は、ソフトウェア関数２０２又は他のソフトウェア関数に基づいて派生されてもよい。このように、ソフトウェア関数２０２又は他のソフトウェア関数は、前提及び前提との関連を制限することにより制約されてもよい前提及び宣言関数の実行によって探索されてもよい。一方、従来のシンボリック実行は、何らかの制約なしにソフトウェア関数を探索してもよい。
【００３８】
宣言関数スケジューリング２１８は、宣言関数を実行する順序を決定するように構成されてもよく、２つ以上の宣言関数があるときに使用されてもよい。いくつかの例では、複数の宣言関数は、同一の変数へのアクセスの共有に基づいて相互に対応して依存してもよい。加えて、依存する宣言関数は、宣言館関数の１つ又は２つ以上のパスが探索に不適切になってもよいように、共有する変数の間での対立により互いに対立してもよい。例えば、第１の宣言関数の変数に関連するパスは、第１の宣言関数に依存する第２の宣言関数の同一の変数に対して対立するために実施不可能になってもよい。
【００３９】
少なくとも１つの実施形態に従うと、宣言関数は、互いに対応して依存する宣言関数が依存に従った群で実行されるように、依存に基づいて順序付けられ且つスケジューリングされてもよい。このように、互いに対応して依存する宣言関数の間で対立が見出されたときに、対立する関数に依存し且つ実行されていない残りの宣言関数は、対立が見つかっているので、スキップされてもよい。これにより、このような宣言関数のスケジューリングは、検索された実行不可能なパスの量を及び実行されてもよい対応する不必要な処理を低減することができる。宣言関数スケジューリング２１８に対する更なる詳細は、図５を参照して更に説明される。
【００４０】
このように、フロー２００を使用して、コードアンダーテスト（ソフトウェア関数２０２等）の遅延シンボリック実行を実行して、従来のシンボリック実行の間に探索されてもよいパスの数と比較して、探索されてもよいパスの数を低減することができる。探索されてもよいパスの数を低減することによって、従来のシンボリック実行と比較してコードアンダーテストの遅延シンボリック実行の間に実行されてもよい処理の量を低減でき、パス爆発の可能性を低減することができる。
【００４１】
図３は、本明細書に記載される少なくとも１つの実施形態に従って配置された抽象化を派生する一例の方法３００のフローチャートである。いくつかの実施形態では、方法３００は、図１Ａ及び１Ｂのテストモジュール１０６のようなテストシステムにより実装されてもよい。加えて、いくつかの実施形態では、方法３００を使用して図２のフロー２００の抽象化フェーズ２０４に関連する１つ又は２つ以上の動作を実行してもよい。個別のブロックとして説明されるものの、種々のブロックは、所望の実装に依存して、付加的なブロックに分割されてもよく、より少ないブロックに組み合わされてもよく、削除されてもよい。
【００４２】
方法３００は、ソフトウェア関数が読み出されるブロック３０２で開始してもよい。例えば図２のソフトウェア関数は、ブロック３０２において読み出されてもよい。抽象化フェーズ２０４は、抽象化情報の一部をそれぞれが計算してもよい複数の実行ラウンドを含んでもよい。いくつかの実施形態では、全体の実行は、更なる抽象化情報が取得できなくなるときに終了してもよい。初期ラウンドは、第１命令からのソフトウェア関数２０２を実行してもよい。より多くのラウンドは、実行の間に生成されてもよい。それぞれのラウンドでは、現在の命令が実行されてもよく、次の命令は、現在の命令が実行されたときに実行されることになる。
【００４３】
ブロック３０４において、ソフトウェア関数の現在の命令「insr」は、読み出されてもよい。現在の命令「instr」は、ソフトウェア関数のミックス実行の間のソフトウェア関数により移動するときに、テストモジュールにより遭遇されてもよい次の命令であってもよい。ブロック３０６において、現在の命令がデータ処理命令に関連するか否かを決定してもよい。現在の命令がデータ処理命令に関連するとき、方法３００は、ブロック３０６からブロック３０８に進む。
【００４４】
ブロック３０８において、シンボリック値及び関連する抽象化値は、データ処理命令に基づいて、生成され且つ派生されてもよい。いくつかの実施形態において、変数は、抽象化値と同様にシンボリック値を与えてもよい。シンボリック値は、現在のパス条件の下でのこの変数の正確な値を記録し、抽象化値は現在のパス条件の下でのこの変数の近似値を示す。抽象化値は、区間、ポリゴン（polygon）又は他のいくつかの幾何学的ドメイン（geometry domain）により示すことができる。次いで、抽象化値及び抽象化値の制約は、「抽象化」とも称される。すなわち、抽象化は、変数の可能な抽象化値を特定するだけではなく、抽象化値に対応するこれらの変数の間の関係をも示す。例えば、データ処理命令は、変数「ｃ」及び「ａ」を含んでもよく、シンボリック値「ｃs」及び「ａs」は、変数「ｃ」及び「ａ」にそれぞれ割り当てられてもよい。加えて、抽象化値「ｃa」及び「ａa」は、変数「ｃ」及び「ａ」にそれぞれ割り当てられてもよい。
【００４５】
加えて、ブロック３０８において、現在の命令がデータ処理命令に関連するとき、対応する抽象化及びシンボリック値は、データ処理命令により示される関係に基づいてリファインされてもよい。例えば、データ処理命令は、シンボリック値「ｃs」及び「ａs」を使用してシンボリック式「ｃs＝ａs＋１０」が生成されるように、「ｃ＝ａ＋１０」にしてもよい。加えて、抽象化値「ａa」は、先に派生されていてもよい「ａa＝［ｉ，ｊ］」として規定される区間であってもよい。このように、データ処理命令「ｃ＝ａ＋１０」において、抽象化値「ｃa」は、抽象化値「ａa＝［ｉ，ｊ］」で示されるシンボリック値「ａs」の境界に基づき、且つデータ処理命令「ｃ＝ａ＋１０」の変数「ａ」と関連するシンボリック値「ａs」との関係及び変数「ｃ」と関連するシンボリック値「ｃs」との関係に基づいて「ｃs＝［ｉ＋１０，ｊ＋１０］」として規定されるように更新されてもよい。ブロック３０８に次いで、方法３００は、先の命令に続いてもよい他の命令が現在の命令として読み出されてもよいブロック３０４に戻ってもよい。
【００４６】
現在の命令がデータ処理命令に関連しないとき、方法３００は、ブロック３０６からブロック３１０に進んでもよい。ブロック３１０において、現在の命令がソフトウェア関数の分岐点であるか否かが決定されてもよい。現在の命令がソフトウェア関数の分岐点であるとき、方法３００は、ブロック３１０からブロック３１２に進んでもよい。
【００４７】
ブロック３１２において、分岐点で第１パスに分岐するソフトウェア関数に関連する抽象化は、リファインされてもよい。命令が分岐点に関連するとき、対応する抽象化の１つ又は２つ以上は、分岐点から発生してもよい種々のパスに関連する条件を有する抽象化の交点によりリファインされてもよい。例えば、命令「ｉｆ（ｃ＞１０）」において、ソフトウェア関数は、第１パス条件「ｃ＞１０」に合致したときに第１パスに分岐してもよく、第２パス条件「ｃ≦１０」に合致したときに第２パスに分岐してもよい。このようにブロック３１２において、第１パスに関連する第１抽象化値「ｃa」の第１表示「ｃa1」は、以下の式「ｃa1＝ｃa∩［１１，＋∞］」による第１パス条件に対してリファインされてもよい。
【００４８】
ブロック３１２において、いくつかの実施形態では、望ましくは（抽象化値「ｃa」よりもむしろ）シンボリック値「ｃs」を使用して「Ｃ＞１０」が充足可能であるか否かを決定してもよい。例えば、分岐条件の前に「ｃs＝５」であり且つ「ｃa＝［０，２０］」であるとする。この例では、条件「Ｃ＞１０」は、シンボリック値「ｃs」に関しては充足可能ではなくてもよく、抽象化値「ｃa」を使用した場合は充足可能であってもよい。一方、抽象化値は、計算の終了を許可するように分岐制御ループのために使用してもよい。また、このミックスされたシンボリック実行及び抽象化実行（「ミックス実行」とも称される）機構は、正確性と効率性との間の良好なバランスを取得することができる。
【００４９】
ブロック３１３において、第１パスは、第１パスが第２パスに結合されてもよい結合点まで実行されてもよい。結合点は、第１パス及び第２パスが合流する制御フローグラフの第１ノード、すなわち制御フローグラフの第１ポストドミネータ（post-dominator）であってもよい。例えば、「ｉｆ−ｅｌｓｅ」命令文に続く次の命令文は、第１パス及び第２パスの分岐結合点を示してもよい。他の例は、ループの繰り返しが合流するループヘッダである。
【００５０】
ブロック３１４において、第２パスに関連する新たなラウンドは、生成され且つスケジューリングされてもよい。例えば、パス条件「ｃ≦１０」に関連する新たなラウンドは、パス条件「ｃ＞１０」の実行が終了した後に実行されるように生成され且つスケジューリングされてもよい。双方は、結合点で１つのラウンドに結合されるように、結合点で後に同期されてもよい。
【００５１】
ブロック３１５において、分岐点で第２パスに分岐するソフトウェア関数に関連する抽象化の１つ又は２つ以上は、リファインされてもよい。例えば、上述のように、命令「ｉｆ（ｃ＞１０）」において、ソフトウェア関数は、第２パス条件「ｃ≦１０」に合致したときに、第２パスに分岐してもよい。また、第２パスに関連する抽象化値「ｃa」の第２表示「ｃa2」は、以下の式「ｃa2＝ｃa∩［−∞，１０］」による第２パス条件に対してリファインされてもよい。ブロック３１６において、第２パスは、結合点まで実行されてもよい。
【００５２】
ブロック３１７において、分岐結合点において結合する第１パス及び第２パスに関連する抽象化の第１表示及び第２表示は、結合に基づいてリファインされてもよい。いくつかの実施形態において、抽象化は、抽象化の第１表示と抽象化の第２表示との共用体（union）により結合されてもよい。例えば、分岐結合点における抽象化値「ｃa」は以下の式「ｃa＝ｃa1∪ｃa2」によってリファインされてもよい。ブロック３１６に続いて、方法３００は、現在の命令に続く他の命令が現在の命令として読み出されるブロック３０４に戻ってもよい。
【００５３】
いくつかの実施形態において、分岐の抽象化は、「ｐ」は「ｑ」であることを示す形式「ｐ⇒ｑ」の述語として保持されてもよい。例えば、分岐結合点において、第１パスの「ｃa」における抽象化は「ｃ＞１０⇒ｃa＝ｃa1」として保持されてもよく、第２パスの抽象化は「ｃ≦１０⇒ｃa＝ｃa2」として保持されてもよい。これらの述語は、関連するパス条件と同様に抽象化値を記載してもよい。いくつかの実施形態では、これらの述語を使用して、パス条件を除外することにより、組み合わせ抽象化値「ｃa＝ｃa1∪ｃa2」を取得してもよい。
【００５４】
現在の命令がブロック３１０における分岐点に関連しないとき、方法３００は、ブロック３１０からブロック３１８に進んでもよい。ブロック３１８において、現在の命令が「ｊｕｍｐ」命令であるか否かが決定されてもよい。現在の命令がジャンプ（jump）命令であるとき、方法３００は、ブロック３１８からブロック３２０に進む。
【００５５】
ブロック３２０において、変数の先の抽象化値は、ジャンプ命令の後にこの変数の現在の抽象化値を含む又は組み込むかを決定してもよい。先の抽象化値がジャンプ命令の後に、現在の抽象化値を含まない又は組み込まないときは、方法３００は、ブロック３２０からブロック３０４に進んでもよい。先の抽象化値がジャンプ命令の後に、現在の抽象化値を含む又は組み込むときは、方法３００は、ブロック３２０からブロック３２２に進んでもよい。
【００５６】
例えば、ジャンプ命令は、整数である変数「ｉ」がある数よりも少ない間に続いてもよい「ｗｈｉｌｅ」ループに関連してもよい。本実施例では、「ｗｈｉｌｅ」ループの終端において、変数「ｉ」は、「ｗｈｉｌｅ」ループに再び入る前にインクリメントされてもよい。加えて、変数「ｉ」は、変数「ｉ」がインクリメントされたときに更新されてもよい、関連する抽象化値「ｉa」を有してもよい。更新された抽象化値「ｉa」は、「ｉa」の先の抽象化値が現在の抽象化値「ｉa」を含む又は組み込んでもよいように、インクリメントのために先の抽象化値「ｉa」のサブセットであってもよい。一例では、抽象化値「ｉa」は、インクリメントに遭遇する前に区間「［ａ，ｂ］」であってもよく、インクリメントに遭遇したとき、抽象化値「ｉa」は、抽象化値「ｉa」が区間「［ａ＋１，ｂ］」になってもよいように、インクリメントに基づいて更新されてもよい。このように、この具体的な例に対して、ブロック３２０において、先の抽象化値「ｉa」は、区間「［ａ＋１，ｂ］」が区間「［ａ，ｂ］」の内部にあるので、現在の抽象化値「ｉa」を含む又は組み込むことを決定してもよい。
【００５７】
ブロック３２２において、ジャンプに関連するミックス実行は、先の抽象化が現在の抽象化を組み込むときに、抽象化は更にリファインされなくてもよいので、停止されてもよい。この場合、ミックス実行の現在のラウンドは、抽象化値の固定点がこのラウンドにおいて到達しているので、終了してもよい。次いで、エグゼキュータは、利用可能な次のラウンドを実行してもよい（例えば、方法３００を使用して）。エグゼキュータにラウンドが残っていないとき、全体の抽象化フェーズは上述のように終了してもよい。
【００５８】
現在の命令がブロック３１８において「ｊｕｍｐ」に関連しないとき、方法３００は、ブロック３１８からブロック３２４に進んでもよい。ブロック３２４において、現在の命令が「ｒｅｔｕｒｎ」命令であるか否かを決定してもよい。現在の命令が「ｒｅｔｕｒｎ」命令であるとき、方法３００は、ブロック３２４からブロック３２６に進んでもよい。ブロック３２６において、「ｒｅｔｕｒｎ」命令の戻り値に対応する抽象化のための前提が生成されてもよい。いくつかの実施形態では、ブロック３２６は、図２のフロー２００の前提生成２０８の一部であってもよい。いくつかの実施形態では、戻り値に対応する抽象化は、ブロック３２６において生成されてもよく、次いで対応する前提が生成されてもよい。これらの実施形態又は他の実施形態において、１つ又は２つ以上の他の動作は、ブロック３２６において抽象化の生成と、対応する過程の生成との間の１つ又は２つ以上の他の命令に応じて実行されてもよい。戻り値に対応する抽象化は、戻り値に適用可能な適当な形式を有するように生成されてもよい。
【００５９】
例えば、戻り値は整数であってもよく、戻り値の抽象化は区間「［ａ，ｂ］」であってもよく、戻り値に関連するシンボリック値は「ｉ」であってもよい。これら上述のプロパティに基づいて、ブロック３２６における前提生成は、「ａ」と「ｂ」との間のシンボリック値「ｉ」を制約する前提命令を生成してもよい。一例では、前提生成２０８は、「ａ」と「ｂ」との間のシンボリック値「ｉ」を制約する以下の命令「＿ａｓｓｕｍｕ（ｉ＞＝ａ＆＆ｉ＜ｂ）」を生成してもよい。
【００６０】
他の例のように、戻り値がブール値であるときに、対応する抽象化はシンボリック述語であってもよく、前提はシンボリック述語に基づいてもよい。例えばソフトウェア関数２０２は、以下のコードのラインを含んでもよい。
【００６１】
【数１】
0006648413.tif 000002
【００６２】
ここで、「ｓ１．ｌｅｎ」が「ｓ２．ｌｅｎ」に等しくないとき、戻り値は、続くシンボリック述語式が抽象化「ｓ１．ｌｅｎ！＝ｓ２．ｌｅｎ⇒ｒｅｔｖａｌ＝ｆａｌｓｅ」として使用されるように、偽であってもよい。上述のコードに基づいて、前提生成２０８に関連する以下のコードが生成されてもよい。
【００６３】
【数２】
0006648413.tif 000003
【００６４】
上述のコードにおいて、「ｂ」は戻り値のシンボリック値であってもよく、シンボリック述語としての抽象化は、前提「＿ａｓｓｕｍｅ（ｓ１．ｌｅｎ＝＝ｓ２．ｌｅｎ｜｜〜ｂ）」が生成されてもよいように、「ｓ１．ｌｅｎ＝＝ｓ２．ｌｅｎ」又は「ｂ」が偽であってもよい。ブロック３２６に続いて、方法３００はブロック３０４に戻ってもよい。
【００６５】
ブロック３２４において、現在の命令が「ｒｅｔｕｒｎ」命令でないとき、方法３００はブロック３２８に進んでもよい。ブロック３２８において、他の命令の型は、意味に従って取り扱われてもよい。
【００６６】
このように、方法３００を使用して、本明細書に記載される少なくとも１つの実施形態に従って抽象化を派生し且つ前提を生成してもよい。方法３００を特定の関数と共に使用する方法の一例は、以下に表１及び２を参照して説明される。当業者は、方法３００で実行される関数は異なる順序で実装されてもよいことを理解するであろう。また、概略的なステップ及び動作のみが一例として提供され、開示される実施形態の本質を損なうことなく、ステップ及び動作のいくつかは、付加的であり、組み合わせてより少ないステップ及び動作にしてもよく、付加的なステップ及び動作に拡張されてもよい。例えば、コードのラインは、２つ以上の形式の命令である２つ以上の命令を含んでもよい。このように、２つ以上の命令の形式は、コードの１つのラインのために方法３００に従って通過し且つ処理されてもよい。
【００６７】
図４は、本明細書に記載される少なくとも１つの実施形態に従って配置された、ソフトウェア関数（例えば、図２のソフトウェア関数２０２）に基づく宣言関数を生成する一例の方法４００のフローチャートである。方法４００は、いくつかの実施形態では、図１Ａ及び１Ｂのテストモジュール１０６のようなテストシステムによって実装されてもよい。加えて、いくつかの実施形態では、方法４００を使用して、図２のフロー２００の宣言実装フェーズ２１０に関連する１つ又は２つ以上の動作を実行してもよい。個別のブロックとして説明されるものの、方法４００の種々のブロックは、所望の実装に依存して、付加的なブロックに分割されてもよく、より少ないブロックに組み合わされてもよく、削除されてもよい。
【００６８】
方法４００は、関数「ｆ」を受信してもよいブロック４０２において開始されてもよい。例えば、図２のソフトウェア関数２０２は、ブロック４０２で受信されてもよい。ブロック４０４において、「ｌａｚｙ」関数「ｌａｚｙ＿ｆ」は、関数「ｆ」に基づいて宣言されてもよい。例えば、「ｌａｚｙ＿ｆ」は、宣言され且つ「ｆ」と実質的に同一の制御フローを有するように形成されてもよい。
【００６９】
ブロック４０６において、１つ又は２つ以上の引数は、「ｌａｚｙ＿ｆ」に加えられてもよい。いくつかの実施形態において、「ｌａｚｙ＿ｆ」は、「ｆ」のコピーとして開始されてもよく、引数は、「ｌａｚｙ＿ｆ」が拡張を提供する加えられた引数によって「ｆ」を拡張するものであってもよいように、「ｌａｚｙ＿ｆ」に加えられてもよい。いくつかの実施形態では、「ｆ」の戻り値に関連するシンボリック値は、「ｌａｚｙ＿ｆ」の引数として加えられてもよい。これらの実施形態又は他の実施形態では、「ｆ」に関連するオブジェクトもまた「ｌａｚｙ＿ｆ」の引数として加えられてもよい。特定の関数に対する引数を加える一例は、以下に図３を参照して説明される。
【００７０】
ブロック４０８において、（「ｆ」の戻り命令文であってもよい）「ｌａｚｙ＿ｆ」の１つ又は２つ以上の「ｒｅｔｕｒｎ」命令文は、「＿ｔｅｓｔ」命令文及び対応する「ｒｅｔｕｒｎ」命令文にそれぞれ置き換えられてもよい。いくつかの実施形態では、「ｌａｚｙ＿ｆ」の「ｒｅｔｕｒｎ」命令文のそれぞれは、「＿ｔｅｓｔ」命令文及び対応する「ｒｅｔｕｒｎ」命令文に置き換えられてもよい。「＿ｔｅｓｔ」命令文は、エグゼキュータに関連する述語（predicate）が偽である場合に現在のパスを停止するように命令してもよい。
【００７１】
戻り命令文を置き換える一例は、先に示したように表３を参照して以下に説明される。ブロック４０８に続いて、「ｌａｚｙ＿ｆ」は、「ｆ」の対応する宣言関数として使用してもよい。
【００７２】
このように、方法４００を使用して、本明細書に記載される少なくとも１つの実施形態に従ってソフトウェア関数に基づく宣言関数を生成してもよい。当業者は、方法４００で実行される関数は異なる順序で実装されてもよいことを理解するであろう。また、概略的なステップ及び動作のみが一例として提供され、開示される実施形態の本質を損なうことなく、ステップ及び動作のいくつかは、付加的であり、組み合わせてより少ないステップ及び動作にしてもよく、付加的なステップ及び動作に拡張されてもよい。
【００７３】
以下は、表１に示すソフトウェア関数「ｉｎｔ  ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」（以下、関数「ｉｎｔ  ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」）に対する抽象化フェーズ（図２の抽象化フェーズ２０４等）及び宣言実装フェーズ（図２の宣言実装フェーズ等）のアプリケーションの一例である。
【００７４】
【表１】
0006648413.tif 000004
【００７５】
表１のライン２のコードは、関数「ｉｎｔ  ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」を規定し、ライン１のコードは、関数「ｉｎｔ  ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」は、文字列オブジェクト「ｓ」を含んでもよいことを規定する。表１のライン３及び４は、割り当て命令文であってもよい関数「ｉｎｔ  ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」の命令文を含む。この割り当て命令文は、図３のブロック３０６及び３０８を参照して説明したようにシンボリック値及び関連する抽象化を派生するために処理されるデータ処理命令であってもよい。例えば、シンボリック値「ｓ．ｌｅｎ」及び関連する抽象化値「ｌｅｎa」は、上掲のコードのライン３の命令文「ｉｎｔ  ｌｅｎ＝ｔｈｉｓ．ｌｅｎｇｔｈ（）」から、以下の式「ｌｅｎ＝ｓ．ｌｅｎ」及び「ｌｅｎ＝［ｓ．ｌｅｎ，ｓ．ｌｅｎ］」によって派生し規定されてもよい。加えて、シンボリック値「ｐｏｓs」及び関連する抽象化値「ｐｏｓa」は、ライン４の命令文「ｉｎｔ  ｐｏｓ＝ｐｏｓ＞ｌｅｎ？ｌｅｎ：ｐｏｓ；」から、以下の式「ｐｏｓs＝ｐｏｓs＞ｓ．ｌｅｎ？ｓ．ｌｅｎ：ｐｏｓs」及び「ｐｏｓa＝［−∞，ｓ．ｌｅｎ］」によって派生し規定されてもよい。
【００７６】
上掲のコードのライン５は、図３のブロック３１０、３１２、３１３、３１４、３１５及び／又は３１６に対して説明されたような１つ又は２つ以上のシンボリック値及び抽象化を更に派生し規定するために使用される分岐点であってもよい「ｆｏｒ」ループのための命令を含んでもよい。加えて、ライン５は、ライン５に対して実行されてもよいブロック３０６および３０８に関連する１つ又は２つ以上の動作のようなデータ処理命令であってもよい割り当て命令文を含んでもよい。ライン５に対して、「ｐｏｓ」が「０」以下のときに「ｆｏｒ」ループに入らないように第１パスが発生してもよい命令「ｆｏｒ（ｉｎｔ  ｋ＝ｐｏｓ；ｋ＞０；−−ｋ）」から２つの異なるパスが生じてもよい。加えて、第２パスは、「ｐｏｓ」が０より大きいときに「ｆｏｒ」ループに入るように発生してもよい。それぞれのパスは、ミックス実行ラウンドで実行されてもよい。２つの実行ラウンドは、ライン５の結合点で同期されてもよい。
【００７７】
「ｐｏｓ」が「０」以下のとき、ライン５の「ｆｏｒ」ループは無視されてもよく、第１パスとして、コードは、「−１」の戻り値が生成されるライン９に進んでもよい。いくつかの実施形態では、第１シンボリック戻り値「ｒｅｔｖａｌs1」は、第１パスに関連するパス条件「ｐｏｓ＜＝０」が充足されるときに対応する「−１」の戻り値に基づいて（方法３００のブロック３２６のように）派生し規定されてもよい。いくつかの実施形態では、第１シンボリック戻り値「ｒｅｔｖａｌs1」及び第１抽象化戻り値「ｒｅｔｖａｌa1」は、「ｒｅｔｖａｌs1＝−１」及び「ｒｅｔｖａｌa1＝［−１、−１］」のように派生し規定されてもよい。
【００７８】
「ｐｏｓ」が「０」より大きいとき、ライン５の「ｆｏｒ」ループは、第２パスとして入ってもよい。加えて、１つ又は２つ以上のシンボリック値及び関連する抽象化は、ライン５に含まれる「ｆｏｒ」ループに入ることに関連する命令、条件及び規定に基づいて生成され及び／又はリファインされてもよい。例えば、「ｆｏｒ」ループに入ることに関連するパス条件「ｐｏｓ＞０」において、シンボリック値「ｐｏｓs」に関連する抽象化値「ｐｏｓa＝［−∞，ｓ．ｌｅｎ］」は、以下の式「ｐｏｓa［−∞，ｓ．ｌｅｎ］∩「１，＋∞」＝［１，ｓ．ｌｅｎ］によってリファインされてもよい。加えて、シンボリック値「ｋs」は、ライン５の式「ｉｎｔ  ｋ＝ｐｏｓ」から以下の式「ｋs＝ｐｏｓs」によってリファインされてもよい。また、シンボリック値「ｋs」に関連する抽象化値「ｋa」は、式「ｋs＝ｐｏｓs」から派生し規定されてもよく、抽象化値「ｐｏｓa」のリファインは、以下の式「ｋa＝ｐｏｓa＝［１，ｓ．ｌｅｎ］」によってもよい。
【００７９】
ライン５の「ｆｏｒ」ループの内部のライン６は、充足するときに関数「ｉｎｔ  ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」を、「ｋ−１」の戻り値に関連してもよいライン７に進める「ｉｆ」命令文を含む。このように、第２シンボリック戻り値「ｒｅｔｖａｌs2」及び関連する第２抽象化値「ｒｅｔｖａｌa2」は、第２パスに関連するパス条件「ｐｏｓ＞０∧ｓ［ｋ−１］＝＝ｃ」が合致したときに対応する戻り値「ｋ−１」に基づいて派生し且つ規定されてもよい。いくつかの実施形態では、第２シンボリック戻り値「ｒｅｔｖａｌs2」及び関連する第２抽象化値「ｒｅｔｖａｌa2」は、式「ｋa＝ｐｏｓa＝［１，ｓ．ｌｅｎ］」に基づいて派生し且つ規定されてもよく、以下の式「ｒｅｔｖａｌa2＝ｋa−１＝＝［１，ｓｌｅｎ］−１＝［０，ｓ．ｌｅｎ−１］」のようにライン７の命令文「ｒｅｔｕｒｎ  ｋ−１」に基づいて派生してもよい。
【００８０】
ライン５の「ｆｏｒ」ループによって、表１に含まれる関数「ｉｎｔ  ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」は、ライン７の後にライン５にジャンプして戻ってもよい。このように、いくつかの実施形態では、方法３００のブロック３１８及び３２２に関連する１つ又は２つ以上の動作は、ライン５にジャンプして戻ったことに応じて実行されてもよい。加えて、ライン５に含まれる他の命令の形式に関連する方法３００の１つ又は２つ以上の動作は、実行されてもよい。
【００８１】
例えば、動作「−−ｋ」及び「ｋ＝ｐｏｓ」は、「ｆｏｒ」ループの次の繰り返しが実行されてもよいように実行されてもよい。関数「ｉｎｔ  ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」のライン５のパス条件「ｋ＞０」、動作「−−ｋ」のデクリメント、及び式「ｋ＝ｐｏｓ」により、「ｆｏｒ」ループに留まる（及びそれによって第２パスに入る）ために、デクリメントの後のパス条件は、「ｐｏｓ−１＞０」として表されてもよい。このように、抽象化値「ｋa」は、「ｐｏｓ−１＞０」のパス条件に基づいてリファインされてもよく、「ｋa＝ｐｏｓa＝［１，ｓ．ｌｅｎ］」の先の式から「ｋa＝ｐｏｓa＝［２，ｓ．ｌｅｎ］」の次の式にリファインされてもよい。「ｋa」（［２，ｓ．ｌｅｎ］）の次の抽象化値は、固定点が「ｆｏｒ」ループに関して到達し、「ｆｏｒ」ループの拡張及び「ｆｏｒ」ループに関連する抽象化値の対応する規定、派生及び／又はリファインが終了してもよいように、「ｋa」（［１，ｓ．ｌｅｎ］）の先の抽象化値に組み込まれてもよい。
【００８２】
「ｆｏｒ」ループの主体の終了及び「ｆｏｒ」ループからの終了のソートによる「ｆｏｒ」ループのスキップは、第１パス及び第２パスが結合される関数「ｉｎｔ  ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」の結合点に対応してもよい。このように、第１及び第２戻り抽象化は、共同体動作によって連結されて、以下に示す「ｒｅｔｖａｌa＝ｒｅｔｖａｌa1∪ｒｅｔｖａｌa2＝［０，ｓ．ｌｅｎ−１］∪［−１，ｓ．ｌｅｎ−１］＝［−１，ｓ．ｌｅｎ−１］」のように、シンボリック戻り値「ｒｅｔｖａｌs」の戻り抽象化値「ｒｅｔｖａｌa」を生成してもよい。
【００８３】
前提は、図３のブロック３２６を参照して説明したように、戻り抽象化値「ｒｅｔｖａｌa」に基づいて生成されてもよい。例えば、以下の表２は、戻り抽象化値「ｒｅｔｖａｌa」に基づいて前提を生成する例が示される表１のソフトウェア関数「ｉｎｔ  ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」のコードと共に挿入されてもよいコードを含む。このコードは、遅延シンボリック実行の間にフロー２００の抽象化実行２１６のステップにおいて使用されてもよい。
【００８４】
【表２】
0006648413.tif 000005
【００８５】
表２に関連する例において、表２のライン５のコードは、戻り抽象化値「ｒｅｔｖａｌa」に基づいて新たなシンボリック戻り値「ｉ」を生成してもよい。加えて、ライン６において戻り抽象化値「ｒｅｔｖａｌa」の区間「［−１，ｓ．ｌｅｎ−１］」に基づいて「ｉ」の前提を生成してもよい。
【００８６】
表２に関連するコードは、表１に関連する関数「ｉｎｔ  ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」に基づいてもよい宣言関数への呼び出しを含んでもよい。例えば、表２のライン７のコードは、表１で説明される関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」に基づき且つ表２のライン１で呼び出されてもよい宣言関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ＿ｉｍｐ」を呼び出すための前提を使用してもよい。表２のライン１及び７の間の比較によって示されるように、宣言関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ＿ｉｍｐ」は、関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」に比較して付加的な入力引数としてシンボリック戻り値「ｉ」及びオブジェクト「＊ｔｈｉｓ」を含んでもよい。宣言関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ＿ｉｍｐ」の宣言及び生成は、表３を参照して以下により詳細に説明される。
【００８７】
オリジナルの関数において、命令文「ｒｅｔｕｒｎ．．．」は、値を戻す。抽象化において、この値は、追加の引数「ｉ」として関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ＿ｉｍｐ」に注入されるシンボリック戻り値「ｒｅｔｖａｌs」により示されている。この宣言関数は、「ｒｅｔｖａｌs」が正しい値を戻すように「ｉ」に関して戻り値を制約することによってこの情報をエンコードする。例えば、命令文「ｒｅｔｕｒｎ−１」は「＿ｔｅｓｔ（ｉ＝＝−１）；ｒｅｔｕｒｎ」により置き換えられ、命令文「ｒｅｔｕｒｎ  ｋ−１」は「＿ｔｅｓｔ（ｉ＝＝ｋ−１）；ｒｅｔｕｒｎ」により置き換えられる。ここで、「＿ｔｅｓｔ」は条件を充足しないパスを中止することをエグゼキュータに通知することで、「＿ｔｅｓｔ（Ｉ＝＝−１）」は戻り値が−１であるもののみを通す。
【００８８】
【表３】
0006648413.tif 000006
【００８９】
上述のように、表３は、本明細書に記載される少なくとも１つの実施形態に従って、宣言関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ＿ｉｍｐ」を宣言し且つ規定するために使用されてもよい。いくつかの実施形態では、表３のコードは、図４を参照して説明された方法４００に基づいて生成されてもよい。例えば、表３のライン１のコードは、図４のブロック４０４を参照して説明されたように宣言関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ＿ｉｍｐ」を「ｌａｚｙ」関数として宣言してもよい。加えて、ライン２のコードは、宣言関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ＿ｉｍｐ」の入力として使用されてもよい引数を規定してもよい。入力は、関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」の入力、シンボリック戻り値「ｉ」の入力「ｉ」及び関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」に関連してもよい文字列オブジェクト「ｓ」の入力「ｓ」を含んでもよい。このように、入力「ｉ」及び入力「ｓ」は、図４のブロック４０６を参照して説明したように、関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」の引数と比較して宣言関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ＿ｉｍｐ」に付加的な引数として加えられてもよい。
【００９０】
ライン６及び８は、表１のライン７及び９に見出すことができる関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」に戻り命令文の「＿ｔｅｓｔ」命令文を挿入する。このように、関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」の戻り命令文は、図４のブロック４０８を参照して説明したように、宣言関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ＿ｉｍｐ」において置き換えられてもよい。
【００９１】
このように、抽象化及び対応する宣言関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ＿ｉｍｐ」は、表１〜３を参照して説明される方法３００及び４００に対応する１つ又は２つ以上に従って、関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」のために生成されてもよい。上述の記載は、方法３００及び４００に関して説明する概念の使用及び動作を説明する単なる例であり、限定されるものではない。いくつかの異なる抽象化及び宣言関数は、方法３００及び４００で説明される概念を使用していくつかの異なる関数のために派生されてもよい。
【００９２】
図５は、本明細書に記載される少なくとも１つの実施形態に従って配置された、宣言関数のスケジューリング実行の一例の方法５００のフローチャートである。方法５００は、いくつかの実施形態では、図１Ａ及び１Ｂのテストモジュールのようなテストシステムによって実装されてもよい。加えて、いくつかの実施形態では、方法５００は、図２のフロー２００の宣言関数スケジューリング２１８に関連する１つ又は２つ以上の動作を実行するために使用されてもよい。個別のブロックとして説明されるものの、方法５００の種々のブロックは、所望の実装に依存して、付加的なブロックに分割されてもよく、より少ないブロックに組み合わされてもよく、削除されてもよい。
【００９３】
方法５００は、宣言関数の組（図５において「ＤＦｓ」として示される）が受信されてもよいブロック５０２において開始してもよい。ブロック５０４において、宣言関数の組の宣言関数の依存性は決定されてもよい。依存性は、何れの変数が同一の宣言関数によってアクセスされてもよいかを決定することにより決定されてもよい。ここで、同一の変数の１つ又は２つ以上にアクセスする宣言関数は、依存すると考えてもよい。いくつかの実施形態では、依存性は、標準データフロー解析（standard data-flow analysis）によって決定されてもよい。
【００９４】
ブロック５０６において、宣言関数は、依存性に基づいて群に分割されてもよい。例えば、第１変数にアクセスする全ての宣言関数は第１群に分割されてもよく、第２変数にアクセスする全ての宣言関数は第２群に分割されてもよい。
【００９５】
ブロック５０８において、宣言関数は、個々の群に従って実行されてもよい。例えば、上述の第１群に関連する宣言関数は、上述の第２群に関連する宣言関数の前に実行されてもよい。加えて、群に不一致が見つかったときに、その群の実行されていない残りの宣言関数は実行されなくてよい。これにより、遅延シンボリック実行の間に探索される必要がなくてもよいパスの数は削減することができる。
【００９６】
このように、方法５００は、遂行してもよい実行の量は削減することができる方法で宣言関数をスケジューリングし且つ実行するために使用してもよい。当業者は、方法５００で実行される関数は異なる順序で実装されてもよいことを理解するであろう。また、概略的なステップ及び動作のみが一例として提供され、開示される実施形態の本質を損なうことなく、ステップ及び動作のいくつかは、付加的であり、組み合わせてより少ないステップ及び動作にしてもよく、付加的なステップ及び動作に拡張されてもよい。
【００９７】
例えば、以下の表４は、計算集中関数（computation intensive function）「ｈａｓｈ」と共に、文字列動作関数「ｆｉｎｄ＿ｌａｓｔ＿ｏｆ」及び「ｃｏｎｔａｉｎｓ」を読み出すコードを含む。第１前提は、文字列「ｓ１」は文字「／」を含むことをアサートし、第２前提は「ｓ１」が「／」を含まないことを要求するので、コードは、有効なテストケースを作り出すことはない。このため、全ての実行パスは、無益である。文字列「ｓ１」の長さがｌｅｎであると仮定する。宣言関数スケジューリングが使用されない場合、エグゼキュータは、それぞれが高価な「ｈａｓｈ」関数を実行するＯ（２len+len+m）のパスを訪れることになる。宣言関数スケジューリングにより、「ｓ１．ｃｏｎｔａｉｎｓ（”／”）」の宣言関数は、これら２つの宣言関数は共通の変数を共有しないように宣言関数の命令文「ｈａｓｈ（ｉ１）」の前に実行するために順序付けされてもよい。このように、この例では、エグゼキュータは、Ｏ（２len+len）のパスを訪れることにより、２m回の向上が導き出される。より重要なことに、高価なｈａｓｈ＿Ｄ１は実行されなくてよい。
【００９８】
【表４】
0006648413.tif 000007
【００９９】
本明細書で使用されるとき、用語「モジュール（module）」又は「コンポーネント（component）」は、コンピューティングシステムの汎用ハードウェア（例えば、コンピュータが読み取り可能な媒体、処理デバイス等）により格納及び／又は実行してもよいモジュール又はコンポーネント及び／又はソフトウェアオブジェクト又はソフトウェアルーティーンの動作を実行するように構成される特定のハードウェア実装を称してもよい。いくつかの実施形態において、本明細書に記載される異なるコンポーネント、モジュール、エンジン及びサービスは、コンピューティングシステムで（異なるスレッドとして）実行されるオブジェクト又は処理として実装されてもよい。本明細書に記載されるシステム及び方法のいくつかは、全般的に、（汎用ハードウェアに格納及び／又は実行される）ソフトウェア実装され、特定のハードウェア実装又ソフトウェア実装及びハードウェア実装の組み合わせが可能であり、予想される。本明細書において、「コンピューティングエンティティ（computing entity」は、本明細書で先に規定したコンピューティングシステム、若しくはいずれかのモジュール又はコンピューティングシステムで走るモジュールの組み合わせのようなコンピューティングシステムとしてもよい。
【０１００】
明細書で引用される全ての例及び条件的な言語は、教育的な目的を意図したものであり、技術を進歩させるため発明者が貢献した発明及び概念を読み手が理解することを支援するためのものであり、具体的に引用された例及び条件に限定されることなく解釈されるものである。本開示の実施形態を詳細に説明してきたが、本開示の精神及び範囲を逸脱することなく、種々の変化、置換、変更が可能であることを理解すべきである。
【図１Ａ】
0006648413.tif 000008
【図１Ｂ】
0006648413.tif 000009
【図２】
0006648413.tif 000010
【図３】
0006648413.tif 000011
【図４】
0006648413.tif 000012
【図５】
0006648413.tif 000013