Code Readingを読んで、ループ性能(妥当性)に関しての議論を考えるときに、有効な手段があると書いてあった。「バリアント(variant)」と「インバリアント(invariant)」という概念を使う方法だ。「バリアント(variant)」とは、変わりやすいとか変更されるといった意味を持っている。
逆に「インバリアント(invariant)」は、変わらないとか不変なとかという意味を持っているらしい。
この「バリアント(variant)」と「インバリアント(invariant)」を使って、ループ構造が正しいかを証明する方法が、Code Readingの2章に載っていたので、忘れないうちに復習しておきたいと思います。
それにしても、Code Readingは面白いですね。技術者のツボをついた本だと思います。
概要と解説
ループ処理の開始と終了の時点で共に成り立つ条件をループインバリアントと呼ぶそうです。直訳すると、「回る不変式」 ・・・何のこっちゃ(–;)。
このループ処理中にインバリアント(不変式)が常に成り立つことを証明し、かつループ終了時に期待する値が得られたことを示すことができるようにインバリアント(不変式)を定めることで、ループのアルゴリズムが正しい結果の範囲内で機能することを保証できます。
(・・・わかったようなわからないような)
まあ要するに、ある定めた式がループ中に常に真になり続けたままループが終了したら、このループは正しく終了したってことが証明できるらしいです。ループが終了することを証明したり、期待した値を示す式を定めたりって事をしないと証明にならないらしいのですが。
とりあえず、例を見ながら整理しておきます。配列の最大値を求めるループがあるとします。
max = array[n];
while (n--) {
if (array[n] > max) {
max = array[n];
}
}
つぎに、以下の式をループ終了時に期待する結果を返す式として定義します。
max = maximum{array[0 : n)}maximum{array[0 : n)} は、配列 array の要素 0からn -1の中から最大の値を返します。
この結果を証明するためのインバリアント(不変式)は次のように定義します。ループ中の max = array[n]; で示される部分を抜き出した感じです。
max = maximum{array[x : n)}このインバリアント(不変式)が常に成り立つことが証明できれば、ループが正しいということになります。逆に考えると、インバリアント(不変式)を常に真に保つようなコーディングをすればよいとも言えます。
このインバリアント(不変式)は、maxに最初の値がセットされたときに開始されるので、ループの最初では妥当性が保たれます。2行目の nのデクリメントで maximum{array[x-1 : n)} は、要素の範囲が広がり、maxの値よりも大きい値を持つ可能性がでてきました。インバリアント(不変式)を真に保つために、3行目のif文で新しい要素がmaxよりも大きいかを調べ、4行目の代入式でmaxを現時点での最大に設定しなおしています。
これでインバリアント(不変式)は、2度目のループでも真に保たれることを保証できました。ループを繰り返してもインバリアント(不変式)は真になることがわかります。whileループが終了する条件は、n==0になったときですので、ループが終了することも確認できました。
ということで、最大値を返すmax = maximum{array[0 : n)}は期待する値(最大値)を返すことを証明できました。
以上が、「バリアント｣と「インバリアント」を使ったループ構造が正しいかどうかの証明ということになります。(たぶん・・・)
こんな風にして、ループ処理の正しさを証明する方法があるということを、Code Readingを読んでしりました。結構奥が深くて、楽しめそうだなぁと思いつつ、次の章に読みふけっていくのであった・・・。