Due: Mon, 11 Apr 2016 23:00:00 -0700
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.
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.
Notice that the command-line arguments are only accessible via functions and methods.
What would problems might arise if they were instead static class members of the HostConstants class?
Semantically, what does it mean if you add preconditions (requires) to the Main method?
Write a specification for Main that defines the copy utility.
That is, it expects two command-line arguments, source and destination,
and copies source to destination, assuming destination doesn’t already exist.
Write an implementation and prove that it meets you specification.
Put your solution in a file called cp.dfy and include it, along with any other files
you depend on, in a file cp.zip.
Extend Io.dfy and IoNative.cs to permit basic user input.
When doing a copy, if the file already exists, ask the user if it should be overwritten.
Prove that this is the only time when you will overwrite an existing file.
Building on your experience in the warm-up exercise, you will now write a utility for losslessly compressing and decompressing files. Your program should run from the command line as:
./compression 1 SourceFile DestFile
to compress SourceFile into DestFile. Given a 0 instead of a 1, it should decompress SourceFile into DestFile. In your file, you should prove that calling decompress on compress is the identity function. Note, however, that you will not receive credit for implementing compress and decompress as the identity function! Be sure to document any references you use for choosing your compression algorithms.
We have included three example files for you to run your compression and decompression routines on. We will test your solution on similar but not identical files. If your compression routine produces a smaller file in all three cases (and your decompression produces the original file) that will be a success.
Put your solution in a file called compression.dfy and include it, along with any other files
you depend on, in a file compression.zip.
In this assignment, your compression algorithm is lossless, which lends itself to a succinct specification. How would you succinctly specify the correctness of a lossy compression algorithm like JPG? This question is a bit speculative, so there isn’t necessarily a “correct” answer.
The solution that achieves the highest compression ratio will receive bonus points on this assignment, as well as incredible bragging rights.