日々の流転

λ. 手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み

手続き型プログラムから書換え系への変換に基づくソフトウェア検証の試み, 古市祐樹, 西田直樹, 酒井正彦, 草刈圭一朗, 坂部俊樹, 信学技報 SS2006-41 (KBSE2006-17), 電子情報通信学会 (2006年-10月).

項書換えの分野では帰納的定理の証明手法として潜在帰納法や書換え帰納法などが広く研究されている．2つの異なる関数が任意の入力に対して同様の出力を返すことは帰納的定理として捉えられるので,帰納的定理の証明法は関数型プログラムの等価性の検証に利用できる．本研究では,項書換えにおける帰納的定理の証明法を利用して手続き型プログラムの等価性の検証を試みる．具体的には,手続き型プログラムから書換え系への変換を与え,その変換により手続き型プログラムの等価性を項書換え系の関数の等価性に帰着できることを示す．

項書き換え系はこんな使い方も出来るのかと驚いた論文。 項書き換え系について詳しくないので、細かい議論はあまり追えてないのだけど、アイディアがとても面白かった。

手続き型のプログラムから、プログラムカウンタと変数の値とを項で表した、(決定可能)条件付き項書き換え系へと変換する。例えば、

int sum1(int x){
  int i=0; int z=0;
  while(i<x){
    i=i+1; z=z+i;
  }
  return z;
}

という関数は

sum1(x) → U1(x, 0)
U1(x, i) → U2(x, i, 0)
U2(x, i, z) → U3(x, i, z) <== i < x
U3(x, i, z) → U4(x, Add(i, S(0)), z)
U4(x, i, z) → U5(x, i, Add(z, i))
U5(x, i, z) → U2(x, i, z)
U2(x, i, z) → U6(x, i, z) <== i >= x
U6(x, i, z) → U7(z)
U7(y) → y

という項書き換え系になる。

さらに、項書き換え系で書いた仕様

sum0(0) → 0
sum0(S(x)) → Add(sum0(x), S(x))

を用意して、sum0(x) = sum1(x) が帰納的定理であることを、潜在帰納法を使って証明する。

項書き換え系に変換して何が嬉しいかというと、普通なら帰納法が必要な定理の証明を、直接帰納法を用いずに出来る潜在帰納法等の方法があって、自動化がしやすいところ。ただ、この論文の時点ではまだ自動化は出来ていないけど。

ちなみに、こないだの第68回情報処理学会・プログラミング研究会で、同じ著者らの「潜在帰納法を利用した手続き型プログラム検証の試み」という題の発表があった。