JavaScriptでソフトウェアの正しさを数学的厳密に証明してみた

現在、Shibuya.js が開催中です！Ustream で http://www.ustream.tv/channel/shibuyajs にて放送されています。これから、このブログの内容をしゃべります！

今回「テスト」がテーマなうえ、Shibuya.js は「役に立つ話担当」「ネタ担当」に分かれていて、僕は「ネタ担当」なんですが（笑）、いつも通りネタです。でも、遠い未来の役立つネタです！

きっかけは、id:t-wada さんに、GUIの自動テスト関係の質問をしたら、凄くいいことを教えてもらいました。

全てのテストはサンプリングテストである

（少し表現違ったらごめんなさい）話の流れで、部屋を移動しなくていけなくて、たしか、それしか話ができなかったのですが、要するに、サンプリングテストである以上、全ての入力パターンをテストすることは不可能であり、できることは、限られたコストの中で、効率よくテストする必要がある、という意味だと思います。だから、手動テスト vs 自動テスト、どっちが良いのかは、その文脈での効率性で決まるという、趣旨の発言だったと、僕は理解しました。（ちょっとしか会話できなかったので、ほとんど推測です。t-wada さんの意図は、全然違ったりして…）

この名言は、本当に凄くいい名言だと思うんですが、Shibuya.js の「ネタ担当」としては、あれ？全て？と引っかかりました (^^♪ 「例外のない規則はない」ということわざもありますしね！この、ことわざは自己矛盾しているんですが…（笑）

自動証明

というわけで、プログラムが与えられて、そのプログラムのテストプログラムが与えられて、数学的にその正しさを式変形を繰り返して、正しさを証明するプログラムを作りました！

ターゲットは、一番やりやすそうな「挿入ソート」を選びました。（申し訳ないですが、挿入ソートとは何かは、検索してください。手抜きごめんなさい）

プログラムは以下の通りです。

function sortInner(ary) {
  if (ary.length < 2) {
    return ary;
  } else {
    if (head(ary) < head(tail(ary))) {
      return ary;
    } else {
      return append(head(tail(ary)), sortInner(tail(swap(ary)));
    }
  }
}

挿入ソートは2重ループなのですが、ループの内側の部分だけです。つまり、ary[1] 以降はソート済みで、ary[0] を適切な位置まで挿入する部分をターゲットにしました。

head(ary) = ary[0]、tail(ary) = ary.slice(1)、swap(ary) は ary[0] と ary[1] を入れ替えを非破壊で（新しい配列を生成して）行います。

ソートの正しさの判定

正しくソートされていることを証明するには、以下の2つを証明する必要があります。

1. ary[i] < ary[i + 1]
2. 「ソート前」「ソート後」で要素が1対1対応すること

扱う問題を小さくするために、今回は、１の方だけを扱います。

というわけで、判定プログラムは以下の通りです。（isOrdered の方が正確な名前かもしれません）

function isSorted(ary) {
  if (ary.length < 2) { 
    return true; 
  } else {
    return head(ary) < head(tail(ary)) && isSorted(tail(ary));
  }
}

証明すること

証明することは、isSorted(sortInner(ARY)) = true です。前提条件として、isSorted(tail(ARY)) = true が成立します。加えて、数学的帰納法を使い証明するので（まだ、この部分は自動化できませんでした）isSorted(sortInner(tail(ARY))) = true を条件に加えます。

証明時に、変数と定数を区別しているのですが、数学的帰納法において、配列の長さは制限が加えられていて、任意の配列というわけではないので、対象の配列を定数化し、ARY で表現しました。

プログラムの表現方法

Haskell のような純粋関数型言語は難しすぎて、人間には書きづらいと思うのですが、自動証明においては、凄く扱いやすく、採用しました。関数は全て副作用がありません。つまり、配列操作は、絶対に配列を破壊しません。なので、sortInner は以下の形になります。

sortInner(ary) = 
  if(lt(len(ary), 2),
    ary,
    if (lt(head(ary), head(tail(ary)),
      ary,
      append(head(tail(ary)),
        sortInner(tail(swap(ary))))))

DOM & XPath

これをひたすら式変形します。上記の通り、関数は木構造になっているので、パターンマッチングでひたすら木構造の変形になります。

木構造をどう扱うか悩んだんですが、最初、正規表現を使おうかと思ったんですが、Perl の正規表現とは違って JavaScript の正規表現は再帰が扱えないので、木構造が扱いづらく、JavaScript (HTML) は DOM が使えて、木構造のための API があるので、関数を DOM に押し込みました！その上で、式変形のパターンマッチングを XPath を使って検索するようにしました。Firebug などを使うと、木構造の変形を追いやすく、便利でした！

定義＆公理

そのほか、使う定義や公理は以下の通り。

head(tail(swap(ary))) = head(ary)
tail(tail(swap(ary))) = tail(tail(ary))
tail(append(ary, v)) = ary
head(append(ary, v)) = v
if(true, a, b) = a
if(false, a, b) = b
if(a, b, b) = b
a && true = a
true && a = a

ちょっとズルなんですが、定義のような定理。

len(append(ary, v)) < 2 = false

連結すると、長さが2以上になるよと言う件です。len と append の関係性を手抜きしました。

上手く扱えなかった数学的帰納法

昨日・今日でこの準備をしていて、発表までに間に合わなかった、数学的帰納法の取り扱いです。以下の2つは単独で証明できると思うのですが、うまく、自動証明の流れの中で証明できなかったので、定理に加えてしまいました。ごめんなさい。次の課題として、これをちゃんと自動証明できるようにしたいです！

1. head(tail(ARY)) < head(tail(tail(ARY)))
2. isSorted(sortInner(head(swap(ARY)))) = true

最初の方は、tail(ARY) はソート済みだから tail(ARY)[0] < tail(ARY)[1] という事です。

次の方は、head(swap(ARY)) は長さ n – 1 だから、数学的帰納法により証明済み という事です。

if 条件の伝搬

さらに、特殊な式変形が2つ必要です。一つ目は、if (A) { B } else { C } において、B の中で A = true であることを使うことが必須です。これが、「if 条件の伝搬」。

if (A, B, C) で

• Bの中でAを使っていたら、A = true
• Cの中でAを使っていたら、A = false

否定形も必要でした

• Bの中でnot Aを使っていたら、not A = false
• Cの中でnot Aを使っていたら、not A = true

if の親関数の繰り込み

2つ目は、if の親関数の繰り込みです。 f(A ? B : C) = A ? f(B) : f(C) です。fの引数の数が任意でも扱えると言うことを上手く表現する方法が思いつかなかったので、別枠でコードを書きました。

証明戦略

式変形において、次の一手は、たくさんあり、指数関数的に増えると思ったのですが、なんと、式変形に優先順位をつけたら、一直線で証明できました。

1. ノード数が減る変形 や if 条件の伝搬。
2. if の親関数の繰り込み
3. ノード数が増える変形（定義の代入）

ノード数が減る方を優先して、それをやることがなくなったら、ノードを数を増える変形をやってみて、さらに、また、ノード数を減らす変形を繰り返して、というので、できました。でも、これは、今回の特例で、おそらく、次にどういう手を繰り出すかは上手い評価関数を作って、証明が分岐していくパターンは絶対に必要だと思います。

if の親関数の繰り込み は少しだけ、木構造が複雑になる方の変形です。

デモ

というわけで、デモです。http://yukoba.jp/autotest/sort.html をごらんください。出力は、console.log() に出ます。Internet Explorer 8は未対応です（XPath の扱いが違います）。細かいアルゴリズムは http://yukoba.jp/autotest/js/sort.js をご覧ください。

というわけで、console.log() をみるとわかるのですが、なんと38回の式変形で証明できちゃうんです！

ログの出力は、「証明すべき対象の式」「使える変形式」を出力した後、そこから先は、式変形ごとに、「どの式を使って変形したか」「証明すべき対象の式の変化した結果」を繰り返し表示しています。

使用したスライド

ソフトウェアの自動証明

View more presentations from yukoba