第２章 抽象解釈概要（主にCousot初期論文から）
２．１ プログラムのセマンティクス（意味論）と抽象解釈の基本用語
ここでは、プログラムの抽象解釈をフォーマルに定義するために関係するプログラムのセマンティクスと抽象解釈で用いられる基本的用語(*)を簡単に紹介する。（この節はCousot初期論文の３節、４節に該当する）
(*)ノードや環境、状態などの用語は、Scott and Stracheyの"Mathematical semantics of Program"(1971)で定義されている。
まず、準備としてプログラムのセマンティクスについて説明する。
■プログラムのセマンティクス（意味論）とは？
プログラムPのセマンティクスとは、そのプログラムを評価したい項目に着目して、それの可能な実行を
記述する「計算モデル」である。したがって、そこではプログラムの評価対象に関係のない項目は捨像
される。プログラムのセマンティクスを記述する方法は多数あるが、ここでは計算ステップ単位にその
状態の変化を記述するトレースベースの操作的セマンティクス(operatinal semantics)を考える。
■トレースベースの操作的セマンティクス例
D. Schmidt, All the World is an abstract interpretationに載っている簡単な例を下記に示す；
（p0, p1, p2, p3はプログラム進行の位置を示すプログラムポイント）
上記のプログラムの操作的セマンティクスは、下記の4つの遷移ルールを使用してプログラムポイントと変数の値の組pp, xを更新する；
このとき、上記のプログラムの操作的セマンティクスは下記のトレースとして表される；
プログラムの変数xの値が12として与えられたとすると、
（p0,12によりx=12、 p1,12によりx=6、 p0,6によりx=6、p1,6によりx=3、p0,3によりx=3、p2,3によりx=12よりp3,12)
これを、横軸に時間の経過によるプログラムポイントの変化、縦軸に変数の値を取り、グラフで表すと、
下の図のように表現できる；
図２．１ 操作的セマンティクスのトレースのグラフ
上記のプログラムで変数の初期値の与え方を変えると異なるトレースが得られる。例えば、
x=3のとき、p0,3→p2,3→p3,12
x=4のとき、p0,4→p1,4→p0,2→p1,2→p0,1→p2,1→p3,4
図２．２ 操作的セマンティクスの可能なトレース（一部分）のグラフ
このように、セマンティクスは全ての可能な実行環境でのプログラムの実行を意味するので、トレースベースの操作的セマンティクスは時間tの関数としてプログラムの変数の値などのベクトルx(t)の変化を示すカーブとして下記のように表現される；
図２．３ 可能なトレースのグラフ表現例
以降、操作的セマンティクスを定義するために下記の用語について簡単な事例により説明する；
・プログラムのノード(Node)と弧(Arc)及びプログラムポイント
・ノードのタイプ（開始、代入、接合、分岐、出口）
・環境(Encironment)
・状態(State)
・コンテキスト(Context)
・コンテキストベクトル(Context-Vector)
・n-コンテキスト(n-context)
・F-cont関数
（１）ノードとそのタイプ
プログラムのノードは図２．４のように、開始、代入、接合、分岐、出口の各ノードがある。各々の
意味は、図の右のノードの説明を参照。
図２．４ プログラムのノード
■代入ノードについての補足説明：代入ノードnは、そのノードnで「右側の式expr(n)の値を左側の
識別子id(n)に代入する。すなわち、id(n) = expr(n) （上の例x:=x+1では、id=x, expr=x+1）
ここで、識別子とは、変数、手続き、関数の名前である。識別子の全体はIdentで表す。
（２）弧(arc)とプログラムポイント
ノード間の遷移とプログラムの進行位置を示すために弧とプログラムポイントがある。図２．５を参照。
図２．５ 弧とプログラムポイント
以上はプログラムの構造についての基本的な用語である。次に、プログラム意味論で使われる用語である「環境」と「状態」について説明する。
（３）環境(Environment)
環境は識別子（変数、手続き、関数の名前）とその値を結び付けるもの。すなわち、環境は識別子
から値領域への関数の全体である： Env = Ident→ Values （Valuesは値の集合）
しかし、ここでは識別子として「変数」にのみ着目して考える。すなわち、「An environment(Env) is a
valuation for each variable of the program」であるとする。簡単に言えば、「環境とは、変数とその値の
対応。変数の中身を定義するもの」である。下の図を参照。
図２．６ 環境の説明
（例）eを変数x, yに5, 10を対応させる環境とする。 これをe＝｛x→5, y→10｝と書くこともある。意味
はe(x)=5, e(y)=10と同じ。→以降は、e(x)=aの表記を使用。意味論ではe(x)=[[x]](e)とも書く。
（４）状態(State)
状態Stateは<Arc, Env>の組であり、プログラム実行時のあるプログラムポイントでのプログラムの状態を示す（States = Arcs×Env）。→図２．７を参照。
図２．７ 状態の説明
■状態<Arc, Env>の簡単な変化例を図２．８に示す。
図２．８ 状態の変化例
上記のプログラムの操作的セマンティクスは下記のトレースとして表される；
σ0→σ1→σ2→ ・・・・・ →σ303
プログラムの状態は、初期状態から出発して、与えられた状態s=<a, e>の「次の状態(next state)」を
示す関数n-state(State<a, e>)から作ることができる；
・I-Statesは初期状態の集合である。プログラムの性質は各プログラムポイントに関係した”状態の
集合”を使用して調べられる。I-Statesは次のように定義される；
I-States = { <入口ノードの後続の弧 ,ボトムのEnv >}
図２．８の例では、I-States=<r0, e(x)=φ}>=σ0である。
・与えられた状態s=<a, e>の「次の状態(next state)」を示す関数n-state(State<a, e>)は論文中の
アルゴリズムを参照。n-state関数により図２．８の状態を表現すると、
σ0=I-States,σ1=n-state(σ0),σ2=n-state(σ1)=n-state(n-state(σ0))=n-state2(σ0),
σ3=n-state(σ2)=n-state(n-state2(σ0))=n-state3(σ0),・・・・σn= n-staten(σ0)
今、n-state0を恒等関数とすると、n=0,1,2,・・・に対して、σn= n-staten(σ0)となる。
すなわち、任意の状態は初期状態とn-state関数から作ることができる。
ここで、（プログラムが収束し）最終状態があるとして、これをn-state∞とすると、
n-state∞= n-state(n-state(・・・(σ0))・・)である。
これは、状態sと次の状態を対応させる関数F(s)=n-state(s)の最小不動点である。
すなわち、n-state∞=F(n-state∞) （Fは汎関数）
[最近の論文からの注釈]
2000年のP. Cousotの論文「抽象解釈：その達成と展望」（文献のNO.１０）では、プログラムの操作的セマンティクスにより、トレースσ0→σ1→σ2→ ・・・・・ →σ303を求めることを、
「このトレースに沿って現れる状態の集合によるトレースの抽象である：αS(σ)={σk： k∈[0, |σ|]}」
と考えている。したがって、図２．８の例は、|σ|=303なので
αS(σ) = {σk ： k∈[0, |σ|]}={σk ： k∈[0, 303]} = {σ0,σ1,σ2,・・・,σ302,σ303 }となる。
次に、プログラムの変数の束論を展開するために
・コンテキスト(Context)
・コンテキストベクトル(Context-Vector)
・n-コンテキスト(n-context)関数
・F-cont関数
という概念が登場する。
（５）コンテキスト(Context)
これは全ての可能な環境の集合であり、プログラムポイント（すなわち、弧(Arc)）に付けられている;
Context = 2Env （コンテキストは環境Envのベキ集合）
フローの例では、Env={e(x)=0, e(x)=1, e(x)=2,・・・(,e(x)=100)}なので、
Contextは、Env={e(x)=0, e(x)=1, e(x)=2,・・・(,e(x)=100)}の全ての部分集合の集合
■コンテキストCq
コンテキストCqとはプログラムポイントq(∈Arcs)でのコンテキストのことである。
すなわち、プログラムの可能な計算シーケンスにおいてqに関係する全ての環境の集合であり、下記
の式で表される；
Cq={ e | <q, e>=n-statesn(i)となるn≧0とi∈I-Statesが存在する}
これはqを固定して上記の式を満たすnが存在すればよいので、<q, e>=n-states(σ0), n-states2(σ0),
n-states3(σ0),・・・, n-statesn(σ0)の状態に対する環境eの集合となる。
（例）事例のプログラムでは、
・q=r1のとき、Cr1={e(x)=Φ}
・q=r4のとき、
Cr4は、{ e(x)=1, ←（n=4,すなわちn-states4(σ0),σ0∈I-Stateの場合）
e(x)=2, ←（n=7,すなわちn-states7(σ0)の場合）
e(x)=3 , ←（n=10,すなわちn-states10(σ0)の場合）
・・・ }又はこれの部分集合
⇒図２．８の状態の変化例と対比すると分かり易い。
（６）コンテキストベクトル(Context-Vector) (Cv)
これは各プログラムポイントq∈Arcsにコンテキストを関係させるベクトルであり、下記の式で定義
される； コンテキストベクトルCv= (Cv(r0),Cv(r1),Cv(r2),・・・,Cv(q),・・・）
= (Cr0, Cr1, Cr2,・・・,Cq,・・・）
ここで、Cv(q)={ e | <q, e>=n-statesn(i)となるn≧0とi∈I-Statesが存在する}(=Cq)
（ Cv（q）は、コンテキストベクトルCvの第q成分）
Cv(q)は各プログラムポイントqで局所的に定義される。
図２．４の例では、下記のようなベクトルとなる（図２．８の状態の変化例と対比すると分かり易い）；
Cv= (Cv(r0),Cv(r1),Cv(r2),Cv(r3),Cv(r4),Cv(r5)）
ここで、
Cv(r0)={e(x)=φ},Cv(r1)={e(x)=0}
Cv(r2)={e(x)=0, e(x)=1, e(x)=2,・・・, e(x)=99, e(x)=100}又はこれの部分集合,
Cv(r3)={e(x)=0, e(x)=1, e(x)=2,・・・, e(x)=99}又はこれの部分集合,
Cv(r4)={e(x)=1, e(x)=2,・・・, e(x)=99}又はこれの部分集合,
Cv(r5)={e(x)=100}
となる。
■コンテキストベクトルの要素の変化例
コンテキストベクトルCvの要素の変化を図２．９に図示してみるコンテキストベクトルCvの要素は
ループ処理の部分で何周するかにより変化することに注意。
図２．９ コンテキストベクトルの要素（r=riでのコンテキスト）の変化例
ここで、上記の説明中の「又はこれの部分集合」という意味は、コンテキストベクトルがループ処理の
部分では、ループの回数により弧rに対して異なるコンテキスト（部分集合）となることを指している。
→このことは、ループの回数によりコンテキストベクトルは複数存在し包含関係にあることを示している。
例えば、Cv1をループ１回目のコンテキストベクトル、Cv2をループ2回目のコンテキストベクトルとすると、図２．９では、
Cv1=(Cv(r0),Cv(r1),ループ１回目のCv(r2),ループ１回目のCv(r3),ループ１回目のCv(r4),Cv(r5)）
=({e(x)=φ}, {e(x)=0}, {e(x)=0}, {e(x)=0}, {e(x)=1}, {e(x)=φ}) ←ベクトルの並びは弧riの番号順(i=0,1,2,3,4,5)
Cv2=(Cv(r0),Cv(r1),ループ2回目のCv(r2),ループ2回目のCv(r3),ループ2回目のCv(r4),Cv(r5)）
=({e(x)=φ}, {e(x)=0}, {e(x)=0, e(x)=1}, {e(x)=0, e(x)=1}, {e(x)=1, e(x)=2}, {e(x)=φ})
となり、任意のr=r1,r2,r3,r4,r5に対して、Cv1(r)⊆Cv2(r)となる。
したがって、コンテキストベクトルの集合は下記の半順序⊆～と和∪～を導入することにより束になる；
Cvi, Cvjを２つのコンテキストベクトルとするとき、
・任意のr∈Arcsに対して、(Cvi⊆～Cvj)(r)をCvi(r)⊆Cvj(r)とすることによりコンテキストベクトルの
半順序Cvi⊆～Cvjを定義する。
・任意のr∈Arcsに対して、(Cvi∪～Cvj)(r)=Cvi(r)∪Cvj(r)によりコンテキストベクトル間の
和を定義する。
[証明]①⊆～は半順序である；
(i)任意のr∈Arcsに対して、Cvi(r)⊆Cvi(r)なのでCvi⊆～Cviである。
(ii)Cvi⊆～CvjかつCvj⊆～Cvkならば、任意のr∈Arcsに対して、
Cvi(r)⊆Cvj(r),Cvj(r)⊆Cvk(r)なので、Cvi(r)⊆Cvj(r)⊆Cvk(r)よりCvi(r)⊆Cvk(r)
したがって、Cvi⊆～Cvkとなる。
(iii)Cvi⊆～CvjかつCvj⊆～Cviならば、任意のr∈Arcsに対して、
Cvi(r)⊆Cvj(r),Cvj(r)⊆Cvi(r)なので、Cvi(r)=Cvj(r)となる。
したがって、Cvi=Cvjとなる。
②コンテキストベクトルの集合(Cv,⊆～)は束である；
任意のr∈Arcsと、Cvi,Cvj∈(Cv,⊆～)に対して、
上限∪{Cvi,Cvj}=(Cvi∪～Cvj)(r)=Cvi(r)∪Cvj(r)が存在するため。
下限は∩{Cvi,Cvj}=Cvi(r)∩Cvj(r)で考えればよい（注）。
（注）コンテキストベクトルの単調増加だけを考えるならば下限は不要。
∪～のみのようにjoinとmeetのどちらか一方しか必要としない束を
半束(semi-lattice)という。
(Q.E.D)
コンテキストベクトルはループ処理の回数により単調増加するが、コンテキストベクトルの集合の
トップT～とボトム⊥～は次のように定義される；
任意のr∈Arcsに対して、T～(r)=Env
任意のr∈Arcsに対して、⊥～(r)=φ
このとき、コンテキストベクトルの集合に{ T～,⊥～}を付加したものを改めてコンテキストベクトルの集合
とすると、任意のコンテキストベクトルCvに対して、
⊥～ ⊆～Cv⊆～T～
このとき、コンテキストベクトルの任意の集合は上限、下限を持つので完備束となる。
（７）n-context関数
（５）ではプログラムポイントqでのコンテキストCqを定義した。以降ではプログラムポイントと弧を同一視して、弧rでのコンテキストCrという言い方をする。
プログラムの意味から弧rでのコンテキストCrは、弧rに(r'の終端ノード=rの始端ノード）という条件で隣接する弧r'のコンテキストCr'と、それらの弧の間のステートメントにより修正されたもので決まる（図２．１０参照）。
図２．１０ 弧rとその前に隣接する弧のコンテキストとの関係
そこで、現在の弧rでのコンテキストCr=Cv(r)を、弧rの開始ノードが終端ノードとなる隣接した弧のコンテキストと、それらの弧の間のステートメントから求める関数を考え、それをn-context (n-はnextの意味）で定義する；
Cr=Cv(r) = n-context(r, Cv)
すなわち、n-contextは「Cv(r)を次のコンテキストとする」ようなコンテキストで表す関数である。
（例）図２．１０の例では、Cr2=Cv(r2)=n-context(r2,Cv)=Cr1∪Cr4
Cr4=Cv(r4)=n-context(r4,Cv)=Cr3∩{x=x+1}
また、n-context関数はプログラムのステートメントをコンテキストに反映するので、「プログラムの基本命令（ステートメント）の解釈」と考えられる。
⇒Cousot初期論文の5.1節では、これに関して下記の記述がある；
「The local interpretation of elementary program constructs which is defined by n-context is used to
associate a system of equations with the program.（n-contextにより定義されるプログラムの局所的
解釈はプログラムの式のシステムに関連させるために使用される）」
コンテキストベクトルの集合は半順序⊆～と∪～により束となるが、ここで、コンテキストベクトルCvが与えられたとき、「Cvを次のコンテキストベクトルとする」ようなコンテキストベクトルを求める関数を考え、これをF-contとする。すなわち、任意のr∈Arcsに対し、
F-cont(Cv)(r)=n-context(r,Cv) あるいは、F-cont(Cv(r))= n-context(r,Cv)
である。このとき、F-contはコンテキストベクトルの半順序⊆～に関して順序保存である；
Cv1⊆～Cv2 ならば、F-cont(Cv1)⊆～ F-cont(Cv2)
[証明]Cv1⊆～Cv2 ならば、任意のr∈Arcsに対し、
F-cont(Cv1)(r)= n-context(r,Cv1)= Cv1(r)⊆Cv2(r)=n-context(r,Cv2)= F-cont(Cv2)(r)
(Q.E.D)
コンテキストベクトルの単調増加列：⊥～⊆～Cv1⊆～Cv2⊆～Cv3⊆～・・・・において、
F-contを考えると、F-contは⊆～に関して順序保存なのでF-contは完備束上の単調増加関数
となる。したがって、タルスキの不動点定理より、F-contは不動点Cvを持つ；F-cont(Cv) =Cv
このCvはプログラムの変数xの取り得る値の最大値となり、プログラムポイントに依存しない
プログラムの大域的な性質である（注）。
（注）Cousot初期論文の要約では、このことが下記のように書かれている；
「The program global properties are defined as one of the extreme fixpoints of that, Tarski.
（プログラムのグローバルな性質はタルスキの不動点の一つとして定義される。）」
[最近の論文からの注釈]
コンテキストとコンテキストベクトルは初期の抽象解釈の論文における非常に重要な概念であるが、
2000年のP. Cousotの論文「抽象解釈：その達成と展望」では、次のような式として表現されるように
なった（すなわち、そこではコンテキストやコンテキストベクトルという言葉はもはや表に出なくなった）；
「抽象解釈の近似が実際に使用して有効であるということを直感的に示すために、安全性の解析(safty analysis)を考える。（ランタイムエラーが存在しないというような）安全性という性質は、何か悪いことは起きない、またはプログラムの実行は健全な状態のままである、ということを規定する。この概念は以下で説明するように抽象の複合(composition)により定式化できる。最初の抽象は、このトレースに沿って現れる状態の集合によるトレースの抽象である：αS(σ)={σk ： k∈[0, |σ|]}
トレースの集合Xの近似は、集合Xの少なくとも一つのトレースを表す状態の集合である：
αS(X)=∪σ∈XαS(σ)
αS(X)が不変(invariant)であるとは、プログラムを実行して初期状態から到達可能な全ての状態がその性質を満たさなければならないということを意味する。
状態sは、プログラムCのプログラムポイントl (∈C)と、整数値(x1, ... ,xn)∈Zを取るプログラムCの変数X1, ... ,Xn（x1∈X1, ... , xn∈Xn)を指定する制御状態から構成されているとする。大局的な不変式
αS(X)は、そのポイントで各プログラムポイントと変数の可能な値の組の集合を関係づける、局所的な不変式のベクトルに同型(isomorphic)である：
αl(Y)=Πl∈C{(x1, ... ,xn)：(l, (x1, ... ,xn))∈Y} ・・・・（式１）
このようにトレースのプログラム集合の計算はn次元整数空間Znの点の集合により近似される。」
この定義をCousotの初期論文での「状態」の定義と対比すると、
状態Stateは<Arc, Env>の組であり、プログラム実行時のあるプログラムポイントでのプログラムの状態を示す（States = Arcs×Env）。→図２．１１参照。
図２．１１ 状態の説明
（式１）は上記の例の場合、C={r0, r1, r2, r3, r4, r5, r6"、整数値x∈Env=Z、Yは状態の集合であり、
αl(Y)=Πl∈C{(x1, ... ,xn)：(l, (x1, ... ,xn))∈Y}=Πl∈C{ x∈Z：(l, x)∈Y}
→この式の意味をCousotの初期論文の言葉で表現すると、
{ x∈Z：(l, x)∈Y} ⇔ プログラムポイントlでのコンテキストClのこと。
各プログラムポイントl∈Cにコンテキストを関係させるベクトルがコンテキストベクトルなので、
Πl∈C{ x∈Z：(l, x)∈Y} ⇔ プログラムCのコンテキストベクトルのこと。
このように初期論文のサンプルプログラムのトレースは1次元整数空間Zの点の集合により近似
される。
２．２ プログラムの抽象解釈
２．１節では、プログラムの変数の取る値に着目して、コンテキストとコンテキストベクトルという２つの概念を導入し、コンテキストベクトルの不動点を求めることを議論した。ここでは、これらの概念を元に抽象解釈をフォーマルに定義する。また、より単純化された世界でコンテキストベクトルの不動点を求めるために、同じプログラムPに対する複数の抽象解釈間のガロア接続が登場する。（この節はCousot初期論文の５節～８節に該当）
２．２．１ コンテキストとコンテキストベクトルに関係する項目
２．１節から、コンテキストとコンテキストベクトルの世界を特徴付ける項目を整理すると、下記のようになり、各項目が対応している；
①コンテキストに関係する項目は、
・Contexts
（・和∪） （注：２．１節では、∪は∪～の定義のために使用した）
（・半順序⊆） （注：２．１節では、⊆は⊆～の定義のために使用した）
・最大元=Env（環境）
・最小元=φ（空集合）
・次のコンテキストを求めるn-context関数
②コンテキストベクトルに関係する項目は、
・Context vectors
・和∪～
・半順序⊆～
・最大元= T～(任意のr∈Arcsに対して、T～(r)=Env )
・最小元=⊥～（任意のr∈Arcsに対して、⊥～(r)=φ）
・次のコンテキストベクトルを求めるF-cont関数
そこで、２．２節では、上記の項目を元に一般化して、抽象解釈の形式定義を行う。
但し、抽象解釈の形式定義の前に、その準備として２．２．２で半束(semilattice)の定義を述べる。
２．２．２ 半束(semilattice)
定義： Lが半束であるとは、任意のx, y, z∈Lに対して下記を満たす演算○が
定義された代数L=(L,○）のことである；
(i) x○x=x
(ii) x○y=y○x
(iii) x○(y○z)=(x○y)○z
このとき、下記の定理が成立する；
定理： 半束Lにおいて、順序x
yをx○y=yにより定義すると、(L,)は任意の要素の組
が上限を持つ半順序集合になる（注）。
証明： まず、が半順序であることを示す；
(i) x○x=xは定義よりxxを意味している。
(ii) xyかつyxならば、x○y=yかつy○x=xしたがって、x= y○x= x○y=yとなり、x=y
(iii) xyかつyzならば、x○z= x○(y○z)= (x○y)○z=y○z=z 従って、xz
次に、x○(x○y)=(x○x)○y=x○yなので、xx○y
同様に、y○(x○y)=y○(y○x)= (y○y)○x= y○x= x○yなので、yx○y
したがって、x○yは{x, y}の上界である。
今、xz, yzとすると、(x○y)○z=x○(y○z)=y○z=zなので、(x○y)z
したがって、x○yは{x, y}の上限である。
（注）同様にして、yxをx○y=xにより定義すると、(L,)は任意の要素の組が下限を持つ
半順序集合になる
以上の準備を元に次の２．２．３で抽象解釈の形式定義を与える。
２．２．３ 抽象解釈の形式定義
２．２．１節から、コンテキストの世界を規定する項目を組(tuple)の形式で表すと、
＜Contexts,（∪）,（⊆）,Env,φ, n-context＞
となる。これは半順序⊆に関し完備束となっている（最大元はEnv,最小元はφ）。
プログラムPの抽象解釈の形式定義は、これを一般化したものである；
定義： プログラムPの抽象解釈の形式定義とは、下記の組のことである；
I=＜A-Cont,○,, T,⊥, Int＞
ここで、
・A-Cont：プログラムPの抽象コンテキスト（注）の集合。
（注）プログラムのコンテキストはプログラムの全ての可能な環境の集合であるが、
抽象コンテキストはコンテキストそのものでもよいし、これを単純化したものでもよい。
例えば、あるプログラムポイントで変数ｘが{0, 1, 2, 3, 4, 5}の値を取り得る場合、
これを単純化して両端の[0, 5]を考えるなど。
・○と：○は (i) x○x=x、(ii) x○y=y○x、(iii)x○(y○z)=(x○y)○zを満たす演算。
はxy⇔x○y=yにより定義された半順序であり、＜A-Cont,＞
は完備○－半束である。
→A-Contの最大元はT。また、A-Contは最小元⊥を持つものとする。
・T：A-contのトップ、⊥：A-Contのボトム
・Int：プログラムＰの弧(arc) rと抽象コンテキストベクトルA-Cont～（注）を入力とし、プログラムP
の抽象コンテキストを返す関数。
（注）抽象コンテキストベクトルは、各弧rに対する抽象コンテキストを成分とするベクトルで、
A-Cont～（r)=Int(r,A-Cont～)
また、２．２．１節から、コンテキストベクトルの世界を規定する項目を組(tuple)の形式で表すと、
＜Context vectors,∪～,⊆～,T～,⊥～, F-cont＞
となる。２．１節（６）での議論からこの組は完備束になる。
プログラムPの抽象解釈の形式定義では、このコンテキストベクトルの世界も次のように定義する。
定義 プログラムPの抽象解釈の形式定義Iに対応する抽象コンテキストベクトルの形式定義とは、
右の組のことである： < A-Cont～,○～,～, T～,⊥～, Int～>
２．１節（７）での議論からこの組は完備束になる。
抽象解釈の形式定義の項目と２．１節の例との対応を纏めると、次のようになる。抽象解釈の形式定義
の各項目の具体的イメージとしてその対応関係を頭に入れておくとよい。
①コンテキストに関係する項目は、
＜抽象解釈の形式定義＞ ＜２．１節の例＞
・抽象コンテキストA-Cont ⇔ ・Contexts
・演算○ ⇔ （・和∪）
・半順序
⇔ （・半順序⊆）
・最大元T ⇔ ・最大元=Env（環境）
・最小元⊥ ⇔ ・最小元=φ（空集合）
・次の抽象コンテキストを求めるInt関数 ⇔ ・次のコンテキストを求めるn-context関数
②コンテキストベクトルに関係する項目は、
＜抽象解釈の形式定義＞ ＜２．１節の例＞
・抽象コンテキストベクトルA-Cont～ ⇔ ・Context vectors
・演算○～ ⇔ ・和∪～
・半順序
～ ⇔ ・半順序⊆～
・最大元= T～ ⇔ ・最大元= T～(任意のr∈Arcsに対し、T～(r)=Env )
・最小元=⊥～ ⇔ ・最小元=⊥～（任意のr∈Arcsに対し、⊥～(r)=φ）
・次の抽象コンテキストベクトルを ⇔ ・次のコンテキストベクトルを求めるF-cont関数
求めるInt～関数
２．２．４ 抽象解釈の一貫性
一般に、プログラムの抽象解釈は１つとは限らない（抽象コンテキストの与え方による）。したがって、
・よりプログラムに近い抽象解釈（Ｃ）→これを「”具体”解釈」とも言う。
・より単純化された抽象解釈（Ａ）→これを「”抽象”解釈」とも言う。
を作り、ＣとＡに束の半順序関係を保存するような適切な写像を構成することができれば、単純化されたAで問題を解けば良いことが示される。２つの抽象解釈にこのような対応関係があることを「抽象解釈の一貫性(Consistent Abstraction Interpretations)」という。
「ガロア接続」はこの対応関係として登場する（図２．１２参照）。
図２．１２ 複数の抽象解釈
上記のことを厳密に定義すると次のようになる。
定義（抽象解釈の一貫性）： 今、プログラムの２つの抽象解釈があったとし、
一方は、プログラムの”抽象”解釈I－=< A-Cont－,○－,－, T－,⊥－, Int－>、
他方は”具体”解釈I = < C-Cont,○,,Τ,⊥, Int>であるとする。
これに対応するコンテキストベクトルの束は、下記である；
I－に対応するもの： < (A-Cont－)～, (○－)～, (－)～, (T－)～, (⊥－)～, (Int－)～>
Iに対応するもの： < C-Cont～,○～,～, T～,⊥～, Int～>
このとき、”抽象”解釈I－=< A-Cont－,○－,－, T－,⊥－, Int－>が、
”具体”解釈I = < C-Cont,○,,Τ,⊥, Int>と一貫性があるということは、
I－から生じるコンテキストベクトルCv－が、より詳細な解釈Iから生じるコンテキスト
ベクトルCvの正しい近似になっている場合のことを言う。
ここで、正しい近似とは、下記の(1),(2)が成立することである；
(1)コンテキストの世界で、C-ContとA-Cont－間にガロア挿入の対応関係が存在する；
すなわち、写像α：C-Cont→A-Cont－,γ：A-Cont－→C-Contに対し、下記が成立する；
①α、γは単調関数である。 ・・・・(G1)
②任意のx∈C-Contに対して、x
γ（α（x）） ・・・・(G2)
③任意のx－∈A-Cont－に対して、x－=α（γ（x－））・・・・(G3)
(2)コンテキストベクトルの世界で、C-Cont～と(A-Cont－)～間にガロア接続の関係が存在する；
すなわち、具体コンテキストベクトルと抽象コンテキストベクトル間の対応（α～：抽象化）と逆の対応
（γ～：具体化）で下記を満たす写像α～,γ～が存在することである。
{Cv～γ～(Cv－)}かつ{α～(Cv)～Cv－)}・・・・(G4) （注）
上記の定義で登場する項目を図示すると、図２．１３のようになる。
図２．１３ 抽象解釈の一貫性の関係図
（注）条件(G4)は任意のrに対して成立する大局的な仮定だが、実際にはこれの代わりにプログラムの
具体と抽象解釈についての以下の局所的仮定が使用される：
{任意の(r, x－)∈Arc×(A-Cont－)～に対し、Int(r,γ～(x－))γ(Int－(r, x－))
かつ
{任意の(r, x)∈Arc×C-Cont～に対し、α(Int(r, x))－Int－(r,α～(x)) ・・・・(G5)
→(G5)は、抽象コンテキストを求める関数Int－が健全(Sound)であることを示している。
すなわち、”具体”解釈の世界で求めたコンテキストInt(r, x)を抽象化写像αで移した
α(Int(r, x))は、”抽象”解釈の世界で求めた抽象コンテキストInt－(r,α～(x))に含まれる。
■抽象解釈の一貫性の事例１：区間の束
Pを単一の整数変数xのプログラムとする。
このとき、環境Envは整数全体Z（変数の値）である。したがって、プログラムPの１つの抽象解釈として
I=＜Zのベキ集合,（∪）,（⊆）, T=Z∪{－∞,+∞},⊥=φ, n-context＞
が考えられる。
ここで、コンテキストCは整数のある集合であるが、これは閉区間α(C)=[min(C), max(C)]により抽象化される。Cが有限でないとき境界は－∞または+∞になる。また、逆の対応γ([a, b])={x| a≦x≦b} とする。このとき、より抽象的な抽象解釈II（サフィックスはIntervalの意味）
II=＜区間のベキ集合,（∪）,（⊆）,T=[－∞,+∞],⊥=φ, n-context＞
が構成でき、α(C)=[min(C), max(C)],γ([a, b])={x| a≦x≦b}はガロア挿入になっている。
（これのn-contextについては次頁で説明する） これを図示すると図２．１４のようになる。
図２．１４ 整数と区間のガロア接続
上記では、対象のプログラムPを「単一の整数変数xのプログラムとする。」と一般的に述べたが、
具体的な下記のプログラムに対してコンテキストベクトルの最小不動点を求める。
図２．１５ 対象プログラム
図２．１５のC0, C1,・・・, C5はコンテキストベクトルの各弧に対する成分とする。したがって、コンテキストベクトルCvは、Cv=(C0, C1, C2, C3, C4, C5)と表される。プログラムの変数xは整数Zである。弧r0のコンテキスト（弧r0での変数xの取る値の集合）は不定なのでC0=Z∪{－∞, +∞}
n-context関数はCv(r)=n-context(r,Cv)なので、
C1=Cv(r1)=n-context(r1,Cv)=C0∩{x=0} ←n-context関数の定義から、r1でのコンテキストはr0での
コンテキストとr1の直前の式の値の集合との積集合
（r0とr1は直列のため積集合となる）
C2=Cv(r2) =n-context(r2,Cv)=C1∪C4 ←n-context関数の定義から、r2でのコンテキストはr1での
コンテキストC1とr4でのコンテキストC2との和集合。
（r2はr1とr4の合流のため和集合となる）
同様にして、
C3= Cv(r3) =n-context(r3,Cv)=C2∩{x≦99}
C4= Cv(r4) =n-context(r4,Cv)=C3∩{x=x+1}
C5= Cv(r4) =n-context(r4,Cv)=C2∩{100≦x}
したがって、図２．１２のプログラムに対するコンテキストベクトルCvが式の集合として求まった；
Cv=(C0, C1, C2, C3, C4, C5)
C0= Z∪{－∞, +∞}
C1=C0∩{x=0}
C2=C1∪C4
C3=C2∩{x≦99}
C4=C3∩{x=x+1}
C5=C2∩{100≦x}
ここで、ガロア挿入によるコンテキストの抽象化α(C)=[min(C), max(C)],γ([a, b])={x| a≦x≦b}をコンテキストベクトルに適用すると、抽象コンテキストベクトルA-Cvは次のようになる；
A-Cv=(A-C0, A-C1, A-C2, A-C3, A-C4, A-C5)
A-C0=[－∞, +∞]
A-C1=(A-C0)∩[0, 0]
A-C2=(A-C1)∪(A-C4)
A-C3=(A-C2)∩[－∞,99]
A-C4=(A-C3)+[1, 1]
A-C5=(A-C2)∩[100,+∞]
上記は区間に関する演算の式である。ここで、区間の演算は下記により定義されるものとする；
・ [a, b]∪[c, d]=[min(a, c), max(b, d)]
・ [a, b]∩[c, d]=[max(a, c), min(b, d)]
・ [a, b]+[c, d]=[a+c, b+d]
コンテキストベクトル間のガロア接続（α～,γ～）は下記となる；
α～(Cv)=(α(C0),α(C1),...,α(C5))=([min(C0), max(C0)], [min(C1), max(C1)],...,[min(C5), max(C5)])
γ～([a0, b0],[a1, b1],...,[a5, b5])=({x| a0≦x≦b0 },{x| a1≦x≦b1",...,{x| a5≦x≦b5 })
以上の全体像を図示すると、図２．１６のようになる。
図２．１６ プログラムの抽象解釈全体像の例
図２．１６を見ると、プログラムの２つの抽象解釈が行われている。１つは変数の集合を整数の束とした”具体”解釈であり、もう一つは変数の集合を区間の束とした”抽象”解釈である。これはガロア挿入(α、γ）により対応付けられている。また、これらのコンテキストに対応してコンテキストベクトルが式の集合として各々表現されていて、それらにはガロア接続（α～,γ～）が対応している。
最終的に行いたいことは、”抽象”解釈の世界でコンテキストベクトルの最小不動点を求めること、すなわち、コンテキストベクトルの式のシステムA-Cv=(A-C0, A-C1, A-C2, A-C3, A-C4, A-C5)
A-C0=[－∞, +∞]
A-C1=(A-C0)∩[0, 0]
A-C2=(A-C1)∪(A-C4)
A-C3=(A-C2)∩[－∞,99]
A-C4=(A-C3)+[1, 1]
A-C5=(A-C2)∩{100≦x}
において、その不動点A-Cv=F-Cont(A-Cv)を求めることである。
式のシステムの不動点を求める方法には、クリーネのシーケンス（注）を計算する”反復”アルゴリズムがある：すなわち、⊥～から出発して、Int～(⊥～)Int～(Int～(⊥～))...を繰り返し、これの最小不動点∪{Int～n(⊥～) | n∈N}をCvとする。
（注）クリーネチェイン(Kleene chain)とも言う。Lを完備半順序集合とし、f:L→LをScott連続関数とする。このとき、Lの最小元⊥からfを反復することにより得られる下記のチェインを上昇クリーネチェイン(ascending Kleene chain)という：
⊥f(⊥) f(f(⊥))... fn(⊥) ...
次の２．２．５節では、コンテキストベクトルの式のシステムA-Cv=(A-C0, A-C1, A-C2, A-C3, A-C4, A-C5)の不動点A-Cv=F-Cont(A-Cv)を反復アルゴリズムで実際に解いてみる。
[最近の論文からの注釈]
2000年のP. Cousotの論文「抽象解釈：その達成と展望」では、プログラムの制御のポイントに付けられた整数変数の値の区間により、トレースの集合を抽象化することは抽象の合成
α(T)=αi(αr(αl(αS(T))))
により与えられる。
ここで、αSはトレースに沿って現れる状態の集合によるトレースの抽象である；
αS(σ)={σk： k∈[0, |σ|]}
αlは状態の集合Yにコンテキストベクトルを対応させる；
αl(Y)=Πl∈C{(x1, ... ,xn)：(l, (x1, ... ,xn))∈Y}
αrはプログラム変数の間の関係を無視した変数領域の近似である：
αr(X)= Πi=1,..,n{xi：∃x1, ... ,xi-1, xi+1, ... ,xn：(x1, .,xi ,.. ,xn)∈X}
これは各変数の関係を無視した直積領域を示している。Cousotの初期論文のサンプルプログラムは、
１次元のコンテキストの世界なのでαr(X)は恒等写像となる。また、Cousotの初期論文のサンプルプログラムでは、この部分（αi(Z)=[min Z, max Z]）がガロア接続として説明されていた。
したがって、α(T)=αi(αr(αl(αS(T))))をCousotの初期論文のサンプルプログラムで対比すると、
図２．１６において、
T⇔ 対象のプログラムのトレースの集合→このトレースに沿って現れる状態の集合σを考える。
αS(T)⇔αS(σ) = {σk ： k∈[0, |σ|]}={σk：k∈[0, 303]}={σ0,σ1,σ2,・・・,σ302,σ303 } (=αS(X) )=Y
αl(αS(T))⇔αl(αS(σ))=αl(Y)=Πl∈C{(x1, ... ,xn)：(l, (x1, ... ,xn))∈Y}=Πl∈C{ x∈Z：(l, x)∈Y}
=プログラムCのコンテキストベクトル（→下の図のCvを構成する所まで）
αr(αl(αS(T))⇔αr(αl(αS(T))=αl(αS(σ))←１次元の世界で考えているのでαrは恒等写像。
αi(αr(αl(αS(T))))⇔αi(Z)=[min Z, max Z] （図２．１６の抽象化写像αに該当）
（補足説明：トレースセマンティクスを区間で抽象化することを図示すると、
図２．１７ トレースセマンティクスの区間による抽象
■抽象解釈の一貫性の事例２：符号の規則 （この部分は、文献の５より）
抽象解釈の最も直感的な例は符号の規則である。符号の規則とは、Xを数とするとき
・Xが負の数ならば-1
・Xが0ならば0
・Xが正ならば+1
を対応させる規則である。
例えば-1515*17は、算術演算の意味論が符号のルールで定義された抽象世界{(+), (-), (±)}での計算を示すものとして理解される。-1515*17の抽象世界での実行は-(+)*(+)→ (-)*(+)→(-)となり、-1515*17は負の数となる。抽象解釈は通常の計算世界の特別な構造（この例では符号）に関係する。それは実際の実行のある側面の要約を与えている。
今、Zを整数の集合とし、{-1, 0, 1}を符号の集合とする。
Zのベキ集合2Zと{-1, 0, 1}のベキ集合2{-1, 0, 1}との間の対応
α：2Z → 2{-1, 0, 1}"γ：2{-1, 0, 1}→ 2Z
を、次のように定義する；
α({z1,z2,...,zn})={z1の符号, z2の符号,...,znの符号}
γ({-1})=負の整数全体,γ({0})={0},γ({-1,0})={0}∪負の整数全体
γ({1})=正の整数全体,γ({0,1})={0}∪正の整数全体,γ({-1,1})=0を除く整数全体,
γ({-1,0,1})=Z
（例）α({-1,-2,-7})={-1},α({0,-2,-5})={-1,0},α({0,2,4,14,5,10,35})={0,1}
●このとき（α、γ）はガロア挿入となる。
明らかにγ(α({z1,z2,...,zn}))=γ({z1の符号, z2の符号,...,znの符号})⊇{z1,z2,...,zn}
なので、X∈2Z とするとき、X⊆γ(α(X))となる。・・・①
また、α(γ({-1}))=α(負の整数全体)=-1,α(γ({0}))={0},
α(γ({-1,0}))=α({0}∪負の整数全体)={-1,0}
α(γ({1}))=α(正の整数全体)={1},α(γ({0,1}))=α({0}∪正の整数全体)={0,1},
α(γ({-1,1}))=α(0を除く整数全体)={-1,1},α(γ({-1,0,1}))=α(Z)= {-1,0,1}
なので、Y∈2{-1, 0, 1}とするとき、Y=α(γ(Y))となる。・・・②
①、②より（α、γ）はガロア挿入である。
符号の規則による抽象解釈の束は下記のようになる。
図２．１８ 符号の規則の束
次に、整数の集合間の和や積は抽象化写像αでどうなるかを考えてみる。
●例えば、整数の集合間の積
{-1,-2,-7}*{0,-2,-5}={0,2,4,14,5,10,35} ・・・③
を考える。③の左辺の各々をαで移すと、α({-1,-2,-7})*－α({0,-2,-5})={-1}*－{-1,0}={1,0}
一方、③の右辺をαで移すと、α({0,2,4,14,,5,10,35})={1,0} 従って、下記が成立；
α({-1,-2,-7}*{0,-2,-5})=α({-1,-2,-7}) *－α({0,-2,-5})
すなわち、抽象世界での変換（積）は具体世界での変換（積）をαで移したものに等しくなる。
整数の集合間の積ではこれが成立するが、これを、抽象変換の完全性(completeness)という。
図２．１９ 整数の集合間の積の抽象化
●次に例えば、整数の集合間の和
{-3,-4,-7}+{1,2,3}={-2,-3,-6,-1,-2,-5,0,-1,-4}・・・④
を考える。④の左辺の各々をαで移すと、α({-3,-4,-7})+－α({1,2,3})={-1}+－{1}={-1,0,1}
一方、④の右辺をαで移すと、α({-2,-3,-6,-1,-2,-5,0,-1,-4})={-1,0} 従って、下記が成立；
α({-3,-4,-7}+{1,2,3})⊆α({-3,-4,-7}) +－α({1,2,3})
すなわち、抽象世界での変換（和）は具体世界での変換（和）をαで移したものを含む。
整数の集合間の和ではこれが成立するが、これを、抽象変換の健全性(soundness)という。
図２．２０ 整数の集合間の和の抽象化
一般に、P, A：集合 P=2P,A=2Aとし、
α:P→Aを抽象化写像（上の例では符号の規則に対応させるα）
F：P→PをP上の変換とする（上の例では和(+)や積(*)）
F～をα(P)=A上の抽象変換とする。F～：A→A（上の例では抽象化での和(+－)や積(*－)）
このとき、抽象変換F～が健全であるとは、任意のp∈Pに対して、α(F(p))⊆F～(α(p))
また、抽象変換F～が完全であるとは、任意のp∈Pに対して、α(F(p)) = F～(α(p))
図２．２１ 抽象変換
２．２．５ 抽象解釈で得られた等式群の解法（反復アルゴリズム）
抽象解釈で得られた下記の等式群を解くことを考える。（ここでは、コンテキストの変数名を
A-C0→X0, A-C1→X1, A-C2→X2, A-C3→X3, A-C4→X4, A-C5→X5と置換えて考える）
これはX2が求まればX3以降はすぐに分かるので、次の問題として設定できる；
【問題】下記のプログラムを実行したときの、プログラムのX2での変数xの取り得る値の範囲をプログラム解析で求めよ。
①、②からX2の値を変数xで表すと、（以降
を∪、∩で表す）
X2=X1∪X4=X1∪(X3[x:=x+1])=X1∪((X2∩[-∞, 99])[x:=x+1])=[0, 0]∪((X2∩[-∞, 99])[x:=x+1])
従って、 X2=[0, 0]∪((X2∩[-∞, 99])[x:=x+1])
これはX2に関する再帰式である。
●上で求めた下記の式からX2を求めるには？
X2=[0, 0]∪((X2∩[-∞, 99])[x:=x+1]) ・・・⑤
【従来のデータフロー解析の方法】
・ｘの値を最小元から始めて、式⑤をi⇒i+1の単調増大する漸化式⑥により、これ以上xの取り得る
範囲が増えない（不動点）に達するまで繰り返し計算する；
X2(i+1)=[0, 0]∪((X2(i)∩[-∞, 99])[x:=x+1]) ・・・⑥
この式を半順序の最小元⊥（ここでは空集合φと考えて良い）から出発して求めていくと、
上記が成立することは⑥式からすぐに分かる；
X2(1)=[0, 0]∪((X2(0)∩[-∞, 99])[x:=x+1]) = [0, 0]∪(⊥∩[-∞, 99])[x:=x+1])
=[0, 0]∪(⊥)[x:=x+1])=[0, 0]∪(⊥)=[0, 0]
X2(2)=[0, 0]∪((X2(1)∩[-∞, 99])[x:=x+1]) = [0, 0]∪([0, 0]∩[-∞, 99])[x:=x+1])
=[0, 0]∪([0, 0])[x:=x+1])=[0, 0]∪([1, 1])=[0, 1]
●これを繰返すと（100回位）、
・・・・
X2(99)=[0, 98]
X2(100)=[0, 0]∪((X2(99)∩[-∞, 99])[x:=x+1])=[0, 0]∪(([0, 98]∩[-∞, 99])[x:=x+1])
=[0, 0]∪(([0, 98])[x:=x+1])=[0, 0]∪(([1, 99])=[0, 99]
X2(101)=[0, 0]∪((X2(100)∩[-∞, 99])[x:=x+1])=[0, 0]∪(([0, 99]∩[-∞, 99])[x:=x+1])
=[0, 0]∪(([0, 99])[x:=x+1])=[0, 0]∪(([1, 100])=[0, 100]
X2(102)=[0, 0]∪((X2(101)∩[-∞, 100])[x:=x+1])=[0,0]∪(([0,100]∩[-∞,99])[x:=x+1])
=[0, 0]∪(([0, 99])[x:=x+1])=[0, 0]∪(([1, 100])=[0, 100]
となり、n≧101ではX2(n)=[0, 100]と、不動点に達する（これが求める解）。
上記の解法を本資料の第１章１．２節の「再帰と不動点」の視点から整理すると、次のようになる；
（１）プログラムのX2を求める等式は、下記のようにX2に関する再帰式(循環定義）となっている。
X2=[0, 0]∪((X2∩[-∞, 99])[x:=x+1]) ・・・①
（２）これを解くために、下記の漸化式を考えた；
X2(i+1)=[0, 0]∪((X2(i)∩[-∞, 99])[x:=x+1]) ・・・②
（３）X2(0)=⊥（最小元）から出発して（２）の漸化式の値を求めると、
X2(1)=[0, 0]∪((X2(0)∩[-∞, 99])[x:=x+1])=[0, 0]∪(⊥∩[-∞, 99])[x:=x+1])
=[0, 0]∪(⊥)[x:=x+1])=[0, 0]∪(⊥)=[0, 0]
X2(2)=[0, 0]∪((X2(1)∩[-∞, 99])[x:=x+1])=[0, 0]∪([0, 0]∩[-∞, 99])[x:=x+1])
=[0, 0]∪([0, 0])[x:=x+1])=[0, 0]∪([1, 1])=[0, 1]
となり、X2(0)⊆ X2(1)⊆X2(2)⊆・・・・⊆X2 ・・・③
すなわち、求めたいX2は、単調増加の集合列の先（極限）にある。
ここで、X2(i)をX2(i+1)に対応させる関数をFとすると、
X2(i+1) =F(X2(i)) ・・・④
（=[0, 0]∪((X2(i)∩[-∞, 99])[x:=x+1])）
この関数Fは、再帰プログラムを表す式X2の漸化式上の関数であり、Fの定義にはもはや再帰が現れないことに注意。Fはまた、変数xも表現に含めると、
F（X2(i))(x)=[0, 0]∪((X2(i)∩[-∞, 99])[x:=x+1]
で表現される。これは、X2(i) (x)を関数と見たときFは関数を変数とする関数（関数の関数）と考えられるので（汎）関数という。
また、X2がX2(i)の極限（X2(0)⊆ X2(1)⊆X2(2)⊆・・・・⊆X2）ということは、X2(i)→X2、 X2(i+1)→X2
したがって、④式から下記が成立する；
X2 =F(X2)
これは、漸化式④の解X2がFの不動点であることを示している。
以上は、抽象解釈で得られた等式群の解法（反復アルゴリズム）であるが、この解法には下記の問題点がある。
【問題点】X2の値を求めるために101回の繰り返し計算が必要だが、これを簡単に出来ないか？また、繰り返し回数が有限でないときはどうするか？これに対する解決法が次の節の抽象解釈のWideningである。
２．３ 不動点近似法・・・Widening
Wideningは抽象解釈において、プログラムから作られた等式群を解く場合、必要な計算ステップの数を大幅に減らして最小不動点の近似を得るために使用する。また、無限回の操作を有限で打ち切ることができるため、プログラム解析の完了を保証する。この節は別資料（文献６）のWideningの内容を中心に説明する（Cousot論文の「９節 不動点近似法」のwideningと同様の例なので）。
２．３．１ Widening演算子
(L,⊆）を完備束（関係⊆に関し上限、下限が存在する）とする。
下記を満たすとき、∇：L×L→Lがwidening演算子であるという；
①∇は上界演算子である。
すなわち、任意のx, y∈Lに対して、x∪y⊆x∇y
②有限鎖(Chain)の条件
Lの単調増大する鎖 x0⊆x1⊆・・・⊆xn・・・に対して、
∇演算子による鎖
y0=x0, y1=y0∇x1, y2=y1∇x2,・・・, yn+1=yn∇xn+1,・・・
は、有限で安定する（増大が有限回で止まる）単調増大鎖である。すなわち、
或るmが存在して、ｙ0⊆y1⊆・・・⊆ym=ym+1=ym+2=・・・
すなわち、無限の鎖(xn)に対して、widening演算子∇により有限で安定する鎖(yn)が定義される。
■windening演算子の例
区間の集合に対してwidening演算子を以下のように定義する
このとき、∇はwidening演算子の条件を満たす；
(xn)：⊥⊆[0, 0]⊆[0, 1]⊆[0, 2]⊆・・・・
に対して、y0=⊥, y1=y0∇x1=⊥∇[0, 0]=[0, 0], y2=y1∇x2=[0, 0]∇[0, 1]=[0,∞],
y3=y2∇x3=[0,∞]∇[0, 2]=[0,∞]
となり、(yn)：⊥⊆[0, 0]⊆[0,∞]=[0,∞]・・・
すなわち、有限回（3回）で[0,∞]に収束する。
２．３．２ 抽象解釈で得られた等式群のWideningによる解法（事例１）
前項で定義した区間のwidenig演算子を２．２．４の等式群に適用すると、下のように3回で収束する。
■上記のwideningの式の説明
①widening前の単調増大する鎖（チェイン）は下記；
②上記鎖に対応するwideningの鎖を求める；
wideningのX2(0)=元の鎖のX2(0)=⊥
wideningのX2(1)= wideningのX2(0)∇元の鎖のX2(1)=⊥∇([0,0]∪⊥)=⊥∇[0,0]
wideningのX2(2)= wideningのX2(1)∇元の鎖のX2(2)= [0,0]∇([0,0]∪[1,1]))
= [0,0]∇[0,1]=[0,∞]
同様に、wideningのX2(3)=[0,∞]となり、収束する。
従って、wideningのX2(i)をX2(i)とすると下の結果が求まる。
③wideningによりX2(2)=[0,∞]に収束した。
この値を式 X2(i+1) = [0, 0]∪((X2(i)∩[-∞, 99])[x:=x+1])
に代入することにより、有限の不動点に到達する。このプロセスをDescending sequenceという。
これは従来の手法の101回の繰り返し計算と同じ結果となっている。
２．３．３ Wideningによる解法（事例１）のまとめ
widening演算子とdescending sequenceにより、「従来の解析手法では101回要していた計算が
わずか4回で求めることができた（注）。」 これはWideningの威力（殆ど計算せずに結果を示す）。
（注）この事例は単純なので同じ解[0, 100]が得られたが一般には正確な解よりは広い近似解となる。
図２．２２ Widening演算の説明
また、Wideningによる収束計算のグラフ表現とdescendingの意味について考えてみる。
X2(i+1)=F(X2(i))=[0, 0]∪((X2(i)∩[-∞, 99])[x:=x+1])
とするとき、これのWideningによる収束計算は図２．１６のように表現される（参考資料５のスライドを元に作成）；
図２．２３ Wideningによる収束計算のグラフ表現
２．３．４ 抽象解釈で得られた等式群のWideningによる解法（事例２：Zero divideの可能性の例）
下記のような単純なプログラムを例にして以下の問題を設定し、解析を行なう。⇒Polyspace Technologiesのスライドで紹介された例。
【問題】下記のプログラムでZero divideが発生するか？
これを通常のデバッグで確認すると、Kの取り得る値が広いのでかなり手間がかかる。
PolySpaceの資料では、式と最小不動点による解がある。⇒どのようにして導かれるかという計算過程は書かれてない。
以降、この式の導出過程を説明する。
変数i,j,kの取り得る範囲に着目すると、プログラムの各ステップの意味は下記のようになる。
すなわち、プログラムの等式表現は下記の右のようになる。
次にこれを「カオス的繰り返し法」と「widening演算法」の２つで解いてみる。
（１）カオス的繰り返し法による解法
上で求めた等式をX1から順に代入して最後のX8を求める；
① X0={ (0, 0, k) | k∈[-231, 231-1] }をX1に代入すると、
X1={ (2, j, k) | (i, j, k)∈X0 }={ (2, 0, k) | k∈[-231, 231-1] }
② 上で求めたX1={ (2, 0, k) | k∈[-231, 231-1] }をX2に代入すると、
X2={ (2, k+5, k) | k∈[-231, 231-1] }
上記の２つは簡単に求められたが、次のX3は収束計算が必要となる；
③ 上で求めたX2={ (2, k+5, k) | k∈[-231, 231-1] }をX3に代入すると、
X3=X2∪X6={ (2, k+5, k) | k∈[-231, 231-1] }∪{ (i, j+3, k) | (i, j, k)∈X4 }
= {(2, k+5, k) | k∈[-231, 231-1] }∪{ (i, j+3, k) | (i-1, j, k)∈X3 , i＜10 }
すなわち、X3のみを変数とする再帰式が求められた；
X3= {(2, k+5, k) | k∈[-231, 231-1] }∪{ (i, j+3, k) | (i-1, j, k)∈X3 , i＜10 }
これをX3の最小元から始めて単調増大する下記の漸化式により、X3の値の範囲が増えなくなるまで
繰り返し計算する(最小不動点計算）；
X3(n+1)= {(2, k+5, k) | k∈[-231, 231-1] }∪{ (i, j+3, k) | (i-1, j, k)∈X3(n) , i＜10}
この漸化式による最小不動点計算を下記に示す。
X3(n+1)= {(2, k+5, k) | k∈[-231, 231-1] }∪{ (i, j+3, k) | (i-1, j, k)∈X3(n) , i＜10} ・・・(1)
この(1)式をnについての漸化式を最小元（空集合）から出発して解いていく；
n=0のとき、X3(0)=φ（空集合）
これを(1)式に代入すると、
X3(1)={(2, k+5, k) | k∈[-231, 231-1] }∪φ={(2, k+5, k) | k∈[-231, 231-1] }
これを再び(1)式に代入すると、
X3(2)={(2, k+5, k) | k∈[-231, 231-1] }∪{(i, j+3, k) | (i-1, j, k)∈X3(1) , i＜10}
={(2, k+5, k) | k∈[-231, 231-1] }∪{(3, k+5+3, k) | k∈[-231, 231-1] , i＜10}
={(i, j, k) | k∈[-231, 231-1], i∈[2, 3], j=k+5又はj=k+5+3}・・・(2)
ここで、j=k+5又はj=k+5+3は次のように考える；
j=k+5=k+3*2-1, j=k+5+3=k+3*3-1すなわち、i=2, 3のとき、j=k+3*i-1と纏められる。
したがって、(2)は次のようになる；
X3(2)={(i, j, k) | k∈[-231, 231-1], i∈[2, 3], j=k+3*i-1}
以下、同様に繰り返し計算していくと、
X3(9)={(i, j, k) | k∈[-231, 231-1], i∈[2, 3, 4,・・・, 10], j=k+3*i-1} ・・・(3)
X3(10)=X3(9)となり、(3)がX3の最小不動点であることが分かる。
すなわち、
X3={(i, j, k) | k∈[-231, 231-1], i∈[2, 3, 4,・・・, 10], j=k+3*i-1}
={(i, j, k) | k∈[-231, 231-1], i∈[2, 10], j=k+3*i-1} （[2, 10]は区間を示す）
④次にX3={(i, j, k) | k∈[-231, 231-1], i∈[2, 10], j=k+3*i-1}をX4の右辺に代入することでX4の値を
求める； X4={ (i+1, j, k) | (i, j, k)∈X3 ,i＜10} ・・・(4)
ここで、X3のiはX4ではi+1に置き換えられているので、X4のi+1をiで表現すると、
X3のiはi-1となる； i-1∈[2, 10]→i∈[2+1, 10], j=k+3*(i-1)-1
したがって、(4)は次のようになる；
X4={(i, j, k) | k∈[-231, 231-1], i∈[2+1, 10], j=k+3*(i-1)-1}
={(i, j, k) | k∈[-231, 231-1], i∈[3, 10], j=k+3*i-4}
⑤同様に、X4 ={(i, j, k) | k∈[-231, 231-1], i∈[3, 10], j=k+3*i-4}をX5の右辺に
代入することでX5の値を求める；
X5={ (i, j+3, k) | (i, j, k)∈X4} ・・・(5)
ここで、X4のjはX5ではj+3に置き換えられているので、X5のj+3をjで表現すると、
X4のjはj-3となる； j-3=k+3*i-4→j=k+3*i-1
したがって、(5)は次のようになる；
X5 ={(i, j, k) | k∈[-231, 231-1], i∈[3, 10], j=k+3*i-1}
⑥X6=X5
⑦同様に、 X3 ={(i, j, k) | k∈[-231, 231-1], i∈[2, 10], j=k+3*i-1}をX7の右辺に代入することで
X7の値を求める。i=10なのでこれを代入すると、
X7={ (i, j, k) | (i, j, k)∈X3,i≧10 }
={(10, j, k) | k∈[-231, 231-1], j=k+3*10-1=k+29}
⑧同様に、 X7 ={(10, j, k) | k∈[-231, 231-1], j=k+29}をX8の右辺に代入することでX8の値を
求める。X8に達するためにはi≠jなので、
X8={ (i, j, k) | (i, j, k)∈X7 ,i≠j }
={(10, j, k) | k∈[-231, 231-1], j=k+29, i≠j } ・・・(6)
以上により、PolySpaceの資料の最小不動点による解が求められた。
次に、最後の式(6)の意味を考える；
X8={(10, j, k) | k∈[-231, 231-1], j=k+29, i≠j }
この式から、j=10のときi=j=10となり、プログラムはラベル７においてZero divide
が発生することが分かる。また、このときのk=-19である。
（２）Wideningによる解法
■下記の(1)式をwideningで解く。
X3(n+1)= {(2, k+5, k) | k∈[-231, 231-1] }∪{ (i, j+3, k) | (i-1, j, k)∈X3(n) , i＜10} ・・・(1)
上記(1)式は(i, j, k)という３変数の式だが、k∈[-231, 231-1]はこれ以上その値の範囲が拡大せず、 j=k+3*i-1からjはi, kにより一意的に決まるので、wideningとして拡大する鎖はiについてのみ考える。すなわち、１変数区間によるwideningで対応できる（注）。
以下、その手順を示す；
①widening前の単調増大する鎖の最初の数項を考える（これは、4.2(4)で計算済）
X3(0)=φ（空集合）
X3(1)={(2, k+5, k) | k∈[-231, 231-1] }
X3(2)={(i, j, k) | k∈[-231, 231-1], i∈[2, 3], j=k+3*i-1}
ここで、iのみについての鎖を考える。iについての鎖は
[X3(0)]i =φ、[X3(1)]i =[2, 2]、[X3(2)]i =[2, 3]
②上記のiについての鎖に対応してwideningの鎖を求める；
wideningの鎖の[X3(0)]i =元の鎖の[X3(0)]i =φ、
wideningの鎖の[X3(1)]i =(wideningの鎖の[X3(0)]i)∇(元の鎖の[X3(1)]i) =φ∇ [2, 2]=[2, 2]
wideningの鎖の[X3(2)]i =(wideningの鎖の[X3(1)]i)∇(元の鎖の[X3(2)]i) =[2, 2]∇[2, 3]=[2,∞]
・・・これ以上iは拡大しないのでwideningは収束！
したがって、wideningで求めたX3(n)の収束値は
X3(2)={(i, j, k) | i∈[2, +∞], k∈[-231,231-1], j=k+3*i-1}・・・(2)
となり、これを(1)式に代入すると、
X3(3)= {(2, k+5, k) | k∈[-231, 231-1] }∪{(i, j+3, k) | (i-1, j, k)∈X3(2) , i＜10}・・・(3)
ここで、 (3)式の{(i, j+3, k) | (i-1, j, k)∈X3(2) , i＜10}の
変数iが取り得る値は、(2)式よりi-1∈[2, +∞] & (i＜10)より、i-1=2, 3, 4, 5, 6, 7, 8, 9
⇒i=3, 4, 5, 6, 7, 8, 9, 10 すなわち、i∈[3, 10]
変数jの値は、 (i-1, j, k)∈X3(2)より、j=k+3*(i-1)-1 ⇒j+3=k+3*(i-1)-1+3=k+3i-1
これにより、{(i, j+3, k) | (i-1, j, k)∈X3(2) , i＜10}
={(i, J, k) | k∈[-231,231-1], i∈[3, 10], J=k+3*i-1}
したがって、(3)式は、
X3(3)= {(2, k+5, k) | k∈[-231, 231-1] }∪{(i, J, k) | k∈[-231,231-1], i∈[3, 10],
J=k+3*i-1} ={(i, J, k) | k∈[-231, 231-1], i∈[2, 10], J=k+3*i-1}
となり、２．３．４（１）の繰り返し計算と同じ結果が得られた。（通常のプログラム解析では10回の繰り返し
処理が必要だが、wideningでは2回で収束！）
⇒Wideningはプログラムのループ処理を一気に解決する手法。
２．３．５ Wideningのまとめ
（１）三者比較
（２）Widening演算子のコンセプト；
・この演算子はループ/サイクルの１つのイテレーション後の状態の変化を調べ、同じ変換が無限回
起きるかもしれないと仮定して、この情報からループの振舞いを外挿しようとする。
・この演算子はループの繰り返しがiの値を増大させていることを検知し、それが無限回起きることを
外挿する。この外挿は控え目過ぎるかもしれないが分析の完了を保証する。
