Think Stitch
PRINCIPIA  最近の更新


関数呼び出しを含むプログラムの正当性証明

Theorem Prover Advent Calendar 2013の参加エントリです.

前回,グラフの探索アルゴリズムの部分正当性証明では Isabelle の持つ Hoare 論理ライブラリについてご紹介しました.このライブラリは代入文,IF 文,WHILE 文から構成されるプログラムを扱うことができるので,原理的にはかなりの範囲のプログラムを検証することができます.

しかし関数呼び出しがないので,ある程度以上大きなプログラムを検証するのは面倒です.そこで今回は,関数呼び出しを含むプログラムを段階的に検証する方法について説明してみたいと思います.

先におことわりしておくと,再帰呼び出しは扱いません.それから関数型のプログラムを検証したい場合には,専用のコマンドが用意されているので,そちらを使うことができます.Isabelle の文書の中にそれについて解説したものがあるのでそちらをご覧になる方がよいと思います.停止性の証明のための証明課題も自動的に出してくれます.

選択ソート

例として選択ソートのアルゴリズムを検証してみます.選択ソートについてはご存知だと思いますが,おおまかに説明します.配列を前から順に昇順にソートするとして,ある段階で(計算の断面で)で 0 から i まで(i を含まない)ソートされていて,それ以降はソートされていないとします.ソートされていない後半の部分からいちばん小さな要素を選んで,インデックス i の位置にある要素と入れ替えます.すると i + 1 までソートされたことになります.これを配列の最後まで繰り返します.

選択ソートのアルゴリズムは,ソートされていない配列の範囲から最小の要素を見つける作業と,入れ替える作業の2つの作業からなります.そこでこの2つのステップを別々に検証してみることにします.

最小要素の選択

ボトムアップに進めることにします.指定された配列上の範囲から最小の要素を見つけて,その位置を返す関数を m = selmin v i j としましょう.v は配列,i, j は探索の範囲を示すインデックスのペアで,0 <= i < j <= length v とします.length v は配列の大きさです.m は最小の要素があるスロットのインデックスになります.

関数 selmin の事前条件は 0 <= i < j <= length v です.事後条件は,インデックス m の要素が指定範囲で最小ということなので,次のように表すことができます.

\[ \begin{split} & i \le m \land m < j \land \\ & \forall p. i \le p \land p < j \Rightarrow v[m] \le v[p] \end{split} \]

プログラムは次のようになります.

theorem "VARS k m
  {i < j & j <= length (v::int list)}
  m := i;
  k := i + 1;
  WHILE k < j
  INV {
    i < k & k <= j &
    i <= m & m < j &
    (ALL p. i <= p & p < k --> v ! m <= v ! p)
  }
  DO
    IF v ! k < v ! m THEN
      m := k
    ELSE
      SKIP
    FI;
    k := k + 1
  OD
  {i <= m & m < j &
   (ALL p. i <= p & p < j --> v ! m <= v ! p)}"
apply(vcg)
apply(auto simp add: nth_list_update)
apply (metis eq_iff le_neq_implies_less not_less_eq)
apply (metis (full_types) less_antisym less_irrefl less_trans not_le)
apply (metis linorder_neqE_nat not_le not_less_eq)
done

配列の要素は簡単のために整数としました.Isabelle では配列要素 v[k] を v ! k と書きます.配列の要素は自然数として扱われるので,下限を 0 で押さえる必要はありません.

変数 k がループ変数で,i から順に j の手前までスキャンします.m は調べた範囲で最小の要素を含むインデックスです.

ループ不変条件は事後条件を弱めた形になっています.ループを脱出した時点では,ループ条件の否定と合わせると事後条件が成り立つことになります.

証明のコマンドはなにやら複雑ですけど,これ,すべて自動証明なんです.Isabelle には Sledgehammer という機能があって,あらかじめ登録された外部の証明支援系に証明を外注することができるんです.このプログラムはすべてこれで証明することができました.プログラムの意味を理解するという点では善し悪しなんですけどね.

ここまではふつうの検証なので,特別なことはありません.

選択ソート本体

つづいて,関数 selmin を使う選択ソートの本体を検証します.そのために関数の仕様を前提に入れます.

一般に,関数 y = f x の事前条件を Q x,事後条件を R x y とすると,その意味は次のようになります.

\[ \forall x. Q\,x \Rightarrow \exists y. y = f\,x \land R\,x\,y \]

つまり,事前条件 Q x を満たすようなすべての x について,関数 f x は結果 y を計算することができて,その結果は事後条件 R x y を満たす,ということです.存在限量は f x が事後条件の中で何度も現れるのを避けるために入れてあるだけで,実際には(1点規則によって)次の式と等価になります.

\[ \forall x. Q\,x \Rightarrow R\,x\,(f\,x) \]

これを検証するプログラムの前提に入れておけばいいわけです.選択ソートの本体は次のようになります.

theorem
  "ALL (v::int list) i j. i < j & j <= length v -->
      (EX m. m = (selmin v i j) &
        i <= m & m < j &
        (ALL k. i <= k & k < j --> v ! m <= v ! k))
  ==>
  VARS (v::int list) i k
  {True}
  i := 0;
  WHILE i < length v
  INV {
    i <= length v &
    (ALL p q. p < q & q < i --> v ! p <= v ! q) &
    (ALL p q. p < i & i <= q & q < length v --> v ! p <= v ! q)
  }
  DO
    k := selmin v i (length v);
    v := v[i := v ! k, k := v ! i];
    i := i + 1
  OD
  {ALL p q. p < q & q < length v --> v ! p <= v ! q}"
apply(vcg)
apply(auto simp add: nth_list_update)
apply (metis not_le order_refl)
apply (metis eq_imp_le le_less_trans not_less_eq)
apply (metis Suc_leD eq_imp_le le_less_trans)
apply (metis Suc_leD le_less_Suc_eq le_less_trans le_refl)
done

関数 selmin のおかげでループの本体をシンプルに書くことができました.まだソートされていない i〜lengthv の範囲から最小の要素を選び,インデックス i の要素と交換します.これを length v まで繰り返します.

配列への代入 v[i] := x は v := v[i:=x] と書きます.インデックス i と j の内容を交換する場合は次のように書くことができます.

v := v[i := v!j, j := v!i]

i = j の場合は NOP になります.

ループ不変条件には2つの全称限量があります.1つは配列の前の部分がソートされているという条件です.もう1つはソートされていない範囲の要素はすべて,ソートされている範囲の要素よりも大きいという条件です.2番目の要素がないと,選択した最小の要素と,前の部分の要素との大小関係がわからないということになります.前の部分はソートされているので,実質いちばん後ろの要素との大小関係だけ書けば十分です.ただし,その場合には,前の部分が空の場合を考慮する必要があります.

選択ソート本体の方もすべて自動証明で処理することができました.

このように,関数を呼び出すプログラムを検証する場合には,関数の仕様を前提に入れておいて利用すればよいということです.1ステップずつ手で証明をしてみると,関数の仕様がどのように使われているのかがよくわかります.ここでもプログラムの性質を深く理解する機会が得られます.

関数のインターフェイス(仕様)を定義する場合には,上のように事前条件・事後条件のペアで指定するようにすれば,提供する方も利用する方も助かると思います.

補足

上の検証では,話をかんたんにするために必要な条件を1つ外してあります.それは配列に対して行うことができる操作は値の交換に限るという条件です.もしこの条件がないと,好き勝手な値を配列に書き込んでもよいということになってしまいます.すると例えば,すべてのスロットに 0 を書き込んでしまえば,ソートの事後条件を満たしてしまいます.

theorem
  "VARS (v::int list) i
  {True}
  i := 0;
  WHILE i < length v
  INV {i <= length v & (ALL k. k < i --> v ! k = 0)}
  DO
    v := v[i := 0];
    i := i + 1
  OD
  {ALL i j. i < j & j < length v --> v ! i <= v ! j}"
apply(vcg)
apply(auto simp add: nth_list_update)
done

これを避けるためには,ソートする前の段階で配列に含まれていた値の種類と個数が,ソートの後でも変わっていないという条件を入れる必要があります.これについては別の機会に書きたいと思います.

(実は v はリストなので,v を空にする(v := [])だけでも条件は成り立ってしまいます :P)

この例からもわかるように,証明では(テストでもそうですが)何と比較して,何を基準にして正しいとか正しくないとかいっているのかということが重要ですよね.仕様,すなわち事前条件・事後条件が間違っていたり,条件が弱かったりすれば,たとえ証明ができたとしても役に立たないかもしれないということです.

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