数理解析研究所講究録1093 巻 1999 年 148-154

148

代数的仕様における振舞等価性証明のための
線形文脈帰納法について
坂部俊樹

二井靖彦

Yasuhiko Nii

Toshiki Sakabe

名古屋大学大学院工学研究科情報工学専攻
464-8603 名古屋市千種区不老町

nii@sakabe nuie nagoya-u .jp
sakabe@nuie nagoya-u .jp$.\mathrm{a}\mathrm{c}$$.\mathrm{a}\mathrm{c}$概要

等式の両辺が振舞等価であることを証明することは、 代数的仕様の実現検証において重要な役割を果たす。 本稿では、 線形文脈という限られた形の文脈の長さに関する帰納法による振舞等価性証明法を提案し、その有効性をいくつかの例で示すとともに、 Coinduction 法との関係について考察する。
キーワ一

1$\vdash’$: 代数的仕様、 振舞等価性、 文脈帰納法
本稿では、 線形来脈帰納法を用いた振舞等価性の検はじめに証法を提案し、 線形文脈帰納法が健全であることを示

代数的仕様の実現検証において、 実現の正しさとは与えられた仕様と実現を記述した仕様 (実現仕様) が振舞的に区別がつかないときであるとされる。 この振舞的な正す。 また、 線形文脈帰納法を用いた検証法の有効性をしさの関係は振舞実現関係 $[1, 2]$ といわれる。

に、 Coinduction 法の発見的な部分を解消するテスト集

振舞実現関係を検証するためには、 与えられた仕様の各公理の両辺が実現仕様のもとで振舞的に等価であることを証明すれば十分である。 2 つの式が振舞的に等価で合 Coinduction 法 $[5, 6]$ との比較も行う。

あるというのは観測可能な結果を返すすべてのテストによってそれらを区別できないことをいう [2]。したがっていくつかの例を用いて示すとともに、 線形文脈帰納法と Coinduction 法との間の関係について考察する。 さら2

振舞等価性と振舞実現関係
振舞的な枠組みにおける代数的仕様を振舞仕様とい振舞等価性を証明するためには、 あらゆる観測可能な文

い、 $\text{振舞仕様}SP$脈で表される、 すべてのテストに対して等価性を調べる$(S, F)$必要がある。 しかし、 無限に存在する観測可能な文脈す
べてについて等価性を調べることは、 一般には容易では蔽ソートの集合) 、公理の集合 $E$ からなる。

ない。

正しいということ、 すなわち、 両者は振舞実現の関係に

振舞等価性を検証する手法の 1 っに Coinduction 法[4] があるが、 これは隠蔽合同 [4] という概念を用いることにより、 振舞等価を間接的に扱い証明をしゃすくする手法である。 しかし隠蔽合同の発見は人間の力に依るところが大きく、 自動化しにくいという欠点がある。

あるということを検証することは、 与えられた仕様の公本研究では線形文脈という限られた形の文脈に対して等価性を調べることにより、 振舞等価性を検証する手法を提案する。 線形文脈とは、 文脈の根から穴までの経路
以外はすべて変数であるような文脈である。 このような文脈の根から穴までの長さに関する帰納法が線形文脈帰納法である。

$=$( $S=V\cup H,$$(\Sigma, V, E)$$V$は、 シグニチャ: 観測可能ソートの集合、$\Sigma$

$H$

$=$

:隠

与えられた振舞仕様に対して、 それを実現する仕様が理が実現のもとで振舞的に等価であるかどうかを検証することである。

まず最初に、 振舞等価性に必要な観測可能文脈を定義する。

定義 1(観測可能文脈 [3, 4])
観測可能文脈は観測可能ソートの項であり、 それは変数に加えて文脈の穴を表す隠蔽ソート $(s \in H)$ の変数(文脈変数$z_{\delta}$項からなり、または I) のちょうど 1 回の出現を含む$c[z_{s}]$または$c\mathrm{I}$で表し、 観測可能文脈の集

149
合を

と表す。 また、 文脈 $c[z_{S}]$ の中の$C_{\Sigma}^{obs}$$T(\Sigma, X)$$z_{s}$

を項

$t$

$\in$

定義 5(線形文脈 〈観測可能線形文脈〉 )で置き換えて得られる項を $c[t]$ と表す。

この観測可能文脈を用いて 2 つの要素の間の振舞等価性を次のように定義する。

線形文脈は次のように定義される文脈である。 ここ: 観測可能ソートの関数とで、 $f$ : 隠蔽ソートの関数、する。

1. I (隠蔽ソートの文脈変数) は線形文脈である。

定義 2(振舞等価性 [3, 4])
次の条件を満たす代数 $A$ 上の関係
係であり、
$a,$

$a$

$\approx$2.

は振舞等価関と $a’$ は振舞等価であるという。 ここで、が線形文脈のとき、$f(x_{1}, \cdots, X_{i-l}, C\square , xi+1, \cdots x_{n})$る。

た、 $V$ を観測可能ソートの集合、 $H$ を隠蔽ソートの集
上の

合とする。

$c\mathrm{I}$sort $(c\mathrm{I})=sort(x_{i})$ ならば$a’\in A$ とし、 sort $(a)$ を $a$ のソートを表すとする。 ま1. sort$\mathit{1}_{\text{、}}$$(a)=\mathrm{s}\mathrm{o}\mathrm{r}\mathrm{t}(a^{l})=v\in V$

のとき、

また、

は線形文脈であ(ここで、 $x_{i}(1\leq i\leq n)$ は新しい変数 )2 を繰り返して構成される文脈が線形文脈であり、 線形文脈の集合を$a\approx_{v}.a’$$\delta$$\mathrm{c}\mathrm{I}$と表す。

$C_{\Sigma}^{lin}$が線形文脈で$s\sigma rt(\mathrm{C}\mathrm{I})=sort(y_{j})$のとき、$\Leftrightarrow a=a’$を観測可能な線形文脈(
ここで、$y_{\mathrm{j}}(1\leq
j\leqm)$ は新しい変数。 )という。

$\delta(y_{1}, \cdots, yj-l, c\square , y_{j}+1, \cdots, yn)$

2. sort$(a)=\mathrm{s}\mathrm{o}\mathrm{r}\mathrm{t}(a;)=h\in H$$a\approx_{h}$$a’\Leftrightarrow\forall c\mathrm{I}\in c_{\Sigma}^{ob_{S}},$のとき、$c[a]=c[a^{l}]$上で定義された線形文脈
長さ$c\mathrm{I}$の、 根から穴までの文脈のに関する帰納法が、 線形文脈帰納法である。 形式
的には、 SPI $=(\Sigma I, EI)$ がの振以上から、 振舞実現は次のように定義される。

$|c|$$\mathrm{S}\mathrm{P}=(\Sigma, E)(\Sigma\subseteq\Sigma I)$

定義 3(振舞実現 [3])$sP=(\Sigma, V, E)\text{、}SPI=(\Sigma I, VI, EI)(\Sigma\subseteq\Sigma I)$

仕様、$E_{\text{、}}EI$をそれぞれ仕様$SP_{\text{、}}$を振舞

舞実現であることの証明の概略は次のようになる。 ここ
で、 $c[],$$SPI$ の公理の集合とをする。 また、 $V\subseteq VI$ を観測可能ソートの集合とする。

仕様 $SP$ のすべての公理を振舞的に満たす代数を$SP$の振舞モデルといい、 $SP$ の振舞モデルの集合を立つならば、 $SPI$ は $SP$ の振舞実現であるという。

$\delta\in\Sigma$$\mathrm{C}^{l}\mathrm{I}\in C_{\Sigma}^{lin}\text{、}$を観測可能関数、$d_{1},$$\cdots$,$d_{n}$の引数とする。

証明の概略:$\mathrm{E}$のすべての等式 $(l=r)$ に対して、 以下のことを証明する。

$Beh(SP)$ とかく。 また、 $Beh(SPI)\neq\emptyset$ とする。

このとき、 $\forall B\in Beh(SPI),$ $B|_{\Sigma}\in Beh(SP)$ が成り$\delta$-

基底段階: 線形文脈の根からI までの長さ $|c|=0$ のとき、 すなわち、 線形文脈がのとき、$\mathrm{I}$sort $(\mathrm{I})=SOTt(di)$ ならば振舞実現を形式的に定義するとこのようになるが、のままでは検証がしにくい。 そこで、 振舞実現に関する
こ

次の定理が [3] で証明されている。

$SPI\backslash \vdash\delta(d_{1}, \cdots, d_{i-1}, \iota, d_{i+1}, \cdots, d_{n})$$=\delta(d_{1}, \cdots, d_{i-1}, r, di+1, \cdots, d_{n})$が成り立つことを証明する。

$SPI$ を代数的仕様、 $E$ を仕定理 4[3]$SP$様の公理の集合とする。 ここで、 を基礎代入とす$SP=(\Sigma, E)\text{、}$$\sigma$

帰納段階: 線形文脈の根からI までの長さ$|c|$が$\mathrm{n}$以下のとき成り立つと仮定する。

る。
$SPI\vdash\delta(d_{1}, \cdots, d_{i-}1,c[l],di+1, \cdots , d_{n})$.

仕様 $SPI$ 3:仕様 $SP$ の振舞実現である。

a,$|\mathrm{c}’|=n+1$$\forall(l=r)\in E,\forall C\mathrm{I}\in C_{\Sigma}^{ob\epsilon},\forall\sigma$$SPI\vdash c[\sigma(l)]=c[\sigma(r)]\cdots(*)$

この定理により、 式$(^{*})$$SPI\vdash\delta(d_{1}, \cdots, d_{i}-1, c[’\iota], di+1, \cdots, dn)$が成り立つことがいえれば振線形文脈帰納法
定理 4 により、のとき、 sort $(c\mathrm{I}l)=sort(d_{i})$ ならばが成り立つ。

舞実現関係を証明できる。

3$=\delta(d_{1}, \cdots , d_{i-1},\mathrm{C}[r],d_{i}+1, \cdots,d_{n})\cdots \mathrm{I}.\mathrm{H}$$=\delta(d_{1}, \cdots, di-1, c[’]r, d_{i+1,n}\ldots, d)$が成り立つことを証明する。
以上の 2 つ段階における命題を、 仕様 SPI の等式を用いた書き換えのみで証明する。
補題 6が成り立つことを証明すれば振舞実現を検証できるが、 これを証明するには、 無限に存在する観測可能な文脈をすべて用いなければならない。 そ$(^{*})$

こで、 我々は無限に存在するすべての文脈を用いるかわ

りに、 線形文脈という文脈を用いて証明する手法を提案する。 線形文脈とは、 文脈の根から穴までのノードには$\Sigma$をシグニチャ、$g$を観測可能関数、$c$[ を根から穴までのノードに観測可能関数力旬つも含まれない文脈とで表されるような文脈の
$D$
集合を
で表す。
集合 $D$ の文脈と観測可能文脈について次のことが成りする。 このとき、$g(\cdots, c\mathrm{I}, \cdots)$

立つ。 ここで、は$\mathcal{B}$$\Sigma$

代数、$l,$ $r\in \mathcal{T}(\Sigma, X)$とする。

関数記号が入り、 それ以外の葉のところにはすべて変数が入る様な形をしている文脈である。

$\forall c\in D,$$B\models c[l]=c[r]$$\Leftrightarrow$$\forall c\in c_{\Sigma}^{\mathrm{o}b\delta},$$B\models c[l]=c[r]$

150
証明

については明らか。 よって、$\Leftarrow$$\Rightarrow$

について不

よって、

す。

$\forall\phi:\mathcal{T}(\Sigma, X)arrow A,$ $\phi(c[\iota])=\emptyset(C[r])$定義より、これと仮定より、$D\subset C_{\Sigma}^{\mathrm{o}bs_{\text{。}}}$$c\in(C_{\Sigma}^{obs}\cap$

であるような文脈については明らかに成り立つ。 よっ$D)$が成り立つので、 次のことが言える。

て、 $c\in(C_{\Sigma}^{obS}-D)$ について示す。 このとき、 次のこと

がいえる。

(2)

$A \models c[\oint]=C[r]$また式 (2) と補題 6 より、$\forall c\in(C_{\Sigma}\circ bs-D),$ $\exists c’\in D,$

ここで、$\forall c\in D,$$c\mathrm{I}|_{p}$は文脈る。 このとき、$c\mathrm{I}$を$c\mathrm{I}$の位置$C”1c^{l}\mathrm{I}$$\exists p,$$\mathrm{P}$(1)$c\mathrm{I}|_{P}=c’\mathrm{I}$における部分文脈とす] と表すとする。

仮定より、 $\mathcal{B}\models c’[l]=c’[r]$ であるから、 両辺に同じを被せても成り立つ。 よって、
文脈$\forall c\in C_{\Sigma}^{\mathrm{O}}b\epsilon,$$A\models C[\iota]=c[r]$が成り立つ。 以上から、 定理は証明された。

この定理により線形文脈帰納法で証明が成功すれば、 す

べての文脈に対する帰納法で証明が成功することがいえ$c”\mathrm{I}$$B\models C’’[c[’\iota]]=c’[\prime C[r]]$が成り立ち、$\Rightarrow$についても成り立つことが言える。 以上から補題は証明された。

続きを示す。

が線形ならば各項で置き換える。

$\mathrm{c}’\mathrm{I}$$\Delta/\Gamma$$\Delta/\Gamma$: 観測可能関数とする。
$t_{i}$

線形文脈帰納法を用いた証明例

本節では、 線形文脈帰納法による証明の手順を、完全な仕様とスタックの、 2 つの例を用いて説明する。

ここで、 $c\mathrm{Q}\equiv f(t_{1}, \cdots, C’\mathrm{I}, \cdots, t_{n})$ とし、$t_{i}\in T(\Sigma, X)(1\leq i\leq n),$ $f$$\mathrm{c}’\mathrm{I}$を用いて説明する。

4

定義 7(集合 $D$ の文脈の線形化)
文脈叶 $\in D$ は次の手続きで線形化される。

2.

線形文脈帰納法は上の証明の概略にしたがって証明が進んでいく。 次節では線形文脈帰納法による証明法を例

次に、集合 $D$ に含まれる文脈の線形化に関する次の手1.

る。

をそれぞれ新しい変数

完全な仕様は、 線形文脈帰納法で完全に自動化できる例であり、 スタックは、 証明の際、 補題を必要とす$x_{i}$

るが、 その補題も自動的に発見し、 証明も自動化が行えるという例である。

が線形でないならば、$\mathrm{c}’\mathrm{I}$を線形化して 1 に戻

る。

41

定義 9(

次に線形文脈帰納法に関する次の定理を示す。

完全な仕様$\triangle/\Gamma$

完全 [4])$\Delta/\Gamma$

仕様 $SP$ のすべての等式が次のような形をしていると定理 8(線形文脈帰納法による証明法の健全性)

き、 $SP$ は$\Delta/\Gamma$

完全であるという。
$\delta(m(x))=t$$\forall(l=r)\in E,\forall C\in CinsP\prime \mathrm{t}\Sigma’ I\models C’[l]=C[lr]$

ここで、$\Downarrow$$\forall(l=r)\in E,\forall c\in C_{\Sigma^{b}}os,$$SPI\models c[\iota]=C[r]$数の集合、$\Delta/\Gamma$が成り立つ。 (ここで、とする。 )$C_{\Sigma}^{lin}$は観測可能線形文脈の集合: 観測可能関数の集合、 $m\in\Gamma$ : 隠蔽関を観測可能な関数のみからなる項とする。

$\delta\in\Delta$$t$

完全な仕様の例としては、 旗の状態を表す Flagの仕様と 2 っのメモリセルを持った状態の仕様がある。

完全な場合の線形文脈帰納法によ
ここでは、仕槌がる振舞等価性証明として、 Flag の仕様を例にとって説明$\Delta/\Gamma$

証明

代数 $A$ を仕様 $SPI$ のモデルとする。

仮定より、 $A\models c’[l]=c’[r]$ がいえるので、 次の式がする。

例 10 (Flag)

成り立づ。

旗の状態を表す仕様記述 FLAG を下に示す。

$\forall\phi:\mathcal{T}(\Sigma, x)arrow A,$ $\phi(c’[\iota])=\emptyset(C’[r])$フラグの仕様ここで、 定義 7 より集合 $D$ に含まれるすべての文脈 $c\in$に対して次のような代入が存在する。
脈$D$$\sigma$:$Xarrow.\mathcal{T}(\Sigma, X)$と線形文$c’\in C_{\Sigma}^{lin}$$\mathrm{c}\mathrm{I}=\sigma(C’\mathrm{I})$ここで、$\phi(c[l])$$\sigma$は準同型写像より、$=\phi 0\sigma(C^{l}[\iota])$$=$$\phi(\sigma(c’[l]))$$=$$\phi\circ\sigma(_{C[r])}l=\phi(\sigma(c^{l}[r]))=\phi(c[r])$th FLAG is sort Flag

DATA(up-) ($\mathrm{p}\mathrm{r}$

ops
op
var
eq
eq
eq
endth

.
(rev-)$\mathrm{d}\mathrm{n}_{-)}$: Flag $->$ Bool$\mathrm{u}_{\mathrm{P}^{7}-}\downarrow$$\mathrm{F}$: Flagup$\mathrm{F}=$up? dn$\mathrm{F}=$$\mathrm{u}\mathrm{p}^{?}$

up? rev

true
false
not

$\mathrm{F}=$: Flag $->$ Flag

.

(F1)

$\mathrm{u}\mathrm{p}^{?}\mathrm{F}$

.

(F2)

(F3)

151
$ops,\mathit{0}_{P}$$(F\mathit{3})$が関数、 $var$ が変数とその型の宣言、 $(Fl)\sim$.

が公理を表している。

このとき、仕様 FLAG のモデルが次の等式を振舞的に満たすこと、 すなわち、 仕様 FLAG のもとで次の式の両辺が振舞等価であることを証明する。

op top- : Stack $->$ Nat
op pop- : Stack $->$ Stackvarvar: Stack: Nat
eq top push(N,S)
eq pop empty empty
eq pop push(N,S)$\mathrm{S}$$\mathrm{N}$$=\mathrm{N}$

.

(S1)

(S2)

$=$

(S3)

$=\mathrm{S}$

rev

(3)

$(\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{f}))=\mathrm{f}$証明 式 (3) の両辺が振舞等価であること、 すなわち定理

4, 定理 8 より

endth

ポインタと配列によるスタックの仕様

th$\mathrm{F}\mathrm{L}\mathrm{A}\mathrm{G}\vdash \mathrm{u}\mathrm{p}?(\mathrm{c}[\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{r}\mathrm{e}\mathrm{V}(\mathrm{f}))])=\mathrm{u}\mathrm{p}?(\mathrm{c}[\mathrm{f}])$is sort Stack$\mathrm{P}\mathrm{T}\mathrm{R}||\mathrm{A}\mathrm{R}\mathrm{R}$$\mathrm{p}\mathrm{r}$ARR

op: Nat Arr $->$ Stack [prec 10]
op empty : $->$ Stackop push : Nat Stack $->$ Stack .
op top- : Stack $->$ Nat
op pop- : Stack $->$ Stackvar I: Nat . var A : Arr$-||_{-}$

が成り立つことを線形文脈の長さ$|c|$に関する帰納法で証明する。

$-Base:|c|=0$ のとき、 すなわち線形文脈が [のとき、次式を証明。

$\mathrm{N}$(4)$\mathrm{u}\mathrm{p}?(\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{r}\mathrm{e}\mathrm{V}(\mathrm{f}))=\mathrm{u}\mathrm{p}?(\mathrm{f})$$Ind.:|c|=n$ の時成り立つと仮定する。

.. .

.
$n+1$ のとき、 線形文脈の根における場合分けによ$\mathrm{u}\mathrm{p}^{\uparrow}(\mathrm{C}[\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{f}))])=\mathrm{u}\mathrm{p}?(\mathrm{c}[\mathrm{f}])$

り、 次の 3 つの場合、 すなわち線形文脈が uP$\mathrm{d}\mathrm{n}(\mathrm{c}\mathrm{I})_{\text{、}}$

rev(叶) の場合を考えれば十分である$\circ$$\mathrm{I}.\mathrm{H}$$(\mathrm{C}\mathrm{I})_{\text{、}}$

よって

eq
eq
eq
eq
eq
eq

nil
empty $=0$
(
A)
,
I
I
push
I
A
A [I]
top
} A $=0$
top
I
A
I
pop
A
A $=0||$ A
pop
$||$

$||$

$\mathrm{N}$$\mathrm{s}$

$0$

$||$

$=$

$||$

$=$

$0$

$\mathrm{u}\mathrm{p}?(\mathrm{d}\mathrm{n}(\mathrm{c}[\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{f}))]))$

up?(rev($\mathrm{c}[\mathrm{r}\mathrm{e}\mathrm{v}$(rev$(\mathrm{f})$

) ))
$]$

$=$

(5)

$=$

$\mathrm{u}\mathrm{p}?(\mathrm{d}\mathrm{n}(\mathrm{c}[\mathrm{f}]))$

(6)

$=$

$\mathrm{u}\mathrm{p}?(\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{C}[\mathrm{f}]))$(7).

$(\mathrm{S}\mathrm{I}2)$$(\mathrm{S}\mathrm{I}3)$$(\mathrm{S}\mathrm{I}4)$$||$$(\mathrm{S}\mathrm{I}5)$$||$$(\mathrm{S}\mathrm{I}6)$endth
このとき、 仕様$\mathrm{u}\mathrm{p}?(\mathrm{u}\mathrm{p}(\mathrm{C}[\mathrm{f}]))$

put$(\mathrm{N}, \mathrm{I},\mathrm{A})$$|$$\mathrm{s}$以下の式を証明する。
$\mathrm{u}\mathrm{p}?(\mathrm{u}\mathrm{p}(\mathrm{c}[\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{f}))]))$$(\mathrm{S}\mathrm{I}1)$$||$$=\mathrm{s}$$\mathrm{P}\mathrm{T}\mathrm{R}||\mathrm{A}\mathrm{R}\mathrm{R}$が仕様 STACK を振舞的に実現していることを証明する。

定理 4, 定理 8 より式 (8) が成り立つことを線形
文脈の長さに関する帰納法で証明すればよい。 ここ
証明$|\mathrm{c}|$以上の 4 つの式が成り立つことが証明され、 よって仕様
FLAG は式 (3) を振舞的に満たすことが示された。

で、 $E=\{(S1), (S2), (S3)\}$ である。
$\forall(l=r)\in \mathrm{E},\forall c\in c_{\Sigma}^{\iota in}\mathrm{s}\mathrm{T}\mathrm{A}\circ\kappa$

’

このように

$\Delta/\Gamma$

完全な仕様の場合においては、 線形文脈

帰納法を用いて証明が可能であり、 線形文脈の長さに関$\text{する素朴な帰納法_{のみ}を用_{い}ているので証明の}\ovalbox{\tt\small REJECT}$
自動化が

式 $(Sl)$ に対しては、 両辺は観測可能な項であるので$-$

次の式を直接示せば良い。

可能である。

42(8)$(\mathrm{P}\mathrm{T}\mathrm{R}||\mathrm{A}\mathrm{R}\mathrm{R})\vdash c[l]=c[r]$

top

スタック

ここでは、 スタックの仕様と配列とポインタを用いて実現したスタックの仕様が振舞実現の関係にあることを証明する。 この例は証明の際補題を必要とし、 その必要

$-$

$=$

$(\mathrm{p}\mathrm{u}\mathrm{s}\mathrm{h}(\mathrm{n},\mathrm{i}||\mathrm{a}))$$\mathrm{n}$式ぴ 2) に対する証明。

1. $Base:|c|=0$ のときすなわち線形文脈が I のとき、 次の式を証明。

な補題が証明の過程で発見できる揚合の例である

top

例 11 (スタック)
スタックの仕様 STACK と、 配列とポインタによりスを下に示す。
タックを実現した仕様$\mathrm{P}\mathrm{T}\mathrm{R}||\mathrm{A}\mathrm{R}\mathrm{R}$$(\mathrm{P}^{\mathrm{o}}\mathrm{p}(\mathrm{e}\mathrm{m}_{\mathrm{P}}\mathrm{t}\mathrm{y}))$$=$top(empty)

2. $Ind.:|c|=n$ の時成り立つと仮定する。
top$(\mathrm{c}[\mathrm{P}\mathrm{o}\mathrm{p}(\mathrm{e}\mathrm{m}\mathrm{p}\mathrm{t}\mathrm{y})])=\mathrm{t}\mathrm{o}\mathrm{p}(\mathrm{c}[\mathrm{e}\mathrm{m}\mathrm{p}\mathrm{t}\mathrm{y}])$$\mathrm{I}.\mathrm{H}$.

スタックの仕様th STACK $is$ sort Stack
DATA$\mathrm{p}\mathrm{r}$op empty : $->$ Stackop push : Nat Stack $->$ Stack

線形文脈の長さが $n+$$1$のとき、 線形文脈の穴の直前における場合分けにより、 線形文脈が$\mathrm{c}(\mathrm{p}\mathrm{o}\mathrm{p}\mathrm{I})\text{、}\mathrm{c}(\mathrm{p}\mathrm{u}\mathrm{S}\mathrm{h}(\mathrm{m}, \mathrm{I}))$の 2 つの場合を考えれば十分である。 よって以下の式を証明する。

152
top ( [push$\mathrm{c}$$(\mathrm{m}$Coinduction 法 [4]5.1$\mathrm{t}_{0}\mathrm{p}(\mathrm{C}[\mathrm{P}^{\mathrm{o}\mathrm{p}}(\mathrm{p}\mathrm{o}\mathrm{p}(\mathrm{e}\mathrm{m}\mathrm{p}\mathrm{t}\mathrm{y}))])=\mathrm{t}\circ \mathrm{p}(_{\mathrm{C}}[\mathrm{P}\mathrm{o}\mathrm{p}(\mathrm{e}\mathrm{m}_{\mathrm{P}^{\mathrm{t}\mathrm{y})])}}$, pop (empty))])

直観的には、 Coinduction 法は隠蔽合同という概念を用いて振舞等価性を間接的に扱うことにより、 検証をし$=\{\circ \mathrm{p}(_{\mathrm{C}[_{\mathrm{P}^{\mathrm{u}\mathrm{s}}}}\mathrm{h}(\mathrm{m}, \mathrm{e}\mathrm{m}\mathrm{p}\mathrm{t}\mathrm{y})])$

式ぴ 3) に対する証明。

ゃすくしょうとする手法である。

1. $BaSe:|c|=0$ のときすなわち線形文脈が I のと

定義 13 (隠蔽合同 [4])き、 次の式を証明。 ここで $s=i||a$ とする。

top

$=$

$(\mathrm{P}^{\mathrm{o}}\mathrm{p}(\mathrm{P}\mathrm{u}\mathrm{s}\mathrm{h}(\mathrm{n},\mathrm{i}||\mathrm{a})))$

top

代数 $A$ 上の合同関係$a,$$(\mathrm{i}||\mathrm{a})$2. $Ind.:|c|=n$ の時成り立つと仮定する。
top$a\cong_{v}$$(\mathrm{c}[\mathrm{P}^{\mathrm{O}}\mathrm{p}(\mathrm{P}\mathrm{u}\mathrm{s}\mathrm{h}(\mathrm{n},\mathrm{i}||\mathrm{a}))])=\mathrm{t}\mathrm{o}\mathrm{p}(\mathrm{C}[\mathrm{i}||\mathrm{a}])\cdots \mathrm{I}.\mathrm{H}$.

$\cong$は、 任意の観測可能な要素にたいして、$a’$$a’\Leftrightarrow a=a’$を満たすとき、 隠蔽合同であるという。 ここで、 $a,$ $a’\in$$A_{v\text{、}}v$: 観測可能ソートとする。

線形文脈の長さが $n+1$ のとき、 線形文脈の穴の直前における場合分けにより、 以下の式を証明す

また、 次の定理が [4] で証明されている。

る。

定理 14 [4] 振舞等価関係は、 最大の隠蔽合同である。

top$=\mathrm{t}\mathrm{o}\mathrm{p}(\mathrm{C}[_{\mathrm{P}^{\mathrm{O}}}\mathrm{p}(\mathrm{i}||\mathrm{a})])$

top

この定理により、 隠蔽合同であるような関係を見つけれ$(\mathrm{C}[\mathrm{p}\mathrm{o}\mathrm{p}(\mathrm{p}\circ \mathrm{P}(\mathrm{P}\mathrm{u}\mathrm{s}\mathrm{h}(\mathrm{n},\mathrm{i}||\mathrm{a})))])$(9)$(\mathrm{c}[\mathrm{P}\mathrm{u}\mathrm{s}\mathrm{h}(\mathrm{m}, \mathrm{p}\mathrm{o}\mathrm{P}(\mathrm{P}^{\mathrm{u}}\mathrm{s}\mathrm{h}(\mathrm{n},\mathrm{i}||\mathrm{a})))])$ば、 それを用いて振舞等価性を証明できる。

Coinduction 法による振舞等価性証明の概略を以下にの公理 のすべての等式が、 SPI の示す。 つまり、
もとで振舞等価であることを証明する。 ここで、 SPを仕様、 SPI を SP を実現する仕様とする。
$\mathrm{E}$$\mathrm{S}\mathrm{P}$$=\mathrm{t}\mathrm{o}\mathrm{p}(\mathrm{c}[\mathrm{p}\mathrm{u}\mathrm{s}\mathrm{h}(\mathrm{m},\mathrm{i}||\mathrm{a})])$$=$

ここで式 (9) の証明の際、 下の補題が必要となる。 この補題は式 (9) の証明の過程において次の式が成り立ってほしいことから発見される。

top ( .IIput$\mathrm{c}\beta$$(\mathrm{n},\mathrm{s}(\mathrm{i}),\mathrm{a})]$)$=\mathrm{t}\mathrm{o}\mathrm{p}(_{\mathrm{C}\mathrm{b}||\mathrm{a}}.])$

補題 12 次の式の両辺は振舞等価である。

if$\mathrm{i}\mathrm{l}||\mathrm{p}\mathrm{u}\mathrm{t}(\mathrm{n},\mathrm{i}2, \mathrm{a})=\mathrm{i}\mathrm{l}||\mathrm{a}$た、 振舞等価性の公理化に関する定理が [1J で証明されており、 この定理は振舞等価なものを公理として用いて良いということを保証しているので、 上の証明の中でこ$\ovalbox{\tt\small REJECT}$

証明の概略:

1. 隠蔽合同の候補が証明される。

以上から上のすべての式が証明され、 よって、 仕様
は仕様 STACK を振舞的に実現することが$\mathrm{P}\mathrm{T}\mathrm{R}||\mathrm{A}\mathrm{R}\mathrm{R}$証明された。

$\mathrm{R}$を見つけ、 それが隠蔽合同であることを証明する。

2. $\forall(l=r)\in E,$$l\mathrm{R}r$

であることを証明する。

ここで問題となるのが、 人間が隠蔽合同

をいかにう

テスト集合 Coinduction 法 $[5,6]$

52

テスト集合 Coinduction 法は、 Coinduction 法におを自動的に振舞等価として構成する手法
ける隠蔽合同である。 直観的に言えば、 観測可能文脈全体の集合の中から必要不可欠な文脈を選びだし、 それから振舞等価を$\mathrm{R}$

構成するのがテスト集合 Coinduction 法である。
テスト集合 Coinduction 法は次の順にしたがって振舞
等価を構成する。 詳細は文献 $[5, 6]$ を参照されたい。
$\bullet$

形文脈帰納法を用いて振舞実現関係を検証できる。 また
これは、 検証の際補題が必要となるがその補題もまた証明の流れの中で発見することができ、 その補題自身も線$\mathrm{R}$

まく発見するかということである。

このように、 このスタックの仕様のような例もまた、 線与えられた仕様の、 条件 (Definition71[6]) を満たす等式から文脈書換えシステムを構成する。
$\bullet$

形文脈帰納法で証明することができるという例である。
したがって自動的な証明が可能な例であるといえる。
$\bullet$

5(SPI 上の) 関係$\mathrm{i}2\geq \mathrm{i}\mathrm{l}$この補題はあとで紹介する Coinduction 法によるスタックの例の証明において使われる補題と同じ補題である。 この補題もまた線形文脈帰納法で証明できる。 まの補題を用いることができ、 式 ($(\Sigma, E)$

振舞等価を構成するために必要な文脈をカバーするような集合 (カバー集合) を構成する。
カバー集合からテスト集合を構成する。
を満たすカテスト集合は条件
バー集合である。 この条件は直観的には、 集合の$(\mathrm{D}\mathrm{e}\mathrm{f}\mathrm{i}\mathrm{n}\mathrm{i}\mathrm{t}\mathrm{i}\mathrm{o}\mathrm{n}74[6])$他の証明法との比較
振舞等価性を検証する手法の 1 つとして Coinduction

法 [4] が知られている。 そこで、 例を用いて Coinduction.

要素の長さに関する条件である。

テスト集合を元に振舞等価を構成する。

法による証明と線形文脈帰納法による証明過程を比較し、 両証明法の間にどのような関係があるか考察する。

最後に証明したい式がここで求めた振舞等価の関係にあ

さらに、 テスト集合 Coinduction 法とも比較する。

ることを、 実現仕様の等式を用いて証明する。

153
53

線形文脈帰納法との比較

次に、 証明の際補題を必要とする例である例 11 を先ほどと同じ例を用いて Coinduction 法による振舞等価性の証明と線形文脈帰納法による証明とを比較し、 また、 スタックの例に対してテスト集合 Coinduction 法と線形文脈帰納法を比較する。

\Delta /\Gamma 完全な仕様について比較してみ完全な仕様の場合、 Coinduction 法では隠蔽

まず、 最初にる。

合同$\Delta/\Gamma$を自動的に決めることができるので、 テスト集合$\mathrm{R}$

Coinduction 法を用いる必要がなくなる。
例 10 を Coinduction 法で証明すると次のようにな

Coinduction 法とテスト集合 Coinduction 法で証明し、線形文脈帰納法による証明法と比較する。
例 16 (スタック)

例 11 の仕様$\mathrm{P}\mathrm{T}\mathrm{R}||\mathrm{A}\mathrm{R}\mathrm{R}$が仕様

STACK を振舞的に実現していることを証明する。

Coinduction 法による証明: この例の場合、 Coinduction 法でも補題 12 を用いて証明する。 しかし Coinduction 法ではこの例に適している補題として補題 12 を人間が発見してやらなければならない。

る。

例 15 ($\Delta/\Gamma$

1. まず、 隠蔽合同の候補 関係

完全な仕様 (Flag))

式 (1) の両辺が仕様 FLAG のもとで振舞等価であるこを次のように定$R$遣する。 ここで、 ,il, はソート.Nat の変数、はソート $:Arr$ の変数であるとする。
$i$$i\mathit{2}$$a,al,a\mathit{2}$とを $Coinductio\dot{n}$ 法により証明する。

il$\mathrm{R}i2$$=$$i\mathrm{l}==i2$$(\mathrm{O}||a1)\mathrm{R}(i||a2)$$=$$I==0$$(i||a)\mathrm{R}(i||a)$

$=$

true

$(s(i1)||a1)\mathrm{R}(s(i2)||a2)$$=$$(i\mathrm{l}==i2)$A$(a1[i1]==a2[i2])$$\wedge$$((i1||a1)\mathrm{R}(i2||a2))$

まず、 隠蔽合同の候補 関係 $R$ を次のように定義す-る。 ここで、 $f,f$ ’ はソート:Flag の変数であるとする。
$f\mathrm{R}f’$

$=$

(10)

$(\mathrm{u}\mathrm{p}?(\mathrm{f}))==(\mathrm{u}\mathrm{p}?(\mathrm{f}’))$

次にこの関係 $R$ が隠蔽合同であることを示すために、$f1\mathrm{R}f2$が成り立っているとき、 以下の式が成り立つ

ことを証明する。
$\mathrm{u}\mathrm{p}?(\mathrm{f}\mathrm{l})$up$(\mathrm{f}\mathrm{l})$.

(dn(fl)(
rev(fl)

(
-

$=$

(11)

$\mathrm{u}\mathrm{p}?(\mathrm{f}2)$

がup(f2)$\mathrm{R}$$\mathrm{u}\mathrm{p}?(\mathrm{u}_{\mathrm{P}}(\mathrm{f}1))=\mathrm{u}\mathrm{p}?(\mathrm{u}\mathrm{p}(\mathrm{f}2))$$\Leftrightarrow$$\mathrm{u}\mathrm{p}?(\mathrm{d}\mathrm{n}(\mathrm{f}\mathrm{l}))=\mathrm{u}\mathrm{p}?(\mathrm{d}\mathrm{n}(\mathrm{f}2))$$\Leftrightarrow$) (13)

rev(f2)$\mathrm{R}$)$\mathrm{u}\mathrm{p}?(\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{f}\mathrm{l}))=\mathrm{u}\mathrm{p}?(\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{f}2))$$\Leftrightarrow$

次に、 式 (3) の両辺がここで定義した $R$ の関係にある明する。

を定めたときに、 補題 12 の両辺の関係にあることを証明する。

$\mathrm{i}\mathrm{l}||\mathrm{p}\mathrm{u}\mathrm{t}(\mathrm{n},\mathrm{i}2, \mathrm{a})\mathrm{R}\mathrm{i}\mathrm{l}||\mathrm{a}$3. この関係$R$

if$\mathrm{i}2\geq \mathrm{i}\mathrm{l}$が隠蔽合同であることを示す。

4. 仕様 STACK の (Sl)\sim (s のすべての等式の両る。

結果的に以上が成り立つことがいえ、 よって、 仕様$\mathrm{P}\mathrm{T}\mathrm{R}||\mathrm{A}\mathrm{R}\mathrm{R}$が仕様 STACK を振舞的に実現していることが示された。

$(\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{f}))$($\mathrm{R}$$\Leftrightarrow$$\mathrm{f}$$\mathrm{u}\mathrm{p}?(\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{r}\mathrm{e}\mathrm{v}(\mathrm{f})))=\mathrm{u}\mathrm{p}?(\mathrm{f})$) (15)

結果的に以上が成り立つことがいえ、 よって、 仕様

FLAG は式 (のを振舞的に満たすことが示された
このように、$R$辺がここで定義した $R$ の関係にあることを証明す(14)ことを証明する。 すなわち次の関係が成り立つことを証

rev

$R$

) (12)dn(f2)$\mathrm{R}$

2. このように関係$\Delta/\Gamma$

完全な仕様の場合、 両証明法とも自動的な証明が可能である。 さらに、 線形文脈帰納法による証明と比較してみると、 上の式 (15) が線形文脈帰納法の基底段階の式 (4) に対応している。 また、 式 (12)$\sim$(14) が線形文脈帰納法の帰納段階の式 (5) $\sim(7)$ にそれぞれ対応していることがわかる。 このことから、$\Delta/\Gamma$

完

全な仕様の場合振舞実現の線形文脈帰納法による証明とCoinduction 法による証明が自然に対応がとれ、 -方の証明スキームから他方の証明スキームを導くことができることがわかる。

テスト集合 Coinduction 法による証明:

次にテスト集合 Coinduction 法で振舞等価 $R$ を構成する。

1. 等式ぴ 1)(S 砂から文脈書換え規則を作ると次のようになる。 このとき、 隠蔽ソートの変数を穴と見なして分岐のない列をつくり、文脈として扱う。

top$push_{\backslash }’n$)$\mathrm{I}arrow\phi$

pop push$(n)\mathrm{I}arrow\psi$

2. カバー集合を構成すると次のような集合になる。
$\{(top, \{push(n),pop\})\}$(16)

3. カバー集合からテスト集合を構成する。 この例の場合、 テスト集合の条件にあてはまるカバー集合
もまた (16) の集合となる。

154
4. 文脈書換え規則により、 除去可能片と壁に分け化向きり、壁は PoP となる。

においては心証明法の対応が自然に取れ、 –方から他方の証明スキームを構成できることを示した。

よって、 ($\mathit{1}\ovalbox{\tt\small REJECT}$の集合から、 除去可能片を取り除いとなり、 こた集合が、 カバ一集合$\{(t_{\mathit{0}}p, \{po_{P}\})\}$

れから振舞等価を構成すると次の式 (17) になる。

$sRt=$ (top $s^{:}=topt$ )5. この振舞等価$R$$\wedge$($popsR$ pop ) (17)$t$を用いて、 仕様 SZACK のすべ$\dot{\text{で}}$あると思われる。、また、$\Delta/\Gamma$

完全な仕様の場合

また、 テスト集合 Coinduction 法では、 振舞等価を構成するのに必要な文脈を絞り込み、 自動的に振舞等価の適切な形を構成できるが、 絞り込んだ文脈が無限に存在する場合、 帰納法が必要となる。 -方、 線形文脈帰納法
は、 簡潔な帰納法による証明が可能なので、 両証明法のての等式の両辺が $R$ の関係にあることを仕様

効率については、 大きな差はないように思われる。

$PTR||ARR$ の等式を用いて証明する。
このとき、 振舞等価が帰納的な定義になっている

形文脈帰納法ではそのような条件を必要としないので、ため、 帰納法や補題が必要となる。

線形文脈帰納法を用いることができる仕様め幅が、 テス.

これがテスト集合 Coinduction 法によるスタックの振舞実現の検証である。
スタックの例の場合、 線形文脈帰納法による証明法と Coinduction 法による証明法の対応は全くとれないことがわかる。 また、 両証明法とも補題を必要としているが、 線形文脈帰納法による証明法はほとんど自動的に行えるのに対し、 Coinduction 法による証明法は隠蔽合同と補題をそれぞれ人間が用意してやる必要があることが欠点であるといえる。
また、 この例におけるテスト集合 Coinduction 法による証明法は、 自動的に振舞等価を発見できるので、Coinduction 法の自動化に役に立つと思われる。 しかし、 与えられた仕様の両辺が振舞等価であることを証明する際に、 帰納法と補題 12 が必要となる。 冗長な文脈は取り除かれているが、 線形文脈帰納法による証明法においても、 それらの文脈についての証明は単純な方法で証明できるので、 両証明法の違いはそれほどない様に思える。 また、 [6] には、 与えられた仕様のすべての等式が、文脈書換えシステムの条件を満たすことを、 テスト集合
Coinduction 法を行える条件としていたが、 線形文脈帰納法では仕様の等式にそのような条件はなくても証明が行えるということが、 両者の違いである。

6に対し、 線形文脈帰納法は人間の関与が少ないので自動る。 この例の場合、 除去可能片は push $(n)$ であ

まとめと今後の課題
本稿では、 振舞等価性を証明する手法として線形文脈帰納法を用いる手法を提案し、 線形文脈帰納法が健全であることを示した。
さらに、 線形文脈帰納法により、 全く自動的に証明が行える例として、 Flag の仕様を、 補題を必要とするがそれも含めて自動的に証明が行える例として、 スタックの仕様を示した。 よって、 これら 2 つの例に対しては、容易に自動化ができそうである。 また、 今回は紹介しな
かったが、$*\mathrm{n}$一の例に対しては、 補題を与える必要があるが、 線形文脈帰納法により、 証明が可能である。 しかし、 補題を与える必要があるので、 証明の自動化については容易ではないと思われる。
他の証明法と比較すると、 Coinduction 法では人間が隠蔽合同や適当な補題を与えてやらなければならないの

また、 与えられた仕様の等式に条件が付いているが線

ト集合 Coinduction 法よりも広いように思われる。
したがって、 線形文脈帰納法 $q$ テスト集合 Coinduc-tion 法であることはいえるが、 線形文脈帰納法 2 テスト
集合 Coinduction 法であるかどうかは、 まだわかっていない。
今後の課題としては、 本稿で提案した振舞等価性のための線形文脈帰納法の能力の更なる分析をすることや、

この証明法をメタ項書換え計算 [8] などで記述し、 自動化
をはかることなどがあげられる。

参考文献[1] M.Bidoit and R.Hennicker : ’Behavioural theories
and the proof of behavioural properties’,TheoreticalComputer Science, $165(1):3$ -55(1996).
[2] M.Bidoit and R.Hennicker : ’Proving Behavioural
Theorems with Standard First-Order Logic’,Lecture
Notes in Computer Science 850,41-58,Berlin: Springer,

1994.
[3] R.Hennicker: ’Context Induction: A Proof Principle for Behavioural Abstractions and Algebraic
Implementations’, Formal Aspects of Computing(1991)3: 326-345.
.
[4] J.Goguen and G.Malcolm: ’A Hidden Agenda’,USCD
Technical Report CS97-538,1997.
[5] 松本充広, 二木厚吉 :’ 振舞意味論に基づく仕様の検証
法’, 日本ソフトウェア科学会第 14 回大会論文集,p473476, 1997.

[6] M.Matsumoto: ’Verification methods for algebraic
specifications’, Ms thesis,JAIST,1998.
[7] F.Baader and T.Nipkow: ’Term Rewriting and All
That’, CAMBRIDGE UNIVERSITY PRESS,1998.

[8] 大島淳史, 坂部俊樹 :’ 動的弁別ネットを用いたメタ
項書換え計算インタプリタの設計’, 電子情報通信学会
ソフトウエアサイエンス研究会,1999 年 3 月.