(57)【要約】  フルワード飽和加算およびフルワード飽和減算の認識を容易にする、式を定式化し、解く方法。この方法には、基礎加算ステートメントｚ＝ｘ＋ｙまたは基礎減算ステートメントｚ＝ｘ−ｙごとに、分析されるプログラム・ステートメントのプロパティを記述するデータ・フロー式を定式化することと、データ・フロー式を解くことが含まれる。プロパティに、（ａ）ｘ、ｙ、およびｚの符号ビットのブール関数としてのプログラム変数の値ＢＩＴＳと、（ｂ）ｘ、ｙ、およびｚの符号ビットのブール関数としての、プログラム・ステートメントがその下で実行される条件ＣＯＮＤと、（ｃ）オーバーフロー／アンダーフロー／どちらもなしが発生する時に変数の値がｚの所与の使用に達する条件ＲＥＡＣＨを含めることができる。
2007528073.tif 000002
【特許請求の範囲】
【請求項１】
すべての基礎ステートメントＡについて、ｚ＝ＡＤＤ（ｘ，ｙ）またはｚ＝ＳＵＢ（ｘ，ｙ）の形の、プログラム内のフルワード飽和加算およびフルワード飽和減算を認識する方法であって、
前記ステートメントＡの直後にステートメントｚｓａｔ＝ＡＤＤＳＡＴ（ｘ，ｙ）またはｚｓａｔ＝ＳＵＢＳＡＴ（ｘ，ｙ）を挿入することと、
前記プログラム内の辺Ｅの変数ｖのビット値ＢＩＴＳ（Ｅ，ｖ）プロパティを計算することと、
前記辺Ｅが前記プログラム内でその下で実行される条件ＣＯＮＤ（Ｅ）プロパティを計算することと、
前記変数ｖのどの値が、オーバーフロー、アンダーフロー、または正常のオカレンスについて前記プログラムの辺ＥでステートメントＳ内の変数ｚの使用に達するかを示すリーチＲＥＡＣＨ（Ｅ，ｖ）プロパティを計算することと、
ａ）オーバーフローが発生した時に、Ｓに達するｚの値だけがｚにＳＡＴＭＡＸを割り当て、ｂ）アンダーフローが発生した場合に、Ｓに達するｚの値だけがｚにＳＡＴＭＩＮを割り当て、ｃ）アンダーフローおよびオーバーフローが発生していない場合に、Ｓに達するｚの値だけが前記基礎ステートメントＡからであるという条件のすべてがステートメントＳについて成り立つ場合に、ｚを使用するステートメントＳのｚをｚｓａｔの使用に置換することと、
前のステップでのｚの使用のｚｓａｔの使用への前記置換によって不要にされたステートメントを除去することと
を含む方法。
【請求項２】
Ｘ、Ｙ、およびＺが、それぞれ、変数ｘ、ｙ、およびｚの符号であるものとして、ＲＥＡＣＨのオーバーフロー述部、アンダーフロー述部、および「正常」述部を、
【表１】
2007528073.tif 000006
のように定義することを含む、請求項１に記載の方法。
【請求項３】
前記ＲＥＡＣＨプロパティは、前記辺Ｅが実行された時に、オーバーフローが発生している場合に、前記変数ｖがとる定数値ＣＯＦ（Ｅ，ｖ）と、前記辺Ｅが実行された時に、アンダーフローが発生している場合に、前記変数ｖがとる定数値ＣＵＦ（Ｅ，ｖ）と、前記辺Ｅが実行された時に、オーバーフローおよびアンダーフローが発生していない場合に、ｖが前記基礎ステートメントＡの前記変数Ｚと同一の値を担持することを示すブール・フラグＩＳＺ（Ｅ，ｖ）とを含む、請求項２に記載の方法。
【請求項４】
フルワード飽和加算およびフルワード飽和減算の認識を容易にする、プログラム分析式を定式化し、解く方法において、基礎加算ステートメントｚ＝ｘ＋ｙまたは基礎減算ステートメントｚ＝ｘ−ｙごとに、分析される前記プログラム・ステートメントのプロパティすなわち、
ａ）Ｘ、Ｙ、およびＺの符号ビットのブール関数としてのプログラム変数ｘ、ｙ、およびｚの値ＢＩＴＳと、
ｂ）Ｘ、Ｙ、およびＺの符号ビットのブール関数としての、プログラム・ステートメントＳがその下で実行される条件ＣＯＮＤと、
ｃ）オーバーフロー、アンダーフロー、または正常のオカレンスについて、変数のどの値がステートメントＳの変数ｚの使用に達するかの条件ＲＥＡＣＨと
を記述するデータ・フロー式を定式化すること
を含む方法。
【請求項５】
オーバーフロー、アンダーフロー、または正常のオカレンスが、Ｘ、Ｙ、およびＺの前記符号ビットの関数として判定される、請求項４に記載の方法。
【請求項６】
ステートメントＳについて、ａ）オーバーフローが発生した時にＳに達するｚの値だけがｚにＳＡＴＭＡＸを割り当て、ｃ）アンダーフローが発生した場合にＳに達するｚの値だけがｚにＳＡＴＭＩＮを割り当て、ｄ）アンダーフローおよびオーバーフローが発生していない場合に、Ｓに達するｚの値だけが前記基礎ステートメントＡからであるという条件のすべてが成り立つ場合に限って、前記プログラムのｚを使用するステートメントＳのｚをｚｓａｔの使用に置換することを含む、請求項４に記載の方法。
【請求項７】
ｚの使用のｚｓａｔの使用への前記置換によって不要にされたステートメントを除去することを含む、請求項６に記載の方法。
【請求項８】
密な技法を使用してＢＩＴＳの式、ＣＯＮＤの式、およびＲＥＡＣＨの式を解くことを含む、請求項４に記載の方法。
【請求項９】
疎なプログラム表現を使用してＢＩＴＳの式、ＣＯＮＤの式、およびＲＥＡＣＨの式を解くことを含む、請求項４に記載の方法。
【請求項１０】
前記値および条件は、ＢＩＴＳ、ＣＯＮＤ、およびＲＥＡＣＨを近似するラティスと、近似をさまざまなプログラム点に関係させる連立方程式とを含むグローバル・データ・フロー分析を使用して近似される、請求項４に記載の方法。
【請求項１１】
前記変数に割り当てられたラティス・ベクトルを圧縮することを含む、請求項１０に記載の方法。
【請求項１２】
ＲＥＡＣＨは、前記辺Ｅが実行された時に、オーバーフローが発生している場合に、前記変数ｖがとる定数値ＣＯＦ（Ｅ，ｖ）と、前記辺Ｅが実行された時に、アンダーフローが発生している場合に、前記変数ｖがとる定数値ＣＵＦ（Ｅ，ｖ）と、前記辺Ｅが実行された時に、オーバーフローおよびアンダーフローが発生していない場合に、ｖが前記基礎ステートメントＡの前記変数Ｚと同一の値を担持することを示すブール・フラグＩＳＺ（Ｅ，ｖ）とを含む、請求項４に記載の方法。
【請求項１３】
基礎加算ステートメントｚ＝ｘ＋ｙまたは基礎減算ステートメントｚ＝ｘ−ｙごとに、分析される前記プログラム・ステートメントのプロパティを記述したデータ・フロー式を定式化することと、
前記データ・フロー式を解くことと
を含む、フルワードフルワード飽和加算およびフルワード飽和減算の認識を容易にする、式を定式化し、解く方法。
【請求項１４】
前記プロパティは、
ａ）Ｘ、Ｙ、およびＺの符号ビットのブール関数としてのプログラム変数ｘ、ｙ、およびｚの値ＢＩＴＳと、
ｂ）Ｘ、Ｙ、およびＺの符号ビットのブール関数としての、プログラム・ステートメントＳがその下で実行される条件ＣＯＮＤと、
ｃ）オーバーフロー、アンダーフロー、または正常のオカレンスについて、変数のどの値がステートメントＳの変数ｚの使用に達するかの条件ＲＥＡＣＨと
を含む、請求項１３に記載の方法。
【請求項１５】
オーバーフロー、アンダーフロー、または正常の前記オカレンスは、Ｘ、Ｙ、およびＺの前記符号ビットの関数として判定される、請求項１４に記載の方法。
【請求項１６】
ステートメントＳについて、ａ）オーバーフローが発生した時にＳに達するｚの値だけがｚにＳＡＴＭＡＸを割り当て、ｃ）アンダーフローが発生した場合にＳに達するｚの値だけがｚにＳＡＴＭＩＮを割り当て、ｄ）アンダーフローおよびオーバーフローが発生していない場合に、Ｓに達するｚの値だけが前記基礎ステートメントＡからであるという条件のすべてが成り立つ場合に限って、前記プログラムのｚを使用するステートメントＳのｚをｚｓａｔの使用に置換することを含む、請求項１４に記載の方法。
【請求項１７】
ｚの使用のｚｓａｔの使用への前記置換によって不要にされたステートメントを除去することを含む、請求項１６に記載の方法。
【請求項１８】
密な技法を使用して前記式を解くことを含む、請求項１３に記載の方法。
【請求項１９】
疎なプログラム表現を使用して前記式を解くことを含む、請求項１３に記載の方法。
【請求項２０】
前記値および条件は、ＢＩＴＳ、ＣＯＮＤ、およびＲＥＡＣＨを近似するラティスと、近似をさまざまなプログラム点に関係させる連立方程式とを含むグローバル・データ・フロー分析を使用して近似される、請求項１４に記載の方法。
【請求項２１】
前記変数に割り当てられたラティス・ベクトルを圧縮することを含む、請求項２０に記載の方法。
【請求項２２】
ＲＥＡＣＨは、前記辺Ｅが実行された時に、オーバーフローが発生している場合に、前記変数ｖがとる定数値ＣＯＦ（Ｅ，ｖ）と、前記辺Ｅが実行された時に、アンダーフローが発生している場合に、前記変数ｖがとる定数値ＣＵＦ（Ｅ，ｖ）と、前記辺Ｅが実行された時に、オーバーフローおよびアンダーフローが発生していない場合に、ｖが前記基礎ステートメントＡの前記変数Ｚと同一の値を担持することを示すブール・フラグＩＳＺ（Ｅ，ｖ）とを含む、請求項１４に記載の方法。
【発明の詳細な説明】
【技術分野】
【０００１】
全般的にはフルワード飽和加算（ｓａｔｕｒａｔｉｎｇ  ａｄｄｉｔｉｏｎ）およびフルワード飽和減算（ｓａｔｕｒａｔｉｎｇ  ｓｕｂｔｒａｃｔｉｏｎ）の認識の新しい方法、具体的には、分析されたコンピュータ・プログラムから導出されたデータ・フロー式の解に基づく方法。これは、プログラム・コード内の固定されたパターンのマッチングに基づく現在使用されている方法と対照的である。
【背景技術】
【０００２】
本明細書で参照され、末尾にリストされた参考文献は、本発明の実施形態を理解するのに必要なものとして本明細書に組み込まれている。
【０００３】
飽和算術は、ディジタル信号処理（ＤＳＰ）アプリケーションで広く使用されている。フルワード飽和算術演算は、対応する基本的な２の補数演算がオーバーフローまたはアンダーフローする情況で結果に事前定義の最大値または最小値をセットすることによって働く。
【０００４】
現代のディジタル信号プロセッサは、飽和演算の高速実装を提供する。それと同時に、多数のＤＳＰアプリケーションが、標準的なプログラミング言語（ＡＮＳＩ  Ｃなど）で記述され、飽和演算は、基本的な２の補数演算に関してサブルーチンまたはマクロとしてコーディングされている。そのようなプログラムの高速実行を提供するために、最適化コンパイラに、可能な時に必ず、コード・フラグメントを自動的に認識させ、個々の飽和演算に変換させることが重要である。
【０００５】
飽和演算を有するディジタル信号プロセッサに関するコンパイルの従来技術は、２つのカテゴリすなわち、ａ）、特殊なデータ型または組み込み関数が、どの±演算を飽和しているものとして扱わなければならないかをコンパイラに知らせるのに使用されるカテゴリ、およびｂ）プログラム・フラグメントのパターン・マッチングが飽和演算の発見に使用されるカテゴリに分類される。飽和演算を自動的に認識するという作業は、そのような演算をプログラミングする多数の形があるという事実によって複雑になる。単純なパターン認識に頼る最適化コンパイラは、多数のパターンをテストしなければならない。
【発明の開示】
【課題を解決するための手段】
【０００６】
本発明は、飽和加算および飽和減算を認識するという問題を、最適化コンパイラの分野で周知の技法（参考文献１、５、６、７参照）を使用して解くことができるデータ・フロープログラム分析式のセットにこれらの動作のエッセンスを取り込むことによって解決する。
【０００７】
フルワード飽和加算およびフルワード飽和減算の認識を容易にする、式を定式化し解く方法に、基本的な加算ステートメントｚ＝ｘ＋ｙまたは減算ステートメントｚ＝ｘ−ｙごとに、分析されるプログラム・ステートメントのプロパティを記述したデータ・フロー式を定式化することと、データ・フロー式を解くことが含まれる。
【０００８】
プログラムの次のプロパティを使用することができる。
（ａ）ｘ、ｙ、およびｚの符号ビットのブール関数としてのプログラム変数の値ＢＩＴＳ、
（ｂ）その下でプログラム・ステートメントが実行される、ｘ、ｙ、およびｚの符号ビットのブール関数としての条件ＣＯＮＤ、および
（ｃ）オーバーフロー／アンダーフロー／どちらもなしが発生する時にその変数の値がｚの所与の使用に達する条件ＲＥＡＣＨ。
【０００９】
この方法は、ステートメントＳについて、ａ）オーバーフローが発生した時にＳに達するｚの値だけがｚにＳＡＴＭＡＸを割り当て、ｃ）アンダーフローが発生した場合にＳに達するｚの値だけがｚにＳＡＴＭＩＮを割り当て、ｄ）アンダーフローおよびオーバーフローが発生していない場合に、Ｓに達するｚの値だけが基礎ステートメントＡからであるという条件のすべてが成り立つ場合に限って、プログラムのｚを使用するステートメントＳのｚをｚｓａｔの使用に置換することを含む。最後に、ｚの使用のｚｓａｔの使用への前記置換によって不要にされたステートメントを除去する。
【００１０】
ＢＩＴＳ、ＣＯＮＤ、およびＲＥＡＣＨの式は、密な技法または疎なプログラム表現を使用することができる。方法の値および条件は、グローバル・データ・フロー分析を使用して近似され、これには、適当なプロパティ（値および条件ＢＩＴＳ、ＣＯＮＤ、およびＲＥＡＣＨ）のラティスおよびさまざまなプログラム点への近似に関する連立方程式が含まれる。変数に割り当てられたらティス・ベクトルを、圧縮することができる。
【００１１】
ＲＥＡＣＨプロパティは、辺Ｅが実行された時に、オーバーフローが発生している場合に、変数ｖがとる定数値ＣＯＦ（Ｅ，ｖ）と、辺Ｅが実行された時に、アンダーフローが発生している場合に、変数ｖがとる定数値ＣＵＦ（Ｅ，ｖ）と、辺Ｅが実行された時に、オーバーフローおよびアンダーフローが発生していない場合に、ｖが基礎ステートメントＡの変数Ｚと同一の値を担持することを示すブール・フラグＩＳＺ（Ｅ，ｖ）とを含む。
本発明の上記および他の態様は、添付図面と共に検討される時に、本発明の次の詳細な説明から明白になる。
【発明を実施するための最良の形態】
【００１２】
最初は、式の導出のためにプログラムがどのように表されるかの説明である。フルワード飽和加算およびフルワード飽和減算という概念を定式化する。次に、連立方程式を定式化し、フルワード飽和加算およびフルワード飽和減算を認識するアルゴリズムを表す形を説明する。
【００１３】
プログラムの提示
ソース言語プログラムが、個々のプロシージャに分解される。本技法は、１時に１プロシージャを、他のプロシージャと独立に操作するという点で、イントラプロシージャ的である。本明細書で、用語「プログラム」および「プロシージャ」は、交換可能に使用される。
各プロシージャは、その制御フローグラフ（ＣＦＧ）を使用して表される。このグラフのノードは、プログラム・ステートメントである。このグラフの辺は、ステートメントの間のプログラム・フローの可能な転送を表す。代入ステートメントの複合式が、それぞれに単一の演算子だけが含まれる単純な代入ステートメントに変換されていると仮定する。そのような表現は、標準的であり、文献では３アドレス・フォーム（参考文献１）と称する。
【００１４】
プログラム・ステートメントには次の４種類がある。
１．一意エントリ・ステートメント。
２．代入ステートメントは、算術演算を介して新しい値を計算し、メモリ・ロードまたはメモリ・ストアを実行し、あるいはプロシージャ呼び出しを実行する。一般性を失わずに、この記述を、下で列挙される代入ステートメントに制限することができる。
算術演算ＯＰＢ（ｘ，ｙ）は、ビット幅によってパラメータ化される。たとえば、８ビット整数値の符号付き加算は、ａｄｄ８（ｘ，ｙ）に変換される。算術演算に、飽和加算ａｄｄｓａｔＢおよび飽和減算ｓｕｂｓａｔＢが含まれる。これらは、最初に下げられる（ｉｎｉｔｉａｌｌｙ  ｌｏｗｅｒｅｄ）ソース・プログラムに存在しない。
３．制御ステートメントは、プログラム・フローの代替方向を提供する。一般性を失わずに、２種類の制御ステートメント、ＩＦＢ（ｖ）およびＲＥＴＵＲＮだけがあると仮定する。スイッチ・ステートメントＩＦＢ（ｖ）は、制御フロー・グラフで２つの子孫を有し、Ｂビット整数として解釈されるｖの値が非０デある場合に、第１の子孫に、そうでない場合に第２の子孫に制御を転送する。他の種類の制御フロー・ステートメント（たとえば、ループ、他方向スイッチ）は、代入ステートメントおよびＩＦステートメントのシーケンスに変換することができる。
ＲＥＴＵＲＮステートメントは１つのプロシージャに１つだけ存在することができる。これは、プログラムの制御を呼出し側プロシージャに転送しなければならないことを示す。任意選択として、ＲＥＴＵＲＮステートメントは、値を返すことができる：ＲＥＴＵＲＮ（ｖ）。
４．マージ・ステートメントは、プログラム実行の代替パスがマージされる点である。
【００１５】
そのような表現について、下記の事実を観察されたい。
・代入ステートメントは、正確に１つの入る辺および正確に１つの出る辺を有する。表記ＩＮ（Ｓ）およびＯＵＴ（Ｓ）は、それぞれ、代入ステートメントＳの入る辺および出る辺を表す。ＰＲＥ（Ｓ）は、前にあるステートメントを表し、ＳＵＣＣ（Ｓ）は、後にあるステートメントを表す。
・エントリ・ステートメントは、入る辺を有しないが、正確に１つの出る辺を有する。ＩＮ（Ｓ）およびＰＲＥ（Ｓ）は、エントリ・ステートメントについて意味がない。ＯＵＴ（Ｓ）およびＳＵＣＣ（Ｓ）は、代入ステートメントと同一の意味を有する。
・制御ステートメント（ＩＦおよびＲＥＴＵＲＮ）のそれぞれは、正確に１つの入る辺を有する。スイッチまたはＩＦは、プログラムの真方向および偽方向の、正確に２つの出る辺、ＯＵＴ（Ｓ，ｔｒｕｅ）およびＯＵＴ（Ｓ，ｆａｌｓｅ）を有する。ＲＥＴＵＲＮは、出る辺を有しない。ＩＮ（Ｓ）およびＰＲＥ（Ｓ）は、制御ステートメントに関して、代入ステートメントと同一の意味を有する。ＩＦステートメントについて、ＳＵＣＣ（Ｓ，ｔｒｕｅ）は、「真」方向に続くノードであり、ＳＵＣＣ（Ｓ，ｆａｌｓｅ）は、「偽」方向に続くノードである。
・マージ・ステートメントは、正確に１つの出る辺を有し、複数の入る辺を有することができる。ＯＵＴ（Ｓ）およびＳＵＣＣ（Ｓ）は、出る辺および後に続くステートメントを表す。ジョイン・ステートメントについて、ＩＮ（Ｓ）およびＰＲＥ（Ｓ）は、入ってくる辺の集合を表す。すべてのマージ・ステートメントが、正確に２つの入ってくる辺を有すると仮定する。これによって、式が単純になるが、本発明の性質は変化しない。
可能な種類の代入ステートメントおよびその説明を、下の表にリストする。
【００１６】
【表２】
2007528073.tif 000003
【００１７】
フルワード飽和演算の定義
フルワード飽和加算およびフルワード飽和減算は、次のように、基本的なＢビットの２の補数の加算および減算に関して定義される。
【００１８】
【表３】
2007528073.tif 000004
【００１９】
飽和値ＳＡＴＭＩＮが最小の数であり、飽和値ＳＡＴＭＡＸが最大の数である場合に、Ｂビット２の補数算術を使用してこれを表すことができる。
【００２０】
【表４】
2007528073.tif 000005
【００２１】
問題
ＡＮＳＩ  Ｃなどの高水準プログラミング言語でフルワードＡＤＤＳＡＴ演算子およびフルワードＳＵＢＳＡＴ演算子をプログラムする多数の可能な形がある。下は、ＡＤＤＳＡＴのある可能な（排他的ではない）実装である。
ｉｎｔ  Ａｄｄ＿Ｓａｔｕｒａｔｅｄ＿１（ｉｎｔ  ｘ，  ｉｎｔ  ｙ）  ｛
ｉｎｔ  ｚ  ＝  ｘ  ＋  ｙ；
ｉｆ  （（ｘ  ＞  ０）  ＆＆  （ｙ  ＞  ０）  ＆＆  （ｚ  ＜  ０））  ｛
ｚ  ＝  ＳＡＴＭＡＸ；      ／＊  オーバーフロー  ＊／
｝
ｅｌｓｅ  ｉｆ  （（ｘ  ＜  ０）  ＆＆  （ｙ  ＜  ０）  ＆＆  （ｚ  ＞  ０））  ｛
ｚ  ＝  ＳＡＴＭＩＮ；      ／＊  アンダーフロー  ＊／
｝
ｒｅｔｕｒｎ  ｚ；
｝
ｉｎｔ  Ａｄｄ＿Ｓａｔｕｒａｔｅｄ＿２（ｉｎｔ  ｘ，  ｉｎｔ  ｙ）  ｛
ｉｎｔ  ｚ  ＝  ｘ  ＋  ｙ；
ｉｎｔ  ｓｉｇｎ＿ｘ  ＝  ｘ  ＆  ＳＡＴＭＩＮ；  ／＊  負の場合に１０００…０００  ＊／
ｉｎｔ  ｓｉｇｎ＿ｙ  ＝  ｙ  ＆  ＳＡＴＭＩＮ；
ｉｎｔ  ｓｉｇｎ＿ｚ  ＝  ｚ  ＆  ＳＡＴＭＩＮ；
ｉｆ  （！ｓｉｇｎ＿ｘ  ＆＆  ！ｓｉｇｎ＿ｙ  ＆＆  ｓｉｇｎ＿ｚ）  ｛
ｚ  ＝  ＳＡＴＭＡＸ；      ／＊  オーバーフロー  ＊／
｝
ｅｌｓｅ  ｉｆ  （ｓｉｇｎ＿ｘ  ＆＆  ｓｉｇｎ＿ｙ  ＆＆  ！ｓｉｇｎ＿ｚ）  ｛
ｚ  ＝  ＳＡＴＭＩＮ；      ／＊  アンダーフロー  ＊／
｝
ｒｅｔｕｒｎ  ｚ;
｝
ｉｎｔ  Ａｄｄ＿Ｓａｔｕｒａｔｅｄ＿３（ｉｎｔ  ｘ，  ｉｎｔ  ｙ）  ｛
ｉｎｔ  ｚ  ＝  ｘ  ＋  ｙ；
ｉｎｔ  ｓｉｇｎ＿ｘ  ＝  ｘ  ＆  ＳＡＴＭＩＮ；    ／＊  負の場合に１０００…０００  ＊／
ｉｎｔ  ｓｉｇｎ＿ｙ  ＝  ｙ  ＆  ＳＡＴＭＩＮ；
ｉｎｔ  ｓｉｇｎ＿ｚ  ＝  ｚ  ＆  ＳＡＴＭＩＮ；
ｉｆ  （  （〜（ｓｉｇｎ＿ｘ  ＾  ｓｉｇｎ＿ｙ））  ＆  （ｓｉｇｎ＿ｘ  ＆  ｓｉｇｎ＿ｚ）  ）  ｛
ｚ  ＝  ｓｉｇｎ＿ｘ  ？  ＳＡＴＭＩＮ  ：  ＳＡＴＭＡＸ；
｝
ｒｅｔｕｒｎ  ｚ；
｝
ｉｎｔ  Ａｄｄ＿Ｓａｔｕｒａｔｅｄ＿４（ｉｎｔ  ｘ，  ｉｎｔ  ｙ）  ｛
ｉｎｔ  ｚ  ＝  ｘ  ＋  ｙ；
ｉｎｔ  ｓｉｇｎ＿ｘ  ＝  ｘ  ＆  ＳＡＴＭＩＮ；    ／＊  負の場合に１０００…０００  ＊／
ｉｎｔ  ｓｉｇｎ＿ｙ  ＝  ｙ  ＆  ＳＡＴＭＩＮ；
ｉｎｔ  ｓｉｇｎ＿ｚ  ＝  ｚ  ＆  ＳＡＴＭＩＮ；
ｉｆ  （  （ＳＡＴＭＩＮ  ＾（ｓｉｇｎ＿ｘ  ＾  ｓｉｇｎ＿ｙ））  ＆  （ｓｉｇｎ＿ｘ  ＆  ｓｉｇｎ＿ｚ）  ）  ｛
ｚ  ＝  ＳＡＴＭＡＸ  ＋  （（ｘ  ＞＞  ３１）  ＆  ０ｘ１）；
｝
ｒｅｔｕｒｎ  ｚ；
｝
ｉｎｔ  Ａｄｄ＿Ｓａｔｕｒａｔｅｄ＿５  （ｉｎｔ  ｘ，  ｉｎｔ  ｙ）  ｛
ｉｎｔ  ｚ  ＝  ｘ  ＋  ｙ；
ｉｎｔ  ＯＦ  ＝  （〜ｘ  ＆  〜ｙ  ＆  ｚ）  ＞＞  ３１；      ／＊  算術シフト  ！  ＊／
ｉｎｔ  ＵＦ  ＝  （ｘ  ＆  ｙ  ＆  〜ｚ）  ＞＞  ３１；
ｉｎｔ  Ｎ  ＝  〜（ＯＦ  ｜  ＵＦ）；
ｒｅｔｕｒｎ  （ＭＡＸ３２  ＆  ＯＦ）  ｜  （ＭＩＮ３２  ＆  ＵＦ）  ｜  （ｚ  ＆  Ｎ）；
｝
【００２２】
上のプログラム・フラグメントは、オーバーフローおよびアンダーフローを検出するためにｘ、ｙ、およびｚの符号ビットの組合せをテストする形が異なる。
一般に、ＡＤＤＳＡＴ演算子およびＳＵＢＳＡＴ演算子を含まない３アドレス中間形式のプログラムが提供される。目標は、ＡＤＤＳＡＴ演算子およびＳＵＢＳＡＴ演算子によって置換できるプログラム・フラグメントを認識することである。
【００２３】
プログラム分析技法
Ｇ＝（Ｎ，Ｅ）が、制御フロー・グラフであるものとする。Ｎは、ノード（ステートメント）の集合であり、Ｅは、辺の集合である。υが、プログラムの変数の集合であるものとする。
このアルゴリズムは、加算ステートメントａｄｄＢ（ｘ，ｙ）ごとに、飽和した値を受け取る割り当てられる変数ｚの使用の集合を計算することによって進行する。考慮される加算ステートメントは、基礎ステートメント（ｂａｓｉｓ  ｓｔａｔｅｍｅｎｔ）である。この基礎ステートメントに用いられる変数ｘ、ｙ、およびｚは、基礎変数（ｂａｓｉｓ  ｖａｒｉａｂｌｅ）である。ｚの飽和した値を受け取る使用は、飽和使用（ｓａｔｕｒａｔｅｄ  ｕｓｅ）である。ｘ、ｙ、およびｚの符号ビットは、基礎符号ビット（ｂａｓｉｓ  ｓｉｇｎ  ｂｉｔ）であり、それぞれＸ、Ｙ、およびＺと称する。
【００２４】
飽和使用を識別するために、変数の値と、ブール関数としての、その下でステートメントが実行される条件とを、基礎ステートメントの基礎符号ビットに関して表す。また、オーバーフロー、アンダーフロー、または通常実行の場合に所与の使用に達する値を計算する。
基礎ステートメントを与えられて、本アルゴリズムは、プログラムの辺Ｅおよび変数ｖについて、次のプロアティを計算する。
・ＢＩＴＳ（Ｅ，ｖ）は、ｖのビットごとに１関数の、基礎符号ビットに関するブール関数のベクトルである。これは、辺Ｅの変数の値を記述する。
・ＣＯＦ（Ｅ，ｖ）は、辺Ｅが実行された時に、オーバーフローが発生した場合に、変数ｖがとる定数値（存在する場合に）である。
・ＣＵＦ（Ｅ，ｖ）は、辺Ｅが実行された時に、アンダーフローが発生した場合に、変数ｖがとる定数値（存在する場合に）である。
・ＩＳＺ（Ｅ，ｖ）は、辺Ｅが実行され、オーバーフローおよびアンダーフローが発生しなかった時に、ｖが基礎ステートメントの変数ｚと同一の値を担持するかどうかを示すブール・フラグである。
・ＣＯＮＤ（Ｅ）は、基礎符号ビットに関する、その下で辺Ｅが実行される条件である。
【００２５】
グループとしてのＣＯＦ、ＣＵＦ、およびＩＳＺは、オーバーフロー、アンダーフロー、正常のオカレンスについて、変数ｖのどの値が、プログラム内の辺ＥのステートメントＳの変数ｚの使用に達するかを示すＲＥＡＣＨプロパティまたは条件である。これらは、飽和使用を識別するために直接に使用される。代入ステートメントまたはスイッチ・ステートメントで使用される変数ｖは、次の条件のすべてが満足される場合に、飽和値を受け取る。
・ＣＯＦ（ＩＮ（Ｓ），ｖ）＝ＳＡＴＭＡＸＢまたはＣＯＮＤ（ＩＮ（Ｓ），ＦＯＦ）＝０
・ＣＵＦ（ＩＮ（Ｓ），ｖ）＝ＳＡＴＭＩＮＢまたはＣＯＮＤ（ＩＮ（Ｓ），ＦＵＦ）＝０
・ＩＳＺ（ＩＮ（Ｓ），ｖ）＝１またはＣＯＮＤ（ＩＮ（Ｓ），ＦＮ）＝０
次のサブセクションでは、プロパティに関してデータ・フロー式を定式化し、解くのに使用されるラティスを定義する。その後、プロパティおよびソース・プログラムに関係する式を説明する。
【００２６】
ラティス
次の３つのラティスを使用する。
・ＣＯＦプロパティおよびＣＵＦプロパティは、定数伝搬（参考文献６参照）で使用されるラティスΛｃｏｎｓｔ上で定義される。Λｃｏｎｓｔ＝｛Ｔ，⊥｝∪Ｚである。
・ＩＳＺは、２値ブール・ラティスΛｂｏｏｌ＝｛０，１｝上で定義される。ミート演算子（ｍｅｅｔ  ｏｐｅｒａｔｏｒ）Πｂｏｏｌは、ブール合接である：０Πｂｏｏｌ１＝０∧１＝０。値は、０＜１によって順序付けられる。
・ＢＩＴＳプロパティおよびＣＯＮＤプロパティは、３つの変数のブール述部から形成されるラティスΛを使用する。Λは、下で詳細に説明するが、単に「ラティス」と称し、他の２つのラティスを明示的に修飾する。
近似ブール関数のラティス
【００２７】
Ｘ、Ｙ、およびＺが、それぞれ変数ｘ、ｙ、およびｚの符号ビットであるものとする。Ｆが、３つの変数Ｘ、Ｙ、およびＺのすべての可能なブール関数（述部）の集合であるものとする。０は、自明な偽の述部すなわち０（Ｘ，Ｙ，Ｚ）＝０を表す。１は、自明な真の述部すなわち１（Ｘ，Ｙ，Ｚ）＝１を表す。
近似ブール述部のラティスは、Λ＝Ｆ∪｛Ｔ，⊥｝である。Λの比較演算子＜は、すべてのＦ∈Ｆについて、⊥＜Ｆ＜Ｔと定義される。ミート演算子Πは、次のように定義される。
・すべてのＦ，Ｇ∈Ｆについて、ＦΠＧ＝⊥
・すべてのλ∈Λについて、Ｆ≠ＧλΠ⊥＝⊥かつλΠＴ＝λ
【００２８】
ブール演算子（ａｎｄ  ∧、ｏｒ  ∨、ｘｏｒ  ◎）は、ルールの優先の順序で、次のようにラティスΛの要素に拡張される（１◎Ｆ＝¬Ｆであり、ｘｏｒがビット反転を包含することを観察されたい）。
（ａ）すべてのブール演算について、Ｆ１，Ｆ２∈Ｆの場合に、λ１  ｏｐ  λ２＝Ｆ１  ｏｐ  Ｆ２
（ｂ）すべてのλ∈Λについて、１∨λ＝１かつ０∧λ＝０
（ｃ）すべてのλ∈Λおよびすべてのブール演算子について、⊥  ｏｐ  λ＝⊥かつＴ  ｏｐ  λ＝Ｔ
【００２９】
ラティス・ベクトル
ΛＢは、長さＢのラティス要素のすべてのベクトルの集合である。そのようなベクトルの要素は、０から（Ｂ−１）までの番号を付けられ、［Ｖ（Ｂ−１），Ｖ（Ｂ−２），…，Ｖ１，Ｖ０］のように、左側に要素（Ｂ−１）がある状態で表示される。（Ｂ−１）は、符号ビットの位置である。ＦＢは、長さＢのブール述部のすべてのベクトルの集合である。明らかに、ＦＢ⊆ΛＢである。
ミート演算子Πは、［ＶＢ−１，…，Ｖ０］Π［ＵＢ−１，…，Ｕ０］＝［ＶＢ−１  Π  ＵＢ−１，…，Ｖ０  Π  Ｕ０］としてベクトルに拡張される。
【００３０】
ラティス・ベクトルの評価および適用
ビットのベクトルを、ＦＢのベクトルとして扱うことが便利である。ベクトルＶ＝［ＶＢ−１，…，Ｖ０］について、関数ｅｖａｌ（Ｖ）は、述部Ｖｋのすべてが０または１のいずれかである場合に、Ｖｋから形成される整数と定義される。ベクトル要素のいずれかが０でも１でもない場合に、ｅｖａｌ（Ｖ）＝⊥である。たとえば、ｅｖａｌ（［０，１，０，１］）＝５であり、ｅｖａｌ（［Ｘ∧Ｙ，０，０，０］＝⊥である。
述部Ｖ＝［ＶＢ−１，…，Ｖ０］∈ＦＢのベクトルを与えられれば、符号ビットＸ、Ｙ、Ｚの所与の値へのＶのＶ（Ｘ，Ｙ，Ｚ）の適用は、ビットのベクトルとして定義される。
Ｖ（Ｘ，Ｙ，Ｚ）＝［ＶＢ−１（Ｘ，Ｙ，Ｚ），…，Ｖ０（Ｘ，Ｙ，Ｚ）］
【００３１】
すなわち、「ベクトルの適用」は、「適用のベクトル」である。述部Ｆへのラティス値のベクトルＶの適用は、次のように定義される。
Ｖ（Ｆ）＝Ｖ（Ｘ１，Ｙ１，Ｚ１）Π…ΠＶ（Ｘｍ，Ｙｍ，Ｚｍ）
ただし、ミート演算子Πは、すべてのＸｋ，Ｙｋ，Ｚｋについて、Ｆ（Ｘｋ，Ｙｋ，Ｚｋ）が真になるようにとられる。
【００３２】
また、ｅｖａｌの逆関数Ｖ＝ｉｅｖａｌＢ（Ｃ）は、Ｃ＝ｅｖａｌ（Ｖ）になるビットのベクトルＶ∈ＦＢと定義される。たとえば、ｉｅｖａｌ４（３）＝［０，０，１，１］およびｉｅｖａｌ４（−３）＝［１，１，０，１］である。ｉｅｖａｌ関数は、Λｃｏｎｓｔラティスに適用され、ｉｅｖａｌＢ（⊥）＝［⊥，⊥，…，⊥］、ｉｅｖａｌＢ（Ｔ）＝［Ｔ，Ｔ，…，Ｔ］である。
【００３３】
ラティス・ベクトルへの算術演算子の拡張
Ｂビット算術演算は、ラティス要素のベクトルに対する演算に拡張される。Ｕ＝［Ｕ（Ｂ−１），…，Ｕ０］およびＶ＝［Ｖ（Ｂ−１），…，Ｖ０］が、変数ｕおよびｖの値を抽象化したラティス要素の２つのベクトルであるものとする。ｗ＝ｏｐＢ（ｕ，ｖ）が、変数に対するＢビット算術演算であるものとする。結果ｗのビットは、入力ｕおよびｖのビットに基本的なブール演算のシーケンスを適用することによって計算される。演算ｏｐＢは、入力ベクトルの要素に、Λに拡張されたブール演算の同一のシーケンスを実行することによって、ΛＢに適用される。拡張された演算が、ｏｐＢである。
【００３４】
たとえば、演算が、Ｂビット加算（ＡＤＤ）である場合に、結果のベクトルの値を導出するルールは、キャリー（繰上）を用いる加算のルールを模倣したものになる。
Ｃ＝０であるものとする（これがキャリー・ビットである）
Ｆｏｒ  ｋ  ｆｒｏｍ  ０  ｔｏ  Ｂ−１：
Ｗｋ＝Ｕｋ◎Ｖｋ◎Ｃ
Ｃ＝（Ｃ∧（Ｕｋ∨Ｖｋ））∨（Ｕｋ∧Ｖｋ）
【００３５】
乗算演算について、正確なビット単位の定義は、可能ではあるが役に立たず、したがって、乗算演算の結果は、すべての底部のベクトルＷ＝［⊥，⊥，…，⊥］と定義される。
もう１つの例が、ｖ＝ＮＯＴＺＥＲＯＢ（ｕ）演算である。変数ｖのベクトルＶは、正確に１つの要素を有するＶ＝［Ｖ０］。Ｕ＝［Ｕ（Ｂ−１），…，Ｕ０）］。これらのベクトルは、次のように関係する。
Ｖ０＝Ｕ（Ｂ−１）∨Ｕ（Ｂ−２）∨  …  ∨Ｕ０
他の演算の拡張は、単純である。
【００３６】
データ・フロー・プロパティ
データ・フロー式の導出で、オーバーフロー、アンダーフロー、およびオーバーフローなしかつアンダーフローなし（「どちらもなし」）述部の次の表記が使用される。
・基礎ステートメントが加算である場合に
○ＦＯＦ＝¬Ｘ∧¬Ｙ∧Ｚ
○ＦＵＦ＝Ｘ∧Ｙ∧¬Ｚ
・基礎ステートメントが減算である場合に
○ＦＯＦ＝¬Ｘ∧Ｙ∧Ｚ
○ＦＵＦ＝Ｘ∧¬Ｙ∧¬Ｚ
・ＦＮ＝¬ＦＯＦ∧¬ＦＵＦ
【００３７】
ＢＩＴＳプロパティおよびＣＯＮＤプロパティ
定義
プログラム制御フロー・グラフのすべての辺Ｅおよびすべての変数ｖについて、ベクトル値を有するプロパティＢＩＴＳ（Ｅ，ｖ）∈ΛＢが定義される。ＢＩＴＳ（Ｅ，ｖ）＝［Ｖ（Ｂ−１），…，Ｖ０］であるものとする。このベクトル要素の値は、次のように解釈される
・Ｖｋ∈｛１，０｝の場合に、変数ｖの第ｋビットは、制御が辺Ｅを通過する時（「Ｅが実行される時」）に、必ず定数である。
・Ｖｋ＝Ｆ∈Ｆ−｛１，０｝の場合に、次が成り立つ。
○基礎ステートメントは、辺Ｅを支配する（参考文献１参照）。
○変数ｖの第ｋビットの値は、Ｅの実行に先立つ基礎ステートメントの最も最近の実行で得られた値Ｘ、Ｙ、およびＺについてＥが実行される時に、Ｆ（Ｘ，Ｙ，Ｚ）と等しい。
・Ｖｋ＝⊥の場合に、Ｘ、Ｙ、およびＺの関数としてのビットの正確な値を判定することはできない。
・Ｖｋ＝Ｔの場合に、このビットの近似の値は、まだ決定されない。この値は、データ・フロー式の反復解の中間ステージで使用されるが、最終的な解に現れない。
添字表記ＢＩＴＳ（Ｅ，ｖ）ｋは、ＢＩＴＳ（Ｅ，ｖ）プロパティの第ｋビットを表すのに使用される。
プログラム・グラフ内のすべての辺Ｅについて、定義された条件プロパティＣＯＮＤ（Ｅ）∈Λは、次のように解釈される。
・ＣＯＮＤ（Ｅ）＝Ｆ∈Ｆの場合に、次が成り立つ。
○辺Ｅは、基礎ステートメントによって支配される。
○基礎ステートメントが実行され、基礎ステートメントが実行された直後のＸ、Ｙ、およびＺの値についてＦ（Ｘ，Ｙ，Ｚ）＝１（真である）場合に、Ｅは、後の時点で実行される。
・ＣＯＮＤ（Ｅ）＝⊥の場合に、Ｅがその下で実行される条件を判定することはできない。
・ＣＯＮＤ（Ｅ）＝Ｔの場合に、Ｅがその下で実行される条件は、まだ判定されない。
ＢＩＴＳおよびＣＯＮＤの式
ＢＩＴＳプロパティおよびＣＯＮＤプロパティの式は、次のルールに従って、制御フロー・グラフから形成される。
・基礎ステートメントＳの式は、次の通りである。
○ＢＩＴＳ（ＯＵＴ（Ｓ），ｚ）＝［Ｚ，⊥，⊥，…，⊥］
○ＢＩＴＳ（ＯＵＴ（Ｓ），ｘ）＝［Ｘ，［⊥，⊥，…，⊥］
○ＢＩＴＳ（ＯＵＴ（Ｓ），ｙ）＝［Ｙ，［⊥，⊥，…，⊥］
○ＣＯＮＤ（ＯＵＴ（Ｓ））＝１
○すべてのｖ∈υ−｛ｘ，ｙ，ｚ｝について、ＢＩＴＳ（ＯＵＴ（Ｓ），ｖ）＝ＢＩＴＳ（ＩＮ（Ｓ），ｖ）である。
・エントリ・ステートメントＳの式は次の通りである。
○すべてのｖ∈υについて、ＢＩＴＳ（ＯＵＴ（Ｓ），ｖ）＝［⊥，…，⊥］である。
○ＣＯＮＤ（ＯＵＴ（Ｓ））＝⊥
・すべてのマージ・ステートメントＳについて、次のように式を形成する。Ｅ０およびＥ１が、Ｓの入る辺であるものとする。
○Ｅ０およびＥ１が、Ｓの入る辺であるものとする。
○すべての変数ｖ∈υについて、ＢＩＴＳ（ＯＵＴ（Ｓ），ｖ）＝ＢＩＴＳ（Ｅ０，ｖ）ΠＢＩＴＳ（Ｅｍ，ｖ）である。
○ＣＯＮＤ（ＯＵＴ（Ｓ））＝ＣＯＮＤ（Ｅ０）∨ＣＯＮＤ（Ｅ１）
・ＩＦＢ（ｖ）の形のすべてのスイッチ・ステートメントＳについて、次のように式を作成する。
○ＢＩＴＳ（ＩＮ（Ｓ），ｖ）＝［Ｖ（Ｂ−１），Ｖ（Ｂ−２），…，Ｖ０］であるものとする。
○Ｐ＝Ｖ（Ｂ−１）∨…∨Ｖ０であるものとする（真の分岐には、ｖが非０の時に進む）。
○ＣＯＮＤ（ＯＵＴ（Ｓ，ｔｒｕｅ））＝ＣＯＮＤ（ＩＮ（Ｓ））∧Ｐ
○ＣＯＮＤ（ＯＵＴ（Ｓ，ｆａｌｓｅ））＝ＣＯＮＤ（ＩＮ（Ｓ））∧¬Ｐ
○すべての変数ｖ∈υおよびすべてのｋ∈［０，Ｂ−１］について、
・ＢＩＴＳ（ＯＵＴ（Ｓ，ｔｒｕｅ），ｖ）ｋ＝ＢＩＴＳ（ＩＮ（Ｓ），ｖ）ｋ
・ＢＩＴＳ（ＯＵＴ（Ｓ，ｆａｌｓｅ），ｖ）ｋ＝ＢＩＴＳ（ＩＮ（Ｓ），ｖ）ｋ
・ｐ＝ＯＰ（ｑ，ｒ）(ＯＰは算術演算）の形の、基礎ステートメント以外のすべての代入ステートメントＳについて、
○ＢＩＴＳ（ＯＵＴ（Ｓ），ｐ）＝ＯＰ（ＢＩＴＳ（ＩＮ（Ｓ），ｑ），ＢＩＴＳ（ＩＮ（Ｓ），ｒ））、ただし、ＯＰは、ラティス要素のベクトルへの算術演算ＯＰの拡張を表す。
○すべてのｖ∈υ−｛ｐ｝について、ＢＩＴＳ（ＯＵＴ（Ｓ），ｖ）＝ＢＩＴＳ（ＩＮ（Ｓ），ｖ）である。
・ロードおよび呼出しを含む変数ｐへの他の代入
○ＢＩＴＳ（ＯＵＴ（Ｓ），ｐ）＝［⊥，⊥，…，⊥］
○すべてのｖ∈υ｛ｐ｝について、ＢＩＴＳ（ＯＵＴ（Ｓ),ｖ）＝ＢＩＴＳ（ＩＮ（Ｓ），ｖ）である。
ＣＯＦプロパティおよびＣＵＦプロパティ
ＣＯＦプロパティおよびＣＵＦプロパティの式は、次の通りである。
・基礎ステートメントおよびエントリ・ステートメントについて、
○すべての変数ｖ（ｘ、ｙ、およびｚを含む）について、ＣＯＦ（ＯＵＴ（Ｓ），ｖ）＝ＣＵＦ（ＯＵＴ（Ｓ），ｖ）＝⊥である。
・ｗ＝ＯＰ（ｕ，ｖ）の形の代入ステートメントＳについて、
○Ｕ＝ＢＩＴＳ（ＩＮ（Ｓ），ｕ）、Ｖ＝ＢＩＴＳ（ＩＮ（Ｓ），ｖ）であるものとする。
○ＣＯＦ＝ｅｖａｌ（ＯＰ（Ｕ（ＦＯＦ），Ｖ（ＦＯＦ）））
○ＣＵＦ＝ｅｖａｌ（ＯＰ（Ｕ（ＦＵＦ），Ｖ（ＦＵＦ）））
【００３８】
これらのルールは、次の直観的洞察を有する：入力変数のビットが担持する定数値がある場合には、それを入手することを試みる。ベクトル／述部評価式、Ｕ（ＦＯＦ）などは、それを実行する。次に、結果のビットに演算を適用し、その結果から定数が形成されるかどうかを調べる。
【００３９】
たとえば、次のコード・フラグメントを検討された（ｘが、基礎ステートメント内のオペランドの１つであり、基礎ステートメントが３２ビット加算であると仮定する）
ｔ１＝（ｘ＞＞３１）＆０ｘ１；
ｚ＝０ｘ７ｆｆｆｆｆｆｆ＋ｔ１；
ｔ１変数のＢＩＴＳ値は、ｔ１がｘの符号ビットを右にシフトさせるので、［０，０，…，０，Ｘ］である。定数のＢＩＴＳ値は、［０，１，１，…，１］である。ＣＯＦおよびＣＵＦの値は、次の通りである。
ＣＯＦ＝ｅｖａｌ（ａｄｄ３２（［０，０，…，０，Ｘ］（ＦＯＦ），［０，１，１，…，１］（ＦＯＦ）））＝
ｅｖａｌ（ａｄｄ３２（［０，０，…，０，０］，［０，１，１，…，１］））＝
ｅｖａｌ（［０，１，１，…，１］）＝０ｘ７ｆｆｆｆｆｆｆ＝ＭＡＸ３２
ＣＵＦ＝ｅｖａｌ（ａｄｄ３２（［０，０，…，０，Ｘ］（ＦＵＦ），［０，１，１，…，１］（ＦＵＦ）））＝
ｅｖａｌ（ａｄｄ３２（［０，０，…，０，１］，［０，１，１，…，１］））＝
ｅｖａｌ（［１，０，０，…，０］）＝０ｘ８０００００００＝ＭＩＮ３２
これが、［０，０，…，０，Ｘ］（ＦＯＦ）および［０，０，…，０，Ｘ］（ＦＵＦ）が計算される形である。基礎ステートメントが加算であると仮定したので、Ｘ＝Ｙ＝０かつＺ＝１の時にＦＯＦが真になる。ＦＵＦは、Ｘ＝Ｙ＝１かつＺ＝０の時に真になる。したがって、ベクトル［０，０，…，０，Ｘ］をＦＯＦに適用するために、その要素が、Ｘ＝Ｙ＝０かつＺ＝１について評価される（これらのすべてがブール関数である）。これによって、ビットの１つのベクトル［０，０，…，０，０］だけが与えられる。同様に、［０，０，…，０，Ｘ］（ＦＵＦ）＝［０，０，…，０，１］である。
【００４０】
スイッチでは、ＣＯＦおよびＣＵＦの値が、出る辺に伝搬する。マージ・ステートメントでは、式が次のように形成される。Ｅ０およびＥ１が、マージ・ステートメントＳの２つの入る辺であるものとする。
・（ＣＯＮＤ（Ｅｋ）∧ＦＯＦ）∈｛０，Ｔ｝である場合に、
ｋ＝０，１について、ＣＯＦ（ＯＵＴ（Ｓ），ｖ）＝ＣＯＦ（Ｅ１−ｋ，ｖ）であり、
そうでない場合に、ＣＯＦ（ＯＵＴ（Ｓ），ｖ）＝ＣＯＦ（Ｅ０，ｖ）ΠＣＯＦ（Ｅ１，ｖ）である。
・（ＣＯＮＤ（Ｅｋ）∧ＦＵＦ）∈｛０，Ｔ｝の場合に、
ｋ＝０，１について、ＣＵＦ（ＯＵＴ（Ｓ），ｖ）＝ＣＵＦ（Ｅ１−ｋ，ｖ），であり、
そうでない場合に、ＣＵＦ（ＯＵＴ（Ｓ），ｖ）＝ＣＵＦ（Ｅ０，ｖ）Π  ＣＵＦ（Ｅ１，ｖ）である。
これらのルールは、入る辺の１つが、オーバーフロー／アンダーフローが発生するかその状態がまだ判定されていない時に限って実行される場合に、他方の辺の値が伝搬されることを述べたものである。
【００４１】
ＩＳＺプロパティ
ＩＳＺプロパティのルールは次の通りである。
・エントリ・ステートメントＳの場合に、すべての変数ｖについてＩＳＺ（ＯＵＴ（Ｓ），ｖ）＝０である。
・基礎ステートメントＳの場合に、ＩＳＺ（ＯＵＴ（Ｓ），ｚ）＝１であり、すべての他の変数についてＩＳＺ（ＯＵＴ（Ｓ），ｖ）＝０である。
・ｗ＝ｏｐ（ｕ，ｖ）の形の他のすべての代入ステートメントＳの場合に、
○ａ＝ｅｖａｌ（ＢＩＴＳ（ＩＮ（Ｓ），ｕ）（ＦＮ））、ｂ＝ｅｖａｌ（ＢＩＴＳ（ＩＮ（Ｓ），ｖ）（ＦＮ））であるものとする。
○ａが定数であり、ｏｐ（ａ，ｖ）＝ｖの場合に、ＩＳＺ（ＯＵＴ（Ｓ），ｗ）＝ＩＳＺ（ＩＮ（Ｓ），ｖ）である。
○ｂが定数であり、ｏｐ（ｕ，ｂ）＝ｕの場合に、ＩＳＺ（ＯＵＴ（Ｓ），ｗ）＝ＩＳＺ（ＩＮ（Ｓ），ｕ）である。
○それ以外の場合に、ＩＳＺ（ＯＵＴ（Ｓ），ｗ）＝０である。
【００４２】
このルールは、代入ステートメントが、オーバーフローもアンダーフローもない条件の下でコピー演算として実際に働く場合に、ＩＳＺの値が伝搬されることを述べたものである。
・スイッチ・ステートメントＳのすべての出る辺Ｅについて、すべての変数ｖについてＩＳＺ（Ｅ，ｖ）＝ＩＳＺ（ＩＮ（Ｓ），ｖ）である。
・入る辺Ｅ０およびＥ１と出る辺Ｅを有するマージ・ステートメントＳについて、
○（ＣＯＮＤ（Ｅｋ）∧ＦＮ）∈｛０，Ｔ｝の場合に、ｋ=０，１およびすべての変数ｖについて、ＩＳＺ（Ｅ，ｖ）＝ＩＳＺ（Ｅｋ−１，ｖ）である。
○そうでない場合に、ＩＳＺ（Ｅ，ｖ）＝ＩＳＺ（Ｅ０，ｖ）∧ＩＳＺ（Ｅ１，ｖ）である（∧がＩＳＺのミート演算子であることを想起されたい）。
要約すると、変数は、コピーを介してＩＳＺプロパティを継承する。マージ・ステートメントの一方が、アンダーフローまたはオーバーフローの下でのみ実行される場合に、ＩＳＺプロパティは、反対の側から伝搬される。
【００４３】
アルゴリズム
フルワード飽和加算およびフルワード飽和減算を認識する全体的なアルゴリズムを、下にリストし、図１に示す。このアルゴリズムは、データ・フロー式を解くのに使用される技法（参考文献１、５、６、７参照）と独立である。
ＲｅｃｏｇｎｉｚｅＡｄｄｓａｔＡｎｄＳｕｂｓａｔ（ＣＦＧ  Ｇ）  ｛
Ｇのすべての加算ステートメントおよび減算ステートメントの
集合になるようにＡを初期化する
ｗｈｉｌｅ  （Ａ  ≠  φ）  ｛
Ｓ  ＝  Ａのメンバ；  Ａ  ＝  Ａ−｛Ｓ｝；
／＊  Ｓは、ｚ＝ａｄｄＢ（ｘ，ｙ）またはｚ＝ｓｕｂＢ（ｘ，ｙ）の形である  ＊／
ＢがＳのビット幅であるものとする；
Ｓの後に、ｚｓａｔ＝ａｄｄｓａｔＢ（ｘ，  ｙ）の形の
Ｓ’のステートメントを追加する
ＢＩＴＳ，  ＣＯＮＤプロパティを計算する
（すべての適用可能な技法を使用して）；
ＣＯＦ，  ＣＵＦ，  およびＩＳＺプロパティを計算する
（すべての適用可能な技法を使用して）；
ＲｅｐｌａｃｅＳａｔｕｒａｔｅｄＵｓｅｓ（Ｇ，Ｓ，Ｓ’，Ｂ）；
デッド・コード消去を実行する；
Ｒが除去されたステートメントの集合であるものとする；
Ａ＝Ａ−Ｒ；
｝
｝
ＲｅｐｌａｃｅＳａｔｕｒａｔｅｄＵｓｅｓ（ＣＦＧ  Ｇ，Ｓｔｍｔ  Ｓ，Ｓｔｍｔ  Ｓ’，ｉｎｔ  Ｂ）  ｛
Ｘ，  Ｙ，  ＺがＳの基礎符号ビットであるものとする；
ＦＯＦがオーバーフロー述部であるものとする；
ＦＵＦがアンダーフロー述部であるものとする；
ＦＮ＝¬ＦＯＦ∧¬ＦＵＦが「どちらもない」または「正常」述部であるものとする；
ＳＡＴＭＡＸＢ＝２（Ｂ−１）−１；  ＳＡＴＭＩＮＢ＝−２（Ｂ−１）であるものとする；
すべての代入ステートメントおよびスイッチ・ステートメントＨについて  ｛
Ｈで使用されるすべての変数ｖについて  ｛
Ｅ＝ＩＮ（Ｈ）であるものとする
その使用は、全ての次の条件が満足される場合に飽和する
（ａ）ＣＯＮＤ（Ｅ）∧ＦＮ＝０またはＩＳＺ（Ｅ，ｖ）＝１
（ｂ）ＣＯＮＤ（Ｅ）∧ＦＯＦ＝０またはＣＯＦ（Ｅ，ｖ）＝ＳＡＴＭＡＸＢ
（ｃ）ＣＯＮＤ（Ｅ）∧ＦＵＦ＝０またはＣＵＦ（Ｅ，ｖ）＝ＳＡＴＭＩＮＢ
使用が飽和する場合
ｖをｚｓａｔ（Ｓ’からの）に置換する
｝
｝
｝
【００４４】
実装の詳細
次に、実装の詳細を説明する。
ブール述部の表現
ブール述部を操作する効率的な形が必要である。というのは、これがこの方法の核心にあるからである。３変数のブール述部は、８ビット整数を使用して表すことができる。関数の引数の値に２３＝８つの組合せがある。この整数は、入力変数のすべての組合せについて１ビットを有する。３入力ブール関数に対するブール演算は、８ビット整数に対するビット単位の演算と同型である。
述部のベクトルの圧縮
通常、各値の単一のビットだけに関心がある。基礎ステートメントの変数ｘ、ｙ、およびｚについて、これは、上位ビット（符号ビット）である。比較の結果である変数について、これは最下位ビットである。中間値が、他の位置にシフトされた符号ビットのある組合せを担持する可能性がある。ＢＩＴＳプロパティのベクトル値を＜ｋ，λ，ｆｌａｇ＞の形の３つ組に圧縮することによって、分析をスピードアップする。ここで、
・ｋは、「関心のある」ビットの位置であり、
・λは、この位置のラティス値であり、
・ｆｌａｇは、値の他のビットが、すべて０、すべて１、すべてλ、またはそれ以外であることを示す。
データ・フロー式を、この表現に対処するように自明に変更することができる。効果的に、この表現は、ラティス値のオリジナル・ベクトルに対するロッシイ圧縮を実行するが、圧縮に起因する認識の劣化はない。
【００４５】
条件伝搬
Ｗｅｇｍａｎ−Ｚａｄｅｃｋスタイルの条件伝搬が、ＢＩＴＳプロパティおよびＣＯＮＤプロパティの計算に使用される。変更は、単純であり、参考文献７の条件伝搬アルゴリズムに類似する。マージ・ステートメントの評価中に、ミート演算子が、実行されることがわかっている入る辺に使われる。この場合に、ＣＯＮＤ（Ｅ）がＴでも０でもない辺Ｅがある。スイッチ・ステートメントの評価中にＣＯＮＤ（Ｅ）が０と評価される出る辺Ｅは、このアルゴリズムによって絶対に訪問されない。
【００４６】
入力正規化プログラム
基本的なアルゴリズムは、コピーの存在に敏感である。たとえば、ルーチンが次のように記述される場合に、
ｉｎｔ  ａｄｄｓａｔ（ｉｎｔ  ｘ，  ｉｎｔ  ｙ）  ｛
ｉｎｔ  ａ＝ｘ；
ｉｎｔ  ｂ＝ｙ；
ｉｎｔ  ｚ＝ａ＋ｂ；
ｉｆ  （ＳＡＴＭＩＮ３２  ＆（〜（ｘ＾ｙ）＆（ａ＾ｚ）））  ｛
ｚ＝ＳＡＴＭＡＸ３２＋（ｂ＞＞３１）＆  ０ｘ１；
｝
ｒｅｔｕｒｎ  ｚ；
｝
基本的なアルゴリズムは、リターン・ステートメントでの飽和使用を識別できない。というのは、基礎ステートメントが、ｚ＝ａ＋ｂであり、このコードにはａまたはｂの符号ビットへの参照がないからである。この問題は、本手法に特有ではない。一般的なサブ式消去などの他のプログラム分析問題およびプログラム最適化問題も、コピーに敏感である。
解決策は、入力プログラムを正規化するためにある形のグローバル値番号付け（参考文献８）を使用することである。
実施形態の現在の例では、グローバル値番号付けおよびコピー伝搬が使用される。依存フロー・グラフが、中間表現として使用される（参考文献３）。スカラ消去と結合されたＤＦＧ構成は、変数ａの使用と変数ｘの使用の間のある同等性も見つける。本発明の基本的な形では、式を、周知の反復技法（参考文献５、６）を使用して解くこともできる。静的単一代入（ＳＳＡ）形式ならびに依存フロー・グラフ（ＤＦＧ）（参考文献３、４）に基づく疎な方法を使用して、解の時間およびスペースの複雑さを減らすことができる。
実施例１
飽和加算の次の計算を検討されたい。
ｉｎｔ  ａｄｄｓａｔ（ｉｎｔ  ｘ，  ｉｎｔ  ｙ）  ｛
ｉｎｔ  ｚ＝ｘ＋ｙ；
ｉｆ  （ＳＡＴＭＩＮ３２  ＆  （〜（ｘ＾ｙ）＆（ｘ＾ｚ）））  ｛
ｚ＝ＳＡＴＭＡＸ３２＋（ｘ＞＞３１）  ＆  ０ｘ１；
｝
ｒｅｔｕｒｎ  ｚ；
｝
【００４７】
中間表現を図２に示す。簡潔にするために、ステートメントを基本ブロックに合体させた。プロパティの選択された値は次の通りである。
・ＢＩＴＳ（ＩＮ（Ｓ６，ｔ４））＝［¬（Ｘ◎Ｙ）∧（Ｘ◎Ｚ），⊥，⊥，…，⊥］。これは、ｔ４がａｎｄ３２（ｎｏｔ３２（ｘｏｒ３２（ｘ，ｙ）），ｘｏｒ３２（ｘ，ｚ））と等しいからである。
・ＢＩＴＳ（ＯＵＴ（Ｓ６），ｔ５）＝［¬（Ｘ◎Ｙ）∧（Ｘ◎Ｚ），０，０，…，０］。これは、このステートメントが、左端以外のすべてのビットをマスク・アウトするからである。
・Ｓ７の条件の真の側は、ｔ５≠０の時に採用される。これは、ｔ５のビットの離接すなわち¬（Ｘ◎Ｙ）∧（Ｘ◎Ｚ）と同等である。したがって、ＣＯＮＤ（Ｅ１）＝¬（Ｘ◎Ｙ）∧（Ｘ◎Ｚ）かつＣＯＮＤ（Ｅ２）＝¬ＣＯＮＤ（Ｅ１）である。
・¬（Ｘ◎Ｙ）∧（Ｘ◎Ｚ）＝ＦＯＦ∧ＦＵＦ＝¬ＦＮであり、したがってＣＯＮＤ（Ｅ１）＝¬ＦＮかつＣＯＮＤ（Ｅ２）＝ＦＮであることを観察されたい。
・ｔ７がａｎｄ３２（１，ｓｈｒａ３２（ｘ，３１））と等しいので、ＢＩＴＳ（ＩＮ（Ｓ１０），ｔ７）＝［０，０，…，０，Ｘ］である。
・ＢＩＴＳ（ＯＵＴ（Ｓ１０），ｚ）＝ａｄｄ３２（［０，０，…，Ｘ］，［０，１，１，…，１］）である。加算ルールに従えば、ＢＩＴＳ（ＯＵＴ（Ｓ１０），ｚ）＝［Ｘ，¬Ｘ，¬Ｘ，…，¬Ｘ］である。
・ＣＯＦ（ＯＵＴ（Ｓ１０），ｚ）＝
ｅｖａｌ（ａｄｄ３２（［０，０，…，０，Ｘ］（ＦＯＦ），［０，１，１，…，１］（ＦＯＦ）））＝
ｅｖａｌ（ａｄｄ３２（［０，０，…，０，０］，［０，１，１，…，１］））＝
ｅｖａｌ（［０，１，１，…，１］）＝ＳＡＴＭＡＸ３２
・ＣＵＦ（ＯＵＴ（Ｓ１０），ｚ）＝
ｅｖａｌ（ａｄｄ３２（［０，０，…，０，Ｘ］（ＦＵＦ），［０，１，１，…，１］（ＦＵＦ）））＝
ｅｖａｌ（ａｄｄ３２（［０，０，…，０，１］，［０，１，１，…，１］））＝
ｅｖａｌ（［１，０，０，…，０］）＝ＳＡＴＭＩＮ３２
・ＩＳＺ（ＯＵＴ（Ｓ１），ｚ）＝１
・ＩＳＺ（Ｅ２，ｚ）＝１
・ＣＯＮＤ（Ｅ３）∧ＦＮ＝¬ＦＮ∧ＦＮ＝０なので、ＩＳＺプロパティは、Ｅ２からＳ１１マージの出力に伝搬される。
ＩＳＺ（ＯＵＴ（Ｓ１１），ｚ）＝ＩＳＺ（ＩＮ（Ｓ１２），ｚ）＝ＩＳＺ（Ｅ２）＝１
・同様に、ＣＵＦおよびＣＯＦは、Ｅ３からマージの出力に伝搬される。したがって、リターン・ステートメントＳ１２で、
ＣＯＦ（ＩＮ（Ｓ１２），ｚ）＝ＳＡＴＭＡＸ３２
ＣＵＦ（ＩＮ（Ｓ１２），ｚ）＝ＳＡＴＭＩＮ３２
ＩＳＺ（ＩＮ（Ｓ１２），ｚ）＝１
これによって、Ｓ１２のｚの使用が飽和することが確立される。
【００４８】
実施例２
下の関数の分析から、ＩＳＺプロパティの伝搬が示される。
ｉｎｔ  ａｄｄｓａｔ＿５（ｉｎｔ  ｘ，  ｉｎｔ  ｙ）  ｛
ｉｎｔ  ｚ＝ｘ＋ｙ；
ｉｎｔ  ＯＦ＝（〜ｘ  ＆  〜ｙ  ＆  ｚ）  ＞＞  ３１；
ｉｎｔ  ＵＦ＝（ｘ  ＆  ｙ  ＆  〜ｚ）  ＞＞  ３１；
ｉｎｔ  Ｎ＝〜（ＯＦ  ｜  ＵＦ）；
ｒｅｔｕｒｎ  （ＳＡＴＭＡＸ３２  ＆  ＯＦ）  ｜  （ＳＡＴＭＩＮ３２  ＆  ＵＦ）  ｜  （ｚ  ＆  Ｎ）；
｝
次が、式の一部が展開されていない中間表現である。
Ｓ１：ｚ＝ａｄｄ３２（ｘ，ｙ）
Ｓ２：ＯＦ＝ｓｈｒａ３２（ａｎｄ３２（ｎｏｔｘ），ａｎｄ３２（ｎｏｔ（ｙ），ｚ）），３１）
Ｓ３：ＵＦ＝ｓｈｒａ３２（ａｎｄ３２（ｘ，ａｎｄ３２（ｙ，ｎｏｔ（ｚ））），３１）
Ｓ４：Ｎ＝ｎｏｔ３２（ｏｒ３２（ＯＦ，ＵＦ））
Ｓ５：ｔ１＝ａｎｄ３２（ＯＦ，０ｘ７ｆｆｆｆｆｆｆ）
Ｓ６：ｔ２＝ａｎｄ３２（ＵＦ，０ｘ８０００００００）
Ｓ７：ｔ３＝ａｎｄ３２（Ｎ，ｚ）
Ｓ８：ｔ４＝ｏｒ３２（ｔ１，ｏｒ３２（ｔ２，ｔ３））
Ｓ９：ｒｅｔｕｒｎｔ４
下は、プロパティの一部の解である。わかりやすくするために、すべての変数が正確に１回だけ定義されているので、辺指定をプロパティから削除した。
・ＢＩＴＳ（ＯＦ）＝［ＦＯＦ，ＦＯＦ，…，ＦＯＦ］，
ＢＩＴＳ（ＵＦ）＝［ＦＵＦ，ＦＵＦ，…，ＦＵＦ］，
ＢＩＴＳ（Ｎ）＝［ＦＮ，ＦＮ，…，ＦＮ］，
ＢＩＴＳ（ｚ）＝［Ｚ，⊥，⊥，…，⊥］
・一方で、ＦＵＦおよびＦＯＦが、他方でＦＮが、相互に排他的なので、ＢＩＴＳ（ＯＦ）（ＦＮ）＝［０，０，…，０］＝ＢＩＴＳ（ＵＦ）（ＦＮ）であることを観察されたい。
・ＩＳＺ（ｚ）＝１
・ｅｖａｌ（ＢＩＴＳ（Ｎ）（ＦＮ））＝０ｘｆｆｆｆｆｆｆｆであり、したがって、Ｓ７のａｎｄ３２演算は、オーバーフローおよびアンダーフローが発生していない時にｔ３へのｚのコピーとして働き、ＩＳＺ（ｔ３）＝１である。
・ＢＩＴＳ（ｔ１）＝［０，ＦＯＦ，ＦＯＦ，…，ＦＯＦ］，
ＢＩＴＳ（ｔ２）＝［ＦＵＦ，０，０，…，０］
・ｅｖａｌ（ＢＩＴＳ（ｔ１）（ＦＮ））＝０かつｅｖａｌ（ＢＩＴＳ（ｔ２）（ＦＮ））＝０である。したがって、Ｓ８の２つのｏｒ３２演算は、オーバーフローおよびアンダーフローが発生してない時にｔ３の値をｔ４にコピーするだけであり、ＩＳＺ（ｔ４）＝１である。
・いくつかのＣＯＦの値は次の通りである。
ＣＯＦ（ｔ１）＝ｅｖａｌ（ａｎｄ３２（ＢＩＴＳ（ＯＦ）（ＦＯＦ），［０，１，１，…，１］（ＦＯＦ）））＝
ｅｖａｌ（ａｎｄ３２（［１，１，…，１］，［０，１，１，…，１］））＝
ｅｖａｌ（［０，１，１，…，１］）＝ＳＡＴＭＡＸ３２
ＣＯＦ（ｔ２）＝ｅｖａｌ（ａｎｄ３２（ＢＩＴＳ（ＵＦ）（ＦＯＦ），［１，０，０，…，０］（ＦＯＦ）））＝
ｅｖａｌ（ａｎｄ３２（［０，０，…，０］，［１，０，０，…，０］））＝
ｅｖａｌ（［０，０，…，０］）＝０
ＣＯＦ（ｔ３）＝ｅｖａｌ（ａｎｄ３２（ＢＩＴＳ（Ｎ）（ＦＯＦ），［Ｚ，⊥，⊥，…，⊥］））＝
ｅｖａｌ（ａｎｄ３２（［０，０，…，０］，［Ｚ，⊥，⊥，…，⊥］））＝
ｅｖａｌ（［０，０，…，０］）＝０
・略式には、ＣＯＦ（ｔ４）＝ｏｒ３２（ＭＡＸ３２，０，０）＝ＭＡＸ３２である。
・いくつかのＣＵＦの値は次の通りである。
ＣＵＦ（ｔ１）＝ｅｖａｌ（ａｎｄ３２（ＢＩＴＳ（ＯＦ）（ＦＵＦ），［０，１，１，…，１］（ＦＵＦ）））＝
ｅｖａｌ（ａｎｄ３２（［０，０，…，０］，［０，１，１，…，１］））＝０
ＣＵＦ（ｔ２）＝ｅｖａｌ（ａｎｄ３２（ＢＩＴＳ（ＵＦ）（ＦＵＦ），［１，０，０，…，０］（ＦＵＦ）））＝
ｅｖａｌ（ａｎｄ３２（［１，１，…，１］，［１，０，０，…，０］））＝
ｅｖａｌ（［１，０，…，０］）＝ＳＡＴＭＩＮ３２
ＣＵＦ（ｔ３）＝ｅｖａｌ（ａｎｄ３２（ＢＩＴＳ（Ｎ）（ＦＵＦ），［Ｚ，⊥，⊥，…，⊥］））＝
ｅｖａｌ（ａｎｄ３２（［０，０，…，０］，［Ｚ，⊥，⊥，…，⊥］））＝
ｅｖａｌ（［０，０，…，０］）＝０
・略式には、ＣＵＦ（ｔ４）＝ｏｒ３２（０，ＳＡＴＭＩＮ３２，０）＝ＳＡＴＭＩＮ３２であり、ＣＵＦ（ｔ４）＝ＳＡＴＭＩＮ３２，ＣＯＦ（ｔ４）＝ＳＡＴＭＡＸ３２およびＩＳＺ（ｔ４）＝１である、したがって、ｔ４は、飽和した値を担持する。
【００４９】
本発明を、詳細に説明し、図示したが、これが、例としてのみ行われたものであり、制限として解釈されてはならないことを理解されたい。本発明の趣旨および範囲は、請求項の言葉だけによって制限される。
【００５０】
参考文献
[１］  Ａｌｆｒｅｄ  Ｖ．  Ａｈｏ，  Ｒａｖｉ  Ｓｅｔｈｉ，  Ｊｅｆｆｒｅｙ  Ｄ．  Ｕｌｌｍａｎ，  ”Ｃｏｍｐｉｌｅｒｓ，  ｐｒｉｎｃｉｐｌｅｓ，  ｔｅｃｈｎｉｑｕｅｓ，  ａｎｄ  ｔｏｏｌｓ”，  Ａｄｄｉｓｏｎ−Ｗｅｓｌｅｙ，  １９８８
［２］  Ｈａｎｓ  Ｚｉｍａ，  Ｂａｒｂａｒａ  Ｃｈａｐｍａｎ，  ”Ｓｕｐｅｒｃｏｍｐｉｌｅｒｓ  ｆｏｒ  Ｐａｒａｌｌｅｌ  ａｎｄ  Ｖｅｃｔｏｒ  Ｃｏｍｐｕｔｅｓ”，  ＡＣＭ  Ｐｒｅｓｓ，  １９９１
［３］  Ｒｉｃｈａｒｄ  Ｊｏｈｎｓｏｎ，  Ｋｅｓｈａｖ  Ｐｉｎｇａｌｉ，  ”Ｄｅｐｅｎｄｅｎｃｅ  Ｂａｓｅｄ  Ｐｒｏｇｒａｍ  Ａｎａｌｙｓｉｓ”，  Ｉｎ  ｔｈｅ  Ｐｒｏｃｅｅｄｉｎｇｓ  ｏｆ  ｔｈｅ  ＡＣＭ  ＳＩＧＰＬＡＮ  １９９３  Ｃｏｎｆｅｒｅｎｃｅ  ｏｆ  Ｐｒｏｇｒａｍｍｉｎｇ  Ｌａｎｇｕａｇｅ  Ｄｅｓｉｇｎ  ａｎｄ  Ｉｍｐｌｅｍｅｎｔａｔｉｏｎ  （ＰＬＤＩ）．
［４］  Ｒｏｎ  Ｃｙｔｒｏｎ  ｅｔ  ａｌ，  ”Ａｎ  ｅｆｆｉｃｉｅｎｔ  ｍｅｔｈｏｄ  ｆｏｒ  ｃｏｍｐｕｔｉｎｇ  ｓｔａｔｉｃ  ｓｉｎｇｌｅ  ａｓｓｉｇｎｍｅｎｔ  ｆｏｒｍ”，  Ｉｎ  Ｃｏｎｆｅｒｅｎｃｅ  Ｒｅｃｏｒｄ  ｏｆ  ｔｈｅ  １６ｔｈ  Ａｎｎｕａｌ  ＡＣＭ  Ｓｙｍｐｏｓｉｕｍ  ｏｎ  Ｐｒｉｎｃｉｐｌｅｓ  ｏｆ  Ｐｒｏｇｒａｍｍｉｎｇ  Ｌａｎｇｕａｇｅｓ．
［５］  Ｐａｒｔｉｃ  Ｃｏｕｓｏｔ，  Ｒａｄｈｉａ  Ｃｏｕｓｏｔ，  ”Ａｕｔｏｍａｔｉｃ  Ｓｙｎｔｈｅｓｉｓ  ｏｆ  Ｏｐｔｉｍａｌ  Ｉｎｖａｒｉａｎｔ  Ａｓｓｅｒｔｉｏｎｓ：  Ｍａｔｈｅｍａｔｉｃａｌ  Ｆｏｕｎｄａｔｉｏｎｓ”，  Ｉｎ  ｔｈｅ  Ｐｒｏｃｅｅｄｉｎｇｓ  ｏｆ  ｔｈｅ  Ｓｙｍｐｏｓｉｕｍ  ｏｎ  Ａｒｔｉｆｉｃｉａｌ  Ｉｎｔｅｌｌｉｇｅｎｃｅ  ａｎｄ  Ｐｒｏｇｒａｍｍｉｎｇ  Ｌａｎｇｕａｇｅｓ，  １９７７．
［６］  Ｇａｒｙ  Ｋｉｌｄａｌｌ，  ”Ａ  Ｕｎｉｆｉｅｄ  Ａｐｐｒｏａｃｈ  ｔｏ  Ｇｌｏｂａｌ  Ｐｒｏｇｒａｍ  Ｏｐｔｉｍｉｚａｔｉｏｎ”，  Ｉｎ  ｔｈｅ  Ｐｒｏｃｅｅｄｉｎｇｓ  ｏｆ  ｔｈｅ  １９７３  Ｓｙｍｐｏｓｉｕｍ  ｏｎ  Ｐｒｉｎｃｉｐｌｅｓ  ｏｆ  Ｐｒｏｇｒａｍｍｉｎｇ  Ｌａｎｇｕａｇｅｓ．
［７］  Ｍａｒｋ  Ｗｅｇｍａｎ，  Ｆ．  Ｋｅｎｎｅｔｈ  Ｚａｄｅｃｋ，  ”Ｃｏｎｓｔａｎｔ  Ｐｒｏｐａｇａｔｉｏｎ  ｗｉｔｈ  Ｃｏｎｄｉｔｉｏｎａｌ  Ｂｒａｎｃｈｅｓ”，  Ｉｎ  ＡＣＭ  Ｔｒａｎｓａｃｔｉｏｎ  ｏｎ  Ｐｒｏｇｒａｍｍｉｎｇ  Ｌａｎｇｕａｇｅｓ  ａｎｄ  Ｓｙｓｔｅｍ，  ｖｏｌ．  １３，  Ｎｏ．  ２，  Ａｐｒｉｌ  １９９１，  ｐｐ．  １８１−２１０．
【図面の簡単な説明】
【００５１】
【図１】本発明の原理を組み込んだ方法を示す流れ図である。
【図２】本発明の原理を使用する実施例の加算演算を示す制御フロー・グラフである。
【図１】
2007528073.tif 000007
【図２】
2007528073.tif 000008
【国際調査報告】
2007528073.tif 000009
2007528073.tif 000010
2007528073.tif 000011