将dafny编译成java

Question

我正在尝试将一个简单的max示例(permalink)编译为java：

$ Scripts/dafny /compileTarget:java /compile:3 max.dfy

Dafny program verifier finished with 3 verified, 0 errors
Wrote textual form of target program to max-java/max.java
Additional target code written to max-java/_System/nat.java
Additional target code written to max-java/_System/__default.java
Additional target code written to max-java/dafny/Tuple0.java
Running...

max element of [7, 4, 2, 9, 6, 3] is 9

所以我可以compile+run作为一个整体，但是不能独立地做

$ Scripts/dafny /compileTarget:java /compile:1 /spillTargetCode:1 /out:main.java max.dfy
$ javac -cp Binaries/DafnyRuntime.jar main-java/main.java
main-java/main.java:3: error: package _System does not exist
import _System.*;
^
main-java/main.java:18: error: package _System does not exist
    dafny.Helpers.withHaltHandling(_System.__default::__Main);
                                          ^
2 errors

另一次尝试：

$ javac -cp Binaries/DafnyRuntime.jar -cp main-java/ main-java/main.java
main-java/main.java:18: error: cannot find symbol
    dafny.Helpers.withHaltHandling(_System.__default::__Main);
         ^
  symbol:   class Helpers
  location: package dafny
1 error

我想我一定是漏掉了什么。

Answer 1

您需要在编译中添加由dafny编译器创建的“附加目标代码”文件。你可以这样做：

$ javac -cp Binaries/DafnyRuntime.jar main-java/main.java main-java/*/*.java

然后，你可以用这样的方法跑

$ cd main-java
$ java -cp ../Binaries/DafnyRuntime.jar:. Main

通过在Dafny源代码的测试文件中查找使用javac的示例，可以找到这一点--但是即使在那里它也失败了，而且您使用的-cp开关是缺少的部分。