Problem Set 0

Install Dafny

First, follow the instructions in Reading 0: Getting Started to get Dafny installed. All assignments will use this programming tool.

Download the problem set

Create a directory for this assignment, e.g. pset00, in the place where you plan to store your work on 6.S057. Don’t put it inside the 6.S057-constellation directory you created for in-class exercises — maybe next to it instead.

Download two files to your pset00 directory:

• pset00.dfy
• pset00_validator.dfy

Complete pset00.dfy

Then start from the provided template file pset00.dfy and complete the method implementations and proofs, as directed by the comments there.

Submit your completed pset00.dfy file on Gradescope by Wednesday, September 16 at 9pm.

The exercise for this assignment gets you started using Dafny.

This pset introduces a pattern we’ll follow throughout the semester: we provide both a template file (pset00.dfy) and a validator file (pset00_validator.dfy). You complete the exercises by editing the template, and, when you’re done, all of the “tests” in the validator should pass. They’re not quite tests in the usual sense, because one of them can cover infinitely many scenarios!

Check your work

From a command-line session in a directory containing both of these files, you can confirm that you completed the assignment with three commands. (Note that here we assume you have the Dafny executable dafny in your path for command-line execution.)

First, check that your solution passes verification. (Actually, we also ask to “run” your solution, but since you haven’t defined a “main” method, there is no actual code execution. Instead, we are making sure that no methods are missing implementations.)

dafny run pset00.dfy

Second, check that your solution doesn’t use any disallowed features (like for giving up on proofs without finishing them!).

dafny audit pset00.dfy

Finally, check that our validator accepts your implementation: every logical claim that the validator makes is provable, given what you have specified and proved.

dafny verify pset00_validator.dfy

Our goal is to set things up so that you earn most of the credit for an assignment if all three of these commands succeed! We won’t be grading on “style,” though we may give style feedback. Sometimes we give you only English specifications for code to write, and it’s possible to misinterpret those specifications and thus pass our “tests” while not meeting the spirit of the requirements, which we’ll try to catch and deduct credit for. Misinterpreting the requirements unintentionally is a lot harder for this method of grading, compared to usual test-based grading in conventional programming classes.