Think Stitch
PRINCIPIA  最近の更新


Hoare 論理と Isabelle による正当性の証明

計算プログラムやプロセスの遷移関数の正当性を確認する最も実践的な方法は、もちろん十分なテストをすることだと思います。 関数型プログラミングだと状態の設定が不要だし、関数単体でテストすることが容易なので、とても楽ですね。 それでも効率その他の理由により、命令型プログラムを書かなければならないこともたくさんあります。 命令型プログラムの場合は、スタブ等周りの環境を整えないと動かせないケースが多いですし、関与するオブジェクトの状態設定をしなければいけないので面倒です。

時には要求される基準が高くて、テストでは品質保証が十分ではないということがあります。 例えば SyncStitch の検査アルゴリズムには高い品質が要求されています。 関数型で書くことができれば、コードもシンプルで正当性の論証もしやすいのですが、実行効率の要求や計算規模の要求から、命令型で書かざるを得ず、場合の数が多いのでテストだけでは不安が残ります。

やや余談ですが Scheme (他の言語でもそうだと思いますが)でリストを処理する関数を書くとき、素朴に再帰を使ってしまうとスタックオーバーフローを起こしてしまいます。 一般に、リストの長さは容易にスタックサイズを超えるからです。 このような時には再帰を開いてといいますか、自分で再帰を制御して、スタックを消費しないようにプログラムを変換しなければなりません。 必然的にアルゴリズムが複雑になるので、正当性の確認が難しくなります。

このような場合には Hoare 論理というものを使うと、プログラムの正当性を証明することができます。 テストと異なり、証明の場合はあり得るすべての場合(無限でも)について正しさを保証することができます。 あらかじめお断りしておくと、Hoare 論理そのものについては説明しません。そのようなことは手に余ります(ほんと、ごめんなさい)。単なるご紹介で、雰囲気をお伝えしたいというだけなんです。 Hoare 論理の Hoare は Tony Hoare さんのことで、もちろん CSP の提唱者、発明者、設計者でもあります。なんてすごい人なのでしょう。

Hoare 論理の解説はどこかで見ていただくとして、実は詳細を知らなくても利用する方法があります。 ツールを使う方法です。ここでは Isabelle というツールをご紹介します。 Isabelle は数学の定理を証明する手助けをしてくれるツールです。 最近は Coq というツールを使っている方が増えているようです。 私は Coq を使ったことがないので比較はできません。 Isabelle は定理証明だけでなく、プログラムのモデルを作って性質を証明したりするためにも使うことができます。

Isabelle は関数型プログラムの正当性を証明するために使うことができます。 加えて Hoare 論理のためのライブラリを持っていて、命令型プログラムの正当性証明をすることができます。これをご紹介します(雰囲気だけ)。

Isabelle の Hoare 論理ライブラリでは、プログラムを次の要素を使って記述します。

  • 空文 SKIP
  • 代入文 <変数> := <式>
  • 文の連接 <文> ; <文>
  • 条件文 IF <式> THEN <文> ELSE<文> FI
  • ループ WHILE <式> INV {<不変条件>} DO <文> OD

(この5要素で書けるプログラムのことを WHILE プログラムというそうです。)

プログラム全体の構成は次のようになります。

VARS <変数宣言> {<事前条件>} <文> {<事後条件>}

<変数宣言> にはプログラムで使う変数をスペースで区切って並べます。 <事前条件>, <事後条件> はご存知だと思います。 それぞれプログラムを実行する前と後で成り立たなければならない条件です。 この2つの条件のペアが、プログラムの仕様になります。

ここでは、やや簡略化した二分探索の例を示します。

lemma "ALL i j. i <= j & j < length (v::int list)
                  --> v ! i <= v ! j
  ==>
  VARS i j m
  {length v > 1 & v ! 0 <= x & x < v ! (length v - 1)}
  i := 0;
  j := length v - 1;
  WHILE j ~= i + 1
  INV {i < length v - 1 &
       0 < j &
       j < length v &
       i + 1 <= j &
       v ! i <= x &
       x < v ! j}
  DO
    m := (i + j) div 2;
    IF v ! m <= x THEN
      i := m
    ELSE
      j := m
    FI
  OD
  {i < length v - 1 & v ! i <= x & x < v ! (i + 1)}"

細かい部分は省略しておおまかに説明すると、lemma は証明したい命題の開始、==> の前にあるのは配列がソートされているという条件です。 配列要素の参照は v!k と書きます。つまり v[k] のことです。 length v は配列の大きさです。 事前条件は、配列が少なくとも2個の要素を持っていて、探索する値が配列の要素の範囲内にあることを主張しています(実際に配列のなかにあるかどうかはわからない)。 事後条件は、もし要素があるとすれば i 番目にあるということを主張しています。

このようなプログラムを Isabelle に入力した後、vcg というコマンドを実行すると、Isabelle はプログラムを証明課題に変換してくれます。 あとは定理証明のコマンドを使って証明します。 証明に成功すれば、プログラムは正しいことになります。 証明できない場合でも、どのような条件が足りなくて証明できないのかを考えると、プログラムの誤りや修正のヒントを得ることができます。 このプログラムの場合、Isabelle にがんばって証明しなさいというと、自動ですべて証明してくれます。

Hoare 論理によるプログラムの正当性証明を体験すると、プログラミングというのは本当に難しい作業なんだと思い知らされます。それと同時に、いままでとは次元の異なる精密さでプログラムの正しさを理解できたような気持ちになれます。

補足

  • Isabelle のサイトは http://www.cl.cam.ac.uk/research/hvg/Isabelle/ です。
  • とてもすばらしいチュートリアルがあります。プログラミングの例もあり、楽しめます。チュートリアルの日本語解説を書いている方がいます。 http://d.hatena.ne.jp/caeruiro/
  • Hoare 論理のライブラリは Isabelle のインストールディレクトリの下、src/HOL/Hoare にあります。そこにある readme.html を見てください。
  • Hoare 論理の解説書としては、例えば The Science of Programming (リンク先は Amazon)があります。日本語訳はプログラミングの科学(同じく Amazon)ですが、入手困難なようです。
  • 珠玉のプログラミング(リンク先は Amazon)という本の中に、二分探索とヒープソートの正当性証明の話が出てきます。ヒープソートについては、不変条件の不足を Knuth さんに指摘されたとの脚注があります。なぜこの条件が必要なのかは自分で証明してみるととてもよくわかります。
  • さらに進んだ手法を知りたい方は、B-method, Event-B, Refineme Calculus などを調べるとよいのではないかと思います。
2013/08/08

追記

大事なことを1つ言い忘れていました。ここで証明したのは部分正当性といって、もしプログラムが停止したとしたら結果は正しいという弱い主張なんです。

プログラムが停止することまで含めた正当性は完全正当性といいます。完全正当性をいうには、部分正当性に加えて停止性の証明が必要です。これには限度関数というものを使います。このあたりの用語、訳語はあまり定まっていないようなので、文献によっては違うかもしれません。

2013/08/10
© 2013,2014,2015 PRINCIPIA Limited