如何将 Dafny 代码与 C# 程序集链接 [英] How to link Dafny code with a C# assembly

问题描述

我正在尝试构建和运行一个 James Wilcox 结合 Dafny 代码和 C# 代码的示例程序.我在 Mac 上使用 mono.该答案中的构建命令对我不起作用:

I'm trying to build and run an example program by James Wilcox that combines Dafny code and C# code. I'm using mono on a Mac. The build command in that answer doesn't work for me:

$ 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 命令行上完成吗?

How can I "add a reference to assembly"? Can it be done on the dafny command line?

推荐答案

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

I don't think you need the System.Net imports for the file example, so you can just delete those includes from the fileionative.cs file.

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

I am not sure about the TextWriter errors, but if you can figure out what assembly reference you need, you can add it to the command line by running csc manually. This is what worked on my machine:

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 行告诉它跳过最后的编译步骤，因此您可以手动完成.

The /spillTargetCode:3 argument tells Dafny to output the fileiotest.cs file. The /compile:0 line tells it to skip the final compilation step, so you can do it manually.

最后，对于您的最后两个错误:

Finally, for your last two errors:

(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 使用名为 __default 的命名空间代码>_module.因此，您只需要更改 fileionative.cs 以使用正确的命名空间 _module 代替.

I believe this is a Dafny version mismatch thing with the conventions expected of Dafny-generated C# code. The fileionative.cs from the other stack overflow answer uses a namespace called __default, but the Dafny-generated fileiotest.cs uses a namespace called _module. So you just need to change fileionative.cs to use the correct namespace _module instead.

这篇关于如何将 Dafny 代码与 C# 程序集链接的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！