从Dafny程序获取C#程序的方法是什么？

Question

我不知道如何从 Dafny 程序获取 C# 程序。

我已在 Visual Studio Code 中下载了 Dafny 并下载了 C#。我有一个 Dafny 程序，可以右键单击该程序并选择编译和运行，但我想生成一个 C# 程序，就像这个视频所示（8:46）：https://www.youtube.com/watch?v=99TjfvyP1z0。

function method Fib (n : int) : int
  decreases n
{
   if n < 2 then n else Fib (n - 2) + Fib (n - 1)
}

method Main ()
{
  print Fib (3);
}

- LyX2394

Answer 1

在内部，Dafny的.NET编译器生成了C#代码，并调用C#编译器将其转换为可执行的.NET程序（或.dll文件）。您可以要求Dafny输出此C#程序，使用命令行开关/spillTargetCode:1。在生成的C#程序顶部的注释中，您会看到哪些命令行开关可直接编译该C#程序。

如果您只想运行Dafny程序，则无需查看C#代码。可以使用/compile:1（默认值）调用Dafny，然后运行生成的.exe文件，或者使用/compile:3来验证、编译和运行您的程序。

我描述这些选项是假设您从命令行运行Dafny。还有一种方法是在VS Code中为Dafny添加这些命令行开关。

如果您想将Dafny与其他C#代码进行交互，可以在Dafny方法和其他Dafny声明上使用{:extern}属性。如果这样做，只需在调用Dafny时在命令行上添加自己的.cs文件即可。例如，在Dafny测试套件中搜索“extern”以获取示例。

Dafny的最新增加（非常新，尚未包含在二进制版本的Dafny中，但如果您自己构建Dafny，则可以立即获得）是JavaScript和Go的编译器。使用命令行开关/compileTarget选择这些编译器。

Rustan

- Rustan Leino

---

我在VS Code中使用Dafny。有什么方法可以在VS Code中生成C#代码吗？ - LyX2394

我在VS Code的终端中使用了这些命令行开关，但是没有成功。相反，我收到了以下错误消息：Windows PowerShell 版权所有 (C) Microsoft Corporation。保留所有权利。/compile:3 : 术语“/compile:3”不被识别为 cmdlet、函数、脚本文件或可操作程序的名称。请检查名称的拼写，或者如果包括路径，请验证路径是否正确，然后重试。 位于第 1 行字符 1

• /compile:3

- LyX2394

那个错误信息听起来不像是来自Dafny。你的Dafny可执行文件路径设置正确吗？（在Windows下，可执行文件名为“Dafny.exe”。在其他平台上，您可以在Mono下运行它，例如“mono Dafny.exe”，或使用Dafny二进制分发包中的脚本“dafny”。） - Rustan Leino

目前，Dafny VSCode不支持将命令行开关传递给编译命令。但是，您可以在此处打开功能请求（或拉取请求）：https://github.com/DafnyVSCode/Dafny-VSCode/issues - Rustan Leino