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
コードと対応付けてチェックしてくれるのは便利だなぁ。
