我看不到如何从 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);
}
【问题讨论】：
在内部，Dafny 的 .NET 编译器生成 C# 代码，它调用 C# 编译器将其转换为可执行的 .NET 程序（或 .dll）。你让 Dafny 输出这个 C# 程序。这是使用命令行开关/spillTargetCode:1 完成的。在生成的 C# 程序顶部的 cmets 中，您将看到要传递给 C# 编译器以直接编译该 C# 程序的命令行开关。
如果您只想运行 Dafny 程序，则无需查看 C# 代码。要么使用/compile:1（默认设置）调用 Dafny，然后运行生成的 .exe 文件，要么使用 /compile:3 调用 Dafny 来验证、编译和运行您的程序。
我已经描述了这些选项，就像您从命令行运行 Dafny 一样。还有一些方法可以在 VS Code 中的 Dafny 设置中添加这些命令行开关。
如果您想连接您的 Dafny 其他 C# 代码，您可以在 Dafny 方法和其他 Dafny 声明上使用 {:extern} 属性。如果您这样做，那么只需在调用 Dafny 时在命令行中添加您自己的 .cs 文件。例如，在 Dafny 的测试套件的文件中搜索“extern”。
最近添加到 Dafny（最近它还没有在 Dafny 的二进制版本中可用，但是如果您自己从源代码构建 Dafny 可以立即获得它）是 JavaScript 和 Go 的编译器。使用命令行开关/compileTarget 选择这些编译器。
鲁斯坦
【讨论】：
Dafny.exe。在其他平台上，您可以在 Mono 下运行它，例如 mono Dafny.exe，或使用脚本 dafny，它是 Dafny 二进制分发的一部分。