Assignment 6: Verification with Dafny

Due Thursday, May 14 at 11:59 PM

Goals for This Assignment

By the time you have completed this work, you should be able to:

• Implement small recursive routines with Dafny
• Prove small recursive routines correct with Dafny

Step-by-Step Instructions

Step 1: Write Implementation for drop

Download the template code here. This is the same code we've been working on in class. This code has drop partially implemented, but it's missing a body. Implement the body, and make sure it verifies. More details are provided in the file.

Step 2: Write Postconditions for append

Now move on to the append routine. In this case, a body has been provided, but postconditions are missing. More details are in the file.

Step 3: Write zip

Now move on to zip. For this one, you'll need to write the whole implementation from scratch, including the signature, preconditions, postconditions, and body. Further details are in the file, though this page is also informative.

Step 3: Submit Everything

Submit your lists.dfy file to the corresponding box on Canvas. In the comments for the submission, list everyone you worked with, if applicable.