Whyインストールメモ

Whyツールの習得について(
http://groups.google.co.jp/group/fm-forum/browse_thread/thread/6fbd1bc05aa8f999)
ということで、
私もやってみた。

Whyというのはプログラムの検証用ツールなのだが、
プログラムコードにアサーションのように挿入したWhyのコードを
もとに、プログラムを自動的に検証してくれるという、
なんだか素晴らしい仕組みを持っているのだ。

私の環境はUbuntu。

1.インストール
Coq(apt-getでインストールできる)以外に必要なものは、

why-2.24.tar.gz(http://why.lri.fr/)

いくつか追加でパッケージが必要。
全部sudo apt-get installでインストールしておく。
libocamlgraph-ocaml-dev(これがないとconfigure時に怒られる)
liblablgtk2-ocaml
liblablgtk2-ocaml-dev(gwhyに必要)
alt-ergo(gwhyが使う検証器の一つ）

コンパイルからインストールまでは、why-2.24.tar.gzを展開したディレクトリで

./configure
make
sudo make install

でOK。あと一つ、gwhyを使うなら、以下をやっておく。

why-config

これをやらないとgwhyが使う検証器の設定ファイル(.gwhyrc)ができてないので、gwhy起動時に怒られる。

1.試してみる
Lesson1.javaなんてファイルを作ってみる。

ken@ubuntu:~/src/why$ cat Lesson1.java
public class Lesson1 {
	/*@ ensures \result >= x && \result >= y &&
	  @   \forall integer z; z >= x && z >= y ==> z >= \result;
	  @*/
	public static int max(int x, int y) {
		if (x>y) return x; else return x;
	}
}

以下で起動する。

> gwhy Lesson1.java

コードと対応付けてチェックしてくれるのは便利だなぁ。