Whyツールの習得について

[yoshihiro503]

WhyはJavaやC用の検証器で、既存のコードにコメントを付け加えるだけで自動検証ができるツールです。勉強会での話やtmiyaさんの資料
http://www.slideshare.net/tmiya/coq-20100208a をみて実際に使ってみたくなった人もいるんじゃないで
しょうか。
私もその一人で、whyツールと自動定理証明器をいくつかインストールしてみました。
まず、Javaのフロントエンド(Krakatoaと呼ばれる)を試してみようとチュートリアル(http://krakatoa.lri.fr/
manual/)をやってみましたが、一部syntax errorになってしまったり通らない部分があるようでした。
まだ動かしたばかりで詳しいことはわからないですが、おそらく構文が一部変わったとかなのだとおもいます。
とりあえず、whyソースコードと一緒に入っていたjavaのサンプルを見ながら \forall integer x,y のコンマがスペースに変
わってることだけはわかりましたが、まだいろいろわからないところもあります。
とにかくドキュメントが少ないのでここでwhyについて情報共有できればと思います。


--
Subscription settings: http://groups.google.com/group/fm-forum/subscribe?hl=ja

[ken coba]

小林です。

私はダウンロードサイトすら分からなかった・・・。
http://why.lri.fr/
でもWindows用インストーラがダウンロードできないみたいですね。

Whyの情報もサイト(http://www39.atwiki.jp/fm-forum/)に書き込んでいきましょう。

2010年4月17日10:47 yoshihiro503 <yim...@gmail.com>:

[ken.coba]

yoshihiro503さん
小林です。

とりあえずインストールと動作確認までは無事終了。
http://d.hatena.ne.jp/kencoba/20100417/1271490659

私が試した範囲では、文法の違いっぽいところは無かったのです。
よろしければ、どんなコードがうまく通らなかったのかお教えください。

#実際動かしてみて思ったけど、これは結構便利に使えるかも。

On 4月17日, 午後2:54, ken coba <ken.c...@gmail.com> wrote:
> 小林です。
>
> 私はダウンロードサイトすら分からなかった・・・。http://why.lri.fr/
> でもWindows用インストーラがダウンロードできないみたいですね。
>
> Whyの情報もサイト(http://www39.atwiki.jp/fm-forum/)に書き込んでいきましょう。
>

> 2010年4月17日10:47 yoshihiro503 <yima...@gmail.com>:
>
> > WhyはJavaやC用の検証器で、既存のコードにコメントを付け加えるだけで自動検証ができるツールです。勉強会での話やtmiyaさんの資料
> >http://www.slideshare.net/tmiya/coq-20100208aをみて実際に使ってみたくなった人もいるんじゃないで

[yoshihiro503]

そうですね。"Why"はそのまま検索しにくいので私は"Why tool"とかで検索しています。
私はWindows環境がないため試すことができませんが、ソースからLinuxにインストールは問題なくできました。

DebianやUbuntuだとapt-get install why でサクッと入るようです。バージョンはちょっと古いかもしれませんが。

> 私が試した範囲では、文法の違いっぽいところは無かったのです。
> よろしければ、どんなコードがうまく通らなかったのかお教えください。

私が遭遇して解決したsyntax errorはKurakatoaのマニュアル( http://krakatoa.lri.fr/manual/krakatoa.pdf
)で10ページの2.2節のlemmaの部分です。ここで
\forall integer x,y,z;
の部分が私のwhy-2.24ではsyntax errorといわれたのですが、コンマをスペースに変えると通るようになりました。

> #実際動かしてみて思ったけど、これは結構便利に使えるかも。

そうですね。私もこれは使いやすくて実務に近いツールだと感じています。

[tmiya]

tmiyaです

On 4月17日, 午後9:17, yoshihiro503 <yima...@gmail.com> wrote:
> > #実際動かしてみて思ったけど、これは結構便利に使えるかも。
>
> そうですね。私もこれは使いやすくて実務に近いツールだと感じています。

私は.NETはほとんど使わないというか環境が無いのですが、
C#と組み合わせるSpec#というのがあって、実務に近いという意味では、
実務の本命はC# + Spec#かなぁ、とも思ってます。
同様に、OOなプログラムに対して、JML的なアノテーションを書いて、
自動証明系もあって、みたいな。案外Visual Studio 2013あたりには
IDEと統合された自動証明系が付いて来るのではないかと思う。
昔、ESC/Javaとかをやっていた人達が、Spec#に関わっているみたいです。

VS2010が出たら、Windows環境を整えて、VS2010を買って、F#とか
Spec#とかやるといいかなぁと思ったり。JVM界隈は最近は形式手法
関係がちょっと薄いというか、MSが関数型＆形式手法に力を入れている
というか。。。

Spec#のページ
http://research.microsoft.com/en-us/projects/specsharp/

[yoshihiro503]

あと、チュートリアル( http://krakatoa.lri.fr/manual/krakatoa.pdf )でいうところの9ページ目の
while文の直前に書いてある
decreases x - sum;
という部分もsyntax errorになるため消していたのですが、
loop_variant x - sum;
とすればコンパイルが通り、停止性の検証も通るようになりました。

また、bitbucketにチュートリアルのリポジトリを作ってコミットしていこうと思うので、チュートリアルをやる方は参考にしてみてください。まだ
2.3節までですが。
http://bitbucket.org/yoshihiro503/whytool/

On 4月17日, 午後9:17, yoshihiro503 <yima...@gmail.com> wrote:

> そうですね。"Why"はそのまま検索しにくいので私は"Why tool"とかで検索しています。
> 私はWindows環境がないため試すことができませんが、ソースからLinuxにインストールは問題なくできました。
>
> DebianやUbuntuだとapt-get install why でサクッと入るようです。バージョンはちょっと古いかもしれませんが。
>
> > 私が試した範囲では、文法の違いっぽいところは無かったのです。
> > よろしければ、どんなコードがうまく通らなかったのかお教えください。
>

> 私が遭遇して解決したsyntax errorはKurakatoaのマニュアル(http://krakatoa.lri.fr/manual/krakatoa.pdf

[tmiya]

そういえば、Coqで命令型プログラミングを扱う為のライブラリYnot
というのもあります。

http://ynot.cs.harvard.edu/

こちらはまぁ、IO Monadとかそういうのに抵抗が無い人向けの
ライブラリみたいです。Coqへの習熟が深まったら、Ynotも
紹介していきたいです。

---
あと、JMLとCoqで検索すると
Embedding JML-Annotated Programs in the Coq Proof System
http://e-collection.ethbib.ethz.ch/eserv/eth:41829/eth-41829-01.pdf
というのを見つけました。
これが修士論文なのかぁ。

[ken.coba]

小林です。

ありがとうございます。
確かに私のところ(why2.24)でもerrorが再現してます。

Tutorialの更新が追いついてないみたいですね。

On 4月17日, 午後9:59, yoshihiro503 <yima...@gmail.com> wrote:
> あと、チュートリアル(http://krakatoa.lri.fr/manual/krakatoa.pdf)でいうところの9ページ目の

[tmiya]

ちょっと調べてみましたが、

http://lists.gforge.inria.fr/pipermail/why-discuss/2008-January/000219.html

によると、/bench/java/good/ 下にある*.javaとかを参考にしろ、ということ
みたいで、PDFマニュアルは正しく無い様です。

なんか JML の文法をちゃんとサポートするのに問題があるので諦めた
みたいですね。

[yoshihiro503]

On 4月20日, 午前12:08, tmiya <tm...@bu.iij4u.or.jp> wrote:
> ちょっと調べてみましたが、
>
> http://lists.gforge.inria.fr/pipermail/why-discuss/2008-January/00021...

>
> によると、/bench/java/good/ 下にある*.javaとかを参考にしろ、ということ
> みたいで、PDFマニュアルは正しく無い様です。

なんという。確かに私もその辺を参考にしましたが、ちょっとひどいですよね。
まあ、でもわかってしまえば単純な変換なので許容範囲ということなのでしょうか。

> なんか JML の文法をちゃんとサポートするのに問題があるので諦めた
> みたいですね。

なるほど。じゃあJMLとはちょっと違う表記でよりリッチな事(表現力という意味で)を目指している感じかもしれないですね。

[yoshihiro503]

yoshihiro503です。
why,krakatoaを使っていてわからなかったのでここに記して置きます。

gwhyを使えばjavaのソースコードを自動検証できるのですが、krakatoaコマンドというものも別にあって
これにjavaのソースコードFoo.javaを食わせると、何やらFoo.jcファイルとFoo.jlocファイルを生成するようでした。
ここでFoo.whyファイルができればwhy --coq Foo.whyとしてCoqでの検証ができるような気がするのですが
その辺の接続がパッと調べた感じではわかりませんでした。

gwhyを行ったときにできるFoo.makefileを使えば.vファイルができますが、成功法ではない気がして、普通はどうやるかを探しています。
見つかり次第また言及するかもしれません。

[tmiya]

On 4月20日, 午前12:23, yoshihiro503 <yima...@gmail.com> wrote:
> yoshihiro503です。
> why,krakatoaを使っていてわからなかったのでここに記して置きます。
>
> gwhyを使えばjavaのソースコードを自動検証できるのですが、krakatoaコマンドというものも別にあって
> これにjavaのソースコードFoo.javaを食わせると、何やらFoo.jcファイルとFoo.jlocファイルを生成するようでした。
> ここでFoo.whyファイルができればwhy --coq Foo.whyとしてCoqでの検証ができるような気がするのですが
> その辺の接続がパッと調べた感じではわかりませんでした。

.../bin/gwhy.shを参考に試してみました。途中まで成功。

適当なディレクトリに Lesson1.java を置きます。

[apple-3:~/why/test] miyamoto% ls
Lesson1.java

ここで krakatoa を実行すると *.java から *.jc, *.jloc を生成します。

[apple-3:~/why/test] miyamoto% krakatoa Lesson1.java
Warning: Lesson1 is not a subpackage of .
Parsing OK.
Typing OK.
Generating JC function Lesson1_max for method Lesson1.max
Generating JC function Lesson1_short_sqrt for method
Lesson1.short_sqrt
Generating JC function Lesson1_sqrt for method Lesson1.sqrt
Generating JC function cons_Lesson1 for constructor Lesson1
Done.
[apple-3:~/why/test] miyamoto% ls
Lesson1.java Lesson1.jc Lesson1.jloc krakatoa.log

更に jessie を実行します。すると why/ ディレクトリに *.why が生成されます。

[apple-3:~/why/test] miyamoto% jessie -locs Lesson1.jloc -why-opt -
split-user-conj Lesson1.jc
Generating Why function Lesson1_max
Generating Why function Lesson1_short_sqrt
Generating Why function Lesson1_sqrt
Generating Why function cons_Lesson1
[apple-3:~/why/test] miyamoto% ls
Lesson1.java Lesson1.loc krakatoa.log
Lesson1.jc Lesson1.makefile why/
Lesson1.jloc jessie.log
[apple-3:~/why/test] miyamoto% cd why
[apple-3:~/why/test/why] miyamoto% ls
Lesson1.why
[apple-3:~/why/test/why] miyamoto%

ここで *.why から *.v を作れればOKだったんですが失敗。

[apple-3:~/why/test/why] miyamoto% why --coq Lesson1.why
File "Lesson1.why", line 15, characters 34-41:
Unbound type 'pointer'
[apple-3:~/why/test/why] miyamoto% ls
Lesson1.why

ということでLesson1.makefileは必要なのかも...。

[Yoshihiro Imai]

tMiyaさん
yoshihiro503です。
いろいろ調べていただいてありがとうございます。
私もkrakatoaがFoo.javaファイルから生成するFoo.jcファイルとFoo.jlocファイルを手がかりにjessieを使えばよいことまでたどり着きました。
そうするとやっぱりFoo.makefileができて、そのなかにcoq/Foo_why.vターゲットが見つかったので、やはりmakeするのが一番かもしれないと思いました。
makefileを見た感じ、具体的に行っているのは次の一行のようです。
why -coq -dir coq -coq-preamble "Require Export jessie_why." -coq-tactic intuition -explain -locs Foo.loc /usr/local/lib/why/why/jessie.why why/Foo.why

まとめると、
- krakatoaでjavaファイルからjcファイルとjlocファイルを生成。
- jessieで.whyファイルと.locファイルを生成
- whyで-coqオプション指定をして.vファイルを生成
という流れっぽいです。

ちなみに2番めで生成したwhyファイルから素直に
why -coq Foo.why
としたときに
Unbound type 'pointer'
と怒られる原因はたぶんjessieから生成されたwhyファイル用のライブラリ/usr/local/lib/why/why/jessie.whyが読み込めてないからだと思います。
さらに-dirによるアウトプット先の指定がないとファイルそのものを上書きしようとするためかわからないですが、Permission deniedと言われてしまうので-dir指定をするとコンパイルが通るようになります。
その他のオプションはたぶんおまけ的なものだと思いますが、-coq-preamble<STR>は<STR>を各.vファイルの先頭に記述し、-coq-tactic<STR>は各.vファイル内でのプレイスフォルダになっている証明の部分にまず適用するtacticコードを記述するとかだと思います。
あとはよくわかりません。

2010年4月20日22:07 tmiya <tm...@bu.iij4u.or.jp>:

--
Yoshihiro Imai
mail: yim...@gmail.com, y.i...@ocaml.jp
twitter: @yoshihiro503