如何从C#主程序调用Dafny方法？

Question

我需要向Dafny函数提供数据并得到它们的输出。为此，我试图创建一个调用Dafny函数的C#程序。

作为一个测试，我创建了一个非常简单的Dafny文件：

module myDafnyModule {
    method boolMethod(b: bool) returns (r:bool) {
        return !b;
    }

    function method boolFunctionMethod(b:bool):bool {
        !b
    }
}

我的主要猜测是，我应该把它作为一个多文件.NET组件来处理。为此，我应该

1. 使用类似于C#的内容为程序的Dafny部分生成dafny /spillTargetCode:1 dafnyModule.dfy
2. 使用类似于csc /target:module dafnyModule.cs的内容将其编译为一个模块
3. 用类似于C#的东西编译主csc Main.cs /addmodule:dafnyModule.netmodule程序。

第一步有效。但是，步骤2中的csc调用失败了，出现了许多错误，如

$ csc dafnyModule.cs                       
Microsoft (R) Visual C# Compiler version 3.6.0-4.20224.5 (ec77c100)
Copyright (C) Microsoft Corporation. All rights reserved.

dafnyModule.cs(50,28): error CS0234: The type or namespace name 'Immutable' does not exist in the namespace 'System.Collections' (are you missing an assembly reference?)
dafnyModule.cs(1718,40): error CS0246: The type or namespace name 'BigInteger' could not be found (are you missing a using directive or an assembly reference?)
...

我的问题是：

• 在步骤2中的csc调用中缺少什么来编译Dafny生成的C#代码？
• 这是与Dafny代码接口的最佳方式吗？我还能想象到其他的选择，尽管它们看起来更加费力和容易出错：。
  • 在Dafny中有主入口点，并调用C#函数来处理输入/输出？
  • 有一个C#程序在运行时加载Dafny编译器生成的DLL吗？

• 实际上，我不是一个C#的人，我更愿意打电话到达夫尼从爪哇！但我想Java支持比C#更不成熟，信息也更少。Java类似的问题没有答案..。

为了完整起见，我在macOS 11.3.1上使用了Dafny3.1，DotNet5.0.104，csc，mono6.12.0.90。

Answer 1

我意识到，达夫尼生成的C#代码从几行代码开始，这些行似乎暗示要使用dotnet来编译，而不是使用csc (因为dafny /help提到了csc)。

沿着这条线，我找到了dotnet。

它起了作用，只需将生成的C#代码放在库的预期位置和应该在哪里的主要应用程序中即可。

dotnet的整个解决方案和项目听起来有些令人望而生畏，给Windows上的Visual带来了痛苦的闪回，但它是非常简单的。