For this homework, you will need to have a machine with VSCode and the Dafny VSCode extension installed. You should have installed these as part of HW0.
This is a programming assignment, where you will directly edit the source files. There are a few parts:
- Part 1 is a series of mini exercises.
- Part 2 is about classes and class invariants.
- Part 3 is about writing verified code with loop invariants.
As with HW1, the assignment will be submitted through Gradescope.
To continue, open and edit the files part1.dfy, part2.dfy, and part3.dfy.
If you get stuck, selected hints for some problems are in the file hints.md.
I have always found the Dafny tutorial and Dafny cheatsheet to be super helpful.
Beyond these: please continue to ask questions on Piazza and drop by office hours!