Assignment 2: Dafny

Due: Fri, 03 Feb 2017 23:59:00 -0500

The goals of this assignment are to practice using Dafny, Dafny’s various language constructs, and some custom extensions to Dafny in order to implement some file-manipulating programs.

For this assignment, you’ll need some additional files.

Please answer the inline questions below in answers.txt.

Background

Dafny can be extended by binding trusted Dafny interfaces to C# code. For example, by default, Dafny doesn’t support any command-line arguments. However, we can extend it to do so as shown in the Io.dfy and IoNative.cs files you downloaded above. Notice that the class HostConstants has methods to determine how many command-line arguments were provided, as well as to retrieve them. It also has a function that lets you talk about those arguments in specification contexts. Notice that each one is marked as {:extern}, which means both that the interface is axiomatically trusted and that Dafny will expect us to provide a C# implementation of each executable method. This is exactly what IoNative.cs provides. Notice that the names used in IoNative.cs carefully line up with those chosen in Io.dfy (though this isn’t necessary if you specify the names when providing the extern annotation). To connect the two, pass IoNative.cs as an extra command-line argument to Dafny when compiling.

To make use of the Io routines, you can use Dafny’s include mechanism. In another file, just write include "Io.dfy" at the top-level of the file, and include IoNative.cs on your command line when invoking Dafny.

Question

Notice that in the FileSystemState and the FileStream classes, all of the functions say they read this. Why is this important?

Question

Notice that it isn’t possible to create new FileSystemState objects. What would problems might arise if this were possible?

Question

Semantically, what does it mean if you add preconditions (requires) to the Main method?

File copy

Write a specification for Main that defines a copy utility. That is, the program expects two command-line arguments, source and destination, and copies source to destination, assuming destination doesn’t already exist. Be sure to make the specification as strong and precise as you can, given the interface defined in Io.dfy.

Write an implementation and prove that it meets your specification. Put your solution in a file called basic-cp.dfy and include it, along with any other files you depend on, in a file basic.zip.

Challenge

Extend Io.dfy and IoNative.cs to permit basic user input.
Extended you specification so that when performaing a copy, if the file already exists, the user is asked if the file should be overwritten. Extend your implementation to support this functionality, and prove that this is the only time when you will overwrite an existing file. Put your solution in a file called advanced-cp.dfy and include it, along with any other files you depend on, in a file advanced.zip.

Suggestions

Start early. Verification will take longer than you expect.
Work in small, incremental steps. Don’t try try to write all of the code at once and then go back and prove it correct.
Using small, well-factored methods will likely help.
Even though we’re verifying everything, comments in the code are still encouraged! They help explain your high-level ideas to others, or even to future versions of you.

Submissions and Grading

Please submit a single zip file dafny-AndrewID.zip via Blackboard (where AndrewID is obviously replaced with your actual ID). The zip file should be arranged such that it contains:

answers.txt
basic.zip
advanced.zip (if you choose to do the challenge problem)

The grading script will expect the following commands to execute correctly, given your zip file:

unzip dafny.zip
mkdir basic
cd basic
unzip ../basic.zip
echo Test > file1.txt
dafny /noCheating:1 /timeLimit:120 basic-cp.dfy IoNative.cs
./basic-cp.dfy file1.txt file2.txt
... other tests here ...
cd ..
mkdir advanced
cd advanced
unzip ../advanced.zip
echo Test > file1.txt
dafny /noCheating:1 /timeLimit:120 advanced-cp.dfy IoNative.cs
./advanced-cp.dfy file1.txt file2.txt
... other tests here ...
cd ..
cat answers.txt

If you decide to include additional files, please add a README explaining how they relate. The grading script will run Dafny over them as well, with the same parameters shown above.