プログラムの動的性質の静的決定(STATIC DETERMINATION OF DYNAMIC PROPERTIES OF PROGRAM)　

Patrick. Cousot and Radhia Cousot :グルノーブル理科医科大学情報研究所(Laboratoire d'Informatique, Universite Scientifique et Medicale de Grenoble)　: 2nd Int. Symposium on Programming, Paris [1976年]

　　　　　　　　　　　　　　　　　　　　　　　　　　　２０１４年１月　日本語訳と解説作成：舟越　和己

１．序論(Introduction)

　高級言語において、コンパイル時の型検証は完全ではなく、動的なチェックが対象のコードに行われなければならない。例えば、PASCALではサブレンジタイプの変数や添字式に代入された値が２つのバウンダリ間にあることや、ポインターがnullでないことを動的に検証しなければならない。

　この論文では、これらの証明の多くをコンパイル時に行うことを可能にする一般的なアルゴリズムを提示する。我々が行うプログラムの静的解析はプログラムの抽象評価から成り、それはALGOL60の式の型を検証するためにNAUR（訳注１）により使用された方法、モジュールとその論理仕様の対応を検証するためにSINTZOFF（訳注２）により使用された方法、プログラムの性質を抽出するためにWEGBREIT（訳注３）により使用された方法、プログラムの変数間のアフィン関係を見つけるためにKARR（訳注４）により使用された方法、及びSETL（訳注５）での自動データ構造選択のためにSCHWARTZ（訳注６）により使用された方法に類似している。

　　（訳注１）Peter Naur(1928-)はデンマークの計算機科学者であり、チューリング賞受賞者。

　　　　　　　バッカス・ナウア記法（BNF notation：Backus-Naur form)に名前が使われている。

　　（訳注２）Michel Sintzoff (12 Aug 1938 - Nov 28, 2010)はベルギーの数学者でコンピュータ科学者。

　　（訳注３）Ben Wegbrite：ACM Programming Systems and Languages Paper Award in 1974.

　　（訳注４）Michael Karr：Affine relationships between variables of a program, Acta Informatica (1976)

　　　　　　　という論文の著者として抽象解釈では知られている。

　　（訳注５）SETL (SET Language)は集合の数学的理論に基づいた高級言語。1960年代終りに

　　　　　　　J. T. Schwartzにより開発された。

　　（訳注６）Jacob T. Schwartz (1930– 2009)はアメリカの数学者、計算機科学者。プログラミング言語

　　　　　　　SETLの設計者。

　その本質的な概念は、プログラムの抽象評価を行うとき、「抽象」値は実際にプログラムの実行で使用される「具体」値に代わる変数に関係づけられるということである。（代入、分岐、ループ処理などの）言語の基本操作は解釈され、その時、抽象解釈（の本質）は推移閉包（Transitive closure）（訳注１）の機構にある。有限でない集合に属する抽象値を考えてもよいが、推移閉包アルゴリズムの特性は抽象解釈が有限のステップの後に安定するように選ばれる。これはコンパイルで完全に解決できることを意味する。言語の基本操作の初等的解釈と抽象値の選択はプログラムから抽出したい特定の動的性質に依存する。抽象値と基本操作の選択がこの論文で規定した一般的なフレームワークを満たすということを示すことにより、抽象評価アルゴリズムの正しさと終了が保証される。単純化の目的のために、我々はPASCALやLIS（訳注２）のような高級言語の整数変数に結び付けて範囲の情報を決定することにより、この手法を図示する。

　　（訳注１）推移閉包とは、集合 Xにおける二項関係 Rに対して、Rを含む X上の最小の推移

　　　　　　関係を意味する。例えば、A={a,b,c,d}のとき、RがA上の関係であり、R={(a,b),(b,c),(d,d)}

　　　　　　であるとすると、Rは推移律が成り立たない。(a,b)∈Rかつ(b,c)∈R⇒(a,c)∈Rが成り立た

　　　　　　ないから。推移律が成り立つように要素を加えた最小の関係が推移閉包。

　　　　　　これをR'で表すとR'={(a,b),(b,c),(a,c),(d,d)}

　　（訳注２）LIs：LISt Processor (リスト処理言語)のことか。

２．抽象値(Abstract Values)

　プログラムの抽象評価は、具体的または実行値の代わりに抽象値を使用する、プログラムの「シンボリック」解釈である。抽象値は、いくつかの動的条件を満たす具体値の集合やそのような集合の性質を示す。Vcを具体値の集合、Vaを抽象値の集合とする。

　この論文で与えられる多くの例では、Vcは整数の集合であり、Vaは整数の区間の集合である。もし、Vc=Z^-（-∞,+∞を含む整数の集合）とすると、整数の区間は[a, b]　(a, b∈Z^-, a≦b)で表される。

　具体値と抽象値の集合間の対応は「抽象化関数」αにより確立される：

　　　　　　　　　

　　（上記の表現で、2^VcはVcのベキ集合を意味する）

例： S⊆Z^-とするとき、α(S)=[MIN(S), MAX(S)]

　　　例えば、α({-1, 5, 3})=[-1,5],α({3, 4, 5,・・・})=[3, +∞]

もう一つの関数γは抽象値から具体値を与える：

　　　　　　　　　　

例：　γ([a, b])={ x | x∈Z^-かつa≦x≦b }

　　　例えば、γ([-1, 5])={-1, 0, 1, 2, 3, 4, 5}

関数α、γは下記を満たすように定義される（ガロア挿入）：

　　任意のs∈2^Vcに対して、s⊆γ(α(s))

　　任意のv∈Vaに対して、v=α(γ(v))

　（整数の集合である）具体値の集合の和∪に対応して、（整数の区間の集合である）抽象値の和∪^〜が抽象評価のために定義されなければならない：

　　　　　　　　

例：　[a₁, b₁]∪^〜[a₂, b₂] = [min(a₁, a₂), max(b₁, b₂)]

【訳での補足】簡単な例を下記に示す；

　　具体値の集合をA={-1, 5, 3}, B={0, 2, 6}とすると、α(A)=[-1, 5],α(B)=[0, 6]

　このとき、具体値の集合A, Bの和A∪B={-1, 0, 2, 3, 5, 6}

　　　　　　　 抽象値α(A),α(B)の和α(A)∪^〜α(B)=[-1, 6]

　　となる。このときα(A∪B)=[-1, 6]なので、

　　　　　　　　　α(A∪B)=α(A)∪^〜α(B)

　　が成立する。

（そこで）抽象関数αは（2^Vc,∪)から（Va,∪^〜)へのmorphism（ここでは、和の構造を保存する写像）であると仮定する。すなわち、

　　　任意の(s₁, s₂)⊆Vc×Vc=Vc²に対して、α（s₁∪s₂)=α（s₁）∪^〜α（s₂)

これは∪^〜が結合的、交換的、冪等的（訳注）性質を持つことを意味している。また、抽象値のnullを□で表すと、α（φ）=□である（φは具体値の世界の空集合）。

　　（訳注）二項演算 "*"を備えた集合 Sについて、Sの元 sはs * s = s

　　　　　を満たすとき（"*"に関して）冪等（idempotent）であるという。

　具体値の集合の包含⊆に関し、抽象評価は下記で定義される抽象値の包含≦^〜を使用する（訳注）：

任意の(v₁, v₂)⊆Va×Va=Va²に対して、

　　　　　　v₁≦^〜v₂を v₁∪^〜v₂=v₂

　　　　　　v₁＜^〜v₂　を {(v₁≦^〜v₂)かつ(v₁≠v₂)}

により定義する。

　　（訳注）抽象値の包含≦^〜が抽象値の和∪^〜により定義されていることに注目。

　この定義と∪^〜についての仮定から、≦^〜は半順序であることを示すことができ、□は全ての抽象値に含まれる。

例：　[a₁, b₁]≦^〜 [a₂, b₂]⇔　[a₁, b₁]∪^〜[a₂, b₂] = [min(a₁, a₂), max(b₁, b₂)] =[a₂, b₂]

　　　　　　　　　　　　　　　　　　　　　⇔ {(a₂≦a₁)かつ(b₂≧b₁)}

　≦^〜は半順序の性質（反射的、推移的、逆対称的）を満たす。一方、Vaは任意のv₁, v₂, v₃∈Vaに対して下記が成立するのでVa=(Va,∪^〜)は半束(semi-lattice)（訳注）である。；

　　　　　　(i) v₁∪^〜v₁=v₁

　　　　　　　(ii) v₁∪^〜v₂= v₂∪^〜v₁

　　　　　　　(iii) v₁∪^〜(v₂∪^〜v₃)= (v₁∪^〜v₂)∪^〜v₃

　　（訳注）半束の定義および性質は「Cousot初期論文を読む」の２．２．２項を参照。

このとき、順序v₁≦^〜v₂が v₁∪^〜v₂=v₂により定義されているので、単調増大列に対して完備な半束となる。

例：狭義の増加（注）無限鎖：　□, [1, 1], [1, 2], [1, 3],・・・　は上限[1,∞]を持つ。　

　　（注）狭義の増加とは等号を含まない真の増加のこと。広義の増加は等号を含む。

【訳での補足】抽象値の集合Vaに対して、「抽象値の和∪^〜」から「抽象値の包含≦^〜」が定義され、

　Vaが半順序≦^〜の下で完備な半束となる。

　→この完備な半束は「∪^〜」をベースとして構成されたので、「完備∪^〜−半束」と呼ぶ。

　この節の最後に、ループの抽象評価にために、有限のステップで狭義に増加する無限鎖の極限を計算するという問題を考える。この目的のために、wideningと呼ばれる演算∇^〜が定義される：

　　　　　　　　　　　

∇^〜は次の２つの条件を満たすときwidening演算子という：

− ∇^〜は上界演算子である；

　　すなわち、任意の(v₁, v₂)⊆Va²に対して、(v₁∪^〜v₂)≦^〜(v₁∇^〜v₂)

− 単調増大する鎖v₁, v₂,・・・, v_n,・・・ に対して、

　　　　　　　　　　　s₀=v₁, s₁=s₀∇^〜v₁, s₂=s₁∇^〜v₂,・・・,s_n=s_n-1∇^〜v_n, ,・・・

　 は狭義の単調増大鎖ではない（すなわち、有限回で増大が止まる）。

例：widening演算子の例

　　　[a₁, b₁]∇^〜 [a₂, b₂] = [ if a₂<a₁ならば−∞,そうでないならばa₁,

　　　　　　　　　　　　　　　　　　　　　　　　　　if b₂>b₁ならば+∞,そうでないならばb₁"

　　　例えば、狭義の増加無限鎖：　□, [1, 10], [1, 11], [0, 12], [-1, 13]・・・に対して

　　　 s₁=□∇^〜[1, 10]=[1, 10], s₂=[1,10]∇^〜[1, 11]=[1, +∞], s₃=[1, +∞]∇^〜[0, 12]=[-∞, +∞],

　　　　s₄=[-∞, +∞]∇^〜[-1, 13]=[-∞, +∞]

　　　この場合、s_nが狭義の単調増加となるのはn=4以下である。

３．抽象コンテキスト(Abstract contexts)

　プログラムの抽象評価は全てのプログラムポイントで近似により抽象コンテキストを計算する。プログラムポイントr_k(k=0, 1, 2,・・m)での抽象コンテキストは(i, v(r_k))というペアの集合である。ここで、(i, v(r_k))は識別子i（注）が、プログラムポイントr_kで抽象値v(r_k)を持つことを表し、抽象コンテキストの要素は識別子iで区別されるものとする（→この意味は、例えば抽象コンテキストCの要素が(i,v)ならば、同じ識別子iを持つ要素(i, v')は別の抽象コンテキストC'の要素であるか、またはv=v'でなければならない）。

　（注）識別子(identifier)とは、変数、手続き、関数の名前である。識別子でアクセスされる対象を

　　　　オブジェクトという。

　このとき、プログラムの全ての実際の実行において、iでアクセスされるオブジェクトはそのプログラムポイントでγ(v)内に値がある。

【訳での補足】

「抽象コンテキストは(i, v)というペアの集合である。ここで、(i, v)は識別子i（注）が、あるプログラムポイントで抽象値vを持つことを表す。」とは、下記のプログラムではどうなるかを示す；

　　　　　

このプログラムの識別子：x　、プログラムポイント：r₀, r₁,・・・, r₆

　　プログラムポイントr₁での抽象コンテキストC_r1=(x, [0, 0])

　　プログラムポイントr₂での抽象コンテキストC_r2,1=(x, [0, 1]), C_r2,2= (x, [0,2]),・・・など複数がある

　　（ループ回数に依存する）。→このとき、具体値はγ([0,1])={0,1},γ({0, 2])={0, 1, 2}内に存在する。

　　プログラムポイントr₃についても同様。

Iを識別子の集合とすると、抽象コンテキストの集合Cは

　　　　　　　　I×(Va-{□})={ (i, v) | i∈I, v∈(Va-{□}) }の全ての部分集合（=ベキ集合）に含まれる。

但し、Va：抽象値の集合,□：抽象値のnull。

また、与えられた抽象コンテキストのペアはそれらの識別子で区別される：

すなわち、任意のi, j∈Iと任意のv, u∈(Va-{□})に対して、

　(i, v), (j, u)∈Cかつ(i, v)≠(j, u)ならばi≠jである。

抽象コンテキストC∈Cにおける識別子iの値をC(i)とする。これは下記で定義できる；

　C(i)={ if ( (i, v)∈Cとなるv∈(Va-{□})が存在する ) then v else□ }

（例）　C={ (x, [1, 10]), (y, [-∞, 0]) }とすると、

　　　　C(x)=[1, 10], C(z)=□

特に、null抽象コンテキストをφで表す。上記の定義から、任意のi∈Iに対してφ(i)=□である。

２つの抽象コンテキストC, C'の和C∪⁼C'は条件文(conditional statements)から生じるコンテキストを表現するために使用され、２つの抽象コンテキストのwidening C∇⁼C'はループで使用される。これらは下記で定義される；

C₁∪⁼C₂={(i, v) | i∈Iかつv∈(Va-{□})かつv=C₁(i)∪^〜C₂(i) }

C₁∇⁼C₂={(i, v) | i∈Iかつv∈(Va-{□})かつv=C₁(i)∇^〜C₂(i) }

これらについては下記の式が成り立つ；

(C₁∪⁼C₂)(i)= C₁(i)∪^〜C₂(i)

(C₁∇⁼C₂)(i)= C₁(i)∇^〜C₂(i)

（例１）C₁={ (x, [1, 10]), (y, [-∞, 0]) }, C₂={ (x, [0, 5]), (z, [1, +∞]) }とすると、

　　　C₁(x)=[1,10], C₂(x)=[0, 5], C₁(y)=[-∞,0], C₂(z)=[1, +∞]であり、

　　　C₁(x)∪^〜C₂(x)=[1, 10]∪^〜[0, 5]=[0, 10]なので、

　　　C₁∪⁼C₂= C₂∪⁼C₁={ (x, [0, 10]), (y, [-∞, 0]), (z, [1, +∞]) }

　　　また、C₁(x)∇^〜C₂(x)=[1,10]∇^〜[0, 5]=[ -∞, 10], C₂(x)∇^〜C₁(x)= [0,5]∇^〜[1, 10]=[0, +∞]

　　　C₁(y)∇^〜C₂(y)= [-∞,0]∇^〜□=[-∞,0], C₁(z)∇^〜C₂(z)=□∇^〜[1, +∞]= [1, +∞]なので

　　　C₁∇⁼C₂={ (x, [-∞, 10]), (y, [-∞, 0]), (z, [1, +∞]) }

　　　C₂∇⁼C₁={ (x, [0, +∞]), (y, [-∞, 0]), (z, [1, +∞]) }

（例２）前の頁の補足のプログラム例では、C_r2,1=(x, [0, 1]), C_r2,2= (x, [0,2])なので、

　　　C_r2,1(x)∪⁼C_r2,2(x)= C_r2,2(x)∪⁼C_r2,1(x)=[0, 1]∪^〜[0, 2]=[0, 2]= C_r2,2(x)

以前と同様に、コンテキストの包含≦⁼を下記で定義する；

　　　　　C₁≦⁼C₂⇔C₁∪⁼C₂=C₂ , C₁＜⁼C₂⇔C₁≦⁼C₂かつC₁≠C₂

これは下記と同等である；

　　C₁≦⁼C₂⇔任意のi∈Iに対して、C₁(i)≦⁼C₂(i)

　（例）前の頁の補足のプログラム例では、C_r2,1(x)∪⁼C_r2,2(x)= C_r2,2(x)なので、C_r2,1≦⁼C_r2,2

Cは半順序≦⁼の下で完備∪⁼半束である。

さらに、任意のC₁, C₂に対して、

　　　　　　　　　　C₁∪⁼C₂≦⁼C₁∇⁼C₂

であり、任意の抽象コンテキストC₁, C₂,・・・, C_n,・・・に対してwidening演算子による列

　　　　　　　　　　S₀=φ, S₁=S₀∇⁼C₁,S₂=S₁∇⁼C₂,・・・・,S_n=S_n-1∇⁼C_n,・・・・

は有限で安定する単調増加列となる（訳注）。

　（訳注）widening演算子の性質において単調関数fとしてf(X)=Xを考えればよい。

４．プログラム

　プログラムの最初の近似として、有限のフローチャートを使用する。フローチャートは以下の基本的なプログラムユニットから組み立てられる：

単一の入口ノード ：

出口ノード　　　　　：

代入ノード　　　　　：

テストノード　　　　　：

　　　　　　　　　　　　　

（特定のプログラミング言語の選択を避けるために、代入やテストの式の評価は副作用がないとする）

単純な接合ノード：

　　　　　　　　　　　　　　　

ループ接合ノード：

　　　　　　　　　　　　　　

ここでは接続されたフローチャートのみを考え、唯一の入口ノードかたフローチャートの全てのノードへ少なくとも一つのパスが存在するとする。これらの条件と共に、フローチャートの全てのサイクルは少なくとも一つの単純またはループの接合ノードを含んでいるとする。さらに、フローチャートの初期のグラフ理論解析が行われ、全てのサイクルは少なくとも一つのループ接合ノードを含み、ループ接合ノードは最小になっているとする。

例：

　　　　　　

５．基本プログラムユニットの初等的抽象解釈

　抽象評価アルゴリズムの適用のために、基本プログラムユニットの評価の定義を提供しなければならない。任意の代入またはテストプログラムユニットnと入力抽象コンテキストCに対し、出力抽象コンテキストT₋(n, C)を以降で定義する。T₋はプログラムユニットnの実行の正しい「抽象」でなければならない。

５．１　代入ノードの初等的抽象解釈T₋(n, C)

　Naを代入ノードの集合とする。任意のn∈Naに対して、代入ノードnは下記の形式で表現される：

　　　　　

ここで、v, v₁,・・・,v_mは識別子（変数）であり、f(v₁,・・・,v_m)は変数v₁,・・・,v_mに言語依存する式である。

このとき、任意の入力抽象コンテキストC∈Cと任意のi∈Iに対して、T₋(n, C)を

　　・ i≠vならば、T₋(n, C)(i)=C(i)　・・・�@

　　・ i=vならば、T₋(n, C)(v)=α({f(μ₁,・・・,μ_m) |μ₁∈γ(C(v₁)),・・・,μ_m∈γ(C(v_m))})・・・�A

により定義する。最初の条件式�@はf(v₁,・・・,v_m)によるvの値がT₋(n, C)(i)に影響を与えないことを示し、

二番目の条件式�Aは、入力抽象コンテキストCによるv₁,・・・,v_mの抽象値C(v₁),・・・,C(v_m)を具体化関数γで戻したγ(C(v₁)),・・・,γ(C(v_m))に属する具体値をμ₁,・・・,μ_mとするとき、式f(μ₁,・・・,μ_m)の値の抽象化α({f(μ₁,・・・,μ_m) |μ₁∈γ(C(v₁)),・・・,μ_m∈γ(C(v_m))})が出力抽象コンテキストのvでの値

T₋(n, C)(v)であることを示している。

（例１）前の頁の補足のプログラム例では、代入ノードの式は

　　　　　　　　　　　　　x:=f(x)=x+1

　　　である。入力コンテキストをC_r3,1=(x, [0, 1])とすると、

　　　T₋(n, C)(x)=α( {f(μ) |μ∈γ(C(x)) } ]=α[ {f(μ) |μ∈γ([0, 1]) } )

　　　　　　　　　　　　=α( {f(μ) |μ=0, 1} )=α( {x:=μ+1 |μ=0, 1} )=α({x=1, 2})=[1, 2]

（例２）下記の図は、

　　　　　入力コンテキスト：C=φ（空集合）、代入ノードの式：　x:=10

　　　　とするとき、T₋(n, C)={ (x, [10, 10]) }となることを示している。

　　　　　　　　　

　　　解説：T₋(n, C)(x)=α( {f(μ) |μ∈γ(C(x)) } )=α( {x:=10 |μ∈γ(undefined) } )

　　　　　　　=α(x:=10)=[10, 10]　　したがって、T₋(n, C)={ (x, [10, 10]) }

（例３）下の図は、

　　　　入力コンテキスト：C={ (x, [1, 10] ), (y, [-2, 3] ) }、代入ノードの式：　x:=x+y+1

　　　　とするとき、T₋(n, C)={ (x, [0, 14] ), (y, [-2, 3] ) }となることを示している。

　　　　　　

　　　　　解説：T₋(n, C)(x)=α({f(μ₁,μ₂) |μ₁∈γ(C(x)), μ₂∈γ(C(y)) } )

　　　　　　　　　　　　　　=α({x:=μ₁+μ₂+1 |μ₁∈γ( [1, 10]), μ₂∈γ( [-2, 3]) } )

　　　　　　　　　　　　　　=α({x:=μ₁+μ₂+1 |μ₁=1,2,・・・,10μ₂=-2,-1,0,1,2,3 } )

　　　　　　　　　　　　　　=α( x:=0,1,2,3,4,5,6,7,8,9,10,11,12,13,14 )=[0, 14]　・・・(1)

　　　　　　　　　y≠xなので、T₋(n, C)(y)=C(y)=[-2, 3]・・・(2)

　　　　　　　　　　(1), (2)よりT₋(n, C)={ (x, [0, 14] ), (y, [-2, 3] ) }が得られる。

 

（例４）下の図は、

　　　　入力コンテキスト：C={ (x, [1, 10] ), (z, [-1, 1] ) }、代入ノードの式：　x:=x+y

　　　　とするとき、T₋(n, C)={ (z, [-1, 1] ) }となることを示している。

　　　　　　

　　解説：C(y)=□なのでx:=x+yは未定義となる。したがって、T₋(n, C)(x)=□

　　　　　　z≠xなので、T₋(n, C)(z)=C(z)=[-1, 1]

５．２　テストノードの初等的抽象解釈T₋(n, C)

　入力抽象コンテキストCはテストノードにより真と偽に関係する２つの出力抽象コンテキストC_TとC_Fを生じる。

N_Tをテストノードの集合とする。任意のn∈N_Tに対して、nは下記の様式とする；

　　　　　　　　　　

ここで、Q(v₁,・・・,v_m)は変数v₁,・・・,v_mに依存するブール式（訳注）である。

　（訳注）ブール式は、TRUEまたはFALSEの論理文。ブール式では、比較する両方の式の基本データ

　　　　　型が同じであれば、すべての型のデータを比較できる。データをテストし、他のデータと等しい、

　　　　　より大きい、またはより小さいかを調べることができる。

このときT₋(n, C)=(C_T, C_F)を下記で定義する：

任意のi∈Iに対して、入力抽象コンテキストCによるv₁,・・・,v_mの抽象値C(v₁),・・・,C(v_m)を具体化関数γで戻したγ(C(v₁)),・・・,γ(C(v_m))に属する具体値をμ₁,・・・,μ_mとするとき、

C_T(i)=α( {τ|τ∈γ(C(i)) }かつ{ Q(μ₁,・・・,μ_m)が真となるようなμ₁∈γ(C(v₁)),・・・,μ_m∈γ(C(v_m)) }

C_F(i)=α( {τ|τ∈γ(C(i)) }かつ{ Q(μ₁,・・・,μ_m)が偽となるようなμ₁∈γ(C(v₁)),・・・,μ_m∈γ(C(v_m)) }

 

（例１）下の図は、

　　　　入力コンテキスト：C={ (x, [-∞, +∞] ) }、テストノードの式：　x≧0

　　　　とするとき、C_T={ (x, [0, +∞] )}、C_F={ (x, [-∞, -1] ) }となることを示している。

　　　

　　　解説：テストノードは抽象値x≧0なのでQ(x)= if x≧0 then true, else falseとなる。したがって、

　　　C_T(x)=α( {τ|τ∈γ(C(x)) }かつ{ Q(μ)が真となるようなμ∈γ(C(x)) }

　　　　　　　=α( {τ|τ∈γ([-∞, +∞]) }かつ{ Q(μ)が真となるようなμ∈γ([-∞, +∞]) } )

　　　　　　　=α({τ=-∞,・・・-2,-1,0,1,2,・・・+∞ }かつ{μ=0,1,2,・・・+∞ } )

　　　　　　　=[0, +∞]

　　　C_F(x)=α( {τ|τ∈γ([-∞, +∞]) }かつ{ Q(μ)が偽となるようなμ∈γ([-∞, +∞]) } )

　　　　　　=α({τ=-∞,・・・-2,-1,0,1,2,・・・+∞ }かつ{μ=-∞,・・・-2,-1 } )

　　　　　　= [-∞, -1]

（例２）下の図は

　　　　入力コンテキスト：C={ (x, [-∞, +∞] ), (y, [1,10]) }、テストノードの式：　x≧y

　　　　とするとき、C_T={ (x, [1, +∞] ), (y, [1,10]) }、C_F={ (x, [-∞, 9] ), (y, [1, 10]) }となることを示している。

　　

　　　解説：テストノードは抽象値x≧yなのでQ(x, y)= if x≧y then true, else falseとなる。

　　　C_T(x)=α( {τ|τ∈γ(C(x)) }かつ{ Q(μ₁,μ₂)が真となるようなμ₁∈γ(C(x)),μ₂∈γ(C(y)) }

　　　　　　　=α( {τ|τ∈γ([-∞, +∞]) }かつ{ Q(μ₁,μ₂)が真となるようなμ₁∈γ([-∞, +∞]),

　　　　　　　　μ₂∈γ([1, 10]) }=α({τ=-∞,・・・-2,-1,0,1,2,・・・+∞ }かつ{μ₁=10, 11, ,・・・+∞ })

　　　　　　　=[-∞, +∞]∩[10, +∞]= [10, +∞]

　　　C_T(y)=α( {τ|τ∈γ(C(y)) }かつ{ Q(μ₁,μ₂)が真となるようなμ₁∈γ(C(x)),μ₂∈γ(C(y)) }

　　　　　　　　==α( {τ|τ∈γ([1,10]) }かつ{ Q(μ₁,μ₂)が真となるようなμ₁∈γ([-∞, +∞]),

　　　　　　　　μ₂∈γ([1, 10]) }=α({τ=1,2,・・・,10}かつ{μ₂=1,2,・・・,10 })=[1, 10]∩[1,10]=[1,10]

５．３　結合ノードの出力コンテキスト

　結合ノードの出力コンテキストを計算するために、結合ノードの入力コンテキストを最初に計算しなければならない。単純な結合ノードnを下記に示す：

　　　　　　　

ここで、C₁, C₂,・・・, C_mは結合ノードnの入力コンテキスト

C=∪⁼C_i, i∈[1, m]は結合ノードの出力コンテキスト

（例）下の図は、

　　入力コンテキスト：C₁={ (x, [1, 1] ) }, C₂={ (x, [2, 2]) }とするとき、

　　結合ノードの出力コンテキスト：C= C₁∪⁼C₂={ (x, [1, 1]∪^〜[2, 2] ) }={ (x, [1, 2] ) }

　　となることを示している。

　　

５．４　ループ結合ノードの出力コンテキスト

　この節は論文の訳ではなく簡単な例での解説を述べる。例えば、下のような例を考えてみる。

この場合、ループには上からと横からという２つの方向からの入力があり、出力は下方向１つである；

　　　　　

ループの最初の入力コンテキストは上からはInputC₁={ (i, [1, 1] ) }である。横からの初回は実際にはないが空集合の入力InputC_2,1=φがあると考える。したがって、このループの初回(j=1)の出力はOutputC₁= InputC₁∪⁼InputC_2,1={ (i, [1, 1] ) }∪⁼φ={ (i, [1, 1] ) }である；

　　　

このループの２回目の入力コンテキストはInputC₁={ (i, [1, 1] ) }とInputC_2,2={ (i, [2, 2] ) }であり、

２回目の出力コンテキストはOutputC₂=InputC₁∪⁼InputC_2.2={ (i, [1, 1] ) }∪⁼{ (i, [2, 2] ) }={ (i, [1, 2]) }

となる；

　

 

３回目を考えると、このループの３回目の入力コンテキストはInputC₁={ (i, [1, 1] ) }とInputC_2,3={ (i, [3, 3] ) }であり、３回目の出力コンテキストはOutputC₃=InputC₁∪⁼InputC_2.3={ (i, [1, 1] ) }∪⁼{ (i, [3, 3] ) }=

{ (i, [1, 3]) }となる；

　　　

同様にして、j回目の入力コンテキストはInputC₁={ (i, [1, 1] ) }とInputC_2,j={ (i, [j, j] ) }であり、j回目の出力コンテキストはOutputC_j=InputC₁∪⁼InputC_2.j={ (i, [1, 1] ) }∪⁼{ (i, [j, j] ) }={ (1, [1, j ] ) }となる；

 　　

　これを有限回で集結させるためにループ結合ノードの出力コンテキストから作られるwideningが使用される：すなわち、下の図のようにOutputC₁, OutputC₂, OutputC₃,・・という単調増大する無限系列の代わりにそれらのwideningからS₁, S₂,・・という有限回で安定する系列が作られる。この例の場合、２回目でwideningによる出力コンテキストは{ (i, [1,∞] ) }という値に安定する。

　　　　

６．抽象解釈器(Abstract Interpretor)

　抽象解釈器は全ての弧（=プログラムポイント)で空集合のコンテキストφからスタートする。第５節で我々は、（代入ノード、テストノード、結合ノード、ループ結合ノードなどの）異なるタイプのノードに対して、その入力弧のコンテキストからノードの出力弧のコンテキストを規定する変換を記述してきた。そのアルゴリズムは全てのコンテキストが安定するまでこれらの変換の適用を行うことである。すなわち、任意のノードでその変換をいくら適用しても出力弧のコンテキストが変化しなくなる状態を作ることである。

　一般的な抽象解釈器は下記の手順で作られる；

　　　　

 

例：

　　　　

下記の表は本論文で示した抽象解釈による上記のプログラムグラフの解析を示している；

　　　　

フローチャートを実行したときの各弧の最終コンテキストはinput arcの番号に丸印で示されている。