(57)【特許請求の範囲】
【請求項１】
一つまたは複数のコンピューティング・デバイスによって：
ソフトウェア・モジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、
前記ソフトウェア・モジュールは：一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、
前記第一の数値制約条件は前記数値変数のうちの特定の一つまたは複数に適用され；
前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、
段階と；
前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する段階と；
前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する段階と；
前記第一および第二の数値制約条件のそれぞれを式で表現する段階と；
前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と；
前記ソフトウェア・モジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェア・モジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う段階とを含む、
方法。
【請求項２】
請求項１記載の方法であって：
前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み；
前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み；
前記入力数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記入力ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの仕様に基づいて決定され；
前記中間数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記中間ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの記号的実行を行うことによって決定される、
方法。
【請求項３】
請求項１または２記載の方法であって：
前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され；
前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、
方法。
【請求項４】
請求項３記載の方法であって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェア・モジュールを実装するプログラミング言語の仕様および前記ソフトウェア・モジュールが実行される実行時環境に基づいて推定される、方法。
【請求項５】
請求項１ないし４のうちいずれか一項記載の方法であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることが：
前記数値変数および前記ストリング変数について可能な値を選び、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで逐次反復的に行い；
解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、
方法。
【請求項６】
請求項１ないし５のうちいずれか一項記載の方法であって：
前記ソフトウェア・モジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し；
前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており；
前記ソフトウェア・モジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェア・モジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、
方法。
【請求項７】
請求項６記載の方法であって：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数は、前記ソフトウェア・モジュールの一つまたは複数の入力変数および前記ソフトウェア・モジュールの一つまたは複数の出力変数を含み、
前記ソフトウェア・モジュールに関連付けられた前記要件が、前記ソフトウェア・モジュールの前記入力変数のうちの特定の一つまたは複数に適用される一つまたは複数の入力要件ならびに前記ソフトウェア・モジュールの前記出力変数のうちの特定の一つまたは複数に適用される一つまたは複数の出力要件を含み、
前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数のうちの特定の一つまたは複数に適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェア・モジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェア・モジュールを対応する実行経路の終わりに到達させるものである、段階と；
前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と；
前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と；
前記事後条件制約条件のそれぞれを否定にする段階と；
前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と；
制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と；
制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェア・モジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、
方法。
【請求項８】
請求項７記載の方法であって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、方法。
【請求項９】
請求項７記載の方法であって、前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：前記ソフトウェア・モジュールの記号的実行を行って前記制約条件の集合を得ることを含む、方法。
【請求項１０】
一つまたは複数のプロセッサによって実行可能な命令を有するメモリと；
前記メモリに結合され、前記命令を実行するよう動作可能な一つまたは複数のプロセッサとを有するシステムであって、前記一つまたは複数のプロセッサは、前記命令を実行するとき：
ソフトウェア・モジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、
前記ソフトウェア・モジュールは：一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、
前記第一の数値制約条件は前記数値変数のうちの特定の一つまたは複数に適用され；
前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、
段階と；
前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する段階と；
前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する段階と；
前記第一および第二の数値制約条件のそれぞれを式で表現する段階と；
前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と；
前記ソフトウェア・モジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェア・モジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う段階とを実行するよう動作する、
システム。
【請求項１１】
ソフトウェアを具現する一つまたは複数のコンピュータ読み取り可能な非一時的記憶媒体であって、前記ソフトウェアは、一つまたは複数のコンピューティング・デバイスによって実行されたときに：
ソフトウェア・モジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、
前記ソフトウェア・モジュールは：一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、
前記第一の数値制約条件は前記数値変数のうちの特定の一つまたは複数に適用され；
前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、
段階と；
前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する段階と；
前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する段階と；
前記第一および第二の数値制約条件のそれぞれを式で表現する段階と；
前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と；
前記ソフトウェア・モジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェア・モジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う段階とを実行するよう動作可能である、
媒体。
【請求項１２】
請求項１１記載の媒体であって：
前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み；
前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み；
前記入力数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記入力ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの仕様に基づいて決定され；
前記中間数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記中間ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの記号的実行を行うことによって決定される、
媒体。
【請求項１３】
請求項１１または１２記載の媒体であって：
前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され；
前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、
媒体。
【請求項１４】
請求項１３記載の媒体であって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェア・モジュールを実装するプログラミング言語の仕様および前記ソフトウェア・モジュールが実行される実行時環境に基づいて推定される、媒体。
【請求項１５】
請求項１１ないし１４のうちいずれか一項記載の媒体であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることが：
前記数値変数および前記ストリング変数について可能な値を選び、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで逐次反復的に行い；
解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、
媒体。
【請求項１６】
請求項１１ないし１５のうちいずれか一項記載の媒体であって：
前記ソフトウェア・モジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し；
前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており；
前記ソフトウェア・モジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェア・モジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、
媒体。
【請求項１７】
請求項１６記載の媒体であって：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数は、前記ソフトウェア・モジュールの一つまたは複数の入力変数および前記ソフトウェア・モジュールの一つまたは複数の出力変数を含み、
前記ソフトウェア・モジュールに関連付けられた前記要件が、前記ソフトウェア・モジュールの前記入力変数のうちの特定の一つまたは複数に適用される一つまたは複数の入力要件ならびに前記ソフトウェア・モジュールの前記出力変数のうちの特定の一つまたは複数に適用される一つまたは複数の出力要件を含み、
前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数のうちの特定の一つまたは複数に適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェア・モジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェア・モジュールを対応する実行経路の終わりに到達させるものである、段階と；
前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と；
前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と；
前記事後条件制約条件のそれぞれを否定にする段階と；
前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と；
制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と；
制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェア・モジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、
媒体。
【請求項１８】
請求項１７記載の媒体であって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、媒体。
【請求項１９】
請求項１７記載の媒体であって、前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：前記ソフトウェア・モジュールの記号的実行を行って前記制約条件の集合を得ることを含む、媒体。
【請求項２０】
ソフトウェア・モジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する手段であって、
前記ソフトウェア・モジュールは：一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、
前記第一の数値制約条件は前記数値変数のうちの特定の一つまたは複数に適用され；
前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、
手段と；
前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する手段と；
前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する手段と；
前記第一および第二の数値制約条件のそれぞれを式で表現する手段と；
前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する手段と；
前記ソフトウェア・モジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェア・モジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う手段とを含む、
システム。
【発明の詳細な説明】
【技術分野】
【０００１】
本開示は概括的にはソフトウェア・モジュールを試験および検証することに関する。
【背景技術】
【０００２】
ソフトウェア・アプリケーションはいくつかのモジュール（たとえば、クラス、関数、プロシージャ、サブルーチンまたはコード・ブロック）を含むことがあり、各モジュールは個々に試験または検証されうる。ソフトウェア・モジュールは手動または自動で試験または検証されうる。前者の場合、人（たとえばソフトウェア試験エンジニア）が手動でソフトウェア・モジュールのための試験ケースを、該モジュールの設計仕様に基づいて設計し、試験ケースのもとでモジュールを実行し、試験ケースに一致しないモジュール挙動または出力があるかどうか検査してもよい。後者の場合、コンピュータ・ソフトウェアまたはハードウェアとして実装されるソフトウェア試験ツールが自動的に試験対象ソフトウェア・モジュールについての試験ケースを生成し、それらの試験ケースをシミュレートしながら試験対象モジュールを実行し、試験ケースに一致しないモジュール挙動または出力があるかどうか検査してもよい。
【発明の概要】
【発明が解決しようとする課題】
【０００３】
本発明は、従来技術の欠点を軽減または解消する。
【課題を解決するための手段】
【０００４】
本発明の課題は、請求項記載の手段によって達成される。
【図面の簡単な説明】
【０００５】
【図１】ソフトウェア・モジュールまたはその変数に対して課された制約条件を決定および解決するための例示的な方法を示す図である。
【図２】ソフトウェア・モジュールまたはその変数に対して課された制約条件を決定および解決するための例示的なシステムを示す図である。
【図３】種々のストリングを表すために使われるいくつかの例示的な有限状態機械を示す図である。
【図４】ストリングおよびその部分ストリングを表すために使われる例示的な有限状態機械を示す図である。
【図５】ストリング・ドメイン内に入れられたストリング制約条件および数値ドメイン内に入れられた数値制約条件をもつ例示的な制約条件のセットを示す図である。
【図６】複数レベルのネストされた条件分岐をもつ例示的なソフトウェア・モジュールの実行経路を示す図である。
【図７】ソフトウェア・モジュールを試験するための例示的な方法を示す図である。
【図８】例示的なソフトウェア・モジュールに対する記号的実行を行うステップを表す例示的な実行フローを示す図である。
【図９Ａ】記号的実行ランの間の例示的なソフトウェア・モジュールおよび種々のアプリケーション結果を生成するための場所について得られる例示的な制約条件のセットを示す図である。
【図９Ｂ】記号的実行ランの間の例示的なソフトウェア・モジュールおよび種々のアプリケーション結果を生成するための場所について得られる例示的な制約条件のセットを示す図である。
【図９Ｃ】記号的実行ランの間の例示的なソフトウェア・モジュールおよび種々のアプリケーション結果を生成するための場所について得られる例示的な制約条件のセットを示す図である。
【図１０】入力および出力に対して課された要求との関連でソフトウェア・モジュールを検証する例示的な方法を示す図である。
【図１１】インジェクション攻撃を検出するよう設計されたセキュリティ・ソフトウェア・モジュールを検証する例示的な方法を示す図である。
【図１２】例示的なネットワーク環境を示す図である。
【図１３】例示的なコンピュータ・システムを示す図である。
【発明を実施するための形態】
【０００６】
本開示について、これから付属の図面に示されるような若干の実施形態を参照しつつ詳細に述べる。以下の記述において、本開示の十全な理解を与えるために数多くの具体的詳細が記載されるが、当業者には、本開示がそのような具体的詳細の一部または全部がなくても実施されうることは明白であろう。その一方、よく知られた処理ステップおよび／または構造は、本開示を無用に埋没させないよう、詳細に述べてはいない。さらに、本開示は具体的実施形態との関連で記述されるが、この記述は本開示を記述される実施形態に限定することを意図したものではないことは理解しておくべきである。逆に、この記述は付属の請求項によって定義される本開示の精神および範囲内に含まれうる代替、修正および等価物をカバーすることが意図されている。
【０００７】
ソフトウェア・アプリケーションはしばしばいくつかのソフトウェア・モジュールに編成され、各ソフトウェア・モジュールは具体的な機能を実行するコードを含みうる。典型的な筋書きでは、ソフトウェア・モジュールは入力または出力変数をいくつ有していてもよい。ソフトウェア・モジュールが呼び出されるとき、ソフトウェア・モジュールの入力変数に割り当てられる値として、実際の入力値が（たとえばソフトウェア・モジュールを呼び出すコードによって）ソフトウェア・モジュールに渡されてもよい。ソフトウェア・モジュールのコードは、実際の入力値との関連で実行されうる。最終的には、ソフトウェア・モジュールの出力変数についての実際の出力値が決定され、ソフトウェア・モジュールによって返されることができ、その時点でソフトウェア・モジュールはその実行を完了する。さらに、ソフトウェア・モジュールのコードによって決定される実際の出力値は、通例、ソフトウェア・モジュールにその呼び出しの際に渡される実際の入力値に依存する。さらに、ソフトウェア・モジュールは、中間変数とも称されるローカル変数をいくつ有していてもよい。ローカル変数の値も直接または間接的に、入力変数の値に依存しうる。ローカル変数はローカルなスコープをもつ。ローカル変数は、そのローカル変数が宣言されているソフトウェア・モジュールのコンテキスト内でのみ存在し、該コンテキスト内からのみアクセス可能である。これに対し、ソフトウェア・モジュールが属するソフトウェア・アプリケーションは、グローバル変数をいくつ有していてもよい。グローバル変数は、ソフトウェア・アプリケーション自身の中においてグローバルなスコープをもち、ソフトウェア・アプリケーションに属すすべてのソフトウェア・モジュールにとってアクセス可能である。ソフトウェア・モジュールが呼び出されるとき、ソフトウェア・モジュールはグローバル変数の値にアクセスするまたはグローバル変数の値を修正してもよく、値修正はソフトウェア・モジュールがその実行を完了した後でさえ持続する。
【０００８】
具体的実施形態では、第一の変数の値が第二の変数の値に基づいて決定される（すなわち、第一の変数の値が第二の変数の値に依存する）とき、第一の変数は第二の変数に依存すると考えられる。変数は、入力変数であれ出力変数であれ、またローカル変数であれグローバル変数であれ、通例、特定のデータ型をもつ。データ型はたとえば、限定するものではないが、キャラクタ〔または文字〕、ストリング〔または文字列〕、整数、浮動小数点、倍精度、ブーリアン、ポインタ、配列および列挙といったものである。変数のデータ型は、どのような型のデータ（たとえば実際の値）がその変数に割り当てられてもよいかを示す。たとえば、整数型の変数には整数値だけが割り当てられるべきであり、ブーリアン型の変数には真偽値だけが割り当てられるべきである。異なるプログラミング言語は、特定の言語で書かれたソフトウェア・モジュールまたはアプリケーションの変数がもちうる異なるデータ型や、それらの特定のデータ型に適用されうる異なる演算を定義することがある。具体的実施形態では、プログラミング言語のデータ型は二つの範疇に分けられる：ストリングと数値である。数値データ型は、たとえば限定するものではないが整数、浮動小数点、倍精度およびブーリアンといった非ストリング・データ型を含んでいてもよい。
【０００９】
ストリングは多くのプログラミング言語において利用可能なデータ型である。ただ、異なるプログラミング言語は「ストリング」を異なる仕方で定義することもある。たとえば、ジャバ（Java(登録商標)）・プログラミング言語は型「string」をジャバ・クラス「java.lang.String」として定義する。これは、ストリングをキャラクタのイミュータブルなアレイとして表す。この場合、ひとたびストリング変数が宣言され、生成されると、その値はその後変えることができない。ストリング変数の値へのいかなる修正も、新しいストリング変数が宣言され、構築されることにつながる。クラス「java.lang.String」は「メソッド」と称される、ストリング変数に適用されうる多くの演算をも提供する。他方、Cプログラミング言語では、ストリングは、ヌル・キャラクタで終わる一次元キャラクタ配列として定義されうる。Cのストリングはミュータブルであり、その値はその場で修正されうる。実は、配列内の各キャラクタは個別に修正されてもよい。
【００１０】
各プログラミング言語は一般にいくつかの数値データ型を定義する。ただ、利用可能な具体的な数値データ型は言語によって異なることがある。整数、浮動小数点、倍精度およびブーリアンはたいていのプログラミング言語によって一般的に定義される数値データ型である。ここでもまた、異なるプログラミング言語は具体的な数値データ型を異なる仕方で定義することもある。たとえば、ジャバ・プログラミング言語は整数変数を宣言する二つの方法を提供する：プリミティブ・データ型「int」として、あるいはジャバ・クラス「java.lang.Integer」としてである。クラス「java.lang.Integer」は整数変数に適用されうる演算（すなわちメソッド）を提供する。他方、Cは、異なるデータ・サイズをもつ整数変数を宣言するために使用されうる三つのプリミティブ・データ型「short」「int」「long」を提供する。
【００１１】
時に、ソフトウェア・モジュールの入力、出力またはローカル変数に対して課される制約条件がいくつかあることがある。具体的実施形態では、変数に課される制約条件は、たとえば、限定するものではないが、その変数にどんな値が割り当てられてもよいか、その変数に割り当てられてもよいデータ値のサイズ、あるいはその変数に対して課される他の任意の適用可能な条件もしくは制限を指定してもよい。そのような変数制約条件は、ソフトウェア・モジュールの設計仕様もしくは形式上の要求、そのソフトウェア・モジュールを実装するために使われるプログラミング言語の仕様、そのソフトウェア・モジュールのプログラミング論理に含まれるコード、そのソフトウェア・モジュールが実行される実行時環境または他の適用可能な因子によって、またはそれらの因子から、指定されてもよい。たとえば、整数変数「a」に課されうる制約条件は、ソフトウェア・モジュールが４バイトを使って各整数を表す実行時環境内で実行されるため、整数変数「a」が0xFFFFFFFF以下の割り当てられた整数値であることしかできないことを指定する。この場合、整数変数「a」に課された制約条件は、式「a＜0xFFFFFFFF」として表現されてもよい。もう一つの例として、ストリング変数「s」に対して課されうる制約条件は、ストリング変数「s」の長さ（すなわちキャラクタ数）が8でなければならないことを指定する。この場合、ストリング変数「s」に対して課される制約条件は、別の式「s.length()＝8」として表現されてもよい。時に、ソフトウェア・モジュールの一つの変数に対して課される制約条件は、直接または間接に、ソフトウェア・モジュールの別の変数の値に課される制約条件に依存してもよい。たとえば、整数変数「b」に対して共同して課されうる二つの制約条件は：（１）整数変数「b」は−10以上の割り当てられた整数値であることしかできない、（２）整数変数「b」は変数「a」の値より小さな割り当てられた整数値であることしかできないことを指定する。この場合、組み合わせて整数変数「b」に課される二つの制約条件は、各制約条件を別個の式として表して、「(b>=−10)&&(b<a)」と表現されてもよい。
【００１２】
具体的実施形態では、ソフトウェア・モジュールは数値またはストリング変数をいくつ有していてもよく、これらの変数はソフトウェア・モジュールの入力変数であっても、あるいはローカル（すなわち中間）変数であってもよい。具体的実施形態では、一組の制約条件がソフトウェア・モジュールの特定の数値またはストリング変数に対して課されてもよい。一組の制約条件がソフトウェア・モジュールの一つ一つすべての変数に課されることは必要ではないことを注意しておく。具体的実施形態では、数値変数が与えられたとき、該数値変数は、数値制約条件またはストリング制約条件をいくつ有していてもよい。たとえば、整数変数「b」は、その値が−10以上でなければならないことを指定する数値制約条件（たとえば、制約条件「b>=−10」）を有していてもよい。整数変数「b」はまた、その値のテキスト（すなわちストリング）表現がストリング「182」に等しくなければならないことを指定するストリング制約条件（たとえば、制約条件「b.toString()="182"」）を有していてもよい。この場合、整数変数「b」に課される制約条件の集合は、数値制約条件とストリング制約条件の両方を含み、したがって、ハイブリッドの制約条件の集合である（たとえば、「(b>=−10)&&(b.toString()="182")」）。同様に、具体的実施形態において、ストリング変数を与えられたとき、該ストリング変数は、ストリング制約条件または数値制約条件をいくつ有していてもよい。たとえば、ストリング変数「s」は、その値が部分ストリング「ca」で始まらなければならないことを指定するストリング制約条件（たとえば、制約条件「s.substring(0,1)="ca"または"s.startsWith("ca")」）を有していてもよい。ストリング変数「s」はまた、その値が8キャラクタの長さをもたなければならないことを指定する数値制約条件（たとえば、制約条件「s.length()=8」）を有していてもよい。この場合もまた、ストリング変数「s」に課される制約条件の集合は、数値制約条件およびストリング制約条件の両方を含み、したがってハイブリッドの制約条件の集合である「(s.substring(0,1)="ca")&&(s.length()=8)」）。
【００１３】
具体的実施形態では、ソフトウェア・モジュールに課される制約条件は、入力変数、出力変数およびローカル変数を含むその変数に対して課される制約条件すべてを組み合わせて含んでいてもよい。たとえば、整数変数「b」およびストリング変数「s」が両方ともソフトウェア・モジュール「m」に属するとする。この場合、ソフトウェア・モジュール「m」自身に課される制約条件の集合は、変数「b」および「s」にそれぞれ課される制約条件の二つの集合の論理和を含み、これは(b>=−10)&&(b.toString()="182")&&(s.substring(0,1)="ca")&&(s.length()=8)に等しい。この集合は数値制約条件およびストリング制約条件の両方を含むので、これもハイブリッドの制約条件の集合である。
【００１４】
具体的実施形態では、任意の数の数値変数またはストリング変数を有するソフトウェア・モジュールに課されるハイブリッドの制約条件の集合を決定および解決することが有用であることがありうる。ソフトウェア・モジュールの特定の変数に対して課されるハイブリッドの制約条件の集合を決定および解決することも有用であることがありうる。具体的実施形態では、制約条件の集合を解決する（solving）とは、集合に含まれる制約条件すべてを満たす一つまたは複数の解を見出すことを試みることを意味する。図１は、ソフトウェア・モジュールまたはソフトウェア・モジュールの変数に対して課される制約条件を決定および解決するための例示的方法を示している。図２は、ソフトウェア・モジュールまたはソフトウェア・モジュールの変数に対して課される制約条件を決定および解決するためのシステム２００を示している。具体的な実施形態では、図２に示されるシステム２００のコンポーネントは、コンピュータ・ハードウェアもしくはソフトウェアまたはそれらの組み合わせとして実装されてもよい。図１および図２については、互いとの関連で記述する。
【００１５】
具体的実施形態では、ソフトウェア・モジュールは任意の数の数値変数またはストリング変数を有していてもよい。たとえば、ソフトウェア・モジュール「m」は整数変数「vi」、ブーリアン変数「vb」およびストリング変数「vs」を有していてもよい。この場合、変数「vi」および「vb」は数値変数である。具体的実施形態では、これらの変数はソフトウェア・モジュールの入力変数、出力変数またはローカル変数であってもよい。
【００１６】
具体的実施形態では、最初に、ソフトウェア・モジュールの特定の諸数値変数に対して課される任意の数の数値制約条件およびソフトウェア・モジュールの特定の諸ストリング変数に対して課される任意の数のストリング制約条件があってもよい。より具体的には、ある特定の数値変数に対して一組の数値制約条件が指定され、課されてもよく、あるいはある特定のストリング変数に対して一組のストリング制約条件が指定され、課されてもよい。制約条件の各組は、一つまたは複数の個別的な制約条件を含んでいてもよい。たとえば、整数変数「vi」に対して数値制約条件（numeric  constraint）の集合「nc1-vi」が指定され、課されてもよく、ブーリアン変数「vb」に対して数値制約条件の集合「nc1-vb」が指定され、課されてもよく、ストリング変数「vs」に対してストリング制約条件（string  constraint）の集合「sc1-vs」が指定され、課されてもよい。具体的実施形態では、これらの制約条件の初期集合（たとえば、「nc1-vi」「nc1-vb」および「sc1-vs」）は、ソフトウェア・モジュールの設計仕様または形式的な要求に基づいて指定されてもよい。
【００１７】
具体的実施形態では、ソフトウェア・モジュール内で、ソフトウェア・モジュールの個別的な諸数値変数に適用される、数値入力を受けるまたは数値出力を生成する演算がいくつあってもよい。たとえば、整数変数「vi」に適用される演算は「ri=vi+10」であってもよい。これは、「vi」の値および「10」の二つの数値を入力として受け、数値つまり「ri」の値を出力として生成する。
【００１８】
具体的実施形態では、ソフトウェア・モジュール内で、ソフトウェア・モジュールの個別的な諸数値変数に適用される、ストリング入力を受けるまたはストリング出力を生成する演算がいくつあってもよい。たとえば、ブーリアン変数「vb」に適用される演算は「vb.toString()」であってもよい。これは、ブーリアン変数「vb」の値のストリング表現であるストリング値を出力として生成する。
【００１９】
具体的実施形態では、ソフトウェア・モジュール内で、ソフトウェア・モジュールの個別的な諸ストリング変数に適用される、ストリング入力を受けるまたはストリング出力を生成する演算がいくつあってもよい。たとえば、ストリング変数「vs」に適用される演算は「rs=vs.concat("abc")」であってもよい。これは、「vs」の値および「abc」の二つのストリング値を入力として受け、ストリング値、つまり「rs」の値を出力として生成する。
【００２０】
具体的実施形態では、ソフトウェア・モジュール内で、ソフトウェア・モジュールの個別的な諸ストリング変数に適用される、数値入力を受けるまたは数値出力を生成する演算がいくつあってもよい。たとえば、ストリング変数「vs」に適用される演算は「vs.length()」であってもよい。これは、ストリング変数「vs」の値に含まれるキャラクタの数を示す数値をその出力として生成する。ストリング変数「vs」に適用されるもう一つの演算は、二つの数値を入力として取る「vs.substring(5,7)」であってもよい。
【００２１】
具体的実施形態は、図１のステップ１０２に示されるように、ソフトウェア・モジュール（たとえばソフトウェア・モジュール「m」）と、ソフトウェア・モジュールの個別的な数値変数に対して最初に指定され、課されている数値制約条件の集合（たとえば、整数変数「vi」に課される数値制約条件「nc1-vi」およびブーリアン変数「vb」に課される数値制約条件「nc1-vb」）と、ソフトウェア・モジュールの個別的なストリング変数に対して最初に指定され、課されているストリング制約条件の集合（たとえば、ストリング変数「vs」に課されるストリング制約条件「sc1-vs」）とを解析してもよい。具体的実施形態では、数値制約条件およびストリング制約条件は、最初、ソフトウェア・モジュールの入力変数または中間変数（すなわちローカル変数）に課されていてもよい。もちろん、具体的実施形態では、ソフトウェア・モジュールの一つ一つすべての数値変数に数値制約条件の集合が最初に課されており、ソフトウェア・モジュールの一つ一つすべてのストリング変数にストリング制約条件の集合が最初に課されていることは必要ではない。特定の諸数値変数だけが関連付けられた数値制約条件を最初に有している、あるいは特定の諸ストリング変数だけが関連付けられたストリング制約条件を最初に有していることも可能である。
【００２２】
具体的実施形態では、ソフトウェア・モジュールの入力変数に最初に課されていた数値制約条件またはストリング制約条件について、該制約条件は、ソフトウェア・モジュールの設計仕様または形式的な要求に従って決定されてもよい。ソフトウェア・モジュールの中間変数に最初に課されていた数値制約条件またはストリング制約条件について、該制約条件は、ソフトウェア・モジュール上で記号的実行を行うことによって決定されてもよい。記号的実行（symbolic  execution）は、下記で図８との関連でより詳細に述べる。手短に言うと、具体的実施形態は、ソフトウェア・モジュールの各入力変数に記号的値（symbolic  value）を代入しながらソフトウェア・モジュール上で記号的実行を行ってもよい。ソフトウェア・モジュールの中間変数は、直接または間接に、ソフトウェア・モジュールの入力変数のうちの一つまたは複数の入力変数に依存することがあるので、ソフトウェア・モジュール上で記号的実行を行う結果として、該中間変数について、それが前記特定の入力変数に対してもつ依存性を示す記号的表現（symbolic  expression）の集合が与えられうる。具体的実施形態は次いで、該中間変数について得られた記号的表現の前記集合と、該中間変数が依存する前記特定の入力変数に課される前記制約条件に基づいて、該中間変数に課される制約条件の集合を決定しうる。たとえば、ソフトウェア・モジュール「m」に関し、「vi」が入力変数、「ri」が中間変数であり、「ri=vi+10」であるとする。この場合、ソフトウェア・モジュール「m」上で記号的実行を行うことで、中間変数「ri」が入力変数「vi」に依存することを決定しうる。さらに、入力変数「vi」に対して、「vi>0」というような数値制約条件が課されているとする。記号的実行の結果および入力変数「vi」に課される数値制約条件に基づいて、中間変数「ri」について、「ri>10」のような数値制約条件が決定されうる。
【００２３】
図１のステップ１０２に示される解析から、図１のステップ１０４に示されるように、具体的実施形態は、ソフトウェア・モジュールの個別的な数値変数に課されるストリング制約条件の集合と、ソフトウェア・モジュールの個別的なストリング変数に課される数値制約条件の集合を推定しうる。具体的実施形態では、図１のステップ１０２および１０４は、図２に示されるシステム２００のコンポーネント２０２〔相互的制約条件発生器／クロス制約条件発生器〕によって実行されてもよい。具体的実施形態では、コンポーネント２０２はソフトウェア・モジュール２１２およびソフトウェア・モジュール２１２の変数に最初に課される制約条件２１４を入力として取りうる。制約条件２１４はソフトウェア・モジュールの数値変数に対して最初に指定され、課される数値制約条件およびソフトウェア・モジュールのストリング変数に対して最初に指定され、課されるストリング制約条件を含んでいてもよい。コンポーネント２０２は、ソフトウェア・モジュール２１２の数値変数に課されることになるストリング制約条件およびソフトウェア・モジュール２１２のストリング変数に課されることになる数値制約条件を推定するために適用可能な解析を実行してもよい。コンポーネント２０２は、ソフトウェア・モジュール２１２の変数に課される指定された制約条件および推定された制約条件の両方を含む数値制約条件およびストリング制約条件のハイブリッドの集合を出力として提供しうる。
【００２４】
具体的実施形態では、ソフトウェア・モジュールの変数についての制約条件は、さまざまな因子に基づいて推定されてもよく、本開示は任意の適用可能な因子を考えている。たとえば、限定するものではないが、特定の変数に適用される演算、ソフトウェア・モジュールを実装するために使われるプログラミング言語の仕様、ソフトウェア・モジュールが実行される実行時環境または複数の因子の組み合わせに基づいて、数値制約条件が数値変数およびストリング変数の両方について推定されてもよく、ストリング制約条件が数値変数およびストリング変数の両方について推定されてもよい。
【００２５】
具体的実施形態では、数値変数を与えられたとき、該数値変数に適用される、ストリング結果を生じうる演算に基づいてストリング制約条件が推定されてもよい。たとえば、ソフトウェア・モジュール「m」において整数変数「vi」に次の二つの演算「(vi.toString()).split("0")」が適用されるとする。これは、まず整数変数「vi」の値のストリング表現（たとえば数182がストリング「182」として表現される）を生成し、次いでそのストリングを、キャラクタ「0」の位置で、二つの新しいストリングに分割する。第二の演算（すなわちストリング分割演算）が成功する（たとえば、結果としてヌル・ストリングを生じない）ために、それらの演算から、整数変数「vi」の値のストリング表現が少なくとも一つのキャラクタ「0」を含まなければならないというストリング制約条件が推定されてもよい。
【００２６】
具体的実施形態では、数値変数が与えられたとき、該数値変数に適用される、数値結果を生じうる演算に基づいて数値制約条件が推定されてもよい。たとえば、ソフトウェア・モジュール「m」において整数変数「vi」に次の演算「Math.sqrt(vi)」が適用されるとする。これは、整数変数「vi」の値の平方根を与える。この演算をエラーに遭遇することなく実行するために、この演算から、整数変数「vi」の値が0以上でなければならないという数値制約条件が推定されてもよい。
【００２７】
具体的実施形態では、ストリング変数を与えられたとき、該ストリング変数に適用される、ストリング結果を生じうる演算に基づいてストリング制約条件が推定されてもよい。たとえば、ソフトウェア・モジュール「m」においてストリング変数「s」に次の演算「s.replaceAll("abc","xyz")」が適用されるとする。これは、ストリング変数「s」の値において見出されるすべての部分ストリング「abc」を「xyz」で置換する。この演算がストリング変数「s」に対して何らかの実際の効果をもつために、この演算から、ストリング変数「s」の値が少なくとも一つの部分ストリング「abc」の生起を含まなければならないというストリング制約条件が推定されてもよい。
【００２８】
具体的実施形態では、ストリング変数を与えられたとき、該ストリング変数に適用される、数値結果を生じうる演算に基づいて、あるいは該ストリング変数に適用される、一つまたは複数の数値入力を取りうる演算に基づいて、数値制約条件が推定されてもよい。たとえば、ソフトウェア・モジュール「m」においてストリング変数「s」に次の演算「s.startsWith("abc")」が適用されるとする。これは、ストリング変数「s」の値が部分ストリング「abc」で始まるかどうかを示すブーリアン結果を真または偽として与える。この演算の実行が成功するためには、ストリング変数「s」の値は少なくとも三つの文字を有する必要がある。よって、この演算から、ストリング変数「s」の長さが3以上でなければならないという数値制約条件が推定されうる。もう一つの例として、ソフトウェア・モジュール「m」においてストリング変数「s」に数値を入力として取る次の演算「s.substring(6)」も適用されるとする。この演算の実行が成功する（たとえば結果としてヌル・ストリングを生じない）ためには、ストリング変数「s」の値は少なくとも６文字を有する必要がある。よって、この演算から、ストリング変数「s」の長さが6以上でなければならないという数値制約条件が推定されうる。
【００２９】
上記の例において、ソフトウェア・モジュール内において、ストリング結果を生じる演算が数値変数に適用されることがあり、あるいは数値入力を取るか数値結果を生じる演算がストリング変数に適用されることがある。具体的実施形態では、これらの演算から、個別的なストリング変数に対して数値制約条件が推定され、課されることができ、個別的な数値変数に対してストリング制約条件が推定され、課されることができる。具体的実施形態では、数値変数であれストリング変数であれ変数が与えられたとき、該変数に課される制約条件の完全な集合は、該変数についてもしあれば最初に指定された制約条件と、該変数についてもしあれば推定された制約条件の両方を含む。この制約条件の集合は、数値制約条件またはストリング制約条件または両方を含むことがありうる。変数に対して課される制約条件の集合が、該変数に適用される個々の演算に基づいて該変数について推定された制約条件を含むことがあるので、具体的実施形態はこのようにして得られた制約条件の集合のことを、制約条件の相互作用するハイブリッドな集合（interacting  hybrid  set  of  constraints）と称する。具体的実施形態では、任意の数の数値変数またはストリング変数を有するソフトウェア・モジュールが与えられたとき、ソフトウェア・モジュール自身に課される制約条件の集合は、該ソフトウェア・モジュールの個々の変数に課される制約条件すべてを含む。
【００３０】
ソフトウェア・モジュールの変数またはソフトウェア・モジュール自身に課される制約条件のハイブリッドの集合を与えられたとき、図１のステップ１０６に示されるように、具体的実施形態は、前記集合中の各数値制約条件を数式で表現してもよく（たとえば、「vi>=0」、「vb=true」または「s.length()>=6」）、前記集合中の各ストリング制約条件を有限状態機械（FSM:  finite  state  machine）で表現してもよい。
【００３１】
一般に、FSMは有限個の状態、該状態間の遷移および作用からなる挙動のモデルである。具体的実施形態では、FSMはストリングを表現するために使用されてもよい。図３は、ストリングを表現するために使われるいくつかのFSMを示している。図３では、各FSMについて、中間状態（intermediate  state）は一本線の丸で表され、受け容れ状態（accepting  state）は二本線の丸で表され、状態への入力は丸につながる矢印によって表されている。
【００３２】
たとえば、FSM  ３１０は、任意のキャラクタを有することができ任意の長さでよいストリング「S」を表す。FSM  ３２０は、少なくとも一つのキャラクタを有し、当該ストリング最後のキャラクタが「Z」であり、制約条件「S.endsWith("Z")=true」を表すために使われてもよいストリング「S」を表す。FSM  ３３０は三つ以上のキャラクタを有し、制約条件「S.length()>=3」を表すために使われてもよいストリング「S」を表す。
【００３３】
FSM  ３４０は、少なくとも一つのキャラクタを有し、少なくとも一つの「Z」を含むストリング「S」を表す。「Z」遷移はストリング中の最後の「Z」を表す。FSM  ３５０は、「Z」であるキャラクタを全くもたないストリング「S」を表す。制約条件「(a=S.lastIndexOf("Z"))」を考える。この制約条件から、「a>=0」であれば「(S.substring(a,a+1)="Z")」であることが推定できる。FSM  ３４０は、上記の制約条件が満足される場合を表している。すなわち、ストリング「S」は少なくとも一つの「Z」キャラクタを含み、「S」中に現れる最後の「Z」は「a」の値に等しいインデックスにある。他方、FSM  ３５０は制約条件の前記集合が満足されない場合を表す。つまり、ストリング「S」はキャラクタ「Z」を全く含まず、よって「a=−1」である。これから、制約条件「a=S.lastIndexOf("Z")」は記号的実行木における岐路（fork）につながり、一方の分枝では追加的な数値制約条件「a>=0」をもつFSM  ３４０の場合を想定し、他方の分枝では追加的な制約条件「a=−1」をもつFSM  ３５０の場合を想定する。
【００３４】
図４は、ストリング「S」およびその部分ストリングの一つ「S.substring(2,4)」を表すために使われるもう一つの例示的なFSM  ４００を示す。この例では、状態４０２がストリング「S」の開始点であり、状態４０４がストリング「S」の受容状態（すなわち終点）である。部分ストリング「S.substring(2,4)」は、三番目のキャラクタで始まり、五番目のキャラクタで終わる「S」の部分ストリングである。ジャバ・プログラミング言語によれば、インデックス付けは0で始まる、つまり最初の要素のインデックス番号が0であることを注意しておく。よって、インデックス番号2は三番目の要素を指し、インデックス番号4は五番目の要素を表すのである。部分ストリング「S.substring(2,4)」について、開始点はストリング「S」の開始状態４０２から進んで三番目の状態であり、これはストリング「S」の三番目のキャラクタに対応する。図４では、開始状態４０２から進んで三番目の状態である三つの状態４１２Ａ、４１２Ｂ、４１２Ｃがあり、これらのうちのいずれもが部分ストリング「S.substring(2,4)」についての可能な開始状態４１２である。部分ストリング「S.substring(2,4)」について、終点（すなわち受容状態）はストリング「S」の開始状態４０２から進んで五番目の状態であり、これはストリング「S」の五番目のキャラクタに対応する。図４では、開始状態４０２から進んで五番目の状態である三つの状態４１４Ａ、４１４Ｂ、４１４Ｃがあり、これらのうちいずれも部分ストリング「S.substring(2,4)」についての可能な受容状態４１４である。図４において、「ε」はヌル入力遷移を示すことを注意しておく。
【００３５】
具体的実施形態では、任意の制約条件の集合が与えられたとき、該集合からの各数値制約条件は適用可能な数式を使って表現されてもよく、該集合からの各ストリング制約条件は適用可能なFSMを使って表現されてもよい。さらに、このように表現された制約条件の集合を与えられたとき、具体的実施形態は、図１のステップ１０８において示されるように、前記集合中の制約条件すべてを同時に満たす一つまたは複数の解を見出すためにそれらの制約条件を解決することを試みてもよい。具体的実施形態では、図１のステップ１０８は、図２に示されるシステム２００のコンポーネント２０４によって実行されてもよい。具体的な実施形態では、コンポーネント２０４は背景理論の枠内での充足可能性（SMT:  Satisfiability  Modulo  Theories）に部分的に基づいて実装される拘束条件ソルバであってもよい。具体的実施形態では、コンポーネント２０４は、数式を使って表現された数値制約条件およびFSMを使って表現されたストリング制約条件のいずれかまたは両方を含んでいてもよい制約条件の集合を入力として取り、該集合からの制約条件すべてを満たす一つまたは複数の解を見出そうと試みてもよい。何らかの解が見出されうる場合、コンポーネント２０４はその解を出力として与えてもよい。もちろん、制約条件の集合が、該集合からの制約条件すべてを満たす解を全くもたないこともありうる。たとえば、制約条件の集合「(s.equals(q))&&(s.startsWith("uvw"))&&(q.endsWith("xyz"))&&(s.length()<a)&&((a+b)<6)&&(b>0)」を考える。ここで、「s」および「q」はストリングであり、「a」および「b」は整数である。この集合からの制約条件すべてを同時に満たすことのできる「s」「q」「a」「b」についての値の組み合わせは存在しない。したがって、この特定の制約条件の集合は充足不可能である。
【００３６】
具体的実施形態は、逐次反復アルゴリズムを使ってハイブリッドの制約条件の集合を解いてもよい。具体的実施形態は、前記集合からの、FSMを使って表現されているストリング制約条件すべてをストリング・ドメインにおいてグループ化し、前記集合からの、数式を使って表現されている数値制約条件すべてを数値ドメインにおいてグループ化する。具体的実施形態は次いで、数値ドメインまたはストリング・ドメインいずれか単独における一つまたは複数の解（すなわち、前記集合中の数値制約条件すべてまたは前記集合中のストリング制約条件すべてのどちらかを満足する解）を見出すことを試み、一方のドメインで見出された解を他方のドメインに供給することを、（１）前記集合中の数値制約条件およびストリング制約条件のすべてを満足する一つまたは複数の解が見出される；（２）前記集合中の制約条件すべてを満たす解が存在しないと判定される；あるいは（３）実行された逐次反復数が所定の閾値に達した、のうちいずれか最初に起こるものが生起するまで、逐次的に行ってもよい。具体的実施形態は、SMTソルバを使って数値領域における数値制約条件を解決し、正規表現の併合、交わり、補集合、クリーネ・スター（Kleene  star）および他の適用可能なアルゴリズムを使ってストリング・ドメイン中のストリング制約条件を解決してもよい。さらに、具体的実施形態は、制約条件のハイブリッドの集合について一つまたは複数の解を見出すことを試みるときに、次のことを考慮に入れてもよい。第一に、数値ドメイン単独における数値制約条件が充足不可能である場合（つまり、前記集合中の数値制約条件だけを満足する解すら存在しない場合）、制約条件の集合全体も充足不能である。第二に、ストリング・ドメイン単独におけるストリング制約条件についての解がヌル・ストリング（すなわち空っぽなストリング）である場合、前記集合中に数値制約条件が全くなければ、前記集合は充足不能であり、そうでなければ前記集合中の数値制約条件が前記ヌル・ストリングによってさらに制約される。
【００３７】
上記の逐次反復プロセスをさらに説明するために、例示的な制約条件の集合「(s.startsWith("uvw"))&&(s.endsWith("xyz"))&&(a=s.lastIndexOf("t"))&&(s.length()<=b)&&(b+c<=8)&&((a+d)>=4)&&(c>0)&&(d<0)」を考える。ここで、「s」はストリングであり、「a」「b」「c」「d」は整数である。この制約条件の集合を満たす解は、ストリング「s」および整数「a」「b」「c」「d」についての五つの値の組み合わせであって、前記集合中の個々の制約条件すべてを同時に満足させる（すなわち、すべての条件が真になる）ものがあることを意味する。より具体的には、制約条件「s.startsWith("uvw")」を満たすためには、「s」の最初の三つのキャラクタが「uvw」でなければならない。制約条件「s.endsWith("xyz")」を満たすためには、「s」の最後の三つのキャラクタが「xyz」でなければならない。制約条件「a=s.lastIndexOf("t")」を満たすためには、「s」においてキャラクタ「t」の最後の生起が「a」の値に等しいインデックス番号をもたなければならない。制約条件「s.length()<=b」を満たすためには、「s」中のキャラクタ数が「b」の値以下でなければならない。制約条件「b+c<=8」を満たすためには、「b」および「c」の値の和が8以下でなければならない。制約条件「(a+d)>=4」を満たすためには、「a」および「d」の値の和は4以上でなければならない。制約条件「c>0」を満たすためには、「c」の値は0より大きくなければならない。制約条件「d<0」を満たすためには、「d」の値は0より小さくなければならない。
【００３８】
図５は、上記の例示的な制約条件の集合におけるストリング制約条件５１２をストリング・ドメイン５１０に入れ、上記の例示的な制約条件の集合における数値制約条件５２２を数値ドメイン５２０に入れることを示している。最初の反復工程５３１の間に、具体的実施形態は、ストリング・ドメイン５１０だけにおいて解を見出すことを試みてもよい。三つのストリング制約条件５１２は合わさって：（１）ストリング「s」の最初の三つのキャラクタが「uvw」でなければならず；（２）ストリング「s」の最後の三つのキャラクタが「xyz」でなければならず；（３）ストリング「s」において「t」の少なくとも一つの生起がなければならず；（４）「t」は「uvw」より後かつ「xyz」より前にこなければならないことを要求している。したがって、四つの要件すべてを満たす最短のストリングは「uvwtxyz」である。四つの要件すべてを満たす他の可能な、より長いストリングもある（たとえば、「uvwabtthxyz」または「uvwt3fkxyz」）。しかしながら、具体的実施形態は、常に、最も単純な可能な解を最初に選択する（すなわち、ストリング制約条件または数値制約条件によって指定される要件すべてを満たす最も短いストリングまたは最も小さい値）。この場合、四つの要件すべてを満たす最も短いストリングは「uvwtxyz」である。ストリング・ドメイン５１０に見出されるこのストリング解「uvwtxyz」が、「a」「b」「c」「d」についての解を見出すのを助けるために数値ドメイン５２０に供給される。
【００３９】
第二の反復工程５３２の間、具体的実施形態は、前の反復工程の間に「s」について見出された解（すなわち「uvwtxyz」）から、整数「a」「b」「c」「d」に対して課される追加的な制約条件５２４を導出してもよい。たとえば、制約条件「s.length()<=b」は、「s」中のキャラクタ数が「b」の値以下でなければならないことを要求する。ストリング・ドメイン５１０において見出された「s」についての最も短いストリング解は最小で七個のキャラクタをもたなければならないので、これは「b>=7」を意味する。制約条件「a=s.lastIndexOf("t")」は、「s」におけるキャラクタ「t」の最後の生起が「a」の値に等しいインデックス番号をもたなければならないことを要求する。「t」は「s」における最後のキャラクタではないので、これは「a<b」を意味する。さらに、「t」は「s」における最初の三つのキャラクタのどれかであることはできないので、これは「a>=3」であることも意味する。具体的実施形態は、「s」についての前記の解から導出される、「a」「b」「c」に課される三つの追加的数値制約条件５２４を、もともと前記集合からの四つの数値制約条件５２２に追加して、もともと前記集合からの制約条件およびストリング「s」についての前記解から導出された制約条件を含む数値制約条件５２２、５２４すべてを満たす「a」「b」「c」「d」についての値を見出すことを試みてもよい。ここでもまた、数値制約条件すべてを満たす整数「a」「b」「c」「d」についての複数の値がある場合には、具体的実施形態は最も小さい値を最初に選択する。前記集合からの四つのもともとの数値制約条件５２２および上記の三つの追加的な、導出された数値制約条件５２４から、具体的実施形態は、「a」「b」「c」「d」についての可能な解を、「a＝5」「b＝7」「c＝1」「d＝−1」として決定してもよい。実は、「a」については、二つの可能な値5および6がある。値5が最小であり、よって「a」についてまず選択される。これら四つの値は、ストリング制約条件に対して検証されるために、ストリング・ドメイン５１０にフィードバックされる。
【００４０】
第三の反復工程５３３では、第二の反復工程５３２の間に数値ドメイン５２０において見出された「a」「b」「c」「d」についての解が、ストリング・ドメイン５１０においてストリング制約条件に対して検証される。「s」が「uvwtxyz」であれば、「a」の値に等しいはずの「t」のインデックスは3なので、「a」は「5」に等しくなることはできない。「a」に対するこの新たな制約５２６（すなわち、「a!=5」）は、再び数値ドメイン５２０にフィードバックされる。
【００４１】
第四の反復工程５３４の間、制約条件５２６、すなわち「a!=5」が他の既存の数値制約条件５２２、５２４に追加される。現在存在している数値制約条件５２２、５２４、５２６すべてを満たす「a」「b」「c」「d」についての次の可能な解は「a＝6」「b＝7」「c＝1」「d＝−1」である。この解がストリング・ドメイン５１０にフィードバックされる。
【００４２】
第五の反復工程５３５の間、前の反復工程の間に数値ドメイン５２０において「a」「b」「c」「d」について見出された解（すなわち、「a＝6」「b＝7」「c＝1」「d＝−1」）が、同じようにして、ストリング・ドメイン５１０においてストリング制約条件に対して検証される。以前と同様、「s」が「uvwtxyz」であれば、「a」は「6」に等しくなることはできない。これは「a」に対する新たな制約条件５２８（すなわち、「a!=6」）を与え、数値ドメイン５２０にフィードバックされる。
【００４３】
第六の反復工程５３６の間、再び、制約条件５２８、すなわち「a!=6」が他の既存の数値制約条件５２２、５２４、５２６に追加される。数値制約条件５２２、５２４、５２６、５２８すべてを満たす解を見出す試みがされる。ところが、現在存在している数値制約条件５２２、５２４、５２６、５２８すべてを満たす「a」「b」「c」「d」についての値は存在しない。したがって、「s」が「uvwtxyz」であるとすると、すべての数値制約条件を満たす「a」「b」「c」「d」について見出すことのできる解は存在しない。この場合、「s」は、「s.length()<b」「b+c<=8」「c>0」という三つの制約条件のため、七個より多くのキャラクタをもつことはできない。より具体的には、「c>0」なので、「c」がもちうる最小の値は1である。「b+c<=8」なので、「c」がもちうる最小の値が1なら、「b」がもちうる最大の値は7である。これは、「s.length()<b」なので、「s」がもちうる最大の長さは七キャラクタであることを意味する。この点で、この制約条件の集合は充足不能であると判定されたことになる。したがって、プロセスは停止してもよい。
【００４４】
図１に示される例示的プロセスは、ソフトウェア・モジュールまたはソフトウェア・モジュールの特定の変数に課されるハイブリッドの制約条件の集合（すなわち、数値制約条件およびストリング制約条件の両方を含む制約条件の集合）を決定するために使われてもよい。そのようなプロセスについては、さまざまな実際的な応用がある。
【００４５】
具体的実施形態では、図１に示されるようなプロセスは、ソフトウェア・モジュールについての試験データを自動的に生成するために使用されてもよい。次いで、その試験データはソフトウェア・モジュールを試験し、ソフトウェア・モジュールにおけるエラーを検出するために使用されてもよい。しばしば、ソフトウェア・モジュールはいくつかの条件分岐点（たとえば「if-else」文）を含むことがあり、各条件分岐点はソフトウェア・モジュールの一つまたは複数の変数（たとえば入力変数またはローカル変数）によって指定される分岐条件をもつ。分岐条件が満たされるかどうかに依存して、ソフトウェア・モジュールは、条件分岐点における異なる実行経路をたどって進行しうる。条件分岐点をさらに説明するために、例示的なソフトウェア・モジュールの次の例示的コード・セグメントを考える。
【表１】
0005786511.tif 000002
【００４６】
上例において、「m」「n」「k」はこの例示的なソフトウェア・モジュールの変数であってもよい。第１行では、条件分岐点があり、分岐条件は「m>n  &&  k<=10」である。分岐条件は複数の下位条件（たとえば「m>n」および「k<=10」）を含んでいてもよいことを注意しておく。第１行における分岐条件が満たされる（すなわち、真である）ためには、変数「m」の値は変数「n」の値より大きい必要があり、変数「k」の値は10以下である必要がある。第１行における分岐条件が満たされる場合、第２〜１１行のコードが実行される。それ以外の場合（すなわち、第１行の分岐条件が満たされない場合）、第１３行のコードが実行される。第３行では、もう一つの条件分岐点があり、分岐条件は「k>2」である。第３行の分岐条件が満たされるためには、変数「k」の値が2より大きくなければならない。同様に、第３行の分岐条件が満たされる場合、第４行のコードが実行される。それ以外の場合には、第６〜１１行のコードが実行される。第６行では、第三の分岐点があり、分岐条件は「n==k  ||  n==m」である。これも複数の下位条件（たとえば「n==k」および「n==m」）を含んでいる。第６行の分岐条件が満たされるためには、変数「n」の値が変数「k」の値または変数「m」の値に等しい必要がある。第６行の分岐条件が満たされる場合、第７行のコードが実行される。それ以外の場合、第９行のコードが実行される。
【００４７】
さらに、第３行の条件分岐点は第１行の条件分岐点内にネストされており、第６行の条件分岐点は第３行の条件分岐点内にさらにネストされている。第１行の条件分岐点に付随する分岐条件が満たされない場合、このコードの実行中に第３行の条件分岐点に到達することは決してない。しかしながら、第３行の条件分岐点に付随する分岐条件が満たされない場合、第６行の条件分岐点はこのコードの実行中に到達される。実は、第６行の条件分岐点に到達するためには、第１行の分岐条件が満たされる必要があるが、第３行の分岐条件は満たされることができない。
【００４８】
したがって、ソフトウェア・モジュール中の各条件分岐点において、条件分岐点に付随する分岐条件が満たされるかどうかに依存して、ソフトウェア・モジュールは異なる実行経路に沿って進む。図６は、複数レベルのネストされた条件分枝をもつ例示的ソフトウェア・モジュールの実行経路を示している。条件分岐点６０２において、「条件１」が満たされる場合、実行経路は処理ステップ６１２のほうに進み、「条件１」が満たされない場合、実行経路は処理ステップ６１４のほうに進む。条件分岐点６０２内にネストされている条件分岐点６０４において、「条件２」が満たされる場合、実行経路は処理ステップ６１６のほうに進み、「条件２」が満たされない場合、実行経路は終了する。やはり条件分岐点６０２内にネストされている条件分岐点６０６では、「条件３」が満たされる場合、実行経路は終了し、「条件３」が満たされない場合、実行経路は条件分岐点６０８のほうに進む。条件分岐点６０６内にさらにネストされている条件分岐点６０８では、「条件６」が満たされる場合、実行経路は処理ステップ６１８のほうに進み、「条件６」が満たされない場合、実行経路は処理ステップ６２２のほうに進む。図６では、五つの可能な実行経路があり、ソフトウェア・モジュールは、個々の条件分岐点６０２、６０４、６０６、６０８において分岐条件が満たされるかどうかに依存して、これら五つの可能な実行経路のうちのどの一つに沿って進むこともありうる。
【００４９】
具体的実施形態は、分岐条件を、分岐条件を表す変数に課された数値制約条件またはストリング制約条件と考えてもよい。たとえば、サンプル・コード１の第１行において、分岐条件は「m>n  &&  k<=10」である。この分岐条件が満たされれば、「m」の値は「n」の値より大きくなければならず、「k」の値は10以下でなければならない。これは、「m」「n」「k」に課される制約条件の集合として、「(m>n)  &&  (k<=10)」と表現されてもよい。この制約条件の集合を満たす「m」「n」「k」についての任意の解は、この分岐条件が満たされる（すなわち成り立つ）結果につながり、ソフトウェア・モジュールをある実行経路（すなわち、コードの「if」部分）に沿って進ませる。この分岐条件が満たされない場合は、「m」の値が「n」の値以下であるか「k」の値が10より大きいということである。これは、「m」「n」「k」に課される別の制約条件の集合として、「(m<=n)  ||  (k>10)」と表現されてもよい。この第二の制約条件の集合を満たす「m」「n」「k」についての任意の解は、この分岐条件が満たされない（すなわち偽になる）結果につながり、ソフトウェア・モジュールを別の実行経路（すなわち、コードの「else」部分）に沿って進ませる。
【００５０】
このように、具体的実施形態は、ソフトウェア・モジュールにおける可能な各実行経路に対応する制約条件の集合を決定し、制約条件の各集合について一つまたは複数の解を見出し、該解を試験入力として使ってソフトウェア・モジュールを試験してもよい。図７は、一つまたは複数の条件分岐点から帰結する複数の可能な実行経路を含むソフトウェア・モジュールを試験する例示的な方法を示している。具体的実施形態では、ソフトウェア・モジュールは任意の数の変数（たとえば入力変数またはローカル変数）および任意の数の条件分岐点（たとえば「if-else」文）を有していてもよい。各条件分岐点は、前記変数の一つまたは複数によって指定される分岐条件に関連付けられていてもよい。具体的実施形態では、分岐条件は任意の数の下位条件を含んでいてもよい。条件分岐点に付随する分岐条件が満たされるかどうかに依存して、ソフトウェア・モジュールは異なる実行経路に沿って進んでもよい。
【００５１】
具体的実施形態は、図７のステップ７０２に示されるように、ソフトウェア・モジュールに対して記号的実行を行って、ソフトウェア・モジュールの可能な各実行経路について、ソフトウェア・モジュールをその実行経路に沿って進ませその実行経路の終わりに到達させる記号的表現の集合を決定してもよい。記号的表現の各集合を決定するとき、具体的実施形態は、もしあればソフトウェア・モジュールの特定の諸変数に最初に課されていた数値制約条件およびストリング制約条件（たとえば図１のステップ１０２との関連で述べたような）と、もしあればソフトウェア・モジュールの特定の諸変数について推定された数値制約条件およびストリング制約条件（たとえば図１のステップ１０４との関連で述べたような）とを組み込んでもよい。具体的実施形態では、図７のステップ７０２は図２に示されるシステム２００のコンポーネント２０６によって実行されてもよい。これは、ソフトウェア・モジュール２１２を入力として取り、ソフトウェア・モジュール２１２に対して記号的実行を行い、ソフトウェア・モジュール２１２の実行経路に対応する記号的表現の集合を出力として与えてもよい。
【００５２】
コンピュータ科学の分野では、記号的実行（symbolic  execution）とは、抽象解釈の場合として、実際の値ではなく記号的な値を追跡することによるソフトウェア・プログラムの解析をいう。それは、ソフトウェア・モジュールへの入力を記号変数として扱う、非明示的な状態モデル検査技法である。それは、記号的変数を用いてソフトウェア・モジュール中のすべての有限経路を実行することによって複雑な数式もしくは表現を生成し、次いでもしあればエラー・シナリオを得るためにソルバ（典型的には決定手順（decision  procedure）として知られる）を用いて複雑な式を解く。明示的な状態モデル検査とは対照的に、記号的実行は、解析対象のソフトウェア・モジュールにおけるすべての入力変数のあらゆる可能な入力値およびあらゆる可能な使用ケースを計算することができる。記号的実行をさらに説明するために、「foo」と名付けられた例示的なソフトウェア・モジュールを考える。
【表２】
0005786511.tif 000003
【００５３】
ソフトウェア・モジュール「foo」は二つの入力変数「a」および「b」および二つのローカル変数「c」および「d」をもつ。具体的実施形態では、ローカル変数の値は、直接または間接に、ソフトウェア・モジュールの一つまたは複数の入力変数の値に依存する。たとえば、モジュール「foo」については、ローカル変数「c」の値は、コードの第３行に示されるように、入力変数「a」および「b」の値に直接的に依存する。ローカル変数「d」の値は、コードの第５行に示されるように、ローカル変数「c」を通じて入力変数「a」および「b」の値に間接的に依存する。さらに、モジュール「foo」はコードの第４行に「if-else」文による条件分岐点を含む。第４行の条件分岐点は分岐条件「!(c.equals("qrs"))」に関連付けられている。この分岐条件が満たされるすなわち成り立つかどうか――すなわちローカル変数「c」が「qrs」に等しいかどうか――に依存して、モジュール「foo」は異なる実行経路を通って進み、モジュール「foo」のコードの異なる部分が実際には実行される。より具体的には、ローカル変数「c」が「qrs」に等しくない場合、コードの第５および６行に示されるように、ローカル変数「d」の値が計算され、返される。他方、ローカル変数「c」が「qrs」に等しい場合には、コードの第８行に示されるように、ローカル変数「c」が返される。
【００５４】
記号的実行がモジュール「foo」に対して実行されるとき、その入力変数および出力変数はそれぞれ、実際の値の代わりに記号的な値を割り当てられる。図８は、モジュール「foo」上で記号的実行を行うステップを表す例示的な実行フロー８００を示している。この例では、入力変数「a」は記号的な値「x」を割り当てられ、入力変数「b」は記号的な値「y」を割り当てられ、ローカル変数「c」は記号的な値「z」を割り当てられ、ローカル変数「d」は記号的な値「w」を割り当てられる。変数「a」「b」「c」「d」は「string」型なので、記号的値「x」「y」「z」「w」はそれぞれ任意のストリングを表す。
【００５５】
加えて、「Φ」は、実行経路に沿ったさまざまな点における記号的実行の結果を表す記号的表現である。より具体的には、モジュール「foo」のコードの第２行に対応する８０２において、変数「a」「b」「c」「d」はそれぞれの記号的値「x」「y」「z」「w」を割り当てられ、「Φ」は初期には空またはヌル表現をもつ。実行がさらに進むにつれ、どのコードが実行されたかに依存して「Φ」に表現が加えられていく。モジュール「foo」のコードの第３行に対応する８０４においては、「Φ」は表現「z=concat(x,y)」をもつ。コードの第３行が「c=a.concat(b)」であり、「x」「y」「z」がそれぞれ変数「a」「b」「c」に割り当てられた記号的値だからである。次に、モジュール「foo」のコードの第４行は条件分岐点であり、実行が進みうる二つの可能な実行経路がある。よって、記号的実行も、８０４から二つの異なる経路を通って進みうる：第一の経路PATH1は、コードの第５および６行に対応する８０６および８０８を含み、第二の経路PATH2は、コードの第８行に対応する８１０を含む。
【００５６】
PATH1を通って進むには、変数「c」は「qrs」に等しくない。これは、記号的値「z」が「qrs」に等しくないことを意味する。よって、表現「z!="qrs"」が８０６において「Φ」に加えられる。逆に、PATH2を進むためには、変数「c」は「qrs」に等しい。これは、記号的値「z」が「qrs」に等しいことを意味する。よって、表現「z="qrs"」が８１０において「Φ」に加えられる。PATH1では、変数「d」の値が、８０８に対応するコードの第５行で決定される。したがって、表現「w=concat(z,"t")」が８０８において「Φ」に加えられる。「z=concat(x,y)」なので、「w」についてのこの表現は「w=concat(concat(x,y),"t")」と書き直してもよい。８０８はPATH1の終わりであり、よって８０８における「Φ」の表現は、PATH1の実行の終わりに達するために満たされる必要のある、記号的な形での、条件を表している。同様に、８１０はPATH2の終わりであり、よって８１０における「Φ」の表現は、PATH2の終わりに達するために満たされる必要のある、記号的な形での、条件を表している。
【００５７】
モジュール「foo」は二つの可能な実行経路をもつので、モジュール「foo」を記号的に実行することは、結果として、各実行経路に対応して一つで、二組の表現を与える。具体的実施形態では、８０８における「Φ」の表現について解くことは、モジュール「foo」にPATH1の終点に到達させる入力変数「a」および「b」についての実際の値を提供することができ、８１０における「Φ」の表現について解くことは、モジュール「foo」にPATH2の終点に到達させる入力変数「a」および「b」についての実際の値を提供することができる。
【００５８】
ソフトウェア・モジュール上で記号的実行を行うことから帰結した表現のこれらの集合を解くには、具体的実施形態は、図７のステップ７０４に示されるように、表現の各集合を、ソフトウェア・モジュールの変数に課される制約条件の集合として表してもよい。たとえば、モジュール「foo」では、８０８における表現の集合は、「a」「b」「c」「d」に対して課される制約条件の集合として「(d=concat(concat(a,b),"t"))&&(c=concat(a,b))&&(c!="qrs")」と表されてもよい。８１０での表現の集合は、「a」「b」「c」「d」に対して課される制約条件の集合として「(c=concat(a,b))&&(c="qrs")」と表されてもよい。
【００５９】
ソフトウェア・モジュールに対して記号的実行を行うことから得られる制約条件の各集合について、具体的実施形態は、該集合からの各数値制約条件を適用可能な数式として表し、該集合からの各ストリング制約条件をアプリケーションFSMとして表してもよい。図９Ａは、例示的なソフトウェア・モジュールについて決定された三つの例示的な制約条件の集合９０２、９０４、９０６を、該ソフトウェア・モジュールの三つの対応する実行経路９１２、９１４、９１６とともに示している。ここで、数値制約条件は数式として表され、ストリング制約条件はFSMとして表されている。この例示的なソフトウェア・モジュールを試験するため、各経路９１２、９１４、９１６の終わりにおいて、制約条件のそれぞれの対応する集合９０２、９０６、９０６が試験ケースについて解かれる。
【００６０】
次いで、具体的実施形態は、図７のステップ７０６に示されるように、図１に示されるプロセスを使って、制約条件の各集合について一つまたは複数の解を見出すことを試み、図７のステップ７０８に示されるように、見出された解を試験入力として使ってソフトウェア・モジュールを試験してもよい。具体的実施形態では、制約条件の集合についての解は、制約条件が課されている変数についての実際の値であって、該集合内のすべての制約条件を満たすものを含みうる。ソフトウェア・モジュールを試験するときは、これらの実際の解の値は、試験入力としてソフトウェア・モジュールの変数に代入されてもよい。制約条件のある集合について見出された解が与えられたとき、その解の諸値は一緒になって対応する制約条件の集合からのすべての制約条件を満たし、制約条件の集合は、ソフトウェア・モジュールが特定の実行経路に沿って進み、該特定の実行経路の終わりに達する際に、該ソフトウェア・モジュールの状態を表す表現の集合（たとえば記号的実行から得られた）に対応するので、実際の値（すなわち、制約条件の前記集合について見出された解からの値）のこの特定の組み合わせを試験入力としてソフトウェア・モジュールに適用することによって、ソフトウェア・モジュールが前記特定の実行経路に沿って進み、前記特定の実行経路の終わりに達することが保証される。結果として、これは、これらの特定の解の値がソフトウェア・モジュールの対応する変数に試験入力として代入されれば前記特定の実行経路がフルに試験されるということを意味する。さらに、ソフトウェア・モジュールの一つ一つのすべての実行経路について得られる表現の一つ一つのすべての集合に対応する制約条件の一つ一つのすべての集合について、解を見出すことができ、解の値がソフトウェア・モジュールに試験入力として適用される（たとえば一つの解の実際の諸値を同時に適用することによって）ならば、ソフトウェア・モジュールのすべての可能な実行経路がフルに試験されうる。ソフトウェア・モジュールの実行経路のいずれかにおいて何らかのエラーがある場合、そのような系統的な試験は最終的にはそのようなエラーを捕捉できることがありうる。
【００６１】
具体的実施形態では、図１に示されるようなプロセスが、ソフトウェア・モジュールの設計条件または仕様要件が満たされているかどうかを検証するために使用されうる。典型的には、任意の所与のソフトウェア・モジュールに関連付けられた形式的な設計要件または仕様要件があってもよい。これらの形式的な要件のいくつかは、ソフトウェア・モジュールの入力または出力に課されてもよい。個別的実施形態では、ソフトウェア・モジュールの入力に課される仕様要件は、そのソフトウェア・モジュールに関連する事前条件と称されてもよく、ソフトウェア・モジュールの出力に課される仕様要件は、そのソフトウェア・モジュールに関連する事後条件と称されてもよい。時に、事後条件は、そのソフトウェア・モジュールに関連する事前条件に依存してもよい。
【００６２】
上で説明したように、しばしば、ソフトウェア・モジュールは、任意の数の条件分岐点（たとえば「if-else」文）を含んでいてもよく、各条件分岐点はソフトウェア・モジュールの一つまたは複数の変数（たとえば入力変数またはローカル変数）によって指定される分岐条件をもつ。分岐条件が満たされるかどうかに依存して、ソフトウェア・モジュールは異なる実行経路を進みうる。よって、ソフトウェア・モジュールが実行されるとき、ソフトウェア・モジュールに含まれる条件分岐点から帰結する可能な実行経路のうちのいずれを進んでもよい。結果として、具体的実施形態では、ソフトウェア・モジュールがその入力および出力に課される形式的な仕様要件（すなわち、そのソフトウェア・モジュールに関連する事前条件および事後条件）を満たすかどうかを検証する際、ソフトウェア・モジュールが検証試験に合格する（すなわち、仕様要件を満たす）と考えられるのは、そのソフトウェア・モジュールに関連するすべての事前条件および事後条件が、そのソフトウェア・モジュールのすべての可能な実行経路について成り立つ場合であり、かつその場合に限られる。
【００６３】
図１０は、ソフトウェア・モジュールの入力および出力に課される要件（たとえば形式的な設計要件または仕様要件）（すなわち、ソフトウェア・モジュールに関連する事前条件および事後条件）との関連でソフトウェア・モジュールを検証する例示的な方法を示している。図１０のステップ１００２に示されるように、具体的実施形態は、ソフトウェア・モジュールの各事前条件（たとえば、入力変数に課される要件）および各事後条件（たとえば出力変数に課される要件）を、ソフトウェア・モジュールの入力変数または出力変数に課される制約条件として表してもよい。たとえば、ストリング型の二つの入力変数「a」および「b」をもつ先の例示的なソフトウェア・モジュール「foo」を考える。上に示した「foo」のコードに基づいて、「foo」がストリング型の一つの出力値を返すことが判別されうる。たとえばソフトウェア・モジュール「foo」の仕様によって指定され、「a」「b」「p」に課される制約条件として表される「a」「b」「p」に課される事前条件および事後条件は次のようになる。
【表３】
0005786511.tif 000004
【００６４】
次いで具体的実施形態は、図１０のステップ１００４に示されるように、ソフトウェア・モジュールの事後条件を否定にしてもよい。上の例では、ソフトウェア・モジュールは一つの事後条件「p.endsWith("t")」をもつ。この事後条件の論理的な否定は、「!(p.endsWith("t"))」となる。
【００６５】
具体的実施形態は、図１０のステップ１００６に示されるように、ソフトウェア・モジュールに対して記号的実行を行って、ソフトウェア・モジュールの可能な各実行経路に対応する制約条件の集合を得、次いで、事前条件および否定にされた事後条件を制約条件の各集合に組み込んでもよい。記号的実行は、図７のステップ７０２との関連で上述してあり、ここでも同様に実行されてもよい。制約条件の各集合を決定するとき、具体的実施形態は、もしあればソフトウェア・モジュールの個別的な変数に最初に課されていた数値およびストリング制約条件（図１のステップ１０２との関連で述べたような）ならびにもしあればソフトウェア・モジュールの個別的な変数について推定された数値およびストリング制約条件（図１のステップ１０４との関連で述べたような）を組み込んでもよい。たとえば、ソフトウェア・モジュール「foo」は、図８に示されるように、二つの可能な実行経路をもつ。こうして、ソフトウェア・モジュール「foo」に対して記号的実行を行うことは、結果として二組の表現を与える。
【００６６】
第一の経路PATH1については、「foo」に対して記号的実行を行うことから得られる表現の集合は、図８の８０８によって示されるように、「(p=concat(concat(a,b),"t"))&&(concat(a,b)!="qrs")」と書いてもよい。「p」はPATH1については「d」の値をもつことを注意しておく。「d」がPATH1の終わりに「foo」によって返される値（すなわち「foo」の出力）であり、「w」は「d」に割り当てられた記号的値だからである。さらに、「x」が「a」に割り当てられた記号的値なので「a」は「x」と等価であり、「b」は「y」と等価であり、「z」は「c」と等価であり、「c」は「foo」のソース・コードによれば「concat(a,b)」に等しい。次いで、事前条件および否定にされた事後条件はこの制約条件の集合に加えられてもよい。よって、PATH1についての最終的な制約条件の集合は、「(p=concat(concat(a,b),"t"))&&(concat(a,b)!="qrs")&&(b.endsWith("s"))&&!(p.endsWith("t"))」となる。
【００６７】
第二の経路PATH2については、「foo」に対して記号的実行を行うことから得られる表現の集合は、図８の８１０によって示されるように、「(p=concat(concat(a,b))&&(concat(a,b)="qrs")」と書いてもよい。「p」はPATH2については「c」の値をもつことを注意しておく。「c」がPATH2の終わりに「foo」によって返される値（すなわち「foo」の出力）であり、「z」は「c」に割り当てられた記号的値だからである。「c」は「foo」のソース・コードによれば「concat(a,b)」に等しい。事前条件および否定にされた事後条件はこの制約条件の集合に同様に加えられてもよい。PATH2についての最終的な制約条件の集合は、「(p=concat(a,b))&&(concat(a,b)!="qrs")&&(b.endsWith("s"))&&!(p.endsWith("t"))」となる。
【００６８】
次いで具体的実施形態は、図１０の１００８に示されるように、図１に示されるプロセスを使って、ソフトウェア・モジュールの可能な各実行経路に対応する制約条件の各集合について、一つまたは複数の解を見出すことを試みてもよい。制約条件の各集合は、ソフトウェア・モジュールに対して記号的実行を行うことから得られる制約条件と、ソフトウェア・モジュールに関連する事前条件および否定にされた事後条件とを含む。具体的実施形態では、ソフトウェア・モジュールの個別的な特定の実行経路に対応する制約条件の各集合について、前記集合からのすべての制約条件を満たす解が見出され得ない場合、この実行経路については、ソフトウェア・モジュールは、事前条件および事後条件によって表される入力および出力に課される要件を満たす。図１０のステップ１００４および１００６で説明されたように、制約条件の各集合はソフトウェア・モジュールの出力に課される否定にされた事後条件を含むことを想起されたい。よって、制約条件の集合について解が見出され得ない（すなわち、その制約条件の集合が充足不能である）場合、特に事後条件の否定を満たす解が見出され得ない場合、それは、対応する実行経路について事前条件および事後条件が成り立つということを意味する。逆に、前記集合からの制約条件すべてを満たす何らかの解が見出されうる場合には、対応する実行経路について、ソフトウェア・モジュールはその入力および出力に課される要件を満たさない。その実行経路については事前条件および事後条件が成り立たないからである。したがって、図１０のステップ１００６において得られた制約条件の任意の集合について何らかの解が見出されうる場合、ソフトウェア・モジュールは、その入力および出力に課される要件に関して検証試験に合格しない。図１０のステップ１００６で得られる制約条件の一つ一つのすべての集合が充足不能であるときにのみ、ソフトウェア・モジュールは、その入力および出力に課される要件に関して検証試験に合格する。
【００６９】
図９Ｂは、図９Ａに示した、前記例示的なソフトウェア・モジュールについて決定された制約条件の三つの例示的な集合９０２、９０４、９０６を、ソフトウェア・モジュールの三つの対応する実行経路９１２、９１４、９１６とともに再度示している。この例示的なソフトウェア・モジュールを、該ソフトウェア・モジュールの入力および出力に課される要件との関連で検証するには、各経路９１２、９１４、９１６の終わりにおいて、制約条件の各対応する集合９０２、９０４、９０６が要件および主張について解かれる。
【００７０】
具体的実施形態では、図１に示されるようなプロセスが、インジェクション攻撃を検出および捕捉するよう設計されたソフトウェア・モジュールを検証するために使用されてもよい。挿入攻撃としても知られるインジェクション攻撃は、しばしばSQLデータベースおよび他の脆弱なウェブサイトを標的にする悪意のあるソフトウェア攻撃の一形である。一般に、SQLインジェクションは、ソフトウェア・アプリケーションのデータベース層に存在するセキュリティ上の脆弱性を活用するコード注入技法である。脆弱性は、プログラミングまたはスクリプティング言語が別のプログラミングまたはスクリプティング言語内に埋め込まれるときに常に起こりうる。より具体的には、脆弱性が存在しうるのは、ユーザー入力がSQL文に埋め込まれたストリング・リテラルのエスケープ・キャラクタについて誤ったフィルタリングがされたとき、あるいはユーザー入力が強く型指定されず、そのため予期せずに実行されるときである。たとえば、インジェクション攻撃は、ストリング「shutdown」を別のストリング（たとえばランダムな文字の集合）に「qk%#d1shutdownsq&^d」として埋め込み、このストリングを入力コマンド（SQL文）としてデータベースに送ることがある。データベース・ソフトウェアが、一見ランダムな入力ストリングに埋め込まれている「shutdown」ストリングを捕捉せずに実行してしまうと、「shutdown」〔シャットダウン〕ストリングがデータベースを意図せずしてシャットダウンさせてしまうことがありうる。このため、たいていのデータベースは、そのようなインジェクション攻撃を検出および捕捉するよう設計されたソフトウェア・モジュールを有する。具体的実施形態では、図１に示されるプロセスが、そのようなセキュリティ・ソフトウェア・モジュールが、インジェクション攻撃として入力に埋め込まれうる悪意のあるストリングの多くの異なる形を検出できるかどうかを、検証するために使用されてもよい。たとえば、セキュリティ・ソフトウェア・モジュールを試験する一つの方法は、そのセキュリティ・ソフトウェア・モジュールが検出できないよう（たとえば、セキュリティ・ソフトウェア・モジュールをだましてその悪意のあるストリングが無害であると思い込ませるよう）悪意のあるストリングまたは悪意のあるストリングを埋め込む方法を考案することでありうる。
【００７１】
図１１は、インジェクション攻撃を検出するよう設計されたセキュリティ・ソフトウェア・モジュールを検証する例示的な方法を示している。具体的実施形態では、セキュリティ・ソフトウェア・モジュールは、入力ストリングが何らかの悪意のあるストリングを含むかどうかを検証するために、セキュリティ・ソフトウェア・モジュールに渡される入力値（たとえば入力ストリング）に対してさまざまなセキュリティ検査を実行してもよい。各セキュリティ・チェックポイントにおいて、入力値がセキュリティ検査を通過した場合には、セキュリティ・ソフトウェア・モジュールは次のセキュリティ・チェックポイントに進んでもよい。それ以外の場合には、セキュリティ・ソフトウェア・モジュールは、入力値が特定のセキュリティ検査に不合格だったとの指示を返してもよい（たとえばFALSEを返す）。入力ストリングが、セキュリティ・ソフトウェア・モジュールに含まれるすべてのセキュリティ検査を通過した場合にのみ、セキュリティ・ソフトウェア・モジュールは、入力値が無害であるとの指示を返す（たとえば、TRUEを返す）。
【００７２】
具体的実施形態は、図１１のステップ１１０２に示されるように、インジェクション攻撃との関連で使われそうな、「shutdown」のような悪意のあるストリングの集合を選択してもよい。「m」がある特定の悪意のあるストリングを表すとする。次いで、具体的実施形態は、図１１のステップ１１０４に示されるように、前記集合からのそれぞれの悪意のあるストリングを「s」で表される別のストリングに埋め込んでもよい。「s」においては、悪意のあるストリングの前のいくつかのキャラクタ（すなわち部分ストリング）および悪意のあるストリングの後のいくつかのキャラクタ（すなわち別の部分ストリング）があってもよい。このように、「s」は、"s=concat(concat(x,m),y)"と表されうる。ここで、「s」において、「x」は悪意のあるストリング「m」の前の部分ストリングを表し、「y」は悪意のあるストリング「m」の後の部分ストリングを表す。「x」も「y」も空ストリングであってもよく、「m」が「s」の別の部分ストリングになることを注意しておく。次いで、ストリン「s」はセキュリティ・ソフトウェア・モジュールに入力値として加えられてもよい。
【００７３】
具体的実施形態は、図１１のステップ１１０６に示されるように、セキュリティ・ソフトウェア・モジュールに関して記号的実行を行って制約条件の集合を得てもよい。該制約条件の集合は、満足されれば、セキュリティ・ソフトウェア・モジュールに終わりまで実行させ、入力値がそこに含まれるすべてのセキュリティ検査に合格したとの指示を返させる（たとえばTRUEを返す）ものである。記号的実行は、図７のステップ７０２との関連で上記してあり、ここでも同様に実行されてもよい。制約条件の集合を決定するとき、具体的実施形態は、もしあればソフトウェア・モジュールの個別的な変数に最初に課されていた数値およびストリング制約条件（図１のステップ１０２との関連で述べたような）ならびにもしあればソフトウェア・モジュールの個別的な変数について推定された数値およびストリング制約条件（図１のステップ１０４との関連で述べたような）を組み込んでもよい。具体的実施形態では、こうして得られた制約条件の集合は、セキュリティ・ソフトウェア・モジュールに含まれるすべてのセキュリティ検査に合格してソフトウェア・モジュールが入力値が無害であることを示す出力値を返すために、セキュリティ・ソフトウェア・モジュールの入力変数に代入された入力値について満足される必要のある制約条件すべてを表す。
【００７４】
具体的実施形態は、図１１のステップ１１０８に示されるように、図１に示されるプロセスを使って、「s」がすべての制約条件を満たすよう、各悪意のあるストリングが埋め込まれている「s」についての一つまたは複数の解を見出すことを試みてもよい。「s」について制約条件の集合を満たす何らかの解が見出されうる場合、それは、セキュリティ・ソフトウェア・モジュールに含まれるすべてのセキュリティ検査をすり抜けうる、「s」に埋め込まれた少なくとも一つの悪意のあるストリングがあることを意味する。その結果、セキュリティ・ソフトウェア・モジュールはインジェクション攻撃に対して脆弱である。
【００７５】
悪意のあるストリング「shutdown」を例として使う。このストリングを「s」に埋め込むと、結果は「s=concat(concat(x,"shutdown"),y)」となる。図１に示したプロセスを使って、具体的実施形態は、「shutdown」が埋め込まれた「s」がセキュリティ・ソフトウェア・モジュールに関する記号的実行を行うことから得られる制約条件の集合からのすべての制約条件を満たしうるよう、部分ストリング「x」および「y」の値を与える「s」についての何らかの解があるかどうかを見出そうと試みてもよい。「x」および「y」についての解があれば、それは、ストリング「s」がセキュリティ・ソフトウェア・モジュールに含まれるすべてのセキュリティ検査に合格できるように（すなわち、セキュリティ・ソフトウェア・モジュールが悪意のあるストリング「shutdown」を埋め込まれたその特定のインジェクション攻撃を検出し損なうように）、値「concat(concat(x,"shutdown"),y)」をもつストリング「s」中に悪意のあるストリング「shutdown」を埋め込む少なくとも一つの方法があることを意味する。
【００７６】
具体的実施形態では、各悪意のあるストリングは、ストリング「s」に埋め込まれるとき、異なるデータ型を使って表されることがある。たとえば、ストリング「shutdown」を十六進数として表すと、「0x73687574646f766e」である。このように、「s」についての一つの可能な値は、ストリング・データ型でこの悪意のあるストリングを表す「exec  shutdown」でありうる。一方、「s」についての別の可能な値は、整数データ型でこの悪意のあるストリングを表す「declare  @a  char(20)  select  @a=0x73687574646f766e  exec(@a)」でありうる。具体的実施形態は、埋め込まれた悪意のあるストリングが異なるデータ型を使って表される場合に「s」についての解を見出そうと試みてもよい。結果として、セキュリティ・ソフトウェア・モジュールは、通常のストリング・データ型として表された悪意のあるストリングに関して試験されるだけでなく、予期されないデータ型で表された（たとえば整数または浮動小数点数として表された）悪意のあるストリングに関しても試験される。
【００７７】
具体的実施形態は、悪意のあるストリングの集合からの各悪意のあるストリング「m」を「s」に埋め込み、次いで、ストリング全体としての（すなわち「x」「m」および「y」を含む）「s」が図１１のステップ１１０６から得られた制約条件の集合を満たすような、「x」および「y」についての特定の値を与える「s」についての解を見出そうと試みてもよい。埋め込まれた何らかの悪意のあるストリング「m」をもつ「s」についての何らかの解が見出されうる場合、それは、そのセキュリティ・ソフトウェア・モジュールは対応するインジェクション攻撃を検出できず、よって脆弱であることを意味する。さらに、埋め込まれた何らかの悪意のあるストリング「m」をもつ「s」についての何の解も見出されえない場合、具体的実施形態はさらに、図１１のステップ１１０６から得られる制約条件の集合を満たす解を見出そうと試みてもよい。何らかの解が見出されうる場合、具体的実施形態は、その解自身が実際に悪意のあるストリングであるかどうかを検証してもよい。セキュリティ・ソフトウェア・モジュールに対するこの検証は、悪意のあるストリングが、別のストリングに埋め込まれることなくそれ自身で、セキュリティ・ソフトウェア・モジュールに含まれるすべてのセキュリティ検査を合格できるかどうか（すなわち、セキュリティ・ソフトウェア・モジュールが何らかの悪意のあるストリングを検出し損なうかどうか）を判定するよう試みる。
【００７８】
図９Ｃは、図９Ａに示した、前記例示的なソフトウェア・モジュールについて決定された制約条件の三つの例示的な集合９０２、９０４、９０６を、ソフトウェア・モジュールの三つの対応する実行経路９１２、９１４、９１６とともに再度示している。この例示的なソフトウェア・モジュールが例示的なセキュリティ・ソフトウェア・モジュールである場合、この例示的なセキュリティ・ソフトウェア・モジュールを検証するには、各経路９１２、９１４、９１６の終わりにおいて、制約条件の各対応する集合９０２、９０４、９０６が、当該ソフトウェアの内部検査を通過したあらゆる可能なストリングを表すホットスポットFSM〔有限状態機械〕と、悪意のあるFSMとの交わりについて、解かれる。交わりがヌルであれば、可能なインジェクション攻撃は一つも見出されることができない。ヌルでない交わりは、ただちに可能なインジェクション攻撃ストリングを指し示す。
【００７９】
具体的実施形態は、ネットワーク環境において実装されてもよい。図１２は、サービスとしてソフトウェア検証を提供するのに好適な例示的なネットワーク環境１２００を示している。ネットワーク環境１２００は、一つまたは複数のサーバー１２２０および一つまた複数のクライアント１２３０を互いに結合するネットワーク１２１０を含む。具体的実施形態では、ネットワーク１２１０はイントラネット、エクストラネット、仮想閉域網（VPN:  virtual  private  network）、ローカル・エリア・ネットワーク（LAN:  local  area  network）、無線LAN（WLAN:  wireless  LAN）、広域ネットワーク（WAN:  wide  area  network）、都市圏ネットワーク（MAN:  metropolitan  area  network）、インターネットの一部または別のネットワーク１２１０または二つ以上のそのようなネットワーク１２１０の組み合わせである。本開示は、任意の好適なネットワーク１２１０を考えている。
【００８０】
一つまたは複数のリンク１２５０はサーバー１２２０またはクライアント１２３０をネットワーク１２１０に結合する。具体的実施形態では、一つまたは複数のリンク１２５０はそれぞれ一つまたは複数の有線、無線または光学式リンク１２５０を含む。具体的実施形態では、一つまたは複数のリンク１２５０はそれぞれ、イントラネット、エクストラネット、VPN、LAN、WLAN、WAN、MAN、インターネットの一部または別のリンク１２５０または二つ以上のそのようなリンク１２５０の組み合わせを含む。本開示は、サーバー１２２０およびクライアント１２３０をネットワーク１２１０に結合する任意の好適なリンク１２５０を考えている。
【００８１】
具体的実施形態では、各サーバー１２２０は単体のサーバーであってもよいし、あるいは複数のコンピュータまたは複数のデータセンターにまたがる分散式のサーバーであってもよい。サーバー１２２０はさまざまな型でありえ、たとえば、限定するものではないが、ウェブ・サーバー、ニュース・サーバー、メール・サーバー、メッセージ・サーバー、広告サーバー、ファイル・サーバー、アプリケーション・サーバー、交換サーバー、データベース・サーバーまたはプロキシ・サーバーといったものでありうる。具体的実施形態では、各サーバー１２２０は、サーバー１２２０によって実装またはサポートされる適切な機能を実行するために、ハードウェア、ソフトウェアまたは埋め込まれた論理コンポーネントまたは二つ以上のそのようなコンポーネントの組み合わせを含んでいてもよい。たとえば、ウェブ・サーバーは一般に、ウェブ・ページまたはウェブ・ページの個別的な要素を含むウェブサイトをホストすることができる。より具体的には、ウェブ・サーバーはHTMLファイルまたは他のファイル型をホストしてもよく、あるいは要求に際してファイルを動的に生成または構築し、クライアント１２３０からのHTTPまたはその他の要求に応答してそれをクライアント１２３０に通信してもよい。メール・サーバーは一般にさまざまなクライアント１２３０に電子メール・サービスを提供することができる。データベース・サーバーは一般に、一つまたは複数のデータ・ストアに記憶されたデータを管理するためのインターフェースを提供することができる。
【００８２】
具体的実施形態では、一つまたは複数のデータ記憶装置１２４０が一つまたは複数のリンク１２５０を介して一つまたは複数のサーバー１２２０に通信上リンクされてもよい。具体的実施形態では、データ記憶装置１２４０はさまざまな型の情報を記憶するために使用されうる。具体的実施形態では、データ記憶装置１２４０に記憶される情報は、特定のデータ構造に従って編成されてもよい。具体的実施形態では、各データ記憶装置１２４０はリレーショナル・データベースであってもよい。具体的実施形態は、サーバー１２２０またはクライアント１２３０がデータ記憶装置１２４０に記憶されている情報を管理する、たとえば取得、修正、追加または削除することができるようにするインターフェースを提供してもよい。
【００８３】
具体的実施形態では、各クライアント１２３０は、ハードウェア、ソフトウェアまたは埋め込まれた論理コンポーネントまたは二つ以上のそのようなコンポーネントの組み合わせを含み、クライアント１２３０によって実装またはサポートされる適切な機能を実行することができる電子装置であってもよい。たとえば、限定するものではないが、クライアント１２３０はデスクトップ・コンピュータ・システム、ノートブック・コンピュータ・システム、ハンドヘルド電子装置または携帯電話であってもよい。本開示は、任意の好適なクライアント１２３０を考えている。クライアント１２３０は、クライアント１２３０のところにいるネットワーク・ユーザーが、ネットワーク１２１０にアクセスできるようにしてもよい。クライアント１２３０は、そのユーザーが他のクライアント１２３０のところにいる他のユーザーと通信できるようにしてもよい。
【００８４】
クライアント１２３０は、「マイクロソフト・インターネット・エクスプローラー」、「グーグル・クローム」または「モジラ・ファイアフォックス」のようなウェブ・ブラウザー１２３２を有していてもよく、一つまたは複数のアドオン、プラグインまたは「ツールバー」または「ヤフー・ツールバー」のような他の拡張を有していてもよい。クライアント１２３０のところにいるユーザーは一様リソース位置指定子（URL:  Uniform  Resource  Locator）またはウェブ・ブラウザー１２３２にサーバー１２２０を指定する他のアドレスを入力してもよく、ウェブ・ブラウザー１２３２はハイパーテキスト転送プロトコル（HTTP:  Hyper  Text  Transfer  Protocol）要求を生成し、該HTTP要求をサーバー１２２０に通信してもよい。サーバー１２２０はHTTP要求を受け容れ、該HTTP要求に応答してクライアント１２３０に一つまたは複数のハイパーテキスト・マークアップ言語（HTML:  Hyper  Text  Markup  Language）ファイルを通信してもよい。クライアント１２３０は、サーバー１２２０からのHTMLファイルに基づいて、ユーザーへの呈示のためにウェブ・ページをレンダリングしてもよい。本開示は、任意の好適なウェブ・ページ・ファイルを考えている。一例として、限定するわけではないが、ウェブ・ページは個別のニーズに応じて、HTMLファイル、拡張可能ハイパーテキスト・マークアップ言語（XHTML:  Extensible  Hyper  Text  Markup  Language）ファイルまたは拡張可能マークアップ言語（XML:  Extensible  Markup  Language）ファイルからレンダリングしてもよい。そのようなページはまた、スクリプトを実行してもよい。スクリプトは、たとえば、限定するものではないが、ジャバスクリプト、ジャバ、マイクロソフト・シルバーライト（SILVERLIGHT）、AJAX（Asynchronous  JAVASCRIPT  and  XML）のようなマークアップ言語およびスクリプトの組み合わせで書かれたものなどである。本稿では、適宜、ウェブ・ページへの言及は、一つまたは複数の対応する（ブラウザーがウェブ・ページをレンダリングするために使うことができる）ウェブ・ページ・ファイルを包含し、逆もまたしかりである〔つまり、ウェブ・ページ・ファイルへの言及は一つまたは複数の対応するウェブ・ページを包含する〕。
【００８５】
具体的実施形態は、一つまたは複数のコンピュータ・システム上で実装されてもよい。図１３は、例示的なコンピュータ・システム１３００を示している。具体的実施形態では、一つまたは複数のコンピュータ・システム１３００が、本願で記載または図示される一つまたは複数の方法の一つまたは複数のステップを実行する。具体的実施形態では、一つまたは複数のコンピュータ・システム１３００は本願で記載または図示される機能を実行する。具体的実施形態では、一つまたは複数のコンピュータ・システム１３００上で走るソフトウェアが本願で記載または図示される一つまたは複数の方法の一つまたは複数のステップを実行し、あるいは本願で記載または図示される機能を提供する。具体的実施形態は、一つまたは複数のコンピュータ・システム１３００の一つまたは複数の部分を含む。
【００８６】
本開示は、任意の好適な数のコンピュータ・システム１３００を考えている。本開示は、任意の好適な物理的形態を取るコンピュータ・システム１３００を考えている。例として、限定するわけではないが、コンピュータ・システム１３００は組み込みコンピュータ・システム、システム・オン・チップ（SOC:  system-on-chip）、単一ボード・コンピュータ・システム（SBC:  single-board  computer  system）（たとえばコンピュータ・オン・モジュール（COM:  computer-on-module）またはシステム・オン・モジュール（SOM:  system-on-module）のような）、デスクトップ・コンピュータ・システム、ラップトップまたはノートブック・コンピュータ・システム、対話的キオスク、メインフレーム、コンピュータ・システムのメッシュ、携帯電話、携帯情報端末（PDA:  personal  digital  assistant）、サーバーまたはこれらの二つ以上の組み合わせであってもよい。適宜、コンピュータ・システム１３００は一つまたは複数のコンピュータ・システム１３００を含んでいてもよいし、単体でも分散式でもよいし、複数の位置にまたがってもよいし、複数の機械にまたがってもよいし、クラウドに存在してもよい。クラウドは、一つまたは複数のネットワークにおける一つまたは複数のクラウド・コンポーネントを含んでいてもよい。適宜、一つまたは複数のコンピュータ・システム１３００は、実質的な空間的または時間的制約なしに、本願で記載または図示される一つまたは複数の方法の一つまたは複数のステップを実行してもよい。一例として、限定するわけではないが、一つまたは複数のコンピュータ・システム１３００は、リアルタイムで、あるいはバッチ・モードで、本願で記載または図示される一つまたは複数の方法の一つまたは複数のステップを実行してもよい。一つまたは複数のコンピュータ・システム１３００は、本願で記載または図示される一つまたは複数の方法の一つまたは複数のステップを、適切であれば異なる複数の時間に、あるいは異なる複数の位置で、実行してもよい。
【００８７】
具体的実施形態では、コンピュータ・システム１３００はプロセッサ１３０２、メモリ１３０４、記憶装置１３０６、入出力（I/O）インターフェース１３０８、通信インターフェース１３１０およびバス１３１２を含む。本開示は具体的な数の具体的なコンポーネントを具体的な構成で有する具体的なコンピュータ・システムを記載および図示しているが、本開示は任意の好適な数の任意の好適なコンポーネントを任意の好適な構成で有する任意の好適なコンピュータ・システムを考えている。
【００８８】
具体的実施形態では、プロセッサ１３０２は、コンピュータ・プログラムをなす命令のような命令を実行するためのハードウェアを含む。一例として、限定するわけではないが、命令を実行するために、プロセッサ１３０２は内部レジスタ、内部キャッシュ、メモリ１３０４または記憶装置１３０６から命令を取得（またはフェッチ）し、それらの命令をデコードおよび実行し、次いで一つまたは複数の結果を内部レジスタ、内部キャッシュ、メモリ１３０４または記憶装置１３０６に書き込んでもよい。具体的実施形態では、プロセッサ１３０２はデータ、命令またはアドレスのための一つまたは複数の内部キャッシュを含んでいてもよい。本開示は、適宜、任意の好適な数の任意の好適な内部キャッシュを含むプロセッサ１３０２を考えている。一例として、限定するわけではないが、プロセッサ１３０２は一つまたは複数の命令キャッシュ、一つまたは複数のデータ・キャッシュおよび一つまたは複数のトランスレーション・ルックアサイド・バッファ（TLB:  translation  lookaside  buffer）を含んでいてもよい。命令キャッシュ中の命令は、メモリ１３０４または記憶装置１３０６中の命令のコピーであってもよく、命令キャッシュはプロセッサ１３０２によるそれらの命令の取得を高速化しうる。データ・キャッシュ中のデータはプロセッサ１３０２で実行中の命令が作用するメモリ１３０４または記憶装置１３０６中のデータのコピーであってもよく、プロセッサ１３０２で実行されるその後の命令によるアクセスのためまたはメモリ１３０４もしくは記憶装置１３０６への書き込みのための、プロセッサ１３０２で実行された前の命令の結果であってもよく、他の好適なデータであってもよい。データ・キャッシュは、プロセッサ１３０２による読み出しまたは書き込み動作を高速化しうる。TLBは、プロセッサ１３０２のための仮想アドレス変換を高速化しうる。具体的実施形態では、プロセッサ１３０２は、データ、命令またはアドレスのための一つまたは複数の内部レジスタを含んでいてもよい。本開示は、適宜、任意の好適な数の任意の好適な内部レジスタを含むプロセッサ１３０２を考えている。適切な場合には、プロセッサ１３０２は、一つまたは複数の算術論理ユニット（ALU:  arithmetic  logic  unit）を含んでいてもよく、マルチコア・プロセッサであってもよく、一つまたは複数のプロセッサ１３０２を含んでいてもよい。本開示は具体的なプロセッサを記載および図示しているが、本開示は任意の好適なプロセッサを考えている。
【００８９】
具体的実施形態では、メモリ１３０４は、プロセッサ１３０２が実行するための命令およびプロセッサ１３０２が作用するためのデータを記憶するためのメイン・メモリを含む。一例として、限定するわけではないが、システム１３００は記憶装置１３０６または他の源（たとえば別のコンピュータ・システム１３００のような）から命令をメモリ１３０４にロードしてもよい。プロセッサ１３０２は次いでメモリ１３０４からの命令を内部レジスタまたは内部キャッシュにロードしてもよい。命令を実行するために、プロセッサ１３０２は内部レジスタまたは内部キャッシュから命令を取得し、それをデコードしてもよい。命令の実行中または実行後に、プロセッサ１３０２は一つまたは複数の結果（これは中間結果であってもよいし、最終結果であってもよい）を内部レジスタまたは内部キャッシュに書き込んでもよい。プロセッサ１３０２は次いでそれらの結果のうちの一つまたは複数をメモリ１３０４に書き込んでもよい。具体的実施形態では、プロセッサ１３０２は、（記憶装置１３０６その他の箇所ではなく）一つまたは複数の内部レジスタまたは内部キャッシュ内またはメモリ１３０４内の命令のみを実行し、（記憶装置１３０６その他の箇所ではなく）一つまたは複数の内部レジスタまたは内部キャッシュ内またはメモリ１３０４内のデータに対してのみ演算する。一つまたは複数のメモリ・バス（これはそれぞれアドレス・バスおよびデータ・バスを含んでいてもよい）がプロセッサ１３０２をメモリ１３０４に結合してもよい。バス１３１２は後述するように一つまたは複数のメモリ・バスを含んでいてもよい。具体的実施形態では、一つまたは複数のメモリ管理ユニット（MMU:  memory  management  unit）がプロセッサ１３０２とメモリ１３０４との間に存在し、プロセッサ１３０２によって要求されるメモリ１３０４へのアクセスを容易にする。具体的実施形態では、メモリ１３０４はランダム・アクセス・メモリ（RAM）を含む。このRAMは適切であれば揮発性メモリであってもよい。適切であれば、このRAMは動的RAM（DRAM）または静的RAM（SRAM）であってもよい。さらに、適切であれば、このRAMは単一ポートまたはマルチポートのRAMであってもよい。本開示は任意の好適なRAMを考えている。メモリ１３０４は適宜一つまたは複数のメモリ１３０４を含んでいてもよい。本開示は具体的なメモリを記述および図示しているが、本開示は任意の好適なメモリを考えている。
【００９０】
具体的実施形態では、記憶装置１３０６はデータまたは命令についての大容量記憶装置を含む。一例として、限定するわけではないが、記憶装置１３０６はHDD、フロッピー(登録商標)ディスクドライブ、フラッシュ・メモリ、光ディスク、光磁気ディスク、磁気テープまたはユニバーサル・シリアル・バス（USB:  Universal  Serial  Bus）ドライブまたはこれらのうち二つ以上の組み合わせを含んでいてもよい。記憶装置１３０６は、適宜、リムーバブルまたは非リムーバブルな（すなわち固定式の）メディアを含んでいてもよい。記憶装置１３０６は適宜コンピュータ・システム１３００の内部または外部であってもよい。具体的実施形態では、記憶装置１３０６は不揮発性の半導体メモリであってもよい。具体的実施形態では、記憶装置１３０６は読み出し専用メモリ（ROM）を含む。適切であれば、このROMはマスク・プログラムされたROM、プログラム可能型ROM（PROM）、消去可能型PROM（EPROM）、電気的消去可能型EPROM（EEPROM）、電気的変更可能型ROM（EAROM）またはフラッシュ・メモリまたはこれらのうち二つ以上の組み合わせであってもよい。本開示は、任意の好適な物理的形態を取る大容量記憶装置１３０６を考えている。記憶装置１３０６は、適宜、プロセッサ１３０２と記憶装置１３０６の間の通信を容易にする一つまたは複数の記憶装置制御ユニットを含んでいてもよい。適切であれば、記憶装置１３０６は一つまたは複数の記憶装置１３０６を含んでいてもよい。本開示は具体的な記憶装置を記載および図示するが、本開示は任意の好適な記憶装置を考えている。
【００９１】
具体的実施形態では、I/Oインターフェース１３０８は、コンピュータ・システム１３００と一つまたは複数のI/O装置との間の通信のための一つまたは複数のインターフェースを提供するためのハードウェア、ソフトウェアまたはその両方を含む。コンピュータ・システム１３００は適宜、これらのI/O装置の一つまたは複数を含んでもよい。これらのI/O装置の一つまたは複数は、人とコンピュータ・システム１３００の間の伝達を可能にしうる。一例として、限定するわけではないが、I/O装置はキーボード、キーパッド、マイクロホン、モニタ、マウス、プリンタ、スキャナ、スピーカー、スチール・カメラ、スタイラス、タブレット、タッチスクリーン、トラックボール、ビデオ・カメラ、他の好適なI/O装置またはこれらのうちの二つ以上の組み合わせを含んでいてもよい。I/O装置は一つまたは複数のセンサーを含んでいてもよい。本開示は任意の好適なI/O装置およびそのための任意の好適なI/Oインターフェース１３０８を考えている。適切であれば、I/Oインターフェース１３０８は、プロセッサ１３０２がこれらのI/O装置の一つまたは複数を駆動できるようにする一つまたは複数の装置またはソフトウェア・ドライバを含んでいてもよい。I/Oインターフェース１３０８は、適宜、一つまたは複数のI/Oインターフェースを含んでいてもよい。本開示は具体的なI/Oインターフェースを記載および図示しているが、本開示は任意の好適なI/Oインターフェースを考えている。
【００９２】
具体的実施形態では、通信インターフェース１３１０は、コンピュータ・システム１３００と一つまたは複数の他のコンピュータ・システム１３００または一つまたは複数のネットワークとの間の通信（たとえばパケット・ベースの通信）のための一つまたは複数のインターフェースを提供するハードウェア、ソフトウェアまたはその両方を含む。一例として、限定するわけではないが、通信インターフェース１３１０は、イーサネット(登録商標)または他の有線ベースのネットワークと通信するためのネットワーク・インターフェース・コントローラ（NIC:  network  interface  controller）またはネットワーク・アダプター、あるいはWI-FIネットワークのような無線ネットワークと通信するための無線NIC（WNIC）または無線アダプターを含んでいてもよい。本開示は任意の好適なネットワークおよびそのための任意の好適な通信インターフェース１３１０を考えている。一例として、限定するわけではないが、コンピュータ・システム１３００はアドホック・ネットワーク、パーソナル・エリア・ネットワーク（PAN）、ローカル・エリア・ネットワーク（LAN）、広域ネットワーク（WAN）、都市圏ネットワーク（MAN）またはインターネットの一つまたは複数の部分またはこれらのうちの二つ以上の組み合わせと通信してもよい。これらのうち一つまたは複数のネットワークの一つまたは複数の部分は有線または無線であってもよい。一例として、コンピュータ・システム１３００は無線PAN（WPAN）（たとえばブルートゥースWPANのような）、WI-FIネットワーク、WI-MAXネットワーク、携帯電話ネットワーク（たとえばグローバル移動通信システム（GSM:  Global  System  for  Mobile  Communications）ネットワーク）または他の好適な無線ネットワークまたはこれらのうちの二つ以上の組み合わせと通信してもよい。コンピュータ・システム１３００は、適宜、これらのネットワークのうちの任意のネットワークのために、任意の好適な通信インターフェース１３１０を含んでいてもよい。通信インターフェース１３１０は、適宜、一つまたは複数の通信インターフェース１３１０を含んでいてもよい。本開示は具体的な通信インターフェースを記載および図示するが、本開示は任意の好適な通信インターフェースを考えている。
【００９３】
具体的実施形態では、バス１３１２は、コンピュータ・システム１３００のコンポーネントを互いと結合するハードウェア、ソフトウェアまたはその両方を含む。一例として、限定するわけではないが、バス１３１２は、加速グラフィクス・ポート（AGP:  Accelerated  Graphics  Port）または他のグラフィクス・バス、向上業界標準アーキテクチャ（EISA:  Enhanced  Industry  Standard  Architecture）バス、フロントサイド・バス（FSB:  front-side  bus）、ハイパートランスポート（HT:  HYPERTRANSPORT）相互接続、業界標準アーキテクチャ（ISA:  Industry  Standard  Architecture）バス、インフィニバンド（INFINIBAND）相互接続、低ピン数（LPC:  low-pin-count）バス、メモリ・バス、マイクロチャネル・アーキテクチャ（MCA:  Micro  Channel  Architecture）バス、周辺コンポーネント相互接続（PCI:  Peripheral  Component  Interconnect）バス、PCIエクスプレス（PCI-X:  PCI-Express）バス、シリアル先進技術アタッチメント（SATA:  serial  advanced  technology  attachment）バス、ビデオ電子標準協会ローカル（VLB:  Video  Electronics  Standards  Association）バスまたは他の好適なバスまたはこれらのうち二つ以上の組み合わせを含んでいてもよい。バス１３１２は適宜一つまたは複数のバスを含んでいてもよい。本開示は具体的なバスを記載および図示しているが、本開示は任意の好適なバスまたは相互接続を考えている。
【００９４】
本稿において、コンピュータ可読記憶媒体への言及は、構造を有する一つまたは複数の非一時的な有形のコンピュータ可読記憶媒体を包含する。一例として、限定するわけではないが、コンピュータ可読記憶媒体は、適宜、半導体ベースのまたは他の集積回路（IC）（たとえば、現場プログラム可能なゲート・アレイ（FPGA:  field-programmable  gate  array）または特定用途向けIC（ASIC:  application-specific  IC））、ハードディスク、HDD、ハイブリッド・ハードドライブ（HHD）、光ディスク、光ディスクドライブ（ODD）、光磁気ディスク、光磁気ドライブ、フロッピー(登録商標)ディスク、フロッピー(登録商標)ディスクドライブ（FDD）、磁気テープ、ホログラフィー記憶媒体、固体式ドライブ（SSD:  solid-state  drive）、RAMドライブ、セキュア・デジタル（SECURE  DIGITAL）カード、セキュア・デジタル（SECURE  DIGITAL）ドライブまたは他の好適なコンピュータ可読記憶媒体またはこれらのうちの二つ以上の組み合わせを含んでいてもよい。本稿では、コンピュータ可読記憶媒体への言及は、特許法のもとでの特許保護の資格のない媒体は除外する。本稿では、コンピュータ可読記憶媒体への言及は、信号伝達の一時的な形（伝搬する電気または電磁信号自身のような）は、それが特許法のもとでの特許保護の対象でない限りにおいて、除外する。
【００９５】
本開示は、任意の好適な記憶装置を実装する一つまたは複数のコンピュータ可読記憶媒体を考えている。具体的実施形態では、コンピュータ可読記憶媒体は、適宜、プロセッサ１３０２の一つまたは複数の部分（たとえば一つまたは複数の内部レジスタまたはキャッシュのような）、メモリ１３０４の一つまたは複数の部分、記憶装置１３０６の一つまたは複数の部分またはこれらの組み合わせを実装する。具体的実施形態では、コンピュータ可読記憶媒体はRAMまたはROMを実装する。具体的実施形態では、コンピュータ可読記憶媒体は揮発性または持続性メモリを実装する。具体的実施形態では、一つまたは複数のコンピュータ可読記憶媒体がソフトウェアを具現する。本稿において、ソフトウェアへの言及は、適宜、一つまたは複数のアプリケーション、バイトコード、一つまたは複数のコンピュータ・プログラム、一つまたは複数の実行形式、一つまたは複数の命令、論理、機械コード、一つまたは複数のスクリプトを包含し、逆もまたしかりである。具体的実施形態では、ソフトウェアは一つまたは複数のアプリケーション・プログラミング・インターフェース（API）を含む。本開示は、任意の好適なプログラミング言語またはプログラミング言語の組み合わせで書かれたまたは他の仕方で表現された任意の好適なソフトウェアを考えている。具体的実施形態では、ソフトウェアはソース・コードまたはオブジェクト・コードとして表現される。具体的実施形態では、ソフトウェアはたとえばC、Perlまたはそれらの好適な拡張のような高レベルプログラミング言語で表現される。具体的実施形態では、ソフトウェアは、アセンブリ言語（または機械コード）のような低レベルプログラミング言語で表現される。具体的実施形態では、ソフトウェアはジャバで表現される。具体的実施形態では、ソフトウェアはハイパーテキスト・マークアップ言語（HTML）、拡張可能マークアップ言語（XML）または他の好適なマークアップ言語で表現される。
【００９６】
本開示は、当業者が把握するような本稿に記載される例示的実施形態へのあらゆる変更、置換、変形、改変および修正を包含する。同様に、適切であれば、付属の請求項は、当業者が把握するような本稿に記載される例示的実施形態へのあらゆる変更、置換、変形、改変および修正を包含する。
【００９７】
以上の実施例を含む実施形態に関し、さらに以下の付記を開示する。
（付記１）
一つまたは複数のコンピューティング・デバイスによって：
ソフトウェア・モジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、
前記ソフトウェア・モジュールは：一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、
前記第一の制約条件は前記数値変数のうちの特定のものに適用され；
前記第一のストリング制約条件は前記ストリング変数のうちの特定のものに適用される、
段階と；
前記ストリング変数のうちの特定のものに適用される一つまたは複数の第二の数値制約条件を推定する段階と；
前記数値変数のうちの特定のものに適用される一つまたは複数の第二のストリング制約条件を推定する段階と；
前記第一および第二の数値制約条件のそれぞれを式で表現する段階と；
前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と；
前記ソフトウェア・モジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェア・モジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定のものについての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることによって行う段階とを含む、
方法。
（付記２）
付記１記載の方法であって：
前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み；
前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み；
前記入力数値変数の特定のものに適用される前記第一の数値制約条件および前記入力ストリング変数の特定のものに適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの仕様に基づいて決定され；
前記中間数値変数の特定のものに適用される前記第一の数値制約条件および前記中間ストリング変数の特定のものに適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの記号的実行を行うことによって決定される、
方法。
（付記３）
付記１記載の方法であって：
前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され；
前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、
方法。
（付記４）
付記３記載の方法であって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェア・モジュールを実装するプログラミング言語の仕様および前記ソフトウェア・モジュールが実行される実行時環境に基づいて推定される、方法。
（付記５）
付記１記載の方法であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることが：
前記数値変数および前記ストリング変数について逐次反復的に異なる可能な値を試し、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで行い；
解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、
方法。
（付記６）
付記１記載の方法であって：
前記ソフトウェア・モジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し；
前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており；
前記ソフトウェア・モジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェア・モジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、
方法。
（付記７）
付記６記載の方法であって：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数は、前記ソフトウェア・モジュールの一つまたは複数の入力変数および前記ソフトウェア・モジュールの一つまたは複数の出力変数を含み、
前記ソフトウェア・モジュールに関連付けられた前記要件が、前記ソフトウェア・モジュールの前記入力変数のうちの特定のものに適用される一つまたは複数の入力要件ならびに前記ソフトウェア・モジュールの前記出力変数のうちの特定のものに適用される一つまたは複数の出力要件を含み、
前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数のうちの特定のものに適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェア・モジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェア・モジュールを対応する実行経路の終わりに到達させるものである、段階と；
前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と；
前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と；
前記事後条件制約条件のそれぞれを否定にする段階と；
前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と；
制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と；
制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェア・モジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、
方法。
（付記８）
付記７記載の方法であって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、方法。
（付記９）
付記７記載の方法であって、前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：前記ソフトウェア・モジュールの記号的実行を行って前記制約条件の集合を得ることを含む、方法。
（付記１０）
一つまたは複数のプロセッサによって実行可能な命令を有するメモリと；
前記メモリに結合され、前記命令を実行するよう動作可能な一つまたは複数のプロセッサとを有するシステムであって、前記一つまたは複数のプロセッサは、前記命令を実行するとき：
ソフトウェア・モジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、
前記ソフトウェア・モジュールは：一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、
前記第一の数値制約条件は前記数値変数のうちの特定のものに適用され；
前記第一のストリング制約条件は前記ストリング変数のうちの特定のものに適用される、
段階と；
前記ストリング変数のうちの特定のものに適用される一つまたは複数の第二の数値制約条件を推定する段階と；
前記数値変数のうちの特定のものに適用される一つまたは複数の第二のストリング制約条件を推定する段階と；
前記第一および第二の数値制約条件のそれぞれを式で表現する段階と；
前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と；
前記ソフトウェア・モジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェア・モジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定のものについての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることによって行う段階とを実行するよう動作可能である、
システム。
（付記１１）
付記１０記載のシステムであって：
前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み；
前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み；
前記入力数値変数の特定のものに適用される前記第一の数値制約条件および前記入力ストリング変数の特定のものに適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの仕様に基づいて決定され；
前記中間数値変数の特定のものに適用される前記第一の数値制約条件および前記中間ストリング変数の特定のものに適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの記号的実行を行うことによって決定される、
システム。
（付記１２）
付記１０記載のシステムであって：
前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され；
前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、
システム。
（付記１３）
付記１２記載のシステムであって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェア・モジュールを実装するプログラミング言語の仕様および前記ソフトウェア・モジュールが実行される実行時環境に基づいて推定される、システム。
（付記１４）
付記１０記載のシステムであって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることが：
前記数値変数および前記ストリング変数について逐次反復的に異なる可能な値を試し、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで行い；
解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、
システム。
（付記１５）
付記１０記載のシステムであって：
前記ソフトウェア・モジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し；
前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており；
前記ソフトウェア・モジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェア・モジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、
システム。
（付記１６）
付記１５記載のシステムであって：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数は、前記ソフトウェア・モジュールの一つまたは複数の入力変数および前記ソフトウェア・モジュールの一つまたは複数の出力変数を含み、
前記ソフトウェア・モジュールに関連付けられた前記要件が、前記ソフトウェア・モジュールの前記入力変数のうちの特定のものに適用される一つまたは複数の入力要件ならびに前記ソフトウェア・モジュールの前記出力変数のうちの特定のものに適用される一つまたは複数の出力要件を含み、
前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数のうちの特定のものに適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェア・モジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェア・モジュールを対応する実行経路の終わりに到達させるものである、段階と；
前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と；
前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と；
前記事後条件制約条件のそれぞれを否定にする段階と；
前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と；
制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と；
制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェア・モジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、
システム。
（付記１７）
付記１６記載のシステムであって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、システム。
（付記１８）
付記１６記載のシステムであって、前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：前記ソフトウェア・モジュールの記号的実行を行って前記制約条件の集合を得ることを含む、システム。
（付記１９）
ソフトウェアを具現する一つまたは複数のコンピュータ読み取り可能な非一時的記憶媒体であって、前記ソフトウェアは、一つまたは複数のコンピューティング・デバイスによって実行されたときに：
ソフトウェア・モジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、
前記ソフトウェア・モジュールは：一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、
前記第一の制約条件は前記数値変数のうちの特定のものに適用され；
前記第一のストリング制約条件は前記ストリング変数のうちの特定のものに適用される、
段階と；
前記ストリング変数のうちの特定のものに適用される一つまたは複数の第二の数値制約条件を推定する段階と；
前記数値変数のうちの特定のものに適用される一つまたは複数の第二のストリング制約条件を推定する段階と；
前記第一および第二の数値制約条件のそれぞれを式で表現する段階と；
前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と；
前記ソフトウェア・モジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェア・モジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定のものについての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることによって行う段階とを実行するよう動作可能である、
媒体。
（付記２０）
付記１９記載の媒体であって：
前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み；
前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み；
前記入力数値変数の特定のものに適用される前記第一の数値制約条件および前記入力ストリング変数の特定のものに適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの仕様に基づいて決定され；
前記中間数値変数の特定のものに適用される前記第一の数値制約条件および前記中間ストリング変数の特定のものに適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの記号的実行を行うことによって決定される、
媒体。
（付記２１）
付記１９記載の媒体であって：
前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され；
前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、
媒体。
（付記２２）
付記２１記載の媒体であって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェア・モジュールを実装するプログラミング言語の仕様および前記ソフトウェア・モジュールが実行される実行時環境に基づいて推定される、媒体。
（付記２３）
付記１９記載の媒体であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることが：
前記数値変数および前記ストリング変数について逐次反復的に異なる可能な値を試し、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで行い；
解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、
媒体。
（付記２４）
付記１９記載の媒体であって：
前記ソフトウェア・モジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し；
前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており；
前記ソフトウェア・モジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェア・モジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、
媒体。
（付記２５）
付記２４記載の媒体であって：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数は、前記ソフトウェア・モジュールの一つまたは複数の入力変数および前記ソフトウェア・モジュールの一つまたは複数の出力変数を含み、
前記ソフトウェア・モジュールに関連付けられた前記要件が、前記ソフトウェア・モジュールの前記入力変数のうちの特定のものに適用される一つまたは複数の入力要件ならびに前記ソフトウェア・モジュールの前記出力変数のうちの特定のものに適用される一つまたは複数の出力要件を含み、
前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数のうちの特定のものに適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェア・モジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェア・モジュールを対応する実行経路の終わりに到達させるものである、段階と；
前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と；
前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と；
前記事後条件制約条件のそれぞれを否定にする段階と；
前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と；
制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と；
制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェア・モジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、
媒体。
（付記２６）
付記２５記載の媒体であって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、媒体。
（付記２７）
付記２５記載の媒体であって、前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：前記ソフトウェア・モジュールの記号的実行を行って前記制約条件の集合を得ることを含む、媒体。
（付記２８）
ソフトウェア・モジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する手段であって、
前記ソフトウェア・モジュールは：一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定のものに適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、
前記第一の制約条件は前記数値変数のうちの特定のものに適用され；
前記第一のストリング制約条件は前記ストリング変数のうちの特定のものに適用される、
手段と；
前記ストリング変数のうちの特定のものに適用される一つまたは複数の第二の数値制約条件を推定する手段と；
前記数値変数のうちの特定のものに適用される一つまたは複数の第二のストリング制約条件を推定する手段と；
前記第一および第二の数値制約条件のそれぞれを式で表現する手段と；
前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する手段と；
前記ソフトウェア・モジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェア・モジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定のものについての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めて解くことを試みることによって行う手段とを含む、
システム。
【００９８】
（付記１′）
一つまたは複数のコンピューティング・デバイスによって：
ソフトウェア・モジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、
前記ソフトウェア・モジュールは：一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、
前記第一の制約条件は前記数値変数のうちの特定の一つまたは複数に適用され；
前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、
段階と；
前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する段階と；
前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する段階と；
前記第一および第二の数値制約条件のそれぞれを式で表現する段階と；
前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と；
前記ソフトウェア・モジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェア・モジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う段階とを含む、
方法。
（付記２′）
付記１′記載の方法であって：
前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み；
前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み；
前記入力数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記入力ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの仕様に基づいて決定され；
前記中間数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記中間ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの記号的実行を行うことによって決定される、
方法。
（付記３′）
付記１′または２′記載の方法であって：
前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され；
前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、
方法。
（付記４′）
付記３′記載の方法であって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェア・モジュールを実装するプログラミング言語の仕様および前記ソフトウェア・モジュールが実行される実行時環境に基づいて推定される、方法。
（付記５′）
付記１′ないし４′のうちいずれか一項記載の方法であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることが：
前記数値変数および前記ストリング変数について可能な値を選び、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで逐次反復的に行い；
解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、
方法。
（付記６′）
付記１′ないし５′のうちいずれか一項記載の方法であって：
前記ソフトウェア・モジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し；
前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており；
前記ソフトウェア・モジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェア・モジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、
方法。
（付記７′）
付記６′記載の方法であって：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数は、前記ソフトウェア・モジュールの一つまたは複数の入力変数および前記ソフトウェア・モジュールの一つまたは複数の出力変数を含み、
前記ソフトウェア・モジュールに関連付けられた前記要件が、前記ソフトウェア・モジュールの前記入力変数のうちの特定の一つまたは複数に適用される一つまたは複数の入力要件ならびに前記ソフトウェア・モジュールの前記出力変数のうちの特定の一つまたは複数に適用される一つまたは複数の出力要件を含み、
前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数のうちの特定の一つまたは複数に適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェア・モジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェア・モジュールを対応する実行経路の終わりに到達させるものである、段階と；
前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と；
前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と；
前記事後条件制約条件のそれぞれを否定にする段階と；
前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と；
制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と；
制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェア・モジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、
方法。
（付記８′）
付記７′記載の方法であって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、方法。
（付記９′）
付記７′記載の方法であって、前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：前記ソフトウェア・モジュールの記号的実行を行って前記制約条件の集合を得ることを含む、方法。
（付記１０′）
一つまたは複数のプロセッサによって実行可能な命令を有するメモリと；
前記メモリに結合され、前記命令を実行するよう動作可能な一つまたは複数のプロセッサとを有するシステムであって、前記一つまたは複数のプロセッサは、前記命令を実行するとき：
ソフトウェア・モジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、
前記ソフトウェア・モジュールは：一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、
前記第一の数値制約条件は前記数値変数のうちの特定の一つまたは複数に適用され；
前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、
段階と；
前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する段階と；
前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する段階と；
前記第一および第二の数値制約条件のそれぞれを式で表現する段階と；
前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と；
前記ソフトウェア・モジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェア・モジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う段階とを実行するよう動作する、
システム。
（付記１１′）
ソフトウェアを具現する一つまたは複数のコンピュータ読み取り可能な非一時的記憶媒体であって、前記ソフトウェアは、一つまたは複数のコンピューティング・デバイスによって実行されたときに：
ソフトウェア・モジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する段階であって、
前記ソフトウェア・モジュールは：一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、
前記第一の制約条件は前記数値変数のうちの特定の一つまたは複数に適用され；
前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、
段階と；
前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する段階と；
前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する段階と；
前記第一および第二の数値制約条件のそれぞれを式で表現する段階と；
前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する段階と；
前記ソフトウェア・モジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェア・モジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う段階とを実行するよう動作可能である、
媒体。
（付記１２′）
付記１１′記載の媒体であって：
前記数値変数が、一つまたは複数の入力数値変数および一つまたは複数の中間数値変数を含み；
前記ストリング変数が、一つまたは複数の入力ストリング変数および一つまたは複数の中間ストリング変数を含み；
前記入力数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記入力ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの仕様に基づいて決定され；
前記中間数値変数の特定の一つまたは複数に適用される前記第一の数値制約条件および前記中間ストリング変数の特定の一つまたは複数に適用される前記第一のストリング制約条件は、前記ソフトウェア・モジュールの記号的実行を行うことによって決定される、
媒体。
（付記１３′）
付記１１′または１２′記載の媒体であって：
前記第二の数値制約条件は、前記第一のストリング制約条件および前記第二の演算に基づいて推定され；
前記第二のストリング制約条件は、前記第一の数値制約条件および前記第一の演算に基づいて推定される、
媒体。
（付記１４′）
付記１３′記載の媒体であって、前記第二の数値制約条件および前記第二のストリング制約条件が、さらに前記ソフトウェア・モジュールを実装するプログラミング言語の仕様および前記ソフトウェア・モジュールが実行される実行時環境に基づいて推定される、媒体。
（付記１５′）
付記１１′ないし１４′のうちいずれか一項記載の媒体であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることが：
前記数値変数および前記ストリング変数について可能な値を選び、該可能な値が一緒になって、前記第一および第二の数値制約条件、前記第一および第二のストリング制約条件ならびに前記要件のすべてを満たす解を与えるかどうかを試験することを、解が見出されるか、前記第一および第二の数値およびストリング制約条件が充足不能であると判定されるか、反復回数が閾値に達するかするまで逐次反復的に行い；
解が見出されたら、前記数値変数および前記ストリング変数についての値を出力することを含む、
媒体。
（付記１６′）
付記１１′ないし１５′のうちいずれか一項記載の媒体であって：
前記ソフトウェア・モジュールがさらに一つまたは複数の条件分岐点および該条件分岐点から帰結する一つまたは複数の実行経路を有し；
前記条件分岐点のそれぞれは、前記数値変数または前記ストリング変数の一つまたは複数によって指定される分岐条件に関連付けられており；
前記ソフトウェア・モジュールの実行中に、前記条件分岐点のそれぞれにおいて、前記ソフトウェア・モジュールが、その条件分岐点に関連付けられた分岐条件が満たされるかどうかに依存して前記実行経路のうちの異なるものを進む、
媒体。
（付記１７′）
付記１６′記載の媒体であって：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数は、前記ソフトウェア・モジュールの一つまたは複数の入力変数および前記ソフトウェア・モジュールの一つまたは複数の出力変数を含み、
前記ソフトウェア・モジュールに関連付けられた前記要件が、前記ソフトウェア・モジュールの前記入力変数のうちの特定の一つまたは複数に適用される一つまたは複数の入力要件ならびに前記ソフトウェア・モジュールの前記出力変数のうちの特定の一つまたは複数に適用される一つまたは複数の出力要件を含み、
前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：
前記ソフトウェア・モジュールの前記数値変数または前記ストリング変数のうちの特定の一つまたは複数に適用される制約条件の一つまたは複数の集合を決定する段階であって、前記制約条件の集合のそれぞれは、前記ソフトウェア・モジュールの前記実行経路の特定の一つに対応し、もし満たされれば、前記ソフトウェア・モジュールを対応する実行経路の終わりに到達させるものである、段階と；
前記入力要件のそれぞれを事前条件制約条件として表して一つまたは複数の事前条件制約条件を得る段階と；
前記出力要件のそれぞれを事後条件制約条件として表して一つまたは複数の事後条件制約条件を得る段階と；
前記事後条件制約条件のそれぞれを否定にする段階と；
前記事前条件制約条件および前記否定にされた事後条件制約条件を、制約条件の各集合に組み込む段階と；
制約条件の各集合を満たす一つまたは複数の解を見出すことを試みる段階と；
制約条件のいずれかの集合について何らかの解が見出される場合、前記ソフトウェア・モジュールが前記入力要件および前記出力要件のすべては満たさないことを示す段階とを含む、
媒体。
（付記１８′）
付記１７′記載の媒体であって、制約条件の各集合が、前記第一および第二の数値制約条件および前記第一および第二のストリング制約条件に基づいて決定される、媒体。
（付記１９′）
付記１７′記載の媒体であって、前記ソフトウェア・モジュールに関連付けられた要件に関して前記ソフトウェア・モジュールを検証することが：前記ソフトウェア・モジュールの記号的実行を行って前記制約条件の集合を得ることを含む、媒体。
（付記２０′）
ソフトウェア・モジュールに関連付けられた一つまたは複数の第一の数値制約条件および一つまたは複数の第一のストリング制約条件を解析する手段であって、
前記ソフトウェア・モジュールは：一つまたは複数の数値変数、一つまたは複数のストリング変数、前記数値変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第一の演算および前記ストリング変数のうち特定の一つまたは複数に適用され数値もしくはストリング結果を生じる一つまたは複数の第二の演算を有し、
前記第一の制約条件は前記数値変数のうちの特定の一つまたは複数に適用され；
前記第一のストリング制約条件は前記ストリング変数のうちの特定の一つまたは複数に適用される、
手段と；
前記ストリング変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二の数値制約条件を推定する手段と；
前記数値変数のうちの特定の一つまたは複数に適用される一つまたは複数の第二のストリング制約条件を推定する手段と；
前記第一および第二の数値制約条件のそれぞれを式で表現する手段と；
前記第一および第二のストリング制約条件のそれぞれを有限状態機械で表現する手段と；
前記ソフトウェア・モジュールに関連付けられた一つまたは複数の要件に関して前記ソフトウェア・モジュールを検証することを、前記数値変数および前記ストリング変数のうちの特定の一つまたは複数についての一つまたは複数の値を有する解であって、前記第一および第二の数値制約条件のすべて、前記第一および第二のストリング制約条件のすべてならびに前記要件のすべてを満たす解を求めることを試みることによって行う手段とを含む、
システム。
【符号の説明】
【００９９】
１０２  ソフトウェア・モジュールと、ソフトウェア・モジュールの数値変数に適用される数値制約条件と、ソフトウェア・モジュールのストリング変数に適用されるストリング制約条件とを解析
１０４  ソフトウェア・モジュールのストリング変数に適用される数値制約条件およびソフトウェア・モジュールの数値変数に適用されるストリング制約条件を推定
１０６  各数値制約条件を数式で表現し、各ストリング制約条件を有限状態機械で表現
１０８  制約条件すべてを満たす解を求めることを試みる
２００  ソフトウェア・モジュールまたはソフトウェア・モジュールの変数に対して課される制約条件を決定および解決するためのシステム
２０２  相互的〔クロス〕制約条件発生器
２０４  制約条件ソルバ
２０６  記号的実行
２１２  ソフトウェア・モジュール
２１４  指定された制約条件
３１０  有限状態機械（FSM）
３２０  有限状態機械（FSM）
３３０  有限状態機械（FSM）
３４０  有限状態機械（FSM）
３５０  有限状態機械（FSM）
４０２  ストリング開始
４０４  ストリング受容
４１２  部分ストリング開始
４１４  部分ストリング受容
５１０  ストリング・ドメイン
５１２  ストリング制約条件
５２０  数値ドメイン
５２２  数値制約条件
５２４  制約条件
５２６  制約条件
５２８  制約条件
５３１  反復工程
５３２  反復工程
５３３  反復工程
５３４  反復工程
５３５  反復工程
５３６  反復工程
６０２  条件１
６０４  条件２
６０６  条件３
６０８  条件４
６１２  処理ステップ
６１４  処理ステップ
６１６  処理ステップ
６１８  処理ステップ
６２２  処理ステップ
７０２  ソフトウェア・モジュールに対して記号的実行を行って、ソフトウェア・モジュールの可能な各実行経路について、記号的表現の集合を決定
７０４  記号的表現の各集合を制約条件の集合として表す
７０６  制約条件の各集合について一つまたは複数の解を見出すことを試みる
７０８  それらの解を使ってソフトウェア・モジュールを試験
８０２  表２のコードの第２行に対応
８０４  表２のコードの第３行に対応
８０６  表２のコードの第５行に対応
８０８  表２のコードの第６行に対応
８１０  表２のコードの第８行に対応
９０２  制約条件の集合
９０４  制約条件の集合
９０６  制約条件の集合
９１２  経路
９１４  経路
９１６  経路
１００２  ソフトウェア・モジュールの入力および出力に課される仕様要件を、ソフトウェア・モジュールの入力変数および出力変数に課される制約条件として表す
１００４  ソフトウェア・モジュールの出力に課される仕様要件を否定に
１００６  ソフトウェア・モジュールの入力変数に課された制約条件およびソフトウェア・モジュールの出力変数に課された制約条件の否定を用いてソフトウェア・モジュールに対して記号的実行を行って、ソフトウェア・モジュールの各実行経路について表現の集合を得る
１００８  表現の各集合について解を見出すことを試みる
１１０２  悪性ストリングの集合を選択
１１０４  各悪性ストリングを入力としての別のストリングに埋め込み
１１０６  セキュリティ・ソフトウェア・モジュールに関して記号的実行を行って、セキュリティ・ソフトウェア・モジュールを成功裏に返させる表現の集合を決定
１１０８  一つまたは複数の悪性ストリングを含みつつ前記表現の集合を満たす、入力ストリングについての一つまたは複数の解を見出そうと試みる
１２１０  ネットワーク
１２２０  サーバー
１２３０  クライアント
１２３２  ウェブ・ブラウザー
１２４０  記憶装置
１２５０  リンク
１３０２  プロセッサ
１３０４  メモリ
１３０６  記憶装置
１３０８  I/Oインターフェース
１３１０  プロセッサ
【図１】
0005786511.tif 000005
【図２】
0005786511.tif 000006
【図３】
0005786511.tif 000007
【図４】
0005786511.tif 000008
【図５】
0005786511.tif 000009
【図６】
0005786511.tif 000010
【図７】
0005786511.tif 000011
【図８】
0005786511.tif 000012
【図９Ａ】
0005786511.tif 000013
【図９Ｂ】
0005786511.tif 000014
【図９Ｃ】
0005786511.tif 000015
【図１０】
0005786511.tif 000016
【図１１】
0005786511.tif 000017
【図１２】
0005786511.tif 000018
【図１３】
0005786511.tif 000019