This homework is a problem set. Please see hw3.pdf for further instructions.
To submit the homework, please upload your solutions as a PDF (hw3.pdf) and accompanying code (hw3.dfy plus any corresponding helper files) to Gradescope.
-
Please ensure that your code is called
hw3.dfyand your file is calledhw3.pdfto get credit. -
You are encouraged (but not required) to write your solutions in LaTeX; if you would like to edit
hw3.texdirectly, please remove or comment out the problem statements and include only your solutions. The homework should be typed.
This homework continues with Dafny and its logical foundations (strongest postconditions, weakest preconditions, and Hoare logic). For the Hoare logic question, it will be helpful to see some coverage of Hoare logic which we will cover in class this week.