Exercise 6: Formal Verification
Exercise Week 50, Thursday
Student Preparation
You should have Dafny installed and come prepared to ask questions about anything you do not understand. The teacher is there to help you. Any questions remaining after the session can be asked via the Canvas discussion thread.
The aim of this exercise session is to practice doing proofs in the weakest precondition calculus, to get a better understanding of roughly what goes on behind the scenes in Dafny’s program verifier.
Files:
Instructions
Solutions
Ex6-sol.pdf Download Ex6-sol.pdf