我一直在查看一些 dafny 教程，但找不到如何读取（或写入）简单文本文件的方法。当然，这一定是可能的吧？
【问题讨论】：
print，打印到标准输出。这足以满足您的要求吗？）如果您想从 Dafny 执行通用文件 I/O，方法是为外部编写签名在 C# 中实现的方法。如果您认为这是您感兴趣的方向，我可以尝试向您展示它是如何工作的，但我想在开始之前检查您是否喜欢这个想法，因为这将是大量的工作。
print 单独确实是不够的，如果你能告诉我如何继续你为外部 C# 实现编写签名的建议，那就太好了。再次感谢！
尝试使用 /r:System.Core.dll /r:System.dll /r:System 编译（使用 csc.exe）两个文件 fileionative.cs 和 fileiotest.cs（后者由 Dafny 编译器生成）。 Collections.dll /r:System.Runtime.dll /r:System.Numerics.dll，引发了很多错误，与无法访问有关，例如：
error CS0122: 'System.Collections.Immutable.ImmutableArray<T>' is inaccessible due to its protection level
error CS0053: Inconsistent accessibility: property type 'System.Collections.Immutable.ImmutableArray<T>' is less accessible than property
'Dafny.Sequence<T>.ImmutableElements'
和其他类似的。
请问，有人可以做一个简单的 Dafny 程序，它使用外部 C# 系统方法（用于读取文件的本机代码）读取文本文件并返回要在 Dafny 程序中使用的读取字符串吗？
【讨论】：
我正在尝试在 Dafny 3.1.0 中使用这个 fileiotest.dfy。为此，我首先修复了 fileio.dfy 中 HostEnvironment 类中缺少构造函数，方法是将其重写为：
class HostEnvironment
{
constructor{:axiom} () requires false
ghost var ok:OkState
}
fileio.dfy 和 fileiotest.dfy 在 Dafny 中都能完美编译。 但是，当我尝试使用 fileionative.cs 进行组装时，出现以下错误：
PS C:\Users\jiplucap\Desktop\CTL_Models_and_Proofs\fileio> & "C:\Program Files\dotnet\dotnet.EXE" "c:\Users\jiplucap\.vscode\extensions\correctnesslab.dafny-vscode-1.6.0\out\resources\dafny\Dafny.dll" "c:\Users\jiplucap\Desktop\CTL_Models_and_Proofs\fileio\fileiotest.dfy" /verifyAllModules /compile:1 /spillTargetCode:1 /out:bin\fileiotest fileionative.cs
Dafny program verifier finished with 12 verified, 0 errors
Wrote textual form of target program to fileiotest.cs
Errors compiling program into fileiotest
(9,30): error CS0234: The type or namespace name 'IPEndPoint' does not exist in the namespace 'System.Net' (are you missing an assembly reference?)
(8,28): error CS0234: The type or namespace name 'Sockets' does not exist in the namespace 'System.Net' (are you missing an assembly reference?)
(1888,18): error CS0117: 'FileStream' does not contain a definition for 'Open'
(1900,23): error CS1061: 'FileStream' does not contain a definition for 'Write' and no accessible extension method 'Write' accepting a first argument of type 'FileStream' cam' could be found (are you missing a using directive or an assembly reference?)
我也尝试使用配置 /spillTargetCode:3，然后我得到了另一种错误。
请问，有什么方法（在 Dafny 3.1.0 中）组装 fileiotest.dfy 和 fileionative.cs 可以生成 fileiote.exe？
【讨论】：
我已经根据Ironfleet project 中的代码为 Dafny 制作了一个非常基本的文件 IO 库。
该库包含两个文件：一个为各种文件操作声明签名的 Dafny 文件 fileio.dfy，以及一个实现它们的 C# 文件 fileionative.cs。
例如，here 是一个简单的 Dafny 程序，它将字符串 hello world! 写入当前目录中的文件 foo.txt。
要编译，请将所有三个文件放在同一目录中，然后运行：
dafny fileiotest.dfy fileionative.cs
应该打印类似的东西
Dafny 2.1.1.10209
Dafny program verifier finished with 4 verified, 0 errors
Compiled program written to fileiotest.cs
Compiled assembly into fileiotest.exe
然后你就可以运行程序了（我用mono，因为我在unix上）：
mono fileiotest.exe
成功时应该打印done。
终于可以查看foo.txt文件的内容了！应该是hello world!
一些最后的笔记。
首先，fileio.dfy 中的操作规范非常薄弱。我还没有为磁盘上的内容定义任何类型的逻辑模型，因此您将无法证明诸如“如果我读取我刚刚编写的文件，我将返回相同的数据”之类的事情。 （事实上，除非对机器上的其他进程等进行额外假设，否则这些事情是不正确的。）如果您有兴趣尝试证明这些事情，请告诉我，我可以提供进一步的帮助。
第二，签名做给你的一件事是强制错误处理。所有操作都会返回一个布尔值，说明它们是否失败，除非您知道所有操作都已成功，否则规范基本上不会告诉您任何内容。如果这对您来说是一个合理的编程规则，那么让 Dafny 来执行它是一件好事。 （如果你不想要这个，很容易拿出来。）
【讨论】：
$ dafny fileiotest.dfy fileionative.cs 时遇到一些解析错误我得到：Dafny program verifier version 1.9.7.30401, Copyright (c) 2003-2016, Microsoft. fileiotest.dfy(7,18): Error: semi expected fileiotest.dfy(7,53): Error: invalid Suffix fileiotest.dfy(26,42): Error: invalid Suffix 在fileiotest.dfy 中检测到3 个解析错误这有意义吗？尤其是第 26 行的错误