时间戳

首页 > 解决方案 > 在 Dafny 中读取（写入）文件

file - 在 Dafny 中读取（写入）文件

问题描述

我一直在看一些dafny教程，但找不到如何读取（或写入）简单文本文件的方法。当然，这必须是可能的，对吧？

标签： fileiodafny

解决方案

我根据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!

一些最后的笔记。

首先，in 中的操作规范fileio.dfy非常薄弱。我还没有为磁盘上的内容定义任何类型的逻辑模型，因此您将无法证明诸如“如果我读取我刚刚编写的文件，我会返回相同的数据”之类的事情。（事实上​​，除非对机器上的其他进程等进行额外假设，否则这些事情是不正确的。）如果您有兴趣尝试证明这些事情，请告诉我，我可以提供进一步的帮助。

其次，签名确实给您的一件事是强制错误处理。所有操作都返回一个布尔值，说明它们是否失败，除非您知道所有操作都成功，否则规范基本上不会告诉您任何内容。如果这对您来说是一个合理的编程规则，那么让 Dafny 来执行它是一件好事。（如果你不想要这个，很容易拿出来。）

推荐阅读