2010-06-17 [長年日記]
λ. Whyでバブルソートの正当性を示す
計算機言語で定理証明 (Proof Party.JP)のときには、Jahobというツールを使って色々やってみたが、最近Whyという似たツールを知ったので、こっちでも同じようなことをやってみる。 まずは、Jahobでも試したバブルソートの例*1。
これを gwhy BubbleSort.java としてgwhyを起動すると、Proof Obligation が抽出されて一覧されるので、あとはメニューから「Proof」「Prove all obligations」とかを選べば定理証明器などが走って証明をしてくれる。
定理照明器としては、Alt-Ergoしかインストールしていなかったけれど、この例ではあっさり全 Proof Obligation が証明された。
以下が結果の画面。 gwhyのこのインターフェースはテストツールに似せてあるのだろうけど、良いなぁ。
![[gwhyのスクリーンショット]](./images/20100617_0.png)
参考
【2010-06-24追記】
マニュアルを一応読んで、異なる要素が保存されている事を追加してみた。 同じ要素の数が変化するかどうかは書けていない。 今度は Alto-Ergo では証明に失敗するのがあったので、CVC3も使ってみたら、片方ですべてを証明するのは無理だったけど、どちらかでは全部証明できた。
【2010-07-20追記】
要素の個数の保存についても書いてみたが、これは証明がタイムアウトしてしまい、うまくいっていない。
*1 事後条件としては、要素が保存されていることとかは置いておいて、実行後に配列がソートされていることだけを書いてある。
[ツッコミを入れる]
