Problem Set 1

Download the problem set

Create a directory for this assignment, e.g. pset01, in the place where you are storing 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 pset01 directory:

• pset01.dfy
• pset01_validator.dfy

Complete pset01.dfy

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

Submit your completed pset01.dfy file on Gradescope by Wednesday, September 23 at 9pm.

The exercises for this assignment get you started writing Dafny code and proving it correct, working just with simple built-in container types.

This pset uses the pattern we’ll follow throughout the semester: we provide both a template file (pset01.dfy) and a validator file (pset01_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 pset01.dfy

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

dafny audit pset01.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 pset01_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.