Why3
をテンプレートにして作成
[
トップ
] [
新規
|
一覧
|
検索
|
最終更新
|
ヘルプ
]
開始行:
* 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 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/
ページ名:
![[PukiWiki]](image/knxmpen.png "[PukiWiki]")
