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は必要なのかも...。