Why3 の編集 - KnxmWiki

* Why3 [#te123ecb]

Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions.

Why3 はフランス国立情報学自動制御研究所 INRIA が公開しているプルーバーマネージャーです．その用途は C や Java で書かれたプログラムの検証ですが，Why3 で実際に行えるのは，TPTP や独自の言語（Why:logical language，WhyML:programming language) で書かれた定理を様々な外部ツールに分担証明させること，具体的には

- 定理を分割簡約，各ゴールに適した外部証明ツールを選択適用すること

- 各ツールのフォーマットに変換した statement を読み込ませたエディターを起動，ユーザーが証明スクリプトやオプションを入力保存した後，再度ツールに通して確認すること

です．

Why3（ver0.81）で利用できる外部ツール

- 自動証明系：Alt-Ergo，beagle，CVC3，CVC4，E，Gappa，iProver，MathSAT，metis，
Princess，Simplify，SPASS，Vampire，veriT，Yices，Yices2，Z3，zenon
- 数式処理系：Mathematica, MetiTarski
- 対話的証明系：Coq, PVS

*Why [#u2b467fe]

Why は Why3 の旧々版で，外部プルーバーのベンチマークと statement の独自言語から証明系言語への変換が可能ですが，対応する対話的証明系言語が Why3 よりも多いので，ひとつの定理の証明スクリプトを複数の証明系で書くのに便利です．

*インストール例 [#z5ffb31c]

適当な書き込み可能ディレクトリにおいて

sudo apt-get -y install liblablgtksourceview2-ocaml-dev libsqlite3-ocaml-dev libsqlite3-ocaml-dev why alt-ergo cvc3
 git clone git://scm.gforge.inria.fr/why3/why3.git
 cd ./why3
 autoconf 
 ./configure
 make
 sudo make install
 cd ..
 why3config --detect
 echo '#!/bin/bash
 why3 -P Alt-Ergo $*
 why3 -P CVC3 $*
 why3 -P Coq $*' > why3cvt
 chmod 777 ./why3cvt
 sudo mv ./why3cvt /usr/local/bin/
 echo '#!/bin/bash
 #why --alt-ergo $*
 why --coq $*
 why --cvcl $*
 why --gappa $*
 why --harvey $*
 why --hol-light $*
 #why --hol4 $*
 why --isabelle $*
 why --mizar $*
 why --pvs $*
 why --simplify $*
 why --smtlib $*
 why --why $*
 why --why3 $*
 why --z3 $*
 why --zenon $*' > whycvt
 chmod 777 ./whycvt
 sudo mv ./whycvt /usr/local/bin/

今回インストールした外部ツールは Alt-Ergo，CVC3 のみですが，上記からお好みでインストールし，why3config --detect 及び why-config を実行すれば登録されます．

*利用例 [#p2a344bb]

**数学的帰納法の例 [#r26eacd4]

echo "theory DemoI
 use import int.Int
 use import int.Power
 function s int:int
 axiom h1: s 0 = 0
 axiom h2: forall n:int. s (n + 1) = s n + 4 * power n 3 + 6 * power n 2 + 4 * n + 1
 lemma lem: s 5 = power 5 4
 predicate p (n:int) = s n = power n 4
 clone int.SimpleInduction
 with predicate p = p, lemma base, lemma induction_step
 end" | why3 -P CVC3 -F why -t 0 -

**連言の分割証明の例 [#p7404f70]

echo "theory Demo1
 use import int.Int
 predicate p int
 lemma lem: (exists x:int. (not p x \/ (forall y:int. p y))) /\ (forall x y:int. (2 <= y - x <-> exists z:int. x < z < y))
 end" > demo1.why

として，ファイルを準備し

why3ide ./demo1.why

とすると，GUI が起動します．

まず上記のゴールである lem の単独プルーバーでの証明を試みましょう．ツリーの「lem」を選択，パネルの「Alt-Ergo」をクリックすると「lem」に＋マークが付きますが，ステータスは？マークのままなので，Alt-Ergo では力不足ということです．更にパネルの「CVC3」をクリックしても同様です（Ctrl + e でツリーを展開，各プルーバーを選択すると，右上に「I don't know」「Unknown.」といったプルーバーからの出力が確認できます）．

そこで lem を分割します．ツリーの「lem」を選択，パネルの「Split」をクリックすると3個のサブゴールが現れるので，パネルの「Alt-Ergo」をクリック．今回は1つ目を除いてグリーンのアイコンになり，更にパネルの「CVC3」をクリックすれば1つ目もグリーンのアイコンになります（Ctrl + e でツリーを展開，成功したプルーバーを選択すると，右上に「Valid」といったプルーバーからの出力が確認できます）．最後にツリーの「lem」を選択，パネルの「Clean」をクリックすると失敗した箇所が消えオールグリーンになります．

&ref(why3-1.png);

**直観主義論理の Coq に二重否定を消去させる例 [#j514b9af]

echo "theory Demo0
 predicate a
 lemma lem: not not a -> a
 end" > demo0.why

として，ファイルを準備し

why3ide ./demo0.why

とすると，GUI が起動します．

ツリーの「lem」を選択，パネルの「Coq」をクリック，Ctrl + e でツリーを展開，ツリーの「not yet edited」となっている「Coq」を選択，パネルの「Edit」をクリックすると，CoqIDE（同じ INRIA が公開している Coq の GUI）が起動します．

この時点で not not a が a に置き換えられてしまっています（笑）ので，intros h1. の次の行に trivial. と書き込み，Ctrl + Alt + End で証明完了，Ctrl + s で保存，Ctrl + q で終了，Why3 に戻り，パネルの「Replay」をクリックすれば，オールグリーンになります．

&ref(why3-0.png);

**入力ファイル変換の例 [#s763cb47]

入力ファイルを TPTP のフォーマットで作成します（上記 Why3 のフォーマットでも構いません）．

echo "fof(gl,conjecture,? [X] : ! [Y] : f (X, Y) => ! [Y] : ? [X] : f (X, Y))." > demo.p

この demo.p を Alt-Ergo，CVC3，Coq のフォーマットに変換します．

mkdir ./demo
 why3cvt -o ./demo ./demo.p
 ls ./demo

生成されたうち，Alt-Ergo（INRIA が公開している，Why に最適化されたプルーバー）のフォーマットは Why と同じなので，demo-T-gl.why を更に HOL Light，Isabelle などのフォーマットに変換します．

whycvt --dir ./demo ./demo/demo-T-gl.why
 ls ./demo

なお，生成される入力ファイルには定理名などの修正を要するものもあります．例えば

leafpad ./demo/demo-T-gl_why.ml

として確認すると

&ref(why3-2.png);

のようになっているので

&ref(why3-3.png);

のように修正保存の後

hol-light

として HOL Light を起動し

#use"./demo/demo-T-gl_why.ml";;

と読み込み

MESON[]gl;;

とすれば，証明完了です．

*リンク [#he21cae9]

- http://why3.lri.fr/
- http://why.lri.fr/

タイムスタンプを変更しない

* Why3 [#te123ecb]

- 定理を分割簡約，各ゴールに適した外部証明ツールを選択適用すること

です．

Why3（ver0.81）で利用できる外部ツール

*Why [#u2b467fe]

*インストール例 [#z5ffb31c]

適当な書き込み可能ディレクトリにおいて

*利用例 [#p2a344bb]

**数学的帰納法の例 [#r26eacd4]

**連言の分割証明の例 [#p7404f70]

echo "theory Demo1
 use import int.Int
 predicate p int
 lemma lem: (exists x:int. (not p x \/ (forall y:int. p y))) /\ (forall x y:int. (2 <= y - x <-> exists z:int. x < z < y))
 end" > demo1.why

として，ファイルを準備し

why3ide ./demo1.why

とすると，GUI が起動します．

&ref(why3-1.png);

**直観主義論理の Coq に二重否定を消去させる例 [#j514b9af]

echo "theory Demo0
 predicate a
 lemma lem: not not a -> a
 end" > demo0.why

として，ファイルを準備し

why3ide ./demo0.why

とすると，GUI が起動します．

&ref(why3-0.png);

**入力ファイル変換の例 [#s763cb47]

入力ファイルを TPTP のフォーマットで作成します（上記 Why3 のフォーマットでも構いません）．

echo "fof(gl,conjecture,? [X] : ! [Y] : f (X, Y) => ! [Y] : ? [X] : f (X, Y))." > demo.p

この demo.p を Alt-Ergo，CVC3，Coq のフォーマットに変換します．

mkdir ./demo
 why3cvt -o ./demo ./demo.p
 ls ./demo

whycvt --dir ./demo ./demo/demo-T-gl.why
 ls ./demo

なお，生成される入力ファイルには定理名などの修正を要するものもあります．例えば

leafpad ./demo/demo-T-gl_why.ml

として確認すると

&ref(why3-2.png);

のようになっているので

&ref(why3-3.png);

のように修正保存の後

hol-light

として HOL Light を起動し

#use"./demo/demo-T-gl_why.ml";;

と読み込み

MESON[]gl;;

とすれば，証明完了です．

*リンク [#he21cae9]

- http://why3.lri.fr/
- http://why.lri.fr/

テキスト整形のルールを表示する