Why3 で遊んでみた

Why3 で遊んでみたのでメモ．インストールで手間取った．環境は Mac OS X 10.9.1 です．

Why3 のインストール

※この方法は Mac OS X かつ Homebrew 専用です．Linux や MacPorts でのインストールはわかりません．

ソースからは面倒なので，OCaml のパッケージマネージャである opam でいれます．(追記: https://github.com/mht208/homebrew-formal に Why3 の formulae があったのでそっちのほうが簡単かもしれない(試してない))

まず依存ライブラリなどをインストール．

• XQuartz をインストール
  • インストール後は再ログインが必要かもしれない
• brew install gmp
• brew install gtksourceview
  • XQuartz が必要

次に，https://github.com/OCamlPro/ocaml-top/issues/42#issuecomment-22091964 に書いてあるように，下のスクリプトを .zshrc か何かに書きこんで source .zshrc をします．これをしないと conf-gtksourceview をインストールするときにコケます．

export PKG_CONFIG_PATH=$PKG_CONFIG_PATH:/usr/X11/lib/pkgconfig/
for i in `ls /usr/local/opt/`;
do
    if [ -d "/usr/local/opt/$i/lib/pkgconfig" ];
    then export PKG_CONFIG_PATH=$PKG_CONFIG_PATH:"/usr/local/opt/$i/lib/pkgconfig";
    fi;
done

最後に opam install why3 でインストールできます．たぶん．

% why3 --version
Why3 platform, version 0.82 (build date: Fri Jan 17 00:48:01 JST 2014)

Why3IDE で遊んでみる

Why3 には IDE が付属しているので，それで遊んでみます．

IDE を起動させる前に，まずは Prover を探させます．

% why3config --detect-provers
Found prover Alt-Ergo version 0.95.2, Ok.
Warning: prover Coq version 8.4pl3 is not known to be supported.
1 provers detected and 1 provers detected with unsupported version
== Found /Users/amutake/.opam/4.01.0/lib/why3/lib/why3/plugins/dimacs.cmxs ==
== Found /Users/amutake/.opam/4.01.0/lib/why3/lib/why3/plugins/genequlin.cmxs ==
== Found /Users/amutake/.opam/4.01.0/lib/why3/lib/why3/plugins/hypothesis_selection.cmxs ==
== Found /Users/amutake/.opam/4.01.0/lib/why3/lib/why3/plugins/tptp.cmxs ==
Save config to /Users/amutake/.why3.conf

なんか Coq 8.4pl3 で Warning でてるけど気にしない．

why3ide コマンドで起動．

% why3ide .
[Info] Init the GTK interface... done.
[Info] reading icons... done.
[Info] Creating tree model... done
[Info] found directory '.' for the project
[Info] Opening session...

[Info] Opening session: update done

[Info] Opening session: done

これで X11 が立ち上がって IDE が起動するはずです．起動しない場合は XQuartz.app を立ち上げた状態で実行してみたり，マシンを再起動してみたりすると直るかもしれません．

Hello Proofs!

さて，無事起動できたので，マニュアルの 1.1 Hello Proofs をやってみます．

一旦 IDE を閉じて，以下の内容の hello_proof.why というファイルを作ってください．

theory HelloProof "My very first Why3 theory"

  goal G1 : true

  goal G2 : (true -> false) /\ (true \/ false)

  use import int.Int

  goal G3 : forall x : int. x * x >= 0

end

そしてターミナルで why3ide hello_proof.why とやると，hello_proof.why を読み込んだ IDE が起動します．

こんなかんじになるはずです．

G1 を選択して，左の Alt-Ergo ボタンを押してみましょう．

緑のチェックマークがつきました．G1 : true という命題が証明された，ということです．

HelloProof を選択して左の Alt-Ergo ボタンを押してみると，こうなります．

G2 : (true -> false) /\ (true \/ false) が残りました． 次はこの G2 をCoqを使って証明し(ようとし)てみます．

G2 を選択して，Coq ボタンを押してください．できた行を選択すると "Please Edit" と書いてあるので，左の Edit ボタンを押します．

hello_proof.why があるディレクトリに hello_proof というディレクトリができ，その中に hello_proof_HelloProof_G2_1.v というCoqのソースファイルができます．このファイルの内容は以下のようになっています．

明らかにこれは証明できません! 命題を編集して証明できるものにしましょう． 現在の Why3IDE は why ファイルを直接編集することはできないので，適当なテキストエディタで G2 を以下のように編集します．

goal G2 : (false -> false) /\ (true \/ false)

編集したら，IDE に戻ってリロード(Ctrl-r)します．obsolete になります．

G2 を選択して Alt-Ergo，Coq ボタンを押すと，もう一度 try させることができます．代わりに左上のラジオボタンを All goals にして Replay ボタンを押しても同じことができます．

Alt-Ergo で証明できてしまいましたが，せっかくなので Coq でも証明してみたいと思います．

hello_proof/hello_proof_HelloProof_G2_1.v を開くと，Theorem G2 : False. だったのがTheorem G2 : True. になっています．これは auto タクティクで証明できそうです．

保存したら IDE に戻り，G2 の Coq の行を選択して，左の Coq ボタンを押します．

緑のチェックマークがつきました!

まとめ

• Why3 をインストールしてみたよ．Why3 のインストールはすこし面倒だった．
• Why3IDE を使って簡単な命題を証明してみたよ．