Problem Set 2

Download

• pset02_definitions.dfy
• pset02.dfy
• pset02_validator.dfy

pset02_definitions  and  {:induction false}

For this assignment, we provide a file pset02_definitions.dfy with some definitions of simple functions. Your job is to start from the provided template file pset02.dfy and fill in the requested lemma proofs. Submit this completed file on Gradescope by the deadline.

Like last time, use the validator file pset02_validator.dfy to check your work roughly as we will in our autograder. All three files should be stored in the same directory. One twist is that we require you write {:induction false} in every lemma definition for this assignment. The purpose is to turn off some automatic lemma-proving, which will certainly come in handy later, but for now we want you to get some practice proving lemmas more manually.

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. (These commands won’t catch a case of explicitly turning on automatic induction with {:induction true}, so don’t write that in your file, and we’ll use other scripts to look for it.)

First, check that your solution passes verification.

dafny run --manual-lemma-induction pset02.dfy

In this case, we do expect exactly one error message! Here’s what it looks like in Dafny 4.11:

Dafny program verifier finished with 16 verified, 0 errors
pset02_definitions.dfy(44,11): Error: Function Defs._default.F has no body so it cannot be compiled
   |
44 |   function F(x: int): int
   |            ^

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

dafny audit pset02.dfy

Finally, check that our validator accepts your implementation.

dafny verify pset02_validator.dfy