代数的仕様の実現検証において、実現の正しさとは与えられた仕様 と実現を記述した仕様(実現仕様)が振舞的に区別がつかないときで あるとされる。この振舞的な正しさの関係は振舞実現関係といわれる。
振舞実現関係を検証するためには、与えられた仕様の各公理の両辺 が実現仕様のもとで振舞的に等価であることを証明すれば十分であ る。２つの式が振舞的に等価であるというのは観測可能な結果を返す すべてのテストによってそれらを区別できないことをいう。 したがって振舞等価性を証明するためには、あらゆる観測可能な文 脈で表される、すべてのテストに対して等価性を調べる必要がある。 しかし、無限に存在する観測可能な文脈すべてについて等価性を調 べることは、一般には容易ではない。
振舞等価性を検証する手法の１つにCoinduction法があるが、これは 隠蔽合同という概念を用いることにより、振舞等価を間接的に扱い証 明をしやすくする手法である。しかし隠蔽合同の発見は人間の力に 依るところが大きく、自動化しにくいという欠点がある。
本研究では線形文脈という限られた形の文脈に対して等価性を 調べることにより、振舞等価性を検証する手法を提案する。 線形文脈とは、文脈の根から穴までの経路以外はすべて変数である ような文脈である。このような文脈の根から穴までの長さに関する 帰納法が線形文脈帰納法である。そして、振舞等価性証明には、 線形文脈帰納法を用いて証明すれば十分であることを示す。 また、線形文脈帰納法を用いた検証法の有効性を３つの例を用いて 示すとともに、線形文脈帰納法とCoinduction法との間の関係について 考察する。