时间戳

首页 > 解决方案 > 将 dafny 编译为 java

java - 将 dafny 编译为 java

问题描述

我正在尝试将一个简单的 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

所以我可以编译+运行它作为一个整体，但不能独立这样做：

$ 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

我想我一定是错过了什么。

标签： javadafny

解决方案

您需要将 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您使用的开关是缺失的部分。

推荐阅读