Think Stitch
PRINCIPIA  最近の更新


事後条件の積項からループ不変条件を求める

最近、雑談ばかり書いていて、若干の後ろめたさを感じていますが、でもまた雑談です。 いつのまにか SyncStitch の話より雑談の方が多くなっちゃいました。 これはいかんなあ。ほんとに。

不思議な計算ループで、事後条件からループ不変条件を求める話を書きました。 これについてちょっと書こうと思います。 読むのが面倒ではない程度に簡単なものがいいかなと。 そこで線形探索を考えます。 (こういうおもちゃみたいなプログラムばかり例に出すので、正当性証明は一部で悪くいわれて来たようです。実用レベルのプログラムも証明できますけど、数千行もある証明例を誰も読みたくないでしょう? :P それに線形探索だってりっぱな実用プログラムですし。)

配列 v の中に値 x が含まれているかどうか調べるとします。 含まれている場合には、そのインデックス i も欲しいです。 そこで事後条件は、おおざっぱには次のようになります。

v[i] = x

これだと x が含まれていない場合が考慮されていないので、「ならば」 -->(含意)を使って次のようにします。 i の変域も明確にしなければいけません。

0 <= i <= length v & (i < length v --> v[i] = x)

ここで length v は配列 v の大きさです。 見つからなかった場合は i = length v としました。 i = -1 とする習慣がよく使われます(使われていました)が、i = length v の方が負の数を扱わなくてよいので優れていると思います。

でも、よく見ると見つからなかったという条件は入っていません。 i = length v のときには v について何もいっていないからです。 見つからなかったということは、すべてのインデックス j について v[j] != x ということです。 そこで、これを加えると事後条件が完成します。

0 <= i <= length v & (i < length v --> v[i] = x) & (ALL j. j < i --> v[j] != x)

j の上限を i にしておけば、見つかった場合のように「i = length v のとき」という条件を「ならば」で加える必要がありません。 さらにこの書き方だと、より多くの情報が得られます。それは何かというと、見つかった場合にも、i よりも小さなインデックスの範囲に x はないということです。 一般に x は配列の中に複数入っている可能性がありますけど、この事後条件は、その中でインデックスが一番小さいものを見つけるという強い条件を主張していることになります。

事後条件からループ不変条件を求める

事後条件からループ不変条件を求めるヒューリスティクスの1つは、事後条件が A & B というように「かつ」で結ばれている場合、一方をループ不変条件にして、残りの否定をループ条件にするというものです。 こうすればループを脱出した時点で事後条件が成り立ちますから。

この例では「かつ」で結ばれた項が3つありますから、分け方は6通りあることになります。 ループ条件は式として簡単に判定できるものでなければいけませんから、全称限量 ALL の入った部分は含められません。 残る可能性は3つですけど、0 <= i <= length v の否定は明らかに不適切ですから、残る可能性は「ならば」を含む項だけになります。 そして残りの2つがループ不変条件の候補です。

ループ不変条件: 0 <= i <= length v & (ALL j. j < i --> v[j] != x)
ループ条件:  !(i < length v --> v[i] = x)

ところで、「ならば」 --> はふつうプログラミング言語の演算子としてはないので、既存の演算子への書き換えを行います。 一般に p --> q は !p | q です(縦棒1つ | は「または」です)。 さらにこれの否定は p & !q になります。 ド・モルガンの法則というやつです。 したがってループ条件は次のようになります。

ループ条件:  i < length v & v[i] != x

初期状態

初期状態は簡単で、i = 0 とすればループ不変条件を満たすことができます。

ループ本体

ループ本体を導出する話は詳しくはしませんが、ループ不変条件を壊さずに計算を前に進めるように決めます。 「計算を前に進める」とはどういうことかも説明してませんけど、省略します。 線形探索なので、i をインクリメントするだけです。

Isabelle による正当性証明

以上をまとめて Isabelle で書いたものを以下に示しました。 そのまま Isabelle に入れれば、証明できます。

theory LinearSearch
  imports  "~~/src/HOL/Hoare/Hoare_Logic"
begin

lemma "VARS i
  {True}
  i := 0;
  WHILE i < length v & v ! i ~= x
  INV {i <= length v & (ALL j. j < i --> v ! j ~= x)}
  DO
    i := i + 1
  OD
  {i <= length v & (i < length v --> v ! i = x) &
   (ALL j. j < i --> v ! j ~= x)}"
apply(vcg)
apply(auto)
apply(case_tac "j=i")
apply(auto)
apply(drule_tac x="j" in spec)
apply(auto)
done

まとめと補足

以上のように、事後条件が「かつ」で結ばれている形になっているとき、一部をループ不変条件とし、残りの否定をループ条件にするとうまくいくことがあります。 これはヒューリスティクスなので、必ずうまくいくというわけではありませんが、積極的に解を見いだす努力ができるという点で優れています。

ループ不変条件を見ると、i が増えるたびに x とは等しくない範囲が広がっていくことがわかります。 2分探索のところでもいいましたが、探索というのは探しているというより、存在しないと確定した範囲を拡大していると解釈できます。

このループ不変条件のように、成果がだんだん増えていくタイプのループ不変条件はよく出てきます。 これを累積型ループ不変条件とでもいいましょうか。 前に紹介したエネルギー保存の法則に似ているタイプとはまたちょっと違いますね。

x が見つからなかった場合は、特に何もしなくても i = length v になります。 こういう自然さが好きなんです。 if (i == length v) return -1 みたいなものは書きたくないですから。 事後条件も例外を扱う項が増えて複雑になるだけです。 でも、i を lengh v - 1 からはじめてデクリメントしていくと・・・。

今日もまたゲリラ豪雨が来ました。 PC をシャットダウンするので、ここまでということで。 前に雷のせいで PC のマザーボードとハブが壊れたことがあるのです。 近所に落ちだだけなんですけど。 電源ケーブルとイーサネットケーブルは抜いた方がいいですよ。

2013/09/02
© 2013,2014,2015 PRINCIPIA Limited