[Why3] Install of Why3 Tool (Theorem Prover Advent Calender)

この記事はTheorem Proving Advent Calendar 2011の3日目の記事です。（なお、Advent Calender の参加者も継続募集中です。）

Why3 をMacOS (Snow Leopard) に導入してみました。
Why3 は Why の後継で、Why というのはプログラム検証プラットホームです。Java や C のプログラムに注釈として事前事後条件などを書くと、why 言語という中間言語に一度処理され、Alt-Ergo などの自動証明器や Coq のような証明支援系に適した出力に変換してくれます。さらに上記を統合した GUI フロントエンドを提供します。その辺の話は昔作った発表資料(Slideshare)を参照して下さい。

■なぜ Why3 を学ぶのか
今年の11月に VSTTE 2012 Software Verification Competition という競技ソフトウェア検証イベントがありました。平日開催で忙しかったという理由もありますが、出された問題の多くが手続き型的コードの検証ということもあり、普通の Coq の証明の知識だけでは手が出ませんでした。そこで来年に活かそう、という理由で Why3 を学ぶことにしました。
実際問題として、手続き的に書かれたプログラムについて検証したいという需要は多いと思われます。（たとえ Coq などの定理証明系は純関数型的なコードと相性が良くても。）
Why3 と同様のツールに関しては CFML という OCaml コードの検証ツールについて @keigoi さんが記事をお書きになっていますので、そちらもご覧下さい --- というか CFML もいずれ動かしてみたいです。

■ Why3 導入
すでに Xcode, macports とか OCaml, Coq は導入済みと仮定します。
Why3 ダウンロードサイトよりversion 0.71のtarを入手し、適当なディレクトリで展開します。configure したら色々無いと判ったのでとりあえず導入。ocamlgraph は ports に無いので別途ここから入手。でも CoqIDE 動いてるのになんで lablgtk2 無いの？

% ./configure
略
% sudo port install lablgtk2% sudo port install caml-menhir
% sudo port install rubber
% sudo port install caml-sqlite3


ocamlgraph 導入
% cd ???/ocamlgraph-1.8.1
% ./configure
% make
% sudo make install
% sudo make install-findlib


why3 ディレクトリに戻る
% ./configure
                 Summary
-----------------------------------------
OCaml version           : 3.12.1
OCaml library path      : /opt/local/lib/ocaml
Verbose make            : no
Why IDE                 : yes
Why bench tool          : yes
Why documentation       : yes
Why plugins             : yes
Coq plugin support      : no  (not yet implemented)
TPTP parser             : yes
Menhir library          : no
hypothesis selection    : yes
profiling               : no
localdir                : no
% make


ここで why3-0.71/src/ide/gmain.ml の GSourceView2 を gSourceView2 に修正など苦労するが結局


File "gmain.ml", line 1180, characters 42-43:
Error: Syntax error: ')' expected
File "gmain.ml", line 1180, characters 25-26:
Error: This '(' might be unmatched


などのコンパイルエラーが消えず、GUIは諦めることにする。


% ./configure --disable-ide
% make clean; make
% sudo make install


各種ツールが /usr/local/bin/ に導入された。



■ 各種自動定理証明器の導入
基本的にどれかで証明出来れば良いと考えると、色々導入した方が有利なんですが、とりあえず Alt-Ergo だけ導入すれば雰囲気は味わえます。どれが一番強力な自動証明器かというのは良く解りません。

Alt-Ergo は Why3 のページから辿って、alt-ergo-0.93 の Mac 版をダウンロードするだけ (make 不要)。

CVC3 についても同様にして 64-bit Intel Mac OS X (Snow Leopard) dynamic library and executable cvc3 2.4.1 を導入。これは展開するだけ。

Yices も同様に Yices 1.0.31 をダウンロードして展開。

Gappa も同様に gappa 0.15.1 をダウンロード。INSTALL を読むと前提が GMP, MPFR, Boost なのでそれぞれダウンロードして導入。GMPは入手先サイトが無くなっていたので ports で代用し、 
% sudo port install gmp
% sudo port install mpfr
% sudo port install boost
% ./configure
GMPが見つからず失敗
% ./configure "CPPFLAGS=-I/opt/local/include" "LDFLAGS=-L/opt/local/lib"
成功
% make
% sudo make install
で代用。

■構成
インストールしたcvc3などにPATHを通して
% why3config --detect
します。なんかyicesが未サポートヴァージョン、cvc3が動かず、Alt-Ergo, Gappa, Coq だけという状況。一度構成したら
% why3 --list-provers
Known provers:
  alt-ergo (Alt-Ergo)
  coq (Coq)
  gappa (Gappa)
  yices (Yices)
と表示されます。証明器を追加したら再度同様に構成します。

■実行例
examples/に入っている

% cat 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
%

を試してみましょう。ちなみにG2はそもそも間違っているので自動証明失敗して当然です。
Coq については出力先ディレクトリを予め作成しておいて、-o オプションで指定します。

% why3 -P alt-ergo hello_proof.why 
hello_proof.why HelloProof G1 : Valid (0.03s)
hello_proof.why HelloProof G2 : Unknown: Unknown (0.04s)
hello_proof.why HelloProof G3 : Valid (0.03s)
% why3 -P gappa hello_proof.why
hello_proof.why HelloProof G1 : Valid (0.00s)
hello_proof.why HelloProof G2 : Unknown: Unknown (0.00s)
hello_proof.why HelloProof G3 : Unknown: Unknown (0.00s)
% why3 -P yices hello_proof.why
hello_proof.why HelloProof G1 : Valid (0.00s)
hello_proof.why HelloProof G2 : Unknown: Unknown (0.00s)
hello_proof.why HelloProof G3 : Unknown: Unknown (0.00s) 

% mkdir hello

% why3 -P coq -o hello hello_proof.why
% ls hello
hello_proof_HelloProof_G1.v hello_proof_HelloProof_G3.v
hello_proof_HelloProof_G2.v 

% cat hello/hello_proof_HelloProof_G2.v 
(* This file is generated by Why3's Coq driver *)
(* Beware! Only edit allowed sections below    *)
Require Import ZArith.
Require Import Rbase.
(* YOU MAY EDIT THE CONTEXT BELOW *)

(* DO NOT EDIT BELOW *)

Theorem G2 : False.
(* YOU MAY EDIT THE PROOF BELOW *)
intuition.

Qed.
(* DO NOT EDIT BELOW *)

% 

G2を下記の様に正しく修正すると、


% grep G2 hello_proof.why
  goal G2 : (true -> false) \/ (true \/ false)
% why3 -P alt-ergo hello_proof.why
hello_proof.why HelloProof G1 : Valid (0.03s)
hello_proof.why HelloProof G2 : Valid (0.03s)
hello_proof.why HelloProof G3 : Valid (0.03s)
%

上記の様に自動証明に成功します。 ツールの導入が終わったので、次回は Why3 を用いたプログラム開発に付いて説明します。

■宣伝
毎月１回週末に、新宿にて形式手法勉強会の Formal Methods Forum を開催しています。内容は Coq を中心とした各種形式手法（定理証明系とモデル検査など）についての勉強会です。東京近隣の方はぜひご参加を。