Problem Set 4

Merge sort & database queries

Before you start this problem set

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

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

• pset04_definitions.dfy
• pset04.dfy
• pset04_validator.dfy

The structure here follows that of previous psets: read pset04_definitions.dfy to see how we’ve set up some examples in sorting and transformation of syntax trees, complete pset04.dfy with your proofs of the requested lemmas, and use pset04_validator.dfy to confirm you’re done.

A note about partial credit

If you do not finish the problem set, the autograder will attempt to give you partial credit for the parts you did complete, but it can only do that if your code passes verification. That may require commenting out some of your work so that the remaining parts are all-green.

In the case of a submitted lemma with no body, the autograder will inject requires false and an empty body so that dafny audit can check for other issues, but you also cannot use that lemma in other proofs. If you don’t understand your autograder report, please visit office hours or post privately on Piazza, but be sure to do this ahead of the deadline.

Do not wait until the last minute to submit your work. While we recommend using VS Code to write your solutions, see instructions in Problem Set 3 for how to check your work on the command-line.