(57)【特許請求の範囲】
【請求項１】
１つ以上の計算装置によって実行される方法であって、
１つ以上のループを有するＣ＋＋関数を記号的実行用に最適化するステップであり、各ループに対し、該ループ内に分岐条件が存在する場合に、該分岐条件を該ループの外側に移動させるように該ループを書き換えることを有する、最適化するステップ、
を有し、
前記Ｃ＋＋関数は１つ以上の条件付き分岐を更に有し、当該方法は更に、
各条件付き分岐に対し、前記Ｃ＋＋関数の解釈を該条件付き分岐まで遅延させるように、中間言語を用いて記号表現を構築するステップ、
を有する、
方法。
【請求項２】
１つ以上のプロセッサによって実行可能な命令を有するメモリと、
前記メモリに結合されて前記命令を実行可能な前記１つ以上のプロセッサであり、前記命令を実行するときに、
１つ以上のループを有するＣ＋＋関数を記号的実行用に最適化し、ここで、該最適化は、各ループに対し、該ループ内に分岐条件が存在する場合に、該分岐条件を該ループの外側に移動させるように該ループを書き換えることを有する、
ように動作する前記１つ以上のプロセッサと、
を有し、
前記Ｃ＋＋関数は１つ以上の条件付き分岐を更に有し、前記１つ以上のプロセッサは、前記命令を実行するときに更に、各条件付き分岐に対し、前記Ｃ＋＋関数の解釈を該条件付き分岐まで遅延させるように、中間言語を用いて記号表現を構築するように動作する、
システム。
【請求項３】
ソフトウェアを格納したコンピュータ読み取り可能記憶媒体であって、前記ソフトウェアは１つ以上のコンピュータシステムによって実行されるときに、
１つ以上のループを有するＣ＋＋関数を記号的実行用に最適化し、ここで、該最適化は、各ループに対し、該ループ内に分岐条件が存在する場合に、該分岐条件を該ループの外側に移動させるように該ループを書き換えることを有する、
ように動作し、
前記Ｃ＋＋関数は１つ以上の条件付き分岐を更に有し、前記ソフトウェアは１つ以上のコンピュータシステムによって実行されるときに更に、各条件付き分岐に対し、前記Ｃ＋＋関数の解釈を該条件付き分岐まで遅延させるように、中間言語を用いて記号表現を構築するように動作する、
コンピュータ読み取り可能記憶媒体。
【発明の詳細な説明】
【技術分野】
【０００１】
この開示は、概して、コンピュータソフトウェアのテスト及び検証を行うことに関し、より具体的には、記号的実行及び自動テスト生成を用いて、Ｃ、Ｃ＃又はＣ＋＋で記述されたコンピュータソフトウェアのテスト及び検証を行うことに関する。
【背景技術】
【０００２】
コンピュータソフトウェアを検証あるいは点検することは、ソフトウェア開発者及びユーザの間での共通の関心事である。一本のソフトウェアが、例えば、１つ以上のクライアントコンピュータシステムでのインストール及び実行のためのデスクトップアプリケーション、又は１つ以上のサーバコンピュータシステムでの実行のためのウェブアプリケーションの何れであろうと、それが正しく機能することを保証するために、そのソフトウェアの品質を注意深く検証することが重要である。例えばバグなど、ソフトウェアにおける一部の種類の間違いは、ソフトウェアのユーザに苛立たしさ又は不便さを感じさせ、ソフトウェアにおける他の一部の種類の間違いは、場合によって機関にかなりの金銭的損失をも生じさせるような、より深刻な問題を生じさせる可能性がある。
【０００３】
ソフトウェアテストは、ソフトウェアの品質を検証する一般的な方法である。ソフトウェアテストを用いて、解析されるソフトウェア又はその１つ以上の部分が、改訂又は修正の後ごとに回帰テストを受け、出力がその正しさに関して評価される。しかしながら、ソフトウェアテストはしばしば、限られた網羅率（カバレッジ）を提供するのみであり、コーナーケースのバグを見落としがちである。形式的検証（formal  verification）はこれらの問題を解決する傾向がある。形式的検証は、解析対象ソフトウェアに関する具体的な要求の充足可能性を数学的に証明し、あるいは、該要求に違反するテストケースの形態で反例を取得し、ひいては、バグを指し示す。
【０００４】
ソフトウェアアプリケーションは任意の数のモジュールを含むことができ、各モジュールが個々にテストあるいは検証され、あるいは、複数のモジュールが組み合わせてテストあるいは検証される。ソフトウェアモジュールは、手動あるいは自動的にテストあるいは検証され得る。手動の場合、人（例えば、ソフトウェアテストエンジニア）が、ソフトウェアモジュールのテストケースを該モジュールの設計仕様に基づいて手作業で設計し、該テストケースの下で該モジュールを実行し、テストケースに合致しないモジュール挙動又は出力を調べる。自動の場合、コンピュータソフトウェア又はハードウェアとして実装されたソフトウェアテストツールが、解析対象のソフトウェアモジュールのテストケースを自動生成し、テストケースをシミュレートしながらモジュールを実行し、テストケースに合致しないモジュール挙動又は出力を調べ得る。
【発明の概要】
【発明が解決しようとする課題】
【０００５】
特定の実施形態によれば、記号的実行を用いてＣ＋＋プログラムを検証するためにライブラリを最適化する方法及びシステムが開示される。
【課題を解決するための手段】
【０００６】
特定の実施形態は、１つ以上のループを有するＣ＋＋関数を記号的実行用に最適化する。この最適化は、各ループに対し、該ループ内に分岐条件が存在する場合に、該分岐条件を該ループの外側に移動させるように該ループを書き換えることを有する。
【図面の簡単な説明】
【０００７】
【図１】一例に係るソフトウェアモジュールについて記号的実行を行うステップを表す実行フロー例を示す図である。
【図２】記号的実行を用いてソフトウェアプログラムを検証するソフトウェアアーキテクチャの一例を示す図である。
【図３】記号的実行を用いてソフトウェアプログラムを検証する方法の一例を示す図である。
【図４Ａ】スタック関数の一例を示す図である。
【図４Ｂ】バイトスワッピングの一例を示す図である。
【図５】一例に係るネットワーク環境を示す図である。
【図６】一例に係るコンピュータシステムを示す図である。
【発明を実施するための形態】
【０００８】
特定の実施形態は、Ｃ、Ｃ＃、又はＣ＋＋で記述されたコンピュータソフトウェアの記号的実行（symbolic  execution）及び自動テスト生成を提供する。より具体的には、特定の実施形態は、Ｃ、Ｃ＃、又はＣ＋＋で記述されたコンピュータソフトウェアの形式的検証を行うための記号的実行・自動テスト生成ツールを提供する。特定の実施形態において、Ｃ、Ｃ＃又はＣ＋＋プログラム（例えば、ソフトウェアアプリケーション又はモジュール）は、低水準仮想機械（Low  Level  Virtual  Machine；ＬＬＶＭ）バイトコードへとコンパイルされ、その後、該プログラムを記号的に実行するために、軽量なＣ又はＣ＋＋ライブラリに動的に結び付けられる（リンクされる）。特定の実施形態において、余分なパス（path）を回避し且つインハウス（社内）解決を支援するため、低水準ライブラリ（例えば、ＰＯＳＩＸ  Ｃライブラリ及びＣ＋＋ライブラリ）が実装される。特定の実施形態において、処理時間を短縮するため、例えば文字列、整数又はベクトルなどの一般的に使用されるデータ構造用の効率的なソルバーが提供される。特定の実施形態において、例えばデータベースアクセスなどのドメインスペシフィック操作の処理を最適化するために、特定のハンドラーが使用される。特定の実施形態において、記号的実行・自動テスト生成ツールは、記号的長さを有するデータ構造をサポートするとともに、高い網羅率を保証するテストケースを自動的に生成し、伝統的なテストツールでは割愛されるＣ、Ｃ＃又はＣ＋＋プログラム内のバグを明らかにすることができる。
【０００９】
ソフトウェアアプリケーションは、しばしば、多数のソフトウェアモジュールに編成され、各ソフトウェアモジュールは特定の機能を実行するコードを含み得る。典型的な状況において、ソフトウェアモジュールは任意数の入力変数又は出力変数を有し得る。ソフトウェアモジュールが呼び出されるとき、該ソフトウェアモジュールの入力変数に割り当てられた値として、（該ソフトウェアモジュールを呼び出したコードによって、）実際の入力値が該ソフトウェアモジュールに渡され得る。該ソフトウェアモジュールのコードが、上記実際の入力値に関して実行され得る。最終的に、該ソフトウェアモジュールの出力変数の実際の出力値が決定されて、該ソフトウェアモジュールによって（例えば、該ソフトウェアモジュールを呼び出したコードへ）返され、この時点で該ソフトウェアモジュールはその実行を完了する。また、ソフトウェアモジュールのコードによって決定される実際の出力値は、通常、その呼び出し時に該ソフトウェアモジュールに渡される実際の入力値に依存する。さらに、ソフトウェアモジュールは任意数のローカル変数を有していてもよい。ローカル変数は中間変数とも呼ばれ、その値も直接的あるいは間接的に入力変数の値に依存し得る。ローカル変数はローカルな範囲を有する。ローカル変数は、それが宣言されたソフトウェアモジュールのコンテキスト内でのみ存在し、該コンテキスト内からのみアクセス可能である。対照的に、ソフトウェアモジュールが属するソフトウェアアプリケーションは任意数のグローバル変数を有し得る。グローバル変数は、ソフトウェアアプリケーション内のグローバルな範囲を有し、そのソフトウェアアプリケーションに属する全てのソフトウェアモジュールにアクセス可能である。或るソフトウェアモジュールが呼び出されるとき、該ソフトウェアモジュールはグローバル変数の値にアクセスしたり、該値を変更したりすることができ、該値の変更は、該ソフトウェアモジュールがその実行を完了した後にも維持される。
【００１０】
特定の実施形態において、第１の変数の値が第２の変数の値に基づいて決定される（すなわち、第１の変数の値が第２の変数の値に依存する）とき、第１の変数は第２の変数に依存すると見なされる。入力若しくは出力の何れであろうと、また、ローカル若しくはグローバルの何れであろうと、変数は通常、以下に限られないが、例えば文字、文字列、整数、浮動小数、ダブル、ブール、ポインタ、配列及び列挙（enumeration）などの、特定のデータ型を有する。変数のデータ型は、どのような種類のデータが（例えば、実際値）がその変数に割り当てられ得るかを指し示す。例えば、整数型を持つ変数には整数値のみが割り当てられるべきであり、ブール型を持つ変数には真−偽値のみが割り当てられるべきである。異なるプログラミング言語は、その特定言語で記述されるソフトウェアモジュール又はアプリケーションの変数が持ち得る異なるデータ型と、その特定のデータ型に適用され得る異なる操作とを定義し得る。
【００１１】
ソフトウェアアプリケーションは形式的にテスト・検証され得る。特定の実施形態において、ソフトウェアアプリケーションの形式的テスト・検証を行うために、該ソフトウェアアプリケーションに含まれる個々のモジュールが形式的にテスト・検証される。特定の実施形態において、ソフトウェアモジュールは記号的実行を用いて形式的にテスト・検証され得る。より具体的には、特定の実施形態は、記号的実行を用いて、ソフトウェアモジュールをテストするために使用するテスト入力値を自動的に生成し得る。解析対象のソフトウェアモジュールがテスト目的で呼び出されるとき、これらのテスト入力値が該ソフトウェアモジュールの入力変数に割り当てられ、これらのテスト入力値に基づいて該ソフトウェアモジュールから得られた出力値が分析されることで、該ソフトウェアモジュールの挙動が決定され、該ソフトウェアモジュールの形式的検証が行われ得る。
【００１２】
コンピュータサイエンスの分野において、記号的実行は、抽象解釈として実際の値ではなく記号的な値を追跡することによるソフトウェアプログラムの解析を意味する。これは、ソフトウェアへの入力を記号変数として扱うノンエクスプリシット状態モデル検査技術である。記号的実行は、記号変数を用いてソフトウェア内の限定された経路の全てを実行することによって複雑な方程式を作成し、ソルバーを用いて該複雑な方程式を解く（典型的に、決定手順として知られる）ことで、もしあれば、誤ったシナリオを得る。エクスプリシット状態モデル検査と異なり、記号的実行は、解析対象ソフトウェアの取り得る全ての入力値、及び取り得る全ての入力値の取り得る全てのユースケースを分析することができる。故に、記号的実行は解析対象ソフトウェアを網羅的に検証することができる。
【００１３】
記号的実行の更なる説明のため、以下の“ｆｏｏ”という名のソフトウェアモジュール例（例えば、Ｃ＋＋で記述されたメソッド）を考える。
（外１）
0005821651.tif 000002
【００１４】
ソフトウェアモジュール“ｆｏｏ”は、２つの入力変数“ａ”及び“ｂ”と、２つのローカル変数“ｃ”及び“ｄ”とを有している。特定の実施形態において、ローカル変数の値は、直接的あるいは間接的に、ソフトウェアモジュールの１つ以上の入力変数の値に依存し得る。例えば、モジュール“ｆｏｏ”では、ローカル変数“ｃ”の値は、上記コードの第３行に指し示されるように、入力変数“ａ”及び“ｂ”の値に直接的に依存し、ローカル変数“ｄ”の値は、上記コードの第５行に指し示されるように、ローカル変数“ｃ”を介して間接的に入力変数“ａ”及び“ｂ”の値に依存する。また、モジュール“ｆｏｏ”は、上記コードの第４行に、“ｉｆ−ｅｌｓｅ”命令文によって引き起こされる条件付き分岐点を含んでいる。第４行の条件付き分岐点は、分岐条件“（ｃ！＝“ｑｒｓ”）”に関連付けられている。この分岐条件が満足される、あるいは成立するかに応じて、すなわち、ローカル変数“ｃ”が“ｑｒｓ”に等しいかに応じて、モジュール“ｆｏｏ”はそれ以降、異なる実行経路へと進み、モジュール“ｆｏｏ”のコードの異なる部分が実際に実行される。より具体的には、ローカル変数“ｃ”が“ｑｒｓ”に等しくない場合には、上記コードの第５及び６行に指し示されるように、ローカル変数“ｄ”の値が計算されて返される。一方、ローカル変数“ｃ”が“ｑｒｓ”に等しい場合には、上記コードの第８行に指し示されるように、ローカル変数“ｃ”の値が返される。
【００１５】
モジュール“ｆｏｏ”について記号的実行が行われるとき、その入力変数及びローカル変数の各々に、実際値に代えて記号値が割り当てられる。図１は、モジュール“ｆｏｏ”について記号的実行を行うステップを表す一例に係る実行フロー１００を示している。この例において、入力変数“ａ”は記号値“ｘ”を割り当てられ、入力変数“ｂ”は記号値“ｙ”を割り当てられ、ローカル変数“ｃ”は記号値“ｚ”を割り当てられ、ローカル変数“ｄ”は記号値“ｗ”を割り当てられている。変数“ａ”、“ｂ”、“ｃ”及び“ｄ”は“ｓｔｒｉｎｇ”型であるので、記号値“ｘ”、“ｙ”、“ｚ”及び“ｗ”は各々、任意の文字列を表す。
【００１６】
また、“Φ”は、実行経路に沿った様々な点での記号的実行の結果を表す記号表現である。より具体的には、モジュール“ｆｏｏ”のコードの第２行に対応する１０２において、変数“ａ”、“ｂ”、“ｃ”及び“ｄ”にそれぞれの記号値“ｘ”、“ｙ”、“ｚ”及び“ｗ”が割り当てられ、“Φ”は当初、エンプティすなわちヌル表現を有する。この実行が更に進むとき、どのコードが実行されたかに応じて“Φ”に表現が追加される。モジュール“ｆｏｏ”のコードの第３行に対応する１０４において、“Φ”は表現“ｚ＝ｘ＋ｙ”を有している。これは、上記コードの第３行が“ｃ＝ａ＋ｂ”であり、“ｘ”、“ｙ”及び“ｚ”がそれぞれ変数“ａ”、“ｂ”及び“ｃ”に割り当てられた記号値であるからである。次いで、モジュール“ｆｏｏ”のコードの第４行は条件付き分岐点であり、それ以降、この実行が進み得る２つの取り得る実行経路が存在する。故に、記号的実行も１０４から下に、上記コードの第５及び６行に対応する１０６及び１０８を含む第１経路“ＰＡＴＨ１”と、上記コードの第８行に対応する１１０を含む第２経路“ＰＡＴＨ２”という２つの異なる経路に進み得る。
【００１７】
ＰＡＴＨ１を進めるには、変数“ｃ”は“ｑｒｓ”に等しくなく、これは記号値“ｚ”が“ｑｒｓ”に等しくないことを意味する。故に、１０６にて、表現“ｚ！＝“ｑｒｓ””が“Φ”に追加される。逆に、ＰＡＴＨ２を進めるには、変数“ｃ”は“ｑｒｓ”に等しく、これは記号値“ｚ”が“ｑｒｓ”に等しいことを意味する。故に、１１０にて、表現“ｚ＝“ｑｒｓ””が“Φ”に追加される。ＰＡＴＨ１に沿うとき、変数“ｄ”の値は上記コードの第５行にて決定され、これが１０８に対応する。故に、１０８にて、表現“ｗ＝ｚ＋“ｔ””が“Φ”に追加される。なお、“ｚ＝ｘ＋ｙ”であるので、“ｗ”の表現は“ｗ＝ｘ＋ｙ＋“ｔ””に書き直され得る。１０８はＰＡＴＨ１の終点であるので、１０８における“Φ”の表現は、実行経路ＰＡＴＨ１の終点に到達するために満足される必要がある条件を記号の形態で表している。同様に、１１０は実行経路ＰＡＴＨ２の終点であるので、１１０における“Φ”の表現は、ＰＡＴＨ２の終点に到達するために満足される必要がある条件を記号の形態で表している。
【００１８】
モジュール“ｆｏｏ”は２つの取り得る実行経路を有するので、モジュール“ｆｏｏ”を記号的に実行することは、各実行経路に１つの組が対応する二組の表現を生じさせる。特定の実施形態において、１０８での“Φ”の表現を解くことは、モジュール“ｆｏｏ”をＰＡＴＨ１の終点まで到達させる入力変数“ａ”及び“ｂ”の実際値を提供し、また、１１０での“Φ”の表現を解くことは、モジュール“ｆｏｏ”をＰＡＴＨ２の終点まで到達させる入力変数“ａ”及び“ｂ”の実際値を提供し得る。
【００１９】
特定の実施形態において、ソフトウェアモジュールを記号的に実行することから得られる表現（例えば、図１の１０８及び１１０における“Φ”）は、ソルバーを用いて解かれ得る。例えば、記号表現を解くソルバーは、部分的に充足可能性モジュロ理論（Satisfiability  Modulo  Theories；ＳＭＴ）に基づいて実装され得る。特定の実施形態において、ＳＭＴソルバーは、ソフトウェアモジュール内の特定の経路へ進むために満たされる必要がある任意数の制約を含み得る記号表現を入力として取って、記号表現からのそれら全ての制約を満足する１つ以上の解を見出すことを試み得る。何らかの解が見出され得る場合、ＳＭＴソルバーはその解を自身の出力として提供し得る。当然ながら、記号表現が該表現内の全ての制約を満足する解を有しないこともあり、その場合、該表現は充足不可能なもの又は解けないものと見なされる。特定の実施形態において、ＳＭＴソルバーからの出力は、ソフトウェアモジュールの形式的テスト・検証を行うためのテストケースとして使用され得る。
【００２０】
例えば、図１において、１０８における“Φ”はＰＡＴＨ１の表現（“Φ＝｛（ｗ＝ｘ＋ｙ＋“ｔ”）＆（ｚ！＝“ｑｒｓ”）｝”）である。この表現を解くことから得られる解は、モジュール“ｆｏｏ”をＰＡＴＨ１に沿ってテストするためのテストケースとして使用され得る。同様に、１１０における“Φ”はＰＡＴＨ２の表現（“Φ＝｛（ｚ＝ｘ＋ｙ）＆（ｚ＝“ｑｒｓ”）｝”）である。この表現を解くことから得られる解は、モジュール“ｆｏｏ”をＰＡＴＨ２に沿ってテストするためのテストケースとして使用され得る。
【００２１】
上述の例が示すように、記号的実行は、ソフトウェアプログラム又はモジュールの実行を、具体的な入力ではなく記号的な入力の上で開始するソフトウェアプログラム又はソフトウェアモジュールの解析技術であり、記号表現（例えば、図１の“Φ”によって表される記号表現）を用いて、これらの記号入力について、ソフトウェアプログラム又はモジュールへの影響を計算する。記号的実行は、探索するソフトウェアモジュール内の各経路を、複数のブール式の結合として定義される経路条件で特徴付ける。各ブール式は、テスト対象プログラム又はモジュールの別個の経路（例えば、図１に示したＰＡＴＨ１及びＰＡＴＨ２）の実行中に為される１つの分岐決定を表す。実行が完了されるとき、ソフトウェアモジュール内のコードの、その記号入力に関する１つの実現可能な実行経路に各々が対応する複数の経路条件が生成され得る。これらの条件に対する解がテスト入力である。また、記号的実行中に、例えば、メモリの禁止区域アクセス、ゼロ（０）による除算、及びユーザ定義されたアサーションなど、幾つかの整合性（サニティ）特性がチェックされてもよい。故に、記号的実行は、伝統的なテスト手法より遙かに高いプログラム挙動網羅率を達成するという利点を有する。
【００２２】
現在、統計的に型付けされるフリーフォーム型、マルチパラダイム型、コンパイル型の汎用プログラミング言語であるＣ＋＋で記述されたコンピュータソフトウェア用の記号的実行ツールは存在していない。Ｃで記述されたコンピュータソフトウェアに適したものなどの既存の記号的実行ツールは、ライブラリー・アプリケーション・プログラミング・インタフェース（ＡＰＩ）、一般的に使用されるデータ構造用の高速ソルバー、ドメインスペシフィックなハンドラーなどの良好な抽象化の欠如のために効率的でない。これらの問題を解決するため、特定の実施形態は、余分な記号経路を回避し且つソルバー性能を向上させるカスタマイズ実装された低水準ライブラリ（例えば、ＰＯＳＩＸ  Ｃライブラリ及びＣ＋＋ライブラリ）を含み、中間言語（ＩＬ）を使用して一組のアプリケーション特定（application-specific；ＡＳ）操作をモデル化し、且つ解析対象のＣ、Ｃ＃又はＣ＋＋プログラムをＬＬＶＭバイトコードへとコンパイルする、Ｃ、Ｃ＃又はＣ＋＋で記述されたソフトウェアに特に好適な記号的実行・自動テスト生成ツールを提供する。
【００２３】
図２は、記号的実行を用いてソフトウェアプログラムを検証する一例に係るシステム２００を示している。図３は、記号的実行を用いてソフトウェアプログラムを検証する一例に係る方法を示している。図２及び３を互いに関連付けて説明する。特定の実施形態において、システム２００は、Ｃ、Ｃ＃、Ｃ＋＋、又はソースコードがバイトコードへとコンパイルされ得るその他のプログラミング言語（例えば、Ｊａｖａ（登録商標）で記述されたプログラム）を検証するのに好適なものとし得る。バイトコードは、ソフトウェアインタープリタによる効率的な実行のために設計される命令セットの一形態であり、マシンコードへの更なるコンパイルに適している。特定の実施形態において、ソフトウェアプログラムは、任意数のソフトウェアモジュール又は単一のソフトウェアモジュール（例えば、オブジェクト、関数、プロシージャ、又はメソッド）を含んだ完全なソフトウェアアプリケーションとし得る。特定の実施形態において、システム２００は、マシンコードコンパイラ２２１、バイトコードコンパイラ２２２、記号的実行部２２４、ソルバー２２６及びテスター２２８を含むことができ、それら各々が、図３に記載されるステップ群の一部を実行し得る。特定の実施形態において、マシンコードコンパイラ２２１、バイトコードコンパイラ２２２、記号的実行部２２４、ソルバー２２６及びテスター２２８は各々、１つのソフトウェアコンポーネント、１つのハードウェアコンポーネント、又は２つ以上のそのようなコンポーネントの組み合わせとし得る。
【００２４】
或るプログラム２０２を解析する（例えば、記号的実行を用いて形式的に検証する）ことを考える。一例として、さらに、プログラム２０２がＣ＋＋で記述されているとする。プログラム２０２は１つ以上の入力変数を有し得る。特定の実施形態において、各入力変数は記号値を割り当てられ得る。故に、プログラム２０２は記号入力を有する。
【００２５】
典型的に、Ｃ又はＣ＋＋プログラムは、コンパイルあるいは実行されるときに１つ以上のランタイムライブラリを必要とし得る。例えば、これらのライブラリは、Ｃ又はＣ＋＋コンパイラによって提供されるＣライブラリ又はＣ＋＋ライブラリを含み得る。さらに、１つ以上のユーザライブラリが存在してもよい。特定の実施形態において、これらのライブラリは実行時にＣ又はＣ＋＋プログラムに動的にリンクされ得る。ライブラリ２１２が、プログラム２０２によって必要とされる必須ライブラリを含んでいるとする。これはＣライブラリ、Ｃ＋＋ライブラリ、及びユーザライブラリを含み得る。
【００２６】
特定の実施形態において、ステップ３１０に示すように、プログラム２０２及びライブラリ２１２がバイトコードコンパイラ２２２によってコンパイルされ、プログラム２０２のプログラムバイトコード２０４と、ライブラリ２１２のライブラリバイトコード２１４とが生成され得る。特定の実施形態において、バイトコードコンパイラ２２２は、Ｃ＋＋プログラムのソースコードをバイトコードへとコンパイルすることが可能な如何なる好適なＣ＋＋コンパイラであってもよい。例えば、バイトコードコンパイラ２２２はＬＬＶＭコンパイラ（例えば、ＬＬＶＭ−Ｇ＋＋コンパイラ）としてもよく、その場合、プログラムバイトコード２０４及びライブラリバイトコード２１４はＬＬＶＭバイトコードである。
【００２７】
特定の実施形態において、プログラムバイトコード２０４及びライブラリバイトコード２１４は、ステップ３２０に示すように、記号的実行部２２４によって記号的に実行され得る。図１に関して上述したように、記号的実行を介して、ソースコード内の条件付き分岐（例えば、“ｉｆ−ｅｌｓｅ”文）によって生成されるソフトウェアモジュール内の可能な実行経路が個別に分析され、各経路の記号表現が取得され得る。
【００２８】
Ｃ＋＋プログラミング言語はオブジェクトベースの言語（オブジェクト指向プログラミング言語）である。これは、例えばクラスなど、Ｃプログラミング言語では利用可能でない特有の機能を有する。Ｃ＋＋プログラムがバイトコードへとコンパイルされるとき、該バイトコードも、例えばＣプログラムをコンパイルすることから得られるバイトコードでは利用可能でない特有の機能を有する。故に、使用される記号的実行部は、Ｃ＋＋プログラムをコンパイルすることから得られたバイトコードを記号的に実行するために、これらＣ＋＋プログラミング言語特有の機能を取り扱うことができる必要がある。特定の実施形態において、記号的実行部２２４は、Ｃ＋＋の全ての機能と、Ｃ、Ｃ＃又はその他の適用可能なプログラミング言語からの機能とを取り扱うことができる。
【００２９】
特定の実施形態において、プログラムのバイトコードを記号的に実行するとき、マシン実行状態をモデル化するために記号的な状態が使用される。特定の実施形態において、レジスタが具体値又は記号表現を格納する。特定の実施形態において、マシンスタックを模倣して、記号スタックが複数のフレームで構成される。特定の実施形態において、メモリが複数のコンポーネントとして編成され、それらの各々が具体的なアドレスとその値を記録するバイトの配列とを有するようにされる。特定の実施形態において、Ｃ＋＋オブジェクトの複数のフィールドに、連続したメモリブロックが割り当てられる。例えば、或るオブジェクトの２つのフィールドのアドレスがそれぞれｍ１，１及びｍ１，２であるとすると、ｍ１，２＝ｍ１，１＋サイズ（ｆｄ１，１）なる関係が成立する。一方、相異なるオブジェクトのメモリブロックは連続的である必要はなく、（より詳細に後述する）自動サイズ変更をサポートすることができる。以下の例は、各々が多数のフィールドを有する２つのオブジェクトに対するメモリブロック割当てを示している。
【表１】
0005821651.tif 000003
【００３０】
オブジェクトレベルの推論（より詳細に後述する）を支援するため、特定の実施形態において、オブジェクト全体が、該オブジェクトのサイズに等しい幅を有する単一の記号表現によって表され得る。幅を検査することは、記号的実行部（例えば、記号的実行部２２４）の整合性を保証するための重要なアプローチである。特定の実施形態において、ポインタが複数のコンポーネントを参照することができる場合、記号表現を解くときにソルバー（例えば、ソルバー２２６）によって決定される可能な参照ごとに１つの新たな状態が生成される。この方法は、大きいポインツツー（points-to）セットを有するポインタでは高くつき得るものの、典型的なプログラムは単一のコンポーネントを参照する記号ポインタを使用するのみであり、その場合の最適化となり得る。
【００３１】
特定の実施形態において、記号的実行部２２４はプログラムバイトコード２０４及びライブラリバイトコード２１４を解釈（インタープリット）する。特定の実施形態において、例えば多様性（ポリモルフィズム）及びテンプレートなどの大抵のＣ＋＋機能は、バイトコードコンパイラ２２２（例えば、ＬＬＶＭ−ＧＣＣコンパイラ）によって取り扱われる。しかしながら、Ｃ＋＋プログラムはＣプログラムより遙かに複雑であるため、これは、記号的実行部２２４によって取り扱われる必要がある追加のＬＬＶＭ命令（主として、ＬＬＶＭ組込関数（イントリンシック））を導入し得る。特定の実施形態において、記号的実行部２２４は、これら追加のＬＬＶＭ命令を取り扱うために、幾つかの拡張命令を実行し得る。実際には、１５個より多いそのような拡張命令が存在し得る。例えば、図４Ａに示すように、ｌｌｖｍ．ｓｔａｃｋｓａｖｅイントリンシックを用いて関数スタックの現在状態が記憶され、それがｌｌｖｍ．ｓｔａｃｋｒｅｓｔｏｒｅによって復元される。他の一例として、図４Ｂに示すように、３つのｌｌｖｍ．ｂｓｗａｐ命令が整数値を偶数のバイトでバイト交換する。記号的実行部２２４はこれらの命令を実行することができ、これらの命令の実行はそれらのセマンティクス（意味）に従う。
【００３２】
Ｃ＋＋プログラミング言語は、例外を提起して対処する組込サポートを提供している。外部例外コールを伴う８個のｌｌｖｍ．ｅｈ命令が、正しい例外セマンティクスで解釈される必要がある（例えば、Ｃ＋＋における例外処理はスタック上に例外を伝播する）。特定の実施形態において、例外を表現するために、特定のデータ構造が記号的実行部２２４によって使用される。記号的実行部２２４は、例外テーブルを構築し、例外命令をそれらのセマンティクスに従って解釈する。実際には、およそ１０個のそのような例外が存在し得る。
【００３３】
特定の実施形態において、記号的実行部２２４は、多数のアトミック操作及び同期化イントリンシックを含むＣ＋＋メモリモデルを使用する。例えば、ｌｌｖｍ．ｍｅｍｏｒｙ．ｂａｒｒｉｅｒは、メモリアクセスタイプの特定の対の間での順序付けを保証し、ｌｖｍ．ａｔｏｍｉｃ．ｌｏａｄ．ａｄｄはアド及びストアをアトミックに実行する。特定の実施形態において、記号的実行部２２４を用いて、これらのイントリンシックは複数の操作をシリアル化することによって実現される。例えば、ａｔｏｍｉｃ．ｃｍｐ．ｓｗａｐは、比較操作とそれに続く交換操作とによって実現され、ａｔｏｍｉｃ．ｌｏａｄ．ｍａｘは、ロードとそれに続くｍａｘ関数とによって実現される。特定の実施形態において、２つの命令間で他の命令からの干渉は許されない。実際には、およそ１３個の命令がＣ＋＋メモリモデルに関与し得る。
【００３４】
特定の実施形態において、記号的実行部２２４は浮動小数点数をサポートする。実際には、浮動小数点数を操作するために３０個を超える命令及びイントリンシックが存在し得る。特定の実施形態は、浮動小数点数をサポートするために、中間表現を拡張するとともに、（例えば、ソルバー２２６の一部としての）より先進的なＳＭＴソルバーを使用する。
【００３５】
特定の実施形態において、ステップ３３０に示すように、各記号表現がソルバー２２６を用いて解かれ、１つ以上のテストケース２３４が取得され得る。特定の実施形態において、ソルバー２２６はＳＭＴソルバーとすることができ、記号表現を入力として取り、出力としてテストケースを提供する。また、特定の実施形態において、記号的実行はまた、例えばバイトコードの網羅率及び整合性並びに機能的な正しさなどの統計情報を提供し得る。
【００３６】
特定の実施形態において、ステップ３４０に示すように、テストケースを使用して、プログラム２０２が例えばテスター２２８を用いて形式的にテスト・検証され得る。例えば、プログラム２０２は、マシンコードコンパイラ２２１を用いてマシンコードへとコンパイルされ、且つ、テストケース２３４を適用しながら現実設定（例えば、プログラムが実行されるよう意図される環境に類似の設定）の計算装置上で実行され、例えばｇｃｏｖ又はｌｃｏｖなどのツールを用いてプログラム２０２に関する網羅率情報が決定される。プログラム２０２のソースコードに何らかの間違い（例えば、プログラムバグ）が存在する場合、それはこのテストプロセスによって発見され得る。特定の実施形態において、マシンコードコンパイラ２２１は、Ｃ＋＋プログラムを実行可能マシンコードへとコンパイルすることができる如何なる好適なＣ＋＋コンパイラ（例えば、ｇｃｃ）であってもよい。マシンコードコンパイラ２２１は、実行時にプログラムマシンコード２０６に動的にリンクされ得るマシン語に既にコンパイルされたＣライブラリ又はＣ＋＋ライブラリを提供し得る。
【００３７】
システム２００を更に改善するため、特定の実施形態は、システム２００の多数の最適化を実装し得る。これらの最適化は、一部の場合において、システム２００の性能を高める。
【００３８】
第１に、特定の実施形態は、システム２００とともに使用されるＣ＋＋ライブラリ（例えば、ライブラリ２１２）を最適化し得る。Ｃ＋＋標準は、一般的に使用される全てのデータ構造及びアルゴリズムに関するライブラリを含んでいる。コンパイラ（例えば、ＧＣＣコンパイラ）に伴う標準Ｃ＋＋ライブラリを用いることに代えて、特定の実施形態は、記号的実行の性能を高めるようにｕＣｌｉｂｃ＋＋ライブラリを選択して最適化する。この場合、システム２００内のライブラリ２１２は、最適化されたＣ＋＋ライブラリである。特定の実施形態は、この最適化されたライブラリをＬＬＶＭバイトコード（例えば、ライブラリバイトコード２１４）へとコンパイルし、記号的実行の開始時に該ＬＬＶＭバイトコードをエンジンにロードする。特定の実施形態は、２つのバージョンのＣ＋＋ライブラリを管理する。１つは記号的実行用であり、もう１つは、例えばシステムＡＰＩなどの外部関数の具体値及びジャスト・イン・タイム・コンパイルを取り扱うためのものである。表現が記号変数を含まないとき、又は外部関数が作成されるべきとき、標準ｕＣｌｉｂｃ＋＋ライブラリが使用され、その他の場合、記号的実行に最適化されたものが使用される。
【００３９】
Ｃ＋＋標準は、４０個を超えるクラスを定義する標準ライブラリを備える。残念ながら、それらは具体的な実行のために設計されている。効率的な記号的実行は、例えば（１）生成される経路の数を削減するため、不要な条件文は排除されるべきである；（２）高価な表現は、より安価な表現に変換される（例えば、ビット演算によって操作が置き換えられる）べきである；及び（３）ライブラリ実装内に高速な決定手順が組み込まれるべきである；などの記号的実行の要求を満たすように、特定の実施形態が一部又は全てのＣ及びＣ＋＋クラス実装を書き直すことを必要とし得る。特定の実施形態において、システム２００で使用されるライブラリ２１２は、記号的実行のために高度に最適化された、多数の一般的に使用されるクラスを含む。
【００４０】
図１に関して上述したように、記号的実行を用いて、ソフトウェアモジュールのソースコード内の個々の実行経路が解析される。実行経路のブランチ又は分岐は、例えば“ｉｆ−ｅｌｓｅ”文などの条件付き分岐命令が存在するときに発生する。典型的に、分岐条件が満たされるとき、プログラムは１つの実行経路へと進み、分岐条件が満たされないとき、プログラムは別の実行経路へと進む。各実行経路は終端において記号表現をもたらす。ソフトウェアモジュール内に存在する実行経路が多いほど、多数の記号表現が記号的実行によってもたらされる。例えばループ内に分岐条件が存在する場合、そのループの繰り返しごとに実行経路のブランチ又は分岐が存在する。そのような場合、ループの繰り返しごとに発生する反復的な分岐生成の結果として、実行経路の数が指数関数的に激増することがあり、それによって、非常に多数の記号表現が生成され得る。それらの記号表現は、それ自体、サイズが指数関数的に増大することとなり、ソルバーによって解くことが困難なものとなる。
【００４１】
特定の実施形態は、標準Ｃ＋＋ライブラリのソースコードを、これらのライブラリ関数の機能を同じに維持しながら分岐条件をループの外側に移動させるように変更し得る。斯くして、何度も繰り返されるループを有していても、多数の実行経路が生成されることがないようにされる。より具体的には、特定の実施形態は、ライブラリ関数の本体を変更して、或る表現を返す。この最適化は、関数の本体が依然として直接的に実行されるので、操作上のアプローチと見なされ得る。例えば、ｕＣｌｉｂｃ＋＋ライブラリ内のＳｔｒｉｎｇクラスのｃｏｍｐａｒｅメソッドは以下のように変更され得る。変更されたｃｏｍｐａｒｅメソッドは、“ｆｏｒ”ループ内に条件付き分岐が存在しないので、２つの（具体的な長さの）入力文字列の値に依らずに唯一の実行経路を生成する。
（外２）
0005821651.tif 000004
【００４２】
特定の実施形態は、記号的実行部２２４にアクセスするための幾つかのハックイン（hack-in）関数を提供し得る。例えば、関数ｉｓ＿ｓｙｍｂｏｌｉｃは変数の値が記号的であるかを伝え、関数ｍａｋｅ＿ｉｔｅは、２つの経路を作成することを回避するようｉｆ−ｔｈｅｎ−ｅｌｓｅ表現を作成するように記号的実行部２２４に依頼する。ライブラリの最適化はこれらの関数を用いて記号的実行部２２４と相互作用する。
【００４３】
この操作方法は、戻り値として、非常に複雑な記号表現を構築することがある。これを回避するため、特定の実施形態は、全てのコードを実行するのではなく、現在状態に制約を付加する別の方法を展開し得る。この最適化は関係上のアプローチと見なされ得る。或る関数に関し、記号的実行部２２４は、戻り値を表す記号変数Ｖｒを作成するよう通知され、そして、論理式を用いてこの変数を関数の入力と関連付ける。例えば、Ｓｔｒｉｎｇクラスのｆｉｎｄ＿ｌａｓｔ＿ｏｆメソッドを以下に例示する。関数ａｓｓｕｍｅは、経路条件に制約を課すことを記号的実行部２２４に指し示す。この実装は、戻り値が−１又は入力文字列内の任意の位置であり得るときであっても、唯一の実行経路を生成する。実際、このような定義はソースコード内の（例えば、Ｓｔｒｉｎｇクラスに関する）決定手順を実現する。特定の実施形態において、ソースコード定義を介してソルバーを（例えば、スタンドアローンソルバー２２６の部分置換として）構築することは、システム２００の基本機能である。これにより、外部ソルバーを実現することの複雑さが回避される。
（外３）
0005821651.tif 000005
【００４４】
以下の例は、最適化されたライブラリ実装がどのように、外部ソルバー２２６の機能の部分を置き換える文字列用の高速ソルバーをもたらすかを例示するものである：
（外４）
0005821651.tif 000006
【００４５】
この例において、Ｓｔｒｉｎｇ．ｆｉｎｄ＿ｌａｓｔ＿ｏｆ（）関数は特定の例示として用いられている。特定の実施形態において、第１行の第１の命令文を訪れると、記号的実行部２２４は、上に示した制約を経路条件に付加し、Ｖｒが新たな変数ｉ１（“ｉ”は整数を表す）で置き換えられる。この変数は宛先のレジスタに書き込まれ、そして、実行に沿って伝播される。故に、上記ソースコード内のｋ変数がｉ１で置き換えられる。同様に、第２行の第２の命令文が実行され、ｒｅｓｔ変数を置き換える新たな文字列変数ｓ１がもたらされる。第３行にて、ｆｉｎｄメソッドが別の整数変数ｉ２をもたらす。そして、経路条件は、ｆｉｎｄ＿ｌａｓｔ＿ｏｆ、ｓｕｂｓｔｒ及びｆｉｎｄに関係する全ての制約の結合を包含する。全ての制約を包含する経路条件とともに条件付き命令文ｉ２！＝ｎｐｏｓがＳＭＴソルバー２２６にダンプされ、一方の実行ブランチの入力文字列ｓｔｒについてのテストケースが得られる。同様に、全ての制約を包含する経路条件とともに条件ｉ２＝ｎｐｏｓがＳＭＴソルバー２２６にダンプされ、他方のブランチの入力文字列ｓｔｒについての第２のテストケースが得られる。換言すれば、特定の実施形態は、単にソースコードを変更することによって文字列ソルバーを実現する。これは、実行部（例えば、記号的実行部２２４）の中間言語を変更すること、又は外部ソルバーにおけるリンク付けを行うことを必要としない。ソースＣ＋＋コードは変更が容易であるので、これは高度に拡張可能である。また、記号的実行を用いてコードの正確性を直接的に検査することができる。この技術は、その他のＣ又はＣ＋＋ライブラリクラスを取り扱うように同様に拡張され得る。
【００４６】
Ｃ＋＋プログラミング言語の主な機能の１つはクラス及びオブジェクトである。特定の実施形態は、システム２００によって使用される中間言語（ＩＬ）を、Ｃ＋＋クラス及びオブジェクトを直接的にモデル化するように拡張する。記号的実行中、記号表現は、オブジェクト、又はこれらオブジェクトに関するメソッド呼出しの名称、を表す記号変数を含み得る。特定の実施形態において、メソッド呼出しは、それが最初に遭遇されるとき、直ちにその実行まで展開されない。その代わりに、オブジェクト及びメソッドの評価をそれらが必要とされるまで遅延させるために、“遅延評価（lazy  evaluation）”アプローチが採用される。これはまた、オブジェクトに関する単純化及び推論の助けとなる。例えば、以下のサンプルコード部分はＳｔｒｉｎｇクラスに関与している。
（外５）
0005821651.tif 000007
【００４７】
第３行の分岐条件に遭遇すると、表現ｓｔｒ．ｓｕｂｓｔｒ（ｓｔｒ．ｆｉｎｄ＿ｌａｓｔ＿ｏｆ（’／’）＋１）＝“ＥａｓｙＣｈａｉｒ”が構築される。これは、これらの文字列操作のセマンティクスに関して、自由文字列変数ｓ１に関するｓｔｒ＝ｓ１＋“／ＥａｓｙＣｈａｉｒ”に単純化され得る。特定の実施形態は、一般的なクラスに関するこのような単純化及び決定手順（更に詳細に後述する）を組み入れる。なお、特定の実施形態は、単純に、この表現を解釈するためのメソッドのライブラリ定義を使用してもよく、その場合、その解釈が条件点まで遅延される。特定の実施形態では、オブジェクトレベルの抽象化のために中間言語を拡張することは、例えばＣ＋＋などのオブジェクト指向プログラミング言語の記号的実行にとって極めて重要になり得る。
【００４８】
オブジェクトレベルの推論の性能を更に高めるため、特定の実施形態は、一部の一般データ構造に特有のソルバー（例えば、ソルバー２２６に含められる）を実装する。例えば、特定の実施形態は、ＳＭＴ解法に基づく文字列ソルバーを実装することができ、それは記号的実行部２２４内にシームレスに組み込まれ得る。上述の例を考えると、特定の実施形態は、固定でない長さを有する文字列変数の値及び長さを制約する以下の表現を作り出す文字列ソルバーを実装し得る：
（外６）
0005821651.tif 000008
【００４９】
この例においては、先ず、各長さの最小インスタンスを得るため、長さについての制約が取り出されてソルバー２２６にダンプされ、その後、各文字列の長さが設定され、そして、充足可能なケースを得るため、文字列についての制約が構築されてソルバー２２６にダンプされる。ソルバー２２６に組み込まれたこのような内蔵ソルバーを用いて、特定の実施形態は、単にシステム２００の性能を向上させ、入力（例えば、可変長さを有する）についての制約を緩める。
【００５０】
時折、記号表現ｅが非常に複雑になるとき、通常のＳＭＴソルバーは応答するのに過大な時間を要することがある。このような場合、特定の実施形態において、ユーザがｅの値を具体化してもよい。特定の実施形態において、ソルバー２２６は、含まれる各記号変数に対して、可能な値又は値の小セットを与えて、ｅを充足可能なものにし得る。そして、含まれる変数をそれらの具体値で置換することによって、この知識が経路条件に付加される。
【００５１】
実際には、ソフトウェア検証システムは通常、小さいＣプログラムに対してさえも、高い網羅率を達成するために１０，０００を超えるテストケースを生成する。特定の実施形態において、システム２００はまた、ループ本体が多数の分岐を含むループを解析対象プログラムが有するとき、この問題に悩まされ得る。特定の実施形態において、特に産業用途に関して、例えばシステム２００などのソフトウェア検証システムを有用且つユーザフレンドリーなものにするには、テストケースの数を最小化す努力が欠かせない。故に、特定の実施形態は、新たなカバレッジをもたらさないブロック又は分岐を訪れないように、何らかの経路削減機構を展開する。特定の実施形態において、第１のアプローチは到達可能性解析に基づく。より具体的には、分岐に遭遇するとき、特定の実施形態は、後続の制御フローを追跡することによって、該分岐が何らかの未訪のコーナー命令につながるかを検査する。コーナー命令は、分岐命令、プロシージャ呼出し命令、又はユーザ指定された命令を含む。この追跡を制限するため、プロシージャ上での追跡に限度が設定される。このアプローチは幾つかの（例えば、巧妙な）分岐を見落とし得るが、多くの冗長性が潜伏している場合に、ユニットテスト当たりの網羅率を犠牲にすることなく、およそ９０％の重複経路を削減するのに有効である。特定の実施形態はまた、主にコンポーネントテストに関して、既訪の経路条件とは独立の経路条件を有する分岐の探査を遅延させる無損失アプローチを展開し得る。これは、モデルチェッカーで使用される半順序削減（Partial  Order  Reduction；ＰＯＲ）アルゴリズムを類似する。特定の実施形態において、以下に限られないが例えば表現書換え、制約セット単純化、制約独立性、コンパクト状態表現、暗黙値具体化、及び反例キャッシュなど、多様な最適化がシステム２００にて採用され得る。
【００５２】
関数呼出しを実装したもののバイトコードを、それに出会う度に実行することは、特に、同じ関数が何度も呼び出され得ることを考えると、非効率である。実際には、複数の関数が相互に関係している。特定の実施形態において、関数間の関係がハイレベルで規定され得る。これらの関数の具体的な実装がこの関係を満たすようにされる。これは特に、データメンバーアクセスに関して共にグループ化され得るメソッドを有するＣ＋＋クラス群に当てはまる。
【００５３】
例えば、Ｃ＋＋クラスは通常、そのクラスの（プライベート）データメンバーにアクセスするために、読出しメソッドｇｅｔｖａｌｕｅ及び書込みメソッドｓｅｔｖａｌｕｅを提供する。それらのセマンティクスは、ｏｂｊ．ｓｅｔｖａｌｕｅ（ｉ，ｖ）．ｇｅｔｖａｌｕｅ（ｉ）＝ｖ、及びｏｂｊ．ｓｅｔｖａｌｕｅ（ｉ，ｖ）．ｇｅｔｖａｌｕｅ（ｊ，ｗ）．ｇｅｔｖａｌｕｅ（ｉ）＝（ｉｆ  ｉ＝ｊ  ｔｈｅｎ  ｗ  ｅｌｓｅ  ｖ）なるルール（定理）を満足する。特定の実施形態は、システム２００を最適化する目的でこれらのルールを利用し得る。特定の実施形態は、先ずこれらのルールを構築し、その後、記号的実行中にこれらのルールを使用することで、これらのメソッドのバイトコード実装を実行することを回避する。この技術は、実行がメタレベルにおいてであり、メソッド定義よりむしろメソッド名称が操作されるので、“メタ実行”と呼ばれることもある。当然ながら、例えば、ポスト（後）条件の注釈付きのバイトコードを記号的に実行することによって、これらのルールの整合性が一度だけ証明されるべきである。
【００５４】
特定の実施形態は、オブジェクト及びそのメソッドを直接的にモデル化するために、システム２００によって使用される中間言語（ＩＬ）を拡張し得る。記号的実行中、記号表現は、オブジェクト及びメソッド名を表す記号変数を包含し得る。メソッド呼出しはそのバイトコード実装に拡張されない。
【００５５】
このような豹変を解くため、特定の実施形態は、一組のルールを適用して、それ以上の単純化が不可能になるまで表現を単純化し得る。例えば、ブール表現では、結果が真又は偽である場合、最終的な回答が得られる。特定の実施形態において、表現内のその他の変数に関係しない変数である独立変数は、任意の値にインスタンス化されることができる。表現を単純化するのに十分なルールが存在しない場合、特定の実施形態は、それを解くために、含まれるメソッドのバイトコード実装又は特定のソルバーを使用し得る。
【００５６】
特定の実施形態において、ルールは、解析対象アプリケーションについて十分且つ具体的な知識を有するユーザによって指定されてもよいし、ソースコード及びユニットテストコードから自動的あるいは半自動的に取得されてもよい。典型的なユニットテストコードは、複数のメソッド間の関係を確立する。
【００５７】
得られた各ルールに対し、特定の実施形態は記号的実行を用いて該ルールの正しさを検証する。ルールは、正しいと証明されると、フォールスアラームを生じることなくメタ実行中の何れの箇所でも使用され得る。
【００５８】
アプリケーション特定メタ実行の概念を更に説明するため、データベースアプリケーションの例を考える。このデータベースアプリケーション例は、データベースにアクセスするために、メソッドｉｎｓｅｒｔ、ｇｅｔ、ｄｅｌｅｔｅ及びｃｏｕｎｔを使用する。エンプティのデータベースオブジェクトをｄｂεと表記する。以下のサンプルコードは一連のデータベース操作を実行する：
（外７）
0005821651.tif 000009
【００５９】
条件文（第５行の“ｉｆ”文）の直前で、ＩＬ表現ｄｂε．ｉｎｓｅｒｔ（ｋ１，ｖ１）．ｉｎｓｅｒｔ（ｋ２，ｖ２）．ｄｅｌｅｔｅ（ｋ１）が構築されている。これは、ｉｆ  ｋ１＝ｋ２  ｔｈｅｎ  ｄｂε  ｅｌｓｅ  ｄｂε．ｉｎｓｅｒｔ（ｋ２，ｖ２）へと単純化され得る。記号的実行中、この分岐表現は、ｋ１＝ｋ２及びエンプティオブジェクトを有する１つと、ｋ１≠ｋ２及びエントリ（ｋ２，ｖ２）を含んだオブジェクトを有するもう１つとの、２つの状態を発生させ得る。第１の状態では、条件は偽である。第２の状態では、表現ｄｂε．ｉｎｓｅｒｔ（ｋ２，ｖ２）．ｇｅｔ（ｋ２）がｖ２へと単純化され、そして、ｖ２及びｖ３が記号変数である場合に述語ｖ２＞ｖ３が２つの実行経路をもたらすことになる。
【００６０】
この例において使用されるルールは以下のものを含んでいる。なお、オブジェクト内のエントリはそれらのキーに従ってソートされる。キーが記号値を有する場合、データベース内の複数のエントリがそれらのキー上で相互に重なり合い得る。例えば、到来エントリのキーは、既存のエントリのキーに相等しいこともあるし、そうでないこともある。この場合、処理は、等しい場合の１つと等しくない場合の１つとの２つの状態を発生させ得る。
（外８）
0005821651.tif 000010
【００６１】
特定の実施形態において、各ルールは検証される必要がある。例えば、第１のルールを検証するため、ポスト条件を有する以下のドライバプログラムがシステム２００内に実装されて（例えば、記号的実行部２２４によって）実行され得る。
（外９）
0005821651.tif 000011
【００６２】
特定の実施形態は、ネットワーク環境内に実装され得る。図５は、サービスとしてソフトウェアの検証を提供するのに好適な、一例に係るネットワーク環境５００を示している。ネットワーク環境５００は、１つ以上のサーバ５２０と１つ以上のクライアント５３０とを相互に結合するネットワーク５１０を含んでいる。特定の実施形態において、ネットワーク５１０は、イントラネット、エクストラネット、仮想プライベートネットワーク（ＶＰＮ）、ローカルエリアネットワーク（ＬＡＮ）、無線ＬＡＮ（ＷＬＡＮ）、ワイドエリアネットワーク（ＷＡＮ）、メトロポリタンエリアネットワーク（ＭＡＮ）、インターネットの一部、若しくはその他のネットワーク、又は２つ以上のこれらネットワークの組み合わせである。この開示は、如何なる好適なネットワーク５１０をも意図している。
【００６３】
１つ以上のリンク５５０が、サーバ５２０又はクライアント５３０をネットワーク５１０に結合する。特定の実施形態において、１つ以上のリンク５５０は各々、１つ以上の有線リンク、無線リンク、又は光リンクを含む。特定の実施形態において、１つ以上のリンク５５０は各々、イントラネット、エクストラネット、ＶＰＮ、ＬＡＮ、ＷＬＡＮ、ＷＡＮ、ＭＡＮ、インターネットの一部、若しくはその他のリンク、又は２つ以上のこれらリンクの組み合わせを含む。この開示は、サーバ５２０及びクライアント５３０をネットワーク５１０に結合する如何なる好適なリンク５５０をも意図している。
【００６４】
特定の実施形態において、各サーバ５２０は、単一のサーバであってもよいし、複数のコンピュータ又は複数のデータセンターに跨る分散サーバであってもよい。サーバ５２０は、例えば、ウェブサーバ、ニュースサーバ、メイルサーバ、メッセージサーバ、広告サーバ、ファイルサーバ、アプリケーションサーバ、交換サーバ、データベースサーバ、又はプロキシサーバなど、様々な種類のサーバとし得る。特定の実施形態において、各サーバ５２０は、そのサーバ５２０によって実現あるいは支援される適切な機能を実行するための、ハードウェア、ソフトウェア、若しくは埋込ロジック要素、又は２つ以上のこれら要素の組み合わせを含み得る。例えば、ウェブサーバは一般的に、ウェブページ、又はウェブページの特定の要素、を含むウェブサイトのホストを務めることが可能である。より具体的には、ウェブサーバは、ＨＴＭＬファイル又はその他のファイルタイプのホストとなることができ、あるいは要求を受けてファイルを動的に作成あるいは構成して、クライアント５３０からのＨＴＴＰ又はその他の要求に応答して該ファイルをクライアント５３０に通信することができる。メイルサーバは一般的に、様々なクライアント５３０に電子メイルサービスを提供することができる。データベースサーバは一般的に、１つ以上のデータ庫に格納されたデータを管理するためのインタフェースを提供することができる。
【００６５】
特定の実施形態において、１つ以上のサーバ５２０に、１つ以上のリンク５５０を介して、１つ以上のデータストレージ５４０が通信可能に結合され得る。特定の実施形態において、データストレージ５４０は、様々な種類の情報を保管するために使用され得る。特定の実施形態において、データストレージ５４０に格納される情報は、特定のデータ構造に従って編成され得る。特定の実施形態において、各データストレージ５４０はリレーショナルデータベースとし得る。特定の実施形態は、サーバ５２０又はクライアント５３０が、データストレージ５４０に格納された情報を管理する（例えば、検索、修正、追加あるいは消去する）ことを可能にするインタフェースを提供し得る。
【００６６】
特定の実施形態において、各クライアント５３０は、ハードウェア、ソフトウェア、若しくは埋込ロジック要素、又は２つ以上のこれら要素の組み合わせを含み、クライアント５３０によって実現あるいは支援される適切な機能を実行することが可能である。例えば、クライアント５３０は、以下に限られないが、デスクトップ型コンピュータシステム、ノート型コンピュータシステム、ネットブック型コンピュータシステム、手持ち式電子機器、又は携帯電話とし得る。この開示は、如何なる好適なクライアント５３０をも意図している。クライアント５３０は、クライアント５３０の位置のネットワークユーザがネットワーク５１０にアクセスすることを可能にし得る。クライアント５３０は、そのユーザが、その他のクライアント５３０の他ユーザと通信することを可能にしてもよい。
【００６７】
クライアント５３０は、例えば、マイクロソフト・インターネットエクスプローラ、グーグル・クローム又はモジラ・ファイアフォックスなどのウェブブラウザ５３２を有することができ、また、１つ以上のアドオン、プラグイン、又は例えばツールバー若しくはヤフー・ツールバーなどのその他のエクステンションを有していてもよい。クライアント５３０のユーザは、ＵＲＬ又はウェブブラウザ５３２をサーバ５２０に導くその他のアドレスを入力することができ、ウェブブラウザ５３２は、ハイパーテキスト転送プロトコル（ＨＴＴＰ）要求を生成して、該ＨＴＴＰ要求をサーバ５２０に通信し得る。サーバ５２０は、ＨＴＴＰ要求を受理し、該ＨＴＴＰ要求に応じた１つ以上のハイパーテキスト・マークアップ言語（ＨＴＭＬ）ファイルをクライアント５３０に通信し得る。クライアント５３０は、サーバ５２０からのＨＴＭＬファイルに基づいて、ユーザへの提示にためにウェブページを表示し得る。この開示は、如何なる好適なウェブページファイルをも意図している。非限定的な一例として、ウェブページは、具体的なニーズに従って、ＨＴＭＬファイル、拡張可能ハイパーテキスト・マークアップ言語（ＸＨＴＭＬ）ファイル、又は拡張マークアップ言語（ＸＭＬ）ファイルから表示を行い得る。このようなページはまた、例えば、以下に限られないが、ＪＡＶＡスクリプト（登録商標）、ＪＡＶＡ（登録商標）、マイクロソフト・シルバーライトで記述されたものなどのスクリプト、例えばＡＪＡＸ（Asynchronous  JavaScript  and  XML）などのマークアップ言語とスクリプトとの組み合わせ、及びこれらに類するものを実行し得る。ここでは、適宜、ウェブページへの言及は、（ブラウザがウェブページを表示するために使用する）１つ以上の対応するウェブページファイルを包含し、その逆も然りである。
【００６８】
特定の実施形態は、１つ以上のコンピュータシステム上で実現され得る。図６は、一例に係るコンピュータシステム６００を示している。特定の実施形態において、１つ以上のコンピュータシステム６００が、ここに記載あるいは図示した１つ以上の方法の１つ以上のステップを実行する。特定の実施形態において、１つ以上のコンピュータシステム６００が、ここに記載あるいは図示した機能を提供する。特定の実施形態において、１つ以上のコンピュータシステム６００上で起動されるソフトウェアが、ここに記載あるいは図示した１つ以上の方法の１つ以上のステップを実行し、あるいは、ここに記載あるいは図示した機能を提供する。特定の実施形態は、１つ以上のコンピュータシステム６００の１つ以上の部分を含む。
【００６９】
この開示は、如何なる好適な数のコンピュータシステム６００をも意図している。この開示は、如何なる物理形態を採るコンピュータシステム６００をも意図している。非限定的な一例として、コンピュータシステム６００は、組込型コンピュータシステム、システム・オン・チップ（ＳＯＣ）、シングルボード・コンピュータシステム（ＳＢＣ）（例えば、コンピュータ・オン・モジュール（ＣＯＭ）若しくはシステム・オン・モジュール（ＳＯＭ）など）、デスクトップ型コンピュータシステム、ラップトップ型又はノート型のコンピュータシステム、対話式キオスク端末、メインフレーム、メッシュ状コンピュータシステム、携帯電話、携帯情報端末（ＰＤＡ）、サーバ、又はこれらの２つ以上の組み合わせとし得る。必要に応じて、コンピュータシステム６００は、単一あるいは分散型の；複数の位置にまたがる；複数の機械にまたがる；あるいはクラウド（１つ以上のネットワーク内に１つ以上のクラウド要素を含み得る）内の；１つ以上のコンピュータシステム６００を含んでいてもよい。必要に応じて、１つ以上のコンピュータシステム６００は、ここに記載あるいは図示した１つ以上の方法の１つ以上のステップを、空間的あるいは時間的な実質的な制約なく実行し得る。非限定的な一例として、１つ以上のコンピュータシステム６００は、ここに記載あるいは図示した１つ以上の方法の１つ以上のステップを、リアルタイムあるいはバッチモードで実行し得る。必要に応じて、１つ以上のコンピュータシステム６００は、相異なる時点で、あるいは相異なる位置で、ここに記載あるいは図示した１つ以上の方法の１つ以上のステップを実行してもよい。
【００７０】
特定の実施形態において、コンピュータシステム６００は、プロセッサ６０２、メモリ６０４、ストレージ６０６、入力／出力（Ｉ／Ｏ）インタフェース６０８、通信インタフェース６１０、及びバス６１２を含んでいる。この開示は、特定の構成にされた特定数の特定の構成要素を有する特定のコンピュータシステムを図示して説明しているが、この開示は、如何なる好適配置にされた如何なる好適数の如何なる好適構成要素を有する如何なる好適なコンピュータシステムをも意図している。
【００７１】
特定の実施形態において、プロセッサ６０２は、例えばコンピュータプログラムを構築する命令などの命令を実行するハードウェアを含む。非限定的な一例として、命令を実行するために、プロセッサ６０２は、内部レジスタ、内部キャッシュ、メモリ６０４、又はストレージ６０６から命令を取り出し（すなわち、フェッチし）；それを復号化して実行し；その後、１つ以上の結果を内部レジスタ、内部キャッシュ、メモリ６０４、又はストレージ６０６に書き込み得る。特定の実施形態において、プロセッサ６０２は、データ、命令又はアドレス用の１つ以上の内部キャッシュを含み得る。この開示は、プロセッサ６０２が必要に応じて、如何なる好適数の如何なる好適な内部キャッシュを含むことも意図している。非限定的な一例として、プロセッサ６０２は、１つ以上の命令キャッシュと、１つ以上のデータキャッシュと、１つ以上のトランスレーション・ルックアサイド・バッファ（ＴＬＢ）とを含み得る。命令キャッシュ内の命令は、メモリ６０４又はストレージ６０６内の命令の複製としてもよく、命令キャッシュは、プロセッサ６０２によるこれら命令の取り出しを高速化し得る。データキャッシュ内のデータは、メモリ６０４又はストレージ６０６内の、プロセッサ６０２にて実行されている命令が処理すべきデータの複製；プロセッサ６０２にて実行される後続の命令によるアクセスのための、あるいはメモリ６０４又はストレージ６０６に書き込むための、プロセッサ６０２にて実行された以前の命令の結果；又はその他の好適データとし得る。データキャッシュは、プロセッサ６０２による読み出し処理又は書き込み処理を高速化し得る。ＴＬＢは、プロセッサ６０２のために仮想アドレス変換を高速化し得る。特定の実施形態において、プロセッサ６０２は、データ、命令又はアドレス用の１つ以上の内部レジスタを含み得る。この開示は、プロセッサ６０２が適宜、如何なる好適数の如何なる好適な内部レジスタを含むことをも意図している。必要に応じて、プロセッサ６０２は、１つ以上の演算論理ユニット（ＡＬＵ）を含んでいてもよく；マルチコアプロセッサであってもよく；あるいは１つ以上のプロセッサ６０２を含んでいてもよい。この開示は特定のプロセッサを図示して説明しているが、この開示は如何なる好適なプロセッサをも意図している。
【００７２】
特定の実施形態において、メモリ６０４は、プロセッサ６０２が実行する命令、又はプロセッサ６０２が処理するデータを格納するメインメモリを含む。非限定的な一例として、コンピュータシステム６００はストレージ６０６又は別のソース（例えば、別のコンピュータシステム６００など）からメモリ６０４に命令をロードし得る。その後、プロセッサ６０２は、メモリ６０４から内部レジスタ又は内部キャッシュに命令をロードし得る。命令を実行するため、プロセッサ６０２は、内部レジスタ又は内部キャッシュから命令を取り出し、取り出した命令を復号化する。命令の実行中又は実行後、プロセッサ６０２は、１つ以上の結果（中間結果又は最終結果とし得る）を内部レジスタ又は内部キャッシュに書き込み得る。そして、プロセッサ６０２は、それらの結果のうちの１つ以上をメモリ６０４に書き込み得る。特定の実施形態において、プロセッサ６０２は、１つ以上の内部レジスタ若しくは内部キャッシュ又はメモリ６０４内の命令のみを実行してもよく（ストレージ６０６又はその他の場所の命令を実行するのとは異なる）、また、１つ以上の内部レジスタ若しくは内部キャッシュ又はメモリ６０４内のデータのみを処理してもよい（ストレージ６０６又はその他の場所のデータを処理するのとは異なる）。１つ以上のメモリバス６１２（各々がアドレスバス及びデータバスを含み得る）が、プロセッサ６０２をメモリ６０４に結合してもよい。バス６１２は、後述のように、１つ以上のメモリバスを含み得る。特定の実施形態において、１つ以上のメモリ管理装置（ＭＭＵ）が、プロセッサ６０２とメモリ６０４との間に存在し、プロセッサ６０２により要求されるメモリ６０４へのアクセスを容易にし得る。特定の実施形態において、メモリ６０４は、ランダムアクセスメモリ（ＲＡＭ）を含む。このＲＡＭは、適当であれば、揮発性メモリであってもよい。必要に応じて、このＲＡＭはダイナミックＲＡＭ（ＤＲＡＭ）又はスタティックＲＡＭ（ＳＲＡＭ）にされ得る。また、必要に応じて、このＲＡＭは、シングルポート又はマルチポートのＲＡＭにされ得る。この開示は、如何なる好適なＲＡＭをも意図している。メモリ６０４は、必要に応じて、１つ以上のメモリ６０４を含んでいてもよい。この開示は特定のメモリを図示して説明しているが、この開示は如何なる好適なメモリをも意図している。
【００７３】
特定の実施形態において、ストレージ６０６は、データ又は命令用の大容量記憶装置を含む。非限定的な一例として、ストレージ６０６は、ＨＤＤ、フロッピーディスク（登録商標）ドライブ、フラッシュメモリ、光ディスク、磁気光ディスク、磁気テープ、若しくはユニバーサル・シリアル・バス（ＵＳＢ）ドライブ、又はこれらの２つ以上の組み合わせを含み得る。ストレージ６０６は、必要に応じて、リムーバブル（取り外し可能）あるいは非リムーバブル（すなわち、固定）のメディアを含み得る。ストレージ６０６は、必要に応じて、コンピュータシステム６００の内部にあってもよいし、外部にあってもよい。特定の実施形態において、ストレージ６０６は、不揮発性のソリッドステートメモリである。特定の実施形態において、ストレージ６０６は、読み出し専用メモリ（ＲＯＭ）を含む。必要に応じて、このＲＯＭは、マスクプログラムされたＲＯＭ、プログラマブルＲＯＭ（ＰＲＯＭ）、消去可能ＰＲＯＭ（ＥＰＲＯＭ）、電気的消去可能ＰＲＯＭ（ＥＥＰＲＯＭ）、電気的消去再書込可能ＲＯＭ（ＥＡＲＯＭ）、若しくはフラッシュメモリ、又はこれらの２つ以上の組み合わせとし得る。この開示は、如何なる好適な物理形態を有する大容量記憶装置６０６をも意図している。ストレージ６０６は、必要に応じて、プロセッサ６０２とストレージ６０６との間での通信を容易にする１つ以上のストレージ制御装置を含み得る。この開示は特定のストレージを図示して説明しているが、この開示は如何なる好適なストレージをも意図している。
【００７４】
特定の実施形態において、Ｉ／Ｏインタフェース６０８は、コンピュータシステム６００と１つ以上のＩ／Ｏ装置との間での通信のための１つ以上のインタフェースを提供するハードウェア、ソフトウェア、又はこれら双方を含む。コンピュータシステム６００は、必要に応じて、これらＩ／Ｏ装置のうちの１つ以上を含んでいてもよい。これらＩ／Ｏ装置のうちの１つ以上は、個人とコンピュータシステム６００との間での通信を可能にし得る。非限定的な一例として、Ｉ／Ｏ装置は、キーボード、キーパッド、マイク、モニタ、マウス、プリンタ、スキャナ、スピーカ、スチルカメラ、スタイラスペン、タブレット、タッチスクリーン、トラックボール、ビデオカメラ、その他の好適なＩ／Ｏ装置、又はこれらの２つ以上の組み合わせを含み得る。Ｉ／Ｏ装置は、１つ以上のセンサを含んでいてもよい。この開示は、如何なる好適なＩ／Ｏ装置、及びそれ用の如何なる好適なＩ／Ｏインタフェース６０８をも意図している。必要に応じて、Ｉ／Ｏインタフェース６０８は、プロセッサ６０２がこれらのＩ／Ｏ装置のうちの１つ以上を駆動することを可能にする１つ以上の装置又はソフトウェアドライバを含んでいてもよい。Ｉ／Ｏインタフェース６０８は、必要に応じて、１つ以上のインタフェース６０８を含んでいてもよい。この開示は特定のＩ／Ｏインタフェースを図示して説明しているが、この開示は如何なる好適なＩ／Ｏインタフェースをも意図している。
【００７５】
特定の実施形態において、通信インタフェース６１０は、コンピュータシステム６００と、１つ以上のその他のコンピュータシステム若しくは１つ以上のネットワークとの間での通信（例えば、パケットベースの通信など）のための１つ以上のインタフェースを提供するハードウェア、ソフトウェア、又はこれら双方を含む。非限定的な一例として、通信インタフェース６１０は、イーサネット（登録商標）若しくはその他のワイヤベースのネットワークと通信するためのネットワークインタフェースコントローラ（ＮＩＣ）若しくはネットワークアダプタ、又は例えばＷｉ−Ｆｉネットワークなどの無線ネットワークと通信するための無線ＮＩＣ（ＷＮＩＣ）若しくは無線アダプタを含み得る。この開示は、如何なる好適なネットワーク及びそれ用の如何なる好適な通信インタフェース６１０をも意図している。非限定的な一例として、コンピュータシステム６００は、アドホックネットワーク、パーソナルエリアネットワーク（ＰＡＮ）、ローカルエリアネットワーク（ＬＡＮ）、ワイドエリアネットワーク（ＷＡＮ）、メトロポリタンエリアネットワーク（ＭＡＮ）、若しくはインターネットの１つ以上の部分、又はこれらの２つ以上の組み合わせと通信し得る。これらのネットワークのうちの１つ以上の１つ以上の部分は、有線であってもよいし、無線であってもよい。一例として、コンピュータシステム６００は、無線ＰＡＮ（ＷＰＡＮ）（例えば、ブルートゥース（登録商標）ＷＰＡＮなど）、Ｗｉ−Ｆｉネットワーク、Ｗｉ−ＭＡＸネットワーク、携帯電話ネットワーク（例えば、グローバル・システム・フォー・モバイル・コミュニケーションズ（ＧＳＭ(登録商標)）ネットワークなど）、若しくはその他の好適な無線ネットワーク、又はこれらの２つ以上の組み合わせと通信し得る。コンピュータシステム６００は、必要に応じて、これらのネットワークの何れかのための如何なる好適な通信インタフェース６１０を含んでいてもよい。この開示は特定の通信インタフェースを図示して説明しているが、この開示は如何なる好適な通信インタフェースをも意図している。
【００７６】
特定の実施形態において、バス６１２は、コンピュータシステム６００の構成要素を相互に結合するための、ハードウェア、ソフトウェア、又はこれら双方を含む。非限定的な一例として、バス６１２は、アクセラレーテッド・グラフィクス・ポート（ＡＧＰ）若しくはその他のグラフィック専用バス、ＥＩＳＡ（Extended  Industry  Standard  Architecture）バス、フロントサイドバス（ＦＳＢ）、ハイパートランスポート（ＨＴ）インターコネクト、業界標準アーキテクチャ（ＩＳＡ）バス、インフィニバンド・インターコネクト、ＬＰＣ（low-pin-count）バス、メモリバス、マイクロ・チャネル・アーキテクチャ（ＭＣＡ）バス、コンピュータ用拡張バスアーキテクチャ（ＰＣＩ）バス、ＰＣＩエクスプレス（ＰＣＩ−Ｘ）バス、シリアルＡＴＡ（ＳＡＴＡ）バス、ＶＬＢ（Video  Electronics  Standards  Association  local）バス、若しくはその他の好適なバス、又はこれらの２つ以上の組み合わせを含み得る。バス６１２は、必要に応じて、１つ以上のバス６１２を含んでいてもよい。この開示は特定のバスを図示して説明しているが、この開示は如何なる好適なバス又はインターコネクトをも意図している。
【００７７】
ここで、コンピュータ読み取り可能記憶媒体への言及は、１つ以上の一過性でない有形のコンピュータ読み取り可能記憶媒体保有構造をも包含するものである。非限定的な一例として、コンピュータ読み取り可能記憶媒体は、必要に応じて、半導体ベースあるいはその他の集積回路（ＩＣ）（例えば、フィールド・プログラマブル・ゲート・アレイ（ＦＰＧＡ）、又は特定用途向けＩＣ（ＡＳＩＣ）など）、ハードディスク、ＨＤＤ、ハイブリッド式ハードドライブ（ＨＨＤ）、光ディスク、光ディスクドライブ（ＯＤＤ）、磁気光ディスク、磁気光ドライブ、フロッピー（登録商標）ディスク、フロッピーディスクドライブ（ＦＤＤ）、磁気テープ、ホログラフィック記憶媒体、ソリッドステートドライブ（ＳＳＤ）、ＲＡＭドライブ、セキュアデジタル（ＳＤ）カード、セキュアデジタルドライブ、若しくはその他の好適なコンピュータ読み取り可能記憶媒体、又はこれらの２つ以上の組み合わせを含み得る。コンピュータ読み取り可能な一過性でない記憶媒体は、必要に応じて、揮発性、不揮発性、又は揮発性と不揮発性との組み合わせとし得る。
【００７８】
この開示は、何らかの好適なストレージを実現する１つ以上のコンピュータ読み取り可能記憶媒体を意図している。特定の実施形態において、コンピュータ読み取り可能記憶媒体は、必要に応じて、プロセッサ６０２の１つ以上の部分（例えば、１つ以上の内部レジスタ若しくはキャッシュなど）、メモリ６０４の１つ以上の部分、ストレージ６０６の１つ以上の部分、又はこれらの組み合わせを実現してもよい。特定の実施形態において、コンピュータ読み取り可能記憶媒体はＲＡＭ又はＲＯＭを実現する。特定の実施形態において、コンピュータ読み取り可能記憶媒体は揮発性あるいは永続的なメモリを実現する。特定の実施形態において、１つ以上のコンピュータ読み取り可能記憶媒体がソフトウェアを具現化する。ここで、ソフトウェアへの言及は適宜、１つ以上のアプリケーション、バイトコード、１つ以上のコンピュータプログラム、１つ以上の実行ファイル、１つ以上の命令、ロジック、機械語、１つ以上のスクリプト、又はソースコードを包含するものであり、この逆もまた然りである。特定の実施形態において、ソフトウェアは、１つ以上のアプリケーション・プログラミング・インタフェース（ＡＰＩ）を含む。この開示は、如何なる好適なプログラミング言語又は複数のプログラミング言語の組み合わせで書き込まれ、あるいはその他の方法で表現された、如何なる好適なソフトウェアをも意図している。特定の実施形態において、ソフトウェアはソースコード又はオブジェクトコードとして表現され得る。特定の実施形態において、ソフトウェアは、例えばＣ、Ｐｅｒｌ又はこれらの好適な拡張版など、より高級（高水準）なプログラミング言語で表現される。特定の実施形態において、ソフトウェアは、例えばアセンブリ言語（又は機械語）など、より低水準のプログラミング言語で表現される。特定の実施形態において、ソフトウェアはＪＡＶＡで表現される。特定の実施形態において、ソフトウェアはハイパーテキスト・マークアップ言語（ＨＴＭＬ）、拡張マークアップ言語（ＸＭＬ）、又はその他の好適なマークアップ言語で表現される。
【００７９】
ここでは、“又は”は、その他のことが明示的或いは文脈的に指し示されない限り、両立的なものであって排他的なものではない。故に、“Ａ又はＢ”は、その他のことが明示的或いは文脈的に指し示されない限り、“Ａ、Ｂ、又は双方”を意味する。また、“及び”は、その他のことが明示的或いは文脈的に指し示されない限り、結合及びそれぞれの双方である。故に、ここでは、“Ａ及びＢ”は、その他のことが明示的或いは文脈的に指し示されない限り、“結合的あるいは個別的にＡ及びＢ”を意味する。
【００８０】
この開示は、ここで例示した実施形態への、当業者に理解されるであろう全ての変更、代用、変形、改変及び改良を包含するものである。同様に、添付の請求項は適宜、ここで例示した実施形態への当業者に理解されるであろう全ての変更、代用、変形、改変及び改良を包含するものである。また、特定の機能を実行するように適応され、構成され、可能にされ、設定され、有効にされ、動作可能にされ、あるいは動作する装置若しくはシステム又はそれらの構成要素への、請求項中での参照は、装置、システム又は構成要素がそのように適応、構成、可能化、設定、有効化、動作可能化あるいは動作される限り、それ又はその特定機能が活性化され、オンにされ、あるいは解除されようとなかろうと、その装置、システム又は構成要素を包含するものである。
【符号の説明】
【００８１】
２００  システム
２０２  プログラム
２０４  プログラムバイトコード
２０６  プログラムマシンコード
２１２  ライブラリ
２１４  ライブラリバイトコード
２２１  マシンコードコンパイラ
２２２  バイトコードコンパイラ
２２４  記号的実行部
２２６  ソルバー
２２８  テスター
２３２  記号表現
２３４  テストケース
２３６  カバレッジ
５００  ネットワーク環境
５１０  ネットワーク
５２０  サーバ
５２２  検索エンジン
５２４  データモニタ／収集部
５３０  クライアント
５４０  データストレージ
５５０  リンク
６００  コンピュータシステム
６０２  プロセッサ
６０４  メモリ
６０６  ストレージ
６０８  Ｉ／Ｏインタフェース
６１０  通信インタフェース
６１２  バス
【図１】
0005821651.tif 000012
【図２】
0005821651.tif 000013
【図３】
0005821651.tif 000014
【図４Ａ】
0005821651.tif 000015
【図４Ｂ】
0005821651.tif 000016
【図５】
0005821651.tif 000017
【図６】
0005821651.tif 000018