我已经根据来自Ironfleet 项目的代码为 Dafny 编写了一个非常基本的文件 IO 库。
该库由两个文件组成：一个 Dafny 文件fileio.dfy声明各种文件操作的签名，以及一个实现它们的 C# 文件fileionative.cs。
例如，这里有一个简单的 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 强制执行它是很好的。（如果你不想要这个，很容易取出。）