3 . 1
序 言並行処理プログラムの正しさの検証法の一つに，所期の目的がプログラム変 数などに関する述語Pで表される場合， Pが不変であることを示すことにより 検証する方法があるO しかし、所与の述語Pが不変式であるか否かは一般に決 定不能である。このような方法に基づいた検証法は既に幾っか報告されている が[4.5J 所与の述語 Pが不変式であるかどうかが決定可能となるような十分条 件について議論したものはほとんどない。
本章では，配列変数を含む並行処理プログラムシステムを定義し，このシス テムにおいて所与の述語が不変式であるためのそれ自身決定可能な十分条件 (これを満たす述語を 強帰納的"であるという〉を
3.2
で述べている。次い で3. 3
で，この決定可能なクラスに属する並行処理プログラム例としてN.
V . S t e n n i n g
[川の抽象的プロトコルをあげ，その検証の対象となる述語が強帰 納的，したがって不変式であることの証明が形式的な議論で行えることを示し ている。更に3.4
で、は，プログラムが必ず進行するか否かなどのいわゆるプロ グラムの動的な性質の検証問題について考察している。プロトコル本来の目的 にのみ使われる変数だけからなるプロトコルで、は，その動的な性質の検証がプ ログラムを直接調べることにより可能となる場合があるが，一般には極めて単 純なプロトコノレにおいても決定不能となることを2
カウンタオートマトンの決 定不能問題に帰着させて証明している。3.2
諸定義と問題並行に動くプログラムの抽象的モデ、ルとして，次のような並行処理プログラ ムシステムを考える。
[定義
3. 1 ]
並行処理プログラムシステム(以下，単にシステムと呼ぶ〉を第3章 プレスプールガ配列式を用いたプロトコルの記述と検証 25
s=
くV，Q
， o， 1 >で表す。ただし，(1) 変数は添字変数、状態変数，媒介変数の
3
種類よりなる。添字変数は配 列形の変数の添字を表す整数形の変数である。状態変数は，並行処理プログラムにおけるプログラム変数やプログラムカウンタなどに対応する制御変数を表 し，整数形の変数か，値としては整数値しかとらない配列形の変数よりなる。
配列形変数の添字には添字っきの配列形変数を含んでもよい。添字はし、くらで も大きくなりうるものとする。システム中で並行に動くすべてのプログラム中 に現れる全状態変数の集合をVで表す。システムで実行される動作は引数をも つことがあるが，媒介変数はその値を表す整数形の変数である。システム
S
の 状態を，V
に属する各整数形変数の値の組Vと各配列形変数の値(各添字の値 に対する値の組〉の組 aの対 (v，a)で定義し，その集合をKで表す。( 2 )
システムで実行可能な動作の有限集合が定義されている。各動作a
は引 数をもつことがあり，その値の組が dであるときa
(d)で表すことにする。動作
a
に対応して，その動作の実行の前後で、成立つ関係を示すため，動作実行 前後の状態変数(の組を整数形変数と配列形変数に分けて，それぞれV，A， V'， A'で表す〉と引数の値を表す媒介変数(の組をDで表す〉をそれぞれ自由 変数とする述語Qa(V， A， V'， A'， D)が与えられている。 ， "は動作実行 後の変化した値を表す変数を意味しており，例えば動作a
が代入操作のとき，Qa (V， A， V'， A'， D)は左辺が動作実行後の状態変数にFをつけたもの，右 辺がそれに対する代入式である幾つかの等式の論理積で表される(変化しない 状態変数については単にその変数を右辺，その変数にFをつけたものを左辺と する等式で表されるものとする〉。ただし，添字変数と媒介変数は動作実行の前 後で変化しないのではっけない。システムで実行可能なすべての動作に対応 する述語の有限集合を
Q
で表す。(3) 任意の動作
a
に対して述語 Oa(V， A， D)が定義されており，状態 S (EK)でOa(S， d)が真のとき動作a
(d)が実行可能， oa (S， d)が偽のと き実行不可能ということを意味している。s
，d
に対し， oa (S，d )
を真とする動 作a
(d)は一般に複数個あり，また，動作a
(d)を一つ決めても次に取る状 態は複数個ありうる。状態 Sでa
(d)が実行されるときの可能な遷移先の状26 第3章 プレスブ、ルガ配列式を用いたプロトコルの記述と検証
態の集合
s '(EK)
全体の集合は{ s 'I
oa( s
，d ) n
Qa( s
，s '
，d ) =true}
に等 しい。 Oa( s
，証)n
Qa( s
，s '
， (1)が真のとき且つそのときのみst
斗s '
と書 き，また， このような一つの動作a
とパラメータの値の組d
が存在するとき 且つそのときのみ単にs
ー→s '
と書いて，状態Sから1
回の動作で状態s '
へ遷 移可能であるとし、う。(4)
1 (V
，A)
はシステムの動作開始時の状態(集合〉を指定する述語である 。 口
[定義
3.2J
システムS
において，状態s
，s ' (εK)
に対しs
からシス テム上の遷移 一→"を零固または有限回適用してs '
に到達できるとき，s ユ →
s '
と書く。すなわち， ーと+"でK
の要素間の2
項関係 →"の反射的，推移的閉包を表す。
口
[定義
3.3J
述語P (V
，A)
をシステムS
の状態変数に関する述語とす る。(YsεK)
[ヨsoEK{ ( 1 ( s o )
二t r u e ) n
(so~s)} コ P (S)Jが真であ るとき，P (V
，A)
は不変式であるという。 口[定義
3.4 J
限定作用素を含まないプレスプルガ( P r e s b u r g e r )
配列式(以 下，P
配列式と呼ぶ〉を定義するため，まず項を定義する。( 1 )
項には整数項と配列項の2
種類があり，(2) 定数と整数型変数は整数項であり，
(3) 配列型変数は配列項である。
(4)
i
1，i
2が整数項のとき ，i
1+ i
2，i
1 ‑i
2は整数項であり，(5) M が 配 列 項 が 整 数 項 の と き M (i)も整数項である (M(i)は配列 項M の添字 iにおける値を表す〉。
(6)
M
が配列項，i
1，i
2が整数項のときAssign [M
，i
1，i
2Jは配列項であ る( A s s i g n [M
，i
1，i
2J
は要素M
(i1)を値i
2で置き換えて得られる 配列を表す〉。(7) (2)‑(6)を有限回適用して得られるものだけが項である。
限定作用素を含まない P配列式を次のように定義する。
(i)
i
r.i
2が整数項のとき ，i
1二i
2，i
1くi
2は限定作用素を含まないP
配 列式である。第3章 プレスブルガ配列式を用いたプロトコルの記述と検証 27 (ii) B1' B2が限定作用素を含まない P配列式ならば，~ (B1)， (B1)
u
(B 2，) (B1)
n
(B2) は限定作用素を含まない P配列式である。上の(i)，(ii)で定義されるものだけが限定作用素を含まない P配列式である。
口 N. S u z u k i
とD .] e f f e r s o n
によってつぎの補題[l1Jが示されている。[補題
3. 1 ]
限定作用素を含まないP
配列式の真偽は決定可能である。口 [命題3. 1 ]
システ S において，次の条件 C1~C3 が満たされるならば，以下の (i)，(ii)が成立つ。
C 1 :各動作
a
~こ対する述語ぬ (V， A， D)ハ
Qa(V， A， V'， A'， D) は，Yjヨ
wT
a( V
，A
，V '
， A'， j，w
，D ) (3.1)
の形である。ただし， j (あるいはw)は添字変数j(あるいはw)の組を表し，Yj (あるいはユw)はj(あるいはw)に属するすべての変数が全称記号Y (あ るいは存在記号ヨ〉で束縛されていることを表す。以下，この略記法を用いる。
C2:
述語I (V
，A)
は，Yh I o ( V
，A
，h )
(3.2) の形である。ただし， hは添字変数hの組を表す。C3:
所与の(検証の対象となる〉述語PV
，A)
は，Y
iP
0(V
，A
， i) (3 . 3 )
の 形 で あ る 。 た だ し は 添 字 変 数iの組を表す。ここで，
T
a，I o
，P o
はそれぞれ括弧の中の変数に関する限定作用素を含まな いP配列式である(刊。(i) に属する変数の j(あるいはh)に属する各変数への代入を σ'1 (j， i) (あるいは0'2
( h
， i))，で表す。各動作a
に対してそれぞれ次の式(3 . 4)
が真となる代入の仕方 qが 存 在 し ， か つ ， 式 (3 . 5)
が真となる代入の仕方 的が存在するならば，述語P (V
，A)
は不変式である。(+) :もちろん，それらの変数をすべて含む必要はなL、。例えば，
T
aでwがなければ式(3 . 1)はヨwを含まない形である。
28 第3章 プレスブ、ルガ配列式を用いたプロトコルの記述と検証
{Po (V
，A
， i)円Ta(V
，A
，V'
，A'
，同( j
，i )
，w
，D)}
コ
P0 (V'， A'， i) (3 .
4 )1 0 (V
，A
，σ2( h
， i))コPo ( V '
，A'
， i) (3 . 5 )
(ii) 式(3.4)
と (3 . 5)
が真であるかどうかは決定可能である。 口【証明】 (i)の証明:式(
3 . 4)
が真であるとする(以下，添字変数のみを 残 し て 他 の 変 数 は 省 略 し をPo
につけた式(3.6)
の形で書く〉。Po
(i)n Ta
(σ ， (j i)，w)
コP
ら(i) (3 . 6 )
式(3.6)
はYw{Po
(i)nTa (σ(j
， i)，w)
コP
ら(i)}と等価であるから，
Po(
i)刊ヨwTa( σ l ( j
，i)，w)
コP b ( i )
が成り立つ。一方，Yi Yj ( P o (
i)n ョ w Ta
(j，w))
つ
( P o (
i)n
ヨwTa
(0'1 ， (j i)，w) )
であるので式 (3.7)と (3.8)より次式が成り立つ。Yi Yj ( P O (
i)n
ヨw Ta
(j，w))
コPb(
i) 式(3.9)
は，Yh (Yi PO(
i)ηYj
ヨwTa(j
，w)コ P b ( h ) )
と等価であるから，(3.7)
(3.8)
(3.9)
Yi Po
(i)門Yj
ヨw Ta
(j，w)
コYiPb
(i)(3.10)
が 成 り 立 つ 。 式 (3 . 1 0 )
は，P(V
，A) n oa(V
，A
，D) nQa(V
，A
，V'
，A'
，D)
コ P( V '
，A ' ) ( 3 . 1 1 )
が成り立つことを示している。一方，式 (3.5)が真のときも同様にして
Yh 10(V
，A
，h )
コYiPo(V
，A
， i)が成り立つことが証明できる。すなわち，
I(V
，A)
コP(V
，A)
が成り立つ。従って，
I(V
，A)
を真とする状態(初期状態〉をs
。とすると，s
。でP ( s o )
も 真である。P ( s )
が 真 と す る と ， 式 (3 . 1 1 )
からs
ー→SF，従ってs
ーじぎであ る任意のs '
についてP ( s ' )
が真となり，定義3.3
からP(V
，A)
は不変式で第3章 プレスフ。ルガ配列式を用いたプロトコルの記述と検証 29 ある。
(ii)の証明:式
(3. 4
)と式(3.5)
の真偽は補題3. 1
より決定可能である 。 .
すべての動作について述語ぬ
(V
，A
，D)
什Qa(V
，A
，V '
，A '
，D)
と述語I (V
，A)
がそれぞれ命題3.1
の条件C 1
，C 2
を満たすシステムにおいて，条 件C3
の形をした述語P(V
，A)が 式 (3 .
4)，(3. 5
)を満たすならば，述語P(V
， A)は 強帰納的"であるという。命題
3. 1
は述語P(V
，A)
が不変式であるためのそれ自身決定可能な一つの 十分条件を示している。しかし，3.4
で示すように，条件C 1
，C 2
を満たす システムにおいて，述語P(V
，A)が条件C3
を満たしていてもその真偽は一般 に決定不能であるので，式(3 . 4)
，(3. 5
)は述語P(V
，A)
が不変式である ための必要条件ではない。一方，命題
3. 1
の十分条件をより広いものにすることは非常に難しい。なぜ なら，式(3.4)
のT
aの前に全称記号が一つ存在する形を許せば， ヒルベル トの第1 0
問題[12J(の否定形〉をP
配列式で表すことができるので，一般に真 偽は決定不能になる[ 8 1通常の
P r e s b u r g e r
の文[3Jの真偽判定の手数は，現在知られている最も能率 の良い一般的なアルゴリズム[9Jで2
22"( n
はP r e s b u r g e r
文の長さc
はc>1
なる定数〉である。P r e s b u r g e r
文が配列変数を含めば手数はさらにかかるが，本章の抽象的プロトコルの検証の例で、は，配列変数への代入操作は動作を表す 述語にしか現れず，かっ，その数は限られており，また，
P
配列式に現れる配 列変数のネストの深さも限られている。さらに 式(3. 4)
や 式 (3 . 5
)が 限定作用素を含まない P配列式(以下， この長さを n とする〉であることを 考慮すると，式 (3. 4 ) や 式 (3 . 5 )の真偽判定の手数は配列変数を消去し てOppenのアノレゴリズム[9Jを適用することにより 22"'"(p(n)はnの多項式〉で可能である。従って，本章で述べている具体例の真偽判定の手数の上界は
2
2 である。しかし，実際の例では，所与のP r e s b u r g e t r
文の特徴を利用する ことにより，より少ない手数で真偽判定が可能となる場合が多いであろう。30 第3章 プレスフ守ルガ配列式を用いたプロトコルの記述と検証
3 . 3
並行処理プログラムの検証システム
S
の述語O a C V
，A
，D) nQaCv
，A
，v '
，A '
，D)
やICV
，A)
が 条件C1
，C 2
を満たし，かつ，検証の対象となる述語PCV
，A)
も条件C3
を 満たしている並行処理プログラムの例として，S t e n n i n g
[川のプロトコルがあ る。プロトコルの正しさの検証に関しては，すべての状態変数についてその有 界性を前もって仮定しない抽象的プロトコルを書き[1.7J その抽象的プロトコ ルに対してそのレベルで、の正しさの検証を行い，それから具体的なプロトコル へ正しさを保存しつつ変換で、きることを形式的に議論できることが望ましい。抽象的プロトコルについて，
S t e n n i n g
はいくつかの述語が不変式であることを プログラムを直接解析することによって述べており，形式的な証明は示してい ない。以下では，S t e n n i n g
が示している述語が強帰納的，従って不変式である ことが，本章の決定可能な枠組みの中で形式的に議論できることを示す。3 . 3 . 1 Stenningの抽象的プロトコル
[プロ卜コルの仮定] 伝送中に起りうる誤りとしてメッセージの消滅，重複，
ピット誤りを仮定し， ピット誤りは受信側で必ず検出できるものとする。メッ セージや返事は必ずしも送信した順番には伝わらない。
[プロトコルの性質]
(1) 全
2
重のハイレベル通信制御手順に基づ、いたパケット通信志向形のプロ トコルで、ある。メッセージにそのシーケンス番号を付して送信する。(2) シーケンス番号は順に 1，2，…とし，無限に大きくなりうる。
(3) 送信したシーケンス番号ごとにタイマが用意されており，タイマの経過 時間を監視することによりメッセージの再送を行う。
[プロトコルに用いられる変数とシステム定数(図
3. 1
参照)]H:これまでに送信したメッセージのシーケンス番号の最大値を示す整数形の 状態変数。