7

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?

OrenIshShalom
  • 5,974
  • 9
  • 37
  • 87
  • Dafny has no standard library or primitives for file I/O. (There is one primitive, `print`, that prints to stdout. Is that enough for what you want to do?) If you want to do general file I/O from Dafny, the way to do it is to write signatures for external methods that are implemented in C#. If you think this is a direction you are interested in, I can try to show you how it works, but I wanted to check if you like the idea before I start, because it will be a decent amount of work. – James Wilcox Sep 23 '18 at 00:47
  • @JamesWilcox thanks! `print` alone is indeed not sufficient, and it would be really great if you can show me how to proceed with your suggestion of writing signatures for external C# implementations. Thanks again! – OrenIshShalom Sep 23 '18 at 07:01

1 Answers1

7

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.)

James Wilcox
  • 5,307
  • 16
  • 25
  • I have some parse errors when I run `$ dafny fileiotest.dfy fileionative.cs` I get: `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` 3 parse errors detected in fileiotest.dfy Does that make sense? especially the error in line 26 – OrenIshShalom Sep 24 '18 at 14:40
  • you're using a quite old version of Dafny. can you try updating and see if it works? – James Wilcox Sep 25 '18 at 03:41
  • Yes, indeed upgrading to 2.2.0.10923 solved everything. – OrenIshShalom Oct 13 '18 at 06:24
  • is there any chance you can explain how to pass an input file name to main? and keep reading text lines from that file until EOF is reached? or should I simply post a separate post just about that? thanks anyway! – OrenIshShalom Oct 14 '18 at 09:23