トップ «前の日記(2010-06-06) 最新 次の日記(2010-06-21)» 月表示 編集

日々の流転


2010-06-17 [長年日記]

λ. Whyでバブルソートの正当性を示す

計算機言語で定理証明 (Proof Party.JP)のときには、Jahobというツールを使って色々やってみたが、最近Whyという似たツールを知ったので、こっちでも同じようなことをやってみる。 まずは、Jahobでも試したバブルソートの例*1

BubbleSort.java

これを gwhy BubbleSort.java としてgwhyを起動すると、Proof Obligation が抽出されて一覧されるので、あとはメニューから「Proof」「Prove all obligations」とかを選べば定理証明器などが走って証明をしてくれる。 定理照明器としては、Alt-Ergoしかインストールしていなかったけれど、この例ではあっさり全 Proof Obligation が証明された。

以下が結果の画面。 gwhyのこのインターフェースはテストツールに似せてあるのだろうけど、良いなぁ。

[gwhyのスクリーンショット]

参考

【2010-06-24追記】

マニュアルを一応読んで、異なる要素が保存されている事を追加してみた。 同じ要素の数が変化するかどうかは書けていない。 今度は Alto-Ergo では証明に失敗するのがあったので、CVC3も使ってみたら、片方ですべてを証明するのは無理だったけど、どちらかでは全部証明できた。

【2010-07-20追記】

要素の個数の保存についても書いてみたが、これは証明がタイムアウトしてしまい、うまくいっていない。

*1 事後条件としては、要素が保存されていることとかは置いておいて、実行後に配列がソートされていることだけを書いてある。