Octagon Abstract Domain概要

２０１6年8月
舟越 和己

はじめに(1)■本資料は下記の論文の紹介です；
Antoine Miné(*) : The Octagon Abstract Domain,
In AST 2001 in WCRE 2001, IEEE, pages 310–319. IEEE CS Press, October 2001.
(*) Ecole Normale Superieure（高等師範学校） de Paris, France■論文の序文からThis article presents practical algorithms to represent and manipulate invariantsof the form (±x±y≦c), where x and y are numerical variables and c is a numeric
constant. Sets described by such invariants are special kind of polyhedra called
octagons because they feature at most eight edges in dimension 2.Using abstract
interpretation, this allows discovering automatically common errors, such as
division by zero, out of bound array access or deadlock, and more generally toprove safety properties for programs.（この論文は、x,yを変数、cを定数とするとき(±x±y≦c)という形式の不変量を求めるアルゴリズムを提供する。この不変量で記述された集合は、２次元の場合高々８つの辺を持つoctagonと呼ばれる多面体の特別なケースになる。抽象解釈により、この集合はゼロ割り、配列の境界オー
バー、デッドロックのようなエラーを自動的に見つけることを可能にする。)

はじめに(2)■下の図で(a)を具体値の集合（例：プログラムの２変数x, yの値）とします。(b),(c),(d)は具体値の集合に対する抽象領域の種類を示しています。
・(b)は区間の直積による抽象。
・(c)は多面体領域による抽象。
・(d)はOctagon領域による抽象。
近似の精度は(b)<(d)<(c)ですが、多面体領域を求めるには変数が増えると指数関数的に使用メモリ量や計算時間が増大します。
一方、Octagon領域は多面体領域に較べて近似の精度はやや低下しますが、変数が増えることによる使用メモリ量はO(n2),計算時間はO(n3)で押さえられます。→Octagon領域が有効な理由。

はじめに(3)■本資料の構成
１．Octagon領域の表現
これはモデル検査で使われる差分境界行列(DBMs)を拡張することにより実現されます。
２．具体値の集合からOctagon領域を求める方法
これは多点間の最短距離を求めるフロイド・ウォーシャル法を適用することにより求めます。
３．Octagon領域による抽象解釈の例
これは、１次元ランダムウォークプログラムを例にして適用します。

１．OCTAGON領域の表現

51.1 Difference-Bound Matrics(DBMs)とは?(1)■v0, v1はその値が数値（Z, Q, 又はR）となる変数とし、その集合を
V={v0, v1}とします。c, dを数値とするとき、v0, v1∈Vに対し
C={ v0 – v1≦c, v1 – v0≦d }をV上のdifference-bound（差分境界）と言います。変数x, y間に制約がないときはx-y≦+∞で明示します。
また、この境界値c, dを使用して
m10=c, m01=d, m00=+∞, m11=+∞により作られる行列m=(mij)をdiffrence-bound Matrix(DBM：差分境界行列)と言います。
v0 v1
v0 +∞ dv1 c +∞

1.1 Difference-Bound Matrics(DBMs)とは?(2)■DBMの例：
3変数の場合の例は、V={v0, v1, v2}として
C={v1-v0≦4, v0-v1≦-1, v2-v0≦3, v0-v2≦-1, v1-v2≦1}とすると、
m01=4, m10=-1, m02=3, m20=-1, m21=1, m00=+∞, m11=+∞, m21=+∞,m22=+∞なので、DBMは下記のようになります；

v0 v1 v2
v0 +∞ 43
v1 -1 +∞ +∞v2 -1 1 +∞

1.1 Difference-Bound Matrics(DBMs)とは?(3)■DBMの一般的定義
vi, vjはその値が数値（Z, Q, 又はR）となる変数とし、その集合を
V={vi, vj}とします。vi, vj∈Vに対し、
C={ vi – vj≦c }をV上のdifference-boundと言います。
尚、差分境界値cは（差分の最大を考えることにより）１つに決まると考えます。即ち、c≠dでvi – vj≦cかつvi – vj≦dとなることはない。このとき、c (vj – vi≦cのとき）
mij=+∞ （上記以外のとき）により作られる行列m=(mij)をdiffrence-bound Matrix(DBM：差分境界行列)と言います。
■DBMの順序⊆は下記により定義されます；
m⊆n ⇔ 任意のi, jに対して、mij≦nij

1.2 Potential Graphとは？(1)■各変数をノードに、変数の有限な差分境界値をノード間のやり取りとして表現したグラフをPotential Graphと呼びます。
（例）V={v0, v1, v2}として
C={v1-v0≦4, v0-v1≦-1, v2-v0≦3, v0-v2≦-1, v1-v2≦1}とするとき、ノード=v0, v1, v2なのでPotential Graphは下記のようになります。
v0

4
−1

v1

−1

3

1

v2

1.2 Potential Graphとは？(2)■Potential Graphの一般的定義
下記を満たすV, A, wをPotential Graph G(m)と言い、G(m)={V, A, w}
で表します。
V={vi, vj}とするとき、
A={(vi, vj) | mij<+∞}：DBMの差分境界値mijが有限となるような
vi, vjの組の集合。
このとき(vi, vj)をmijに対応させる関数をwとします；
w((vi, vj))=mij

1.3 V-domainとは？(1)■V={v0, v1}に対して
C={ v1 – v0≦4, v0 – v1≦-1 }とします。DBMで表せば、
mij= +∞ 4
-1 +∞
このとき、
D(m) = { (s0, s1) | 任意のi, jに対してsj – si≦mij }v1
をV-domainと言います。
これを図示すると、
4
右図のような領域となります。
v
0−1

1.3 V-domainとは？(2)■V-domainの一般的定義
DBM m , vj – vi≦mij が与えられたとき、D(m) = { (s0,・・・, sN-1) | 任意のi, jに対してsj – si≦mij }をV-domainと言います。
■m⊆n ⇒ D(m)⊆D(n) だが逆は真ではありません。

1.4 DBMの拡張：その１(1)
これまでV={v0, v1}に対してC={ vi – vj≦c }という制約を考えてきましたが、これに±vi≦cという制約も追加します。
そのために「常に0の値をとる変数0」をVに追加します；
V={0, v0, v1}
変数0を追加したVと、追加する前のVを区別するために追加する前のVをV0で表すようにします；
V0={v0, v1}
V上の制約Cについても同様にC0={ vi – vj≦c }で表します。
（例）C={ v1 – v0≦4, v0 – v1≦-1, v0 - 0≦1, 0 - v1≦-2 }は
V={0, v0, v1}上の制約です。

1.4 DBMの拡張：その１(2)
今度は
C={ v1 – v0≦4, v0 – v1≦-1, v0 - 0≦1, 0 - v1≦-2 }のDBM（差分境界行列) mを求めると、

0

v0 v1
0 +∞ +∞ -2
v0 1 +∞ 4
v1 +∞ 1 +∞m=(mij)となります。
このmは、V={0, v0, v1}上の制約Cの差分境界行列ですが、これは「V0={v0, v1}上の拡張された制約Cの差分境界行列である」とも言うことができます。この意味を表すためにmに上付き文字0を付けた
m0を「V0={v0, v1}上の拡張された制約Cの差分境界行列」とします。

1.4 DBMの拡張：その１(3)次に、m0のV-domain D(m0)を考えます。
C={ v1 – v0≦4, v0 – v1≦-1, v0 - 0≦1, 0 - v1≦-2 }の例では、D(m0)={ (0, s0, s1) | s1 – s0≦4, s0 – s1≦-1, s0 - 0≦1,
0 - s1≦-2 }となります。
しかし、変数0, s0, s1の中で変数の値の存在領域として興味あるのは,s0とs1です。従って、D(m0)を変数s0, s1に制限した領域をD0(m0)で表します。すなわち、
D0(m0)={ (s0, s1) | (0, s0, s1) ∈D(m0) }1.4 DBMの拡張：その２：差分での八角形の表現(1)
今度は V+={v0, v1}に対して±vi±vj≦cという制約に拡張します。
そのために
V={v0+, v0-, v1+, v1-} 但し、v0+ = +v0, v0- = -v0, v1+ = +v1, v1- = -v1という集合Vを導入し、これに対して差分境界（２変数の差分≦c）を定義すると、下記のようにoctagon domainを表現することができます(c, d, e, f, g, h, i, j は定数）；v1⑦
v0+ - v1+≦c（これは、v1- - v0-≦cと同じ）①②③
v1+ - v0+≦d（これは、v0- - v1-≦dと同じ）②v0+ - v1-≦e（これは、v1+ - v0-≦eと同じ）③⑤
v0- - v1+≦f（これは、v1- - v0+≦fと同じ）④ ⑥
v0
v0+ - v0-≦g ⑤
v0- - v0+≦h ⑥④①
v1+ - v1-≦i ⑦⑧
v1- - v1+≦j ⑧

1.4 DBMの拡張：その２：差分での八角形の表現(2)（例）V={v0+, v0-, v1+, v1-}に対し下記の差分境界は図のような八角形となります；
v1+ - v0+≦4 ⇔ v1-v0≦4,
v0+ - v1+≦4 ⇔ v0-v1≦4,
v0+ - v1-≦4 ⇔ v0-(-v1)≦4 ⇔ v1+v0≦4,
v0- - v1+≦4 ⇔ (-v0)-(v1)≦4 ⇔ v0+v1≧-4,
v0+ - v0-≦4 ⇔ v0-(-v0)≦4 ⇔ v0≦2,
v0- - v0+≦6 ⇔ (-v0)-v0≦6 ⇔ v0≧-3,
v1+ - v1-≦6 ⇔ v1-(-v1)≦6 ⇔ v1≦3,
v1- - v1+≦4 ⇔ (-v1)-v1≦4 ⇔ v1≧-2

v1- - v0-=v0+ - v1+≦4
v0- - v1-=v1+ - v0+≦4
v1+ - v0-=v0+ - v1-≦4
v1- - v0+=v0- - v1-≦4

1.4 DBMの拡張：その２：DBM（差分境界行列) m+
前頁の例で、
C={m13=v1+ - v0+≦4, m31=v0+ - v1+≦4, m41=v0+ - v1-≦4,
m32=v0- - v1+≦4, m21=v0+ - v0-≦4, m12=v0- - v0+≦6,m43=v1+ - v1-≦6, m34=v1- - v1+≦4 }はV={v0+, v0-, v1+, v1-}上の制約。これのDBMm+を求めると、
j= 1

v0+

2

v0-

3

v1+

4

-

v1
i=
4
4
1 v0+ +∞ 6
4
2 v0- 4 +∞ 4
3 v1+ 44 +∞ 44 v1- 44
6 +∞

m+=(mij)+m+のVドメインD(m+)は下記となります。
D(m+)={(s0, -s0, s1, -s1) | s1+ - s0+≦4, s0+ - s1+≦4, s1+ - s0-≦4,
s0- - s1-≦4, s0+ - s0-≦4, s0- - s0+≦6, s1+ - s1-≦6,
s1- - s1+≦4 }1.4 DBMの拡張：その２：D+(m+)
前頁の例
D(m+)={(s0, -s0, s1, -s1) | s1+ - s0+≦4, s0+ - s1+≦4, s1+ - s0-≦4,
s0- - s1-≦4, s0+ - s0-≦4, s0- - s0+≦6, s1+ - s1-≦6,
s1- - s1+≦4 }はDBM m+のVドメインですが、我々が必要とするのはDBM m+のV+ドメインです。これはD+(m+)={(s0, s1) | (s0, -s0, s1, -s1) ∈D(m+) }により定義されます。
D+(m+)は右図のグリーンの領域（八角形）になります。

２．具体値の集合からOCTAGON領域を
求める方法

20

2.1 具体値の集合から差分境界行列m+の求め方(1)■変数がx0, x1の２変数の場合を考えます。
右図のように(x0, x1)の具体値が６個の点として与えられているとします。
このとき、異なる変数x0+, x0-,
x1+, x1-の差を全ての具体値に対して求め、それらの最大値を決定します。
①x1+-x0+=x1-x0= 3-1=2
1-2=-15-1.5=3.5
4-4=0
3-3=0
2-5=-3x1(1.5, 5)(4, 4)(1, 3)(3, 3)(5, 2)(2, 1)x0

従って、m13=x1+-x0+=x1-x0≦3.5
これは与えられた６個の具体値に対して成立する不等式です。

2.1 具体値の集合から差分境界行列m+の求め方(2)②x0+-x1+=x0-x1=③x1+-x0-=x1+x0=

1-3=-22-1=1
1.5-5=-3.5
4-4=0
3-3=0
5-2=3
1+3=4
2+1=3
1.5+5=6.5
4+4=8
3+3=6
5+2=7

従って、m31=x0+-x1+=x0-x1≦3

従って、m23=x1+-x0-=x1+x0≦8

2.1 具体値の集合から差分境界行列m+の求め方(3)④x0--x1+=-x0-x1= -1-3=-4-2-1=-3-1.5-5=-6.5-4-4=-8
従って、m32=x0--x1+=-x0-x1≦-3-3-3=-6-5-2=-7⑤x0+-x0-=x0+x0=

1+1=2
2+2=4
1.5+1.5=3
4+4=8
3+3=6
5+5=10

従って、m21=x0+-x0-=x0+x0≦102.1 具体値の集合から差分境界行列m+の求め方(4)⑥x0--x0+=-x0-x0= -1-1=-2-2-2=-4-1.5-1.5=-3-4-4=-8
従って、m12=x0--x0+=-x0-x0≦-2-3-3=-6-5-5=-10⑦x1+-x1-=x1+x1=

3+3=6
1+1=2
5+5=10
4+4=8
3+3=6
2+2=4

従って、m43=x1+-x1-=x1+x1≦102.1 具体値の集合から差分境界行列m+の求め方(5)⑧x1--x1+=-x1-x1=-3-3=-6-1-1=-2-5-5=-10-4-4=-8-3-3=-6-2-2=-4

従って、m34=x1--x1+=-x1-x1≦-2

この他の組合せの結果は下記；
・x1--x0+=-x1-x0=x0--x1+→上記④と同じ。
・x1--x0-=-x1+x0=x0+-x1+→上記②と同じ。
・x0+-x1-=x0+x1=x1+-x0-→上記③と同じ。
・x0--x1-=-x0+x1=x1+-x0+→上記①と同じ。

2.1 具体値の集合から差分境界行列m+の求め方(6)以上から異なる変数x0+, x0-, x1+, x1-の差が求まったので差分境界行列m+が求まります；
j= 1

x0+

2

x0-

3

x1+

4

-

x1
i=
1 x0+ +∞ -2 3.5 -3
2 x0- 10 +∞ 8 3
3 x1+ 3 -3 +∞ -2
4 x1- 8 3.5 10 +∞m+=(mij)+2.2 差分境界行列m+のグラフ表示(Octagon domain)
次に、差分境界行列m+をグラフ表示します；
D(m+)={(x0, -x0, x1, -x1) | x1+-x0+=x1-x0≦3.5, x0+-x1+=x0-x1≦3,
x1+-x0-=x1+x0≦8, x0--x1+=-x0-x1≦-3, x0+-x0-=x0+x0≦10,
x0--x0+=-x0-x0≦-2, x1+-x1-=x1+x1≦10, x1--x1+=-x1-x1≦-2}+) }D+(m+)={(x0, x1) | (x0, -x0, x1, -x1) ∈D(mx1
は右図のグリーンの領域（八角形）になります。
(1.5, 5)→６個の具体値（点）を含む(4, 4)
Octagon domainが求められ++
D (m )ました。
(1, 3)(3, 3)
このOctagonは６個の具体値(5, 2)
を含む最小のOctagon(2, 1)
でしょうか? 次に具体値の集合を含む最小のOctagonx0について考えます。

2.3 具体値の集合を含む最小のOctagon domainについて(1)
今、下の右のようなOctagon D+(m+)’を考えてみます。２つのOctagonの包含関係
は D+(m+)⊂D+(m+)’であり、その差異は
x1+-x0+=x1-x0≦3.5 に対して x1+-x0+=x1-x0≦4.0という制約条件の上限値の違い(3.5と4.0)です。
→制約条件の上限が大きいとoctagon domainは大きくなる。従って、最小のoctagonは制約条件の上限が最も小さいものを見つけることです。
x1

x1(1.5, 5)

(1.5, 5)(4, 4)

D+(m+)(1, 3)

D+(m+)’(3, 3)(1, 3)(3, 3)(5, 2)(2, 1)(4, 4)(5, 2)(2, 1)

2.3 具体値の集合を含む最小のOctagon domainについて(2)
それでは、具体値の集合を含む最小のOctagon domainはどのようにして求められるでしょうか？これまでOctagonを求めた方法を振り返ると、「異なる２つの変数の差の上限」を全て求めていく方法でした。これは「枝１本で２つの変数を繋ぐ」ことに対応します。
++
x1 -x0 =x1-x0≦3.5

x0

3.5

x1

ところが変数が多い場合、２つの変数間の差の真の上限が隠れていて、２つの変数以外を経由することによりそれが分かることがあります。
（例）下の式の最初の３つの制約は「２つの変数間の上限」です。
・ V1 – V3 <= 44・ V1 – V2 <= 1
・ V2 – V3 <= 2
V3
V2
V1
2
1
しかし、V1-V3=(V1-V2)+(V2-V3)<=1+2=3のようにV1とV3の差をV2経由で求めるとV1とV3の「より小さな上限」が求まります：V1 – V3 <= 3
これは「枝２本で２つの変数V3, V1を繋ぐ」ことに対応します。
このように２つの変数以外を経由することにより「より小さな上限」を求めていけば、
具体値の集合を含む最小のOctagonが得られます。

2.3 具体値の集合を含む最小のOctagon domainについて(3)以上のことは・変数 ⇔ 地点
・２つの変数の差の上限 ⇔ ２つの地点間の距離・同じ変数間の上限 ⇔ 同じ地点の距離=0と考えることにより多点間の最短距離を求める問題の解法と同じであることが分かります。
j= 1

i=
1 x0+
2 x03 x1+
4 x1-

x0+

2

x0-

3

x1+

4

x10 -2 3.5 -3
10 0
83
3 -3 0 -2
8 3.5 10 0m+=(mij)+2.4 フロイド・ウォーシャル法
多点間の最短距離を求める問題の解法として「フロイド・ウォーシャ
ル法(Floyd-Warsall method)」があります。これは、次のような手順で最短距離を求めます；
縦に起点、横に終点の行列を考え、１．枝1本だけ使う場合の最短距離の行列（枝1本だけで繋がらない
区間は適当に大きな距離を入れておく）をつくる。
→これは起点と終点間の距離を表す行列となります。
２．枝2本を使う場合の最短距離を計算し、もし枝1本だけ使う場合より短くなっていたら先の行列の数値をこれに置き換える。
３．この更新行列の中の、枝2本を使う場合の最短距離を計算して、行列を再更新すると、枝4本以下を使う場合の最短距離行列となる。
これをn回繰り返すと2n以下の枝を使う場合の最短距離行列が求まります。

2.5 フロイド・ウォーシャル法の適用例(1)
今、A, B, C, D, E, Fの２点間の距離を
A

1

B
3

2
D

2

4

1
E

C

1

3

3
F

とするとき、各点間の最短距離を求めます。
まず、２点間を枝１本で繋いだときの距離を求めます。枝１本で繋げない所は∞を設定します；

2.5 フロイド・ウォーシャル法の適用例(2)1

次に、枝２本を使う場合の距離を計算し、 AB
枝１本の場合より短ければ枝２本を使う
321
場合で行列の値を置換えます。
（例）AからCへ行く場合；
DE
2
枝１本では行けないので∞
枝２本で行く場合は、A→B→Cならば距離は1+4=5,
A→E→Cならば距離は3+1=4
従って、枝２本以下でのAからCへの最短距離は4
これを全ての点について求めると、

4

C

1

3

黄色の部分は
枝２本で行くことにより距離が短くなった所

3
F

2.5 フロイド・ウォーシャル法の適用例(3)

黄色の部分は
枝２本で行くことにより距離が短くなった所

今度は、上の行列の中の枝2本を使う場合の最短距離を計算します。
・上の行列からA→B：1, B→C：2 従ってA→C：3となり上の行列の値A→C：4より小さくなるので置換えます。
・上の行列からA→E：2, E→F：3 従ってA→F：5となり上の行列の値A→F：6より小さくなるので置換えます。
これは枝4本以下を使う場合の最短距離となります。
→この結果、上の行列は次頁のようになります。

2.5 フロイド・ウォーシャル法の適用例(4)

黄色の部分は枝４本以下で行くことにより距離が短くなった所

今度は、上の行列の中の枝2本を使う場合の最短距離を計算しても新たに短くなる所は見つからないので最短距離の計算は終了です。

2.6 差分境界行列m+のshortest-path closure(1)それでは、先程求めた差分境界行列m+についてフロイド・ウォーシャ
ル法を適用し、最小のoctagonを求めてみます。
変数の添字と行列の要素の添字の対応を付けるために、大文字の変数XnをX1=x0+, X2=x0-, X3=x1+, X4=x1-となるように導入すると、先程求めた差分境界行列m+は次のようになります。
j= 1

i=
1 X1
2 X2
3 X3
4 X4

2

3

4

X1 X2 X3 X4
0 -2 3.5 -3
10 0 83
3 -3 0 -2
8 3.5 10 0

これは２つの変数を枝1本だけ使った上限値の行列を示しています。
次に、枝２本を使う場合の上限値を計算します。

2.6 差分境界行列m+のshortest-path closure(2)
j= 1

i=
1 X1
2 X2
3 X3
4 X4

2

3

4

X1 X2 X3 X4
0 -2 3.5 -3
10 0 83
3 -3 0 -2
8 3.5 10 0上の行列で例えばX2-X1に着目すると、2本の枝を使うケースは・X2-X1=(X2-X3)+(X3-X1)≦-3+3.5=0.5
・X2-X1=(X2-X4)+(X4-X1)≦3.5-3=0.5→何れにしても１本の枝を使う場合のX2-X1≦-2の方が上限値が小さい。
同様に他の場合も計算すると、全てのケースで１本の枝を使う
場合の方が上限値が小さいことが分かります。

2.6 差分境界行列m+のshortest-path closure(3)
従って、差分境界行列m+についてフロイド・ウォーシャル法を適用して求めた行列をm*とすると、この例のように２変数(x0, x1)の場合
m+=m*です。変数が３以上の場合、一般には、m+⊆m*です。
m＊を差分境界行列m+のshortest-path closureと言います。

３．OCTAGON領域による抽象解釈の例

39

3.1 １次元ランダムウォークプログラムの解析(1)■下記はm歩の１次元ランダムウォークをM回実行するプログラムです。配列∇
tab[a]にはaという位置に止まった回数をカウントして格納します。
q0
これを実行したときに配列tab[a]に範囲外エラー(buffer overrun)
a:=0; i:=1が発生しないことをOctagonによる抽象解釈で示します。
q1
int tab[−m. . .m];for i = −m to m tab[i] = 0;
q2
for j = 1 to M do
false
I≦m
int a = 0; int i=1;
q11
フローチャートではtrue q3
while i ≦ m do
if rand(2) = 0
q10
rand(2)=0?
then a = a + 1;
q4
q5
else a = a − 1;
a:=a+1a:=a - 1
fi
q7
q6
i=i+1
q8
tab[a] = tab[a] + 1;
i:=i+1
done;
q9（注）rand(n)は0からn-1までの数のうちいずれかをランダムに返す。

m=100歩の酔歩をM=10回試行の例

tab[a]:=tab[a]+1

3.1 １次元ランダムウォークプログラムの解析(2)S^(q0)=α(a, iの任意の値)=T
S^(q1)={ i=1, a=0 }ループに初めて入ったときはS^(q10)=Φ（空集合）なのでS^(q2)=S^(q1)∪S^(q10)=S^(q1) ={ i=1, a=0 }S^(q4)=S^(q5)=S^(q3)=S^(q2)
a=a+1なのでS^(q6)={i=1, a=1}
a=a-1なのでS^(q7)={i=1, a=-1}
S^(q8)=S^(q6)∪S^(q7)を含む最小のoctagon={i=1, a∈[-1, 1]}
i=i+1なのでS^(q9)={i=2, a∈[-1, 1]}

aS^(q6)(1, 1)

S^(q8)i(1, -1)S^(q7)
a(2, 1)

S^(q9)i(2, -1)

3.1 １次元ランダムウォークプログラムの解析(3)次にループ処理の２回目に入ります。
このとき、S^(q2)は下記のwideningを考えます；
S^(q2)∇=S^(q2)∇(S^(q1)∪S^(q9))={ i=1, a=0 }∇({ i=1, a=0 }∪{i=2, a∈[-1, 1]} )ここで、{ i=1, a=0 }∪{i=2, a∈[-1, 1]}の部分はこれを含む最小のoctagonを考えると下の真中の三角形のようになります。
従って、上記のwideningは下の右端のようになります。
S^(q2)∇={ (i, a) | a-i≦-1 & -i-a≦-1 }={ (i, a) | 1-i≦a≦i-1 }aS^(q2)∇

a { i=1, a=0 }∪{i=2, a∈[-1, 1]} aを含む最小のoctagon(2, 1)(1, 0)

S^(q9)i(2, -1)(2, 1)(2, 1)i(1, 0)(2, -1)i(1, 0)(2, -1)

3.1 １次元ランダムウォークプログラムの解析(4)S^(q3)=S^(q2)&(i≦m)={ (i, a) | 1-i≦a≦i-1, i≦m }S^(q4)=S^(q5)=S^(q3) a=a+1なのでS^(q6)={ (i, a) | 1-i≦a+1≦i-1, i≦m }={ (i, a) | -i≦a≦i-2, i≦m }また、a=a-1なのでS^(q7)={ (i, a) | 1-i≦a-1≦i-1, i≦m }={ (i, a) | 2-i≦a≦i, i≦m }S^(q8)=S^(q6)∪S^(q7)={ (i, a) | -i≦a≦i-2, i≦m }∪{ (i, a) | 2-i≦a≦i, i≦m }→S^(q8)=S^(q6)∪S^(q7)は下図のように頂点が2つありoctagonではないのでこれを含む最小のoctagonに置換えます（下の右図）。
aaS^(q6)∪S^(q7)(0, 2)i(0, m)i(0, 1)(0, m)

3.1 １次元ランダムウォークプログラムの解析(5)
従って、S^(q8)={ (i, a) | -i≦a≦i, 1≦i≦m }となります。
i=i+1なのでS^(q9)={ (i, a) | -(i-1)≦a≦i-1, 2≦i≦m+1 }={ (i, a) | 1-i≦a≦i-1, 2≦i≦m+1 }aS^(q8)
(0,1)
1)
(0,

i
(0, m)

aS^(q9)(0, 1) (0, 2)i(0, m+1)

3.1 １次元ランダムウォークプログラムの解析(6)次にループ処理の３回目に入ります。
このとき、S^(q2)は下記のnarrowingを考えます；
S^(q2)Δ=S^(q2)∇Δ(S^(q1)∪S^(q9))={ (i, a) | 1-i≦a≦i-1 }Δ(S^(q1)∪S^(q9))
ここで、S^(q1)∪S^(q9)={ i=1, a=0 }∪{ (i, a) | 1-i≦a≦i-1, 2≦i≦m+1 }を含む最小のoctagonは下の図の真中のようになります。
従って、上記のnarrowingは下の右端のようになります。
S^(q1)∪S^(q9)
a を含む最小のoctagonaaS^(q2)ΔS^(q9)(0, 1) (0, 2)i(0, m+1)i(0, 1)(0, m+1)i(0, 1)(0, m+1)

3.1 １次元ランダムウォークプログラムの解析(7)S^(q11)={条件式i≦mが偽となるようなS^(q2)Δの変数の領域}={ (i, a) | 1-i≦a≦i-1, i=m+1 }従って、変数aの範囲は-m≦a≦mとなり、配列tab[a]に範囲外エラーが発生しないことが分かります。
（参考） このプログラムは区間の直積領域では解けません。
→これを次頁以降に示します。

3.2 補足：直積領域近似では解けない(1)このプログラムは区間の直積領域では解けません。
これを以下に示します。
S^(q0)=α(a, iの任意の値)=T
S^(q1)={ i=1, a=0 }ループに初めて入ったときはS^(q10)=Φ（空集合）なのでS^(q2)=S^(q1)∪S^(q10)=S^(q1) ={ i=1, a=0 }S^(q4)=S^(q5)=S^(q3)=S^(q2)
a=a+1なのでS^(q6)={i=1, a=1}
a=a-1なのでS^(q7)={i=1, a=-1}
S^(q8)=S^(q6)∪S^(q7)を含む最小の直積領域={i=1, a∈[-1, 1]}
i=i+1なのでS^(q9)={i=2, a∈[-1, 1]}

aS^(q6)(1, 1)

S^(q8)i(1, -1)S^(q7)
a(2, 1)

S^(q9)i(2, -1)

3.2 補足：直積領域近似では解けない(2)次にループ処理の２回目に入ります。
このとき、S^(q2)は下記のwideningを考えます；
S^(q2)∇=S^(q2)∇(S^(q1)∪S^(q9))={ i=1, a=0 }∇({ i=1, a=0 }∪{i=2, a∈[-1, 1]} )ここで、{ i=1, a=0 }∪{i=2, a∈[-1, 1]}の部分はこれを含む最小の直積領域を考えると下の真中の矩形のようになります。
S^(q2)∇
従って、上記のwideningは下の右端のようになります。
S^(q2)∇={ (i, a) | 1≦i , aは任意}aa { i=1, a=0 }∪{i=2, a∈[-1, 1]} aを含む最小の矩形(2, 1)(1, 0)

S^(q9)i(2, -1)(2, 1)(2, 1)i(1, 0)(2, -1)i(1, 0)(2, -1)

3.2 補足：直積領域近似では解けない(3)S^(q3)=S^(q2)&(i≦m)={ (i, a) |1≦i≦m , aは任意}S^(q4)=S^(q5)=S^(q3) a=a+1でもaは任意なのでS^(q6)={ (i, a) |1≦i≦m , aは任意}
また、a=a-1でもaは任意なので
S^(q7)={ (i, a) |1≦i≦m , aは任意}
従ってS^(q8)=S^(q6)∪S^(q7)={ (i, a) |1≦i≦m , aは任意}
i=i+1なのでS^(q9)={ (i, a) |2≦i≦m+1 , aは任意}次にループ処理の３回目に入ります。
このとき、S^(q2)は下記のnarrowingを考えます；
S^(q2)Δ=S^(q2)∇Δ(S^(q1)∪S^(q9))={ (i, a) | 1≦i , aは任意}Δ(S^(q1)∪S^(q9))
ここで、S^(q1)∪S^(q9)={ i=1, a=0 }∪{ (i, a) |2≦i≦m+1 , aは任意}=
従って、上記のnarrowingは下の右端のようになります。
(0, m)

3.2 補足：直積領域近似では解けない(4)次にループ処理の３回目に入ります。
このとき、S^(q2)は下記のnarrowingを考えます；
S^(q2)Δ=S^(q2)∇Δ(S^(q1)∪S^(q9))={ (i, a) | 1≦i , aは任意}Δ(S^(q1)∪S^(q9))
ここで、S^(q1)∪S^(q9)={ i=1, a=0 }∪{ (i, a) |2≦i≦m+1 , aは任意} を含む最小の直積領域は下の図の真中のようになります。
従って、上記のnarrowingは下の右端のようになります。
aaS^(q9)(0, 1) (0, 2)

S^(q1)∪S^(q9)を含む最小の直積領域

i(0, m+1)

aS^(q2)Δi(0, 1)(0, m+1)i(0, 1)(0, m+1)

3.2 補足：直積領域近似では解けない(5)S^(q11)={条件式i≦mが偽となるようなS^(q2)Δの変数の領域}={ (i, a) | i=m+1, aは任意 }従って、変数aの範囲は不定となり、配列tab[a]に範囲外エラーが発生しないかどうかは不明です。

END：Octagon Abstract Domain