Problem Set 3

Before you start this problem set

Please fill out this very brief survey about the time you spent on Problem Set 2.

Your responses help us gauge how the problem sets are going so we can improve future problem sets and future iterations of 6.S057!

Download

• pset03_definitions.dfy
• pset03.dfy
• pset03_validator.dfy

This assignment is broken into files like the last one was: pset03_definitions.dfy with definitions your code will refer to, pset03.dfy as the template for you to edit, and pset03_validator.dfy as the checker that you completed the assigned tasks.

Check your work

From a command-line session in a directory containing all three of these files, you can confirm that you completed the assignment with three commands.

First, check that your solution passes verification.

dafny run pset03.dfy

Second, check that your solution doesn’t use any disallowed features.

dafny audit pset03.dfy

Finally, check that our validator accepts your implementation.

dafny verify pset03_validator.dfy