Reading from (Writing to) files in Dafny

Question

I've been looking at some dafny tutorials and couldn't find how to read from (or write to) simple text files. Surely, this has to be possible right?

Answer 1

I have cooked up a very basic file IO library for Dafny based on code from the Ironfleet project.

The library consists of two files: a Dafny file fileio.dfy declaring signatures for various file operations, and a C# file fileionative.cs that implements them.

As an example, here is a simple Dafny program that writes the string hello world! to the file foo.txt in the current directory.

To compile, place all three files in the same directory, then run:

dafny fileiotest.dfy fileionative.cs

which should print something like

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

Then you can run the program (I use mono since I'm on unix):

mono fileiotest.exe

which should print done on success.

Finally, you can check the contents of the file foo.txt! It should say hello world!

---

A few last notes.

First, the specifications for the operations in fileio.dfy are pretty weak. I haven't defined any kind of logical model of what's on disk, so you won't be able to prove things like "if I read the file I just wrote, I get back the same data". (Indeed, such things are not true except under additional assumptions about other processes on the machine, etc.) If you are interested in trying to prove such things, let me know and I can help further.

Second, one thing the signatures do give you is enforced error handling. All operations return a bool saying whether or not they failed, and the specifications basically tell you nothing unless you know all operations have succeeded. If this is a reasonable programming discipline for you, it's nice to have it enforced by Dafny. (If you don't want this, it's easy to take out.)