如何将 Dafny 代码与 C# 程序集链接

Question

我正在尝试构建和运行example program by James Wilcox that combines Dafny code and C# code。我在 Mac 上使用mono。该答案中的构建命令对我不起作用：

$ dafny fileiotest.dfy fileionative.cs
Dafny 3.0.0.20820

Dafny program verifier finished with 4 verified, 0 errors
Compiled program written to fileiotest.cs
Errors compiling program into fileiotest
(8,24): error CS0234: The type or namespace name 'Net' does not exist in the namespace 'System' (are you missing an assembly reference?)

(9,26): error CS0234: The type or namespace name 'Net' does not exist in the namespace 'System' (are you missing an assembly reference?)

(28,28): error CS0012: The type 'TextWriter' is defined in an assembly that is not referenced. You must add a reference to assembly 'System.Runtime.Extensions, Version=4.2.2.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a'.

(43,28): error CS0012: The type 'TextWriter' is defined in an assembly that is not referenced. You must add a reference to assembly 'System.Runtime.Extensions, Version=4.2.2.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a'.

(58,28): error CS0012: The type 'TextWriter' is defined in an assembly that is not referenced. You must add a reference to assembly 'System.Runtime.Extensions, Version=4.2.2.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a'.

(73,28): error CS0012: The type 'TextWriter' is defined in an assembly that is not referenced. You must add a reference to assembly 'System.Runtime.Extensions, Version=4.2.2.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a'.

(87,28): error CS0012: The type 'TextWriter' is defined in an assembly that is not referenced. You must add a reference to assembly 'System.Runtime.Extensions, Version=4.2.2.0, Culture=neutral, PublicKeyToken=b03f5f7f11d50a3a'.

(1858,18): error CS0117: 'FileStream' does not contain a definition for 'Open'

(1870,23): error CS1061: 'FileStream' does not contain a definition for 'Write' and no accessible extension method 'Write' accepting a first argument of type 'FileStream' could be found (are you missing a using directive or an assembly reference?)

如何“添加对程序集的引用”？可以在dafny命令行上完成吗？

Answer 1

我认为文件示例不需要 System.Net 导入，因此您可以从 fileionative.cs 文件中删除这些包含。

我不确定TextWriter 错误，但如果您能找出您需要的程序集引用，您可以通过手动运行csc 将其添加到命令行。这是在我的机器上工作的：

dafny fileiotest.dfy /spillTargetCode:3 /compile:0
csc fileionative.cs fileiotest.cs /r:System.Core.dll /r:System.dll /r:System.Collections.Immutable.dll /r:System.Runtime.dll /r:System.Numerics.dll

/spillTargetCode:3 参数告诉 Dafny 输出 fileiotest.cs 文件。 /compile:0 行告诉它跳过最后的编译步骤，所以你可以手动完成。

最后，对于你的最后两个错误：

(1858,18): error CS0117: 'FileStream' does not contain a definition for 'Open'

(1870,23): error CS1061: 'FileStream' does not contain a definition for 'Write' and no accessible extension method 'Write' accepting a first argument of type 'FileStream' could be found (are you missing a using directive or an assembly reference?)

我认为这是 Dafny 版本与 Dafny 生成的 C# 代码的约定不匹配的问题。来自另一个堆栈溢出答案的 fileionative.cs 使用名为 __default 的命名空间，但 Dafny 生成的 fileiotest.cs 使用名为 _module 的命名空间。因此，您只需更改 fileionative.cs 以使用正确的命名空间 _module。