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(これがないとconfigur

