file - 从 Dafny 中读取(写入)文件

Question

我一直在看一些 dafny教程并且找不到如何读取(或写入)简单的文本文件。当然，这一定是可能的吧？

Answer 1

我根据 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中的操作规范很弱。我还没有定义磁盘上的任何类型的逻辑模型，因此您将无法证明诸如“如果我读了我刚写的文件，我会得到相同的数据”之类的东西。 (确实，这些事情不是真的，除非对机器上的其他进程有额外的假设等。)如果您有兴趣尝试证明这些事情，请告诉我，我可以提供进一步的帮助。

其次，签名为您提供的一件事是强制错误处理。所有操作都返回一个 bool 值，说明它们是否失败，除非您知道所有操作都已成功，否则规范基本上不会告诉您任何信息。如果这对您来说是一个合理的编程规则，那么由 Dafny 强制执行它是很好的。 (如果你不想要这个，很容易取出。)