Assignment 3: Proving Correctness in Dafny
- Due Mar 8, 2016 by 11:59pm
- Points 20
- Submitting a file upload
- File Types zip
- Available until Mar 8, 2016 at 11:59pm
Your Task
The assignment consists of 5 problems. Your task for each problem is to prove its postcondition correct in Dafny. Apart from adding necessary annotations, do not change the source code of the assignment problems. Make sure to double-check that your preconditions are satisfiable, as we discussed in class. You do not have to prove termination. If needed, assume that input arrays are not empty.
Problems
Problem 1 [2 points]. Open LinearSearch.dfy
Download LinearSearch.dfy in Dafny. Add preconditions and loop invariants needed to prove the postcondition and any default Dafny checks (e.g., array out of bounds). Do not change the postcondition.
Problem 2 [2 points]. Open Abs.dfy
Download Abs.dfy in Dafny. Add preconditions and loop invariants needed to prove the postcondition and any default Dafny checks (e.g., array out of bounds). Do not change the postcondition.
Problem 3 [2 points]. Open BubbleSort.dfy
Download BubbleSort.dfy in Dafny. Add preconditions and loop invariants needed to prove the postcondition and any default Dafny checks (e.g., array out of bounds). Do not change the postcondition. This is a warm-up sorting problem since the solution is explained in great detail in the textbook (The Calculus of Computation). So you are encouraged to study the solution and read that part of the textbook. You can find a link to the free electronic version of the textbook on the course webpage.
Problem 4 [4 points]. Open InsertionSort.dfy
Download InsertionSort.dfy in Dafny. Add preconditions and loop invariants needed to prove the postcondition and any default Dafny checks (e.g., array out of bounds). Do not change the postcondition.
Problem 5 [10 points]. Open MergeSort.dfy
Download MergeSort.dfy in Dafny. Add preconditions, postconditions, and loop invariants needed to prove the postcondition and any default Dafny checks (e.g., array out of bounds). Do not change the postcondition of method MergeSort.
Assignment Deliverables
Submit your solutions in the form of (zip archived) Dafny files with missing annotations. No separate write-up is needed. Make sure you acknowledge collaboration with other students.