Assignment 5: Proving Correctness in Dafny

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. I strongly suggest you read Chapter 6 of your textbooks, which contains step-by-step guidelines on how to prove programs correct.

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, Chapter 6). 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 archived Dafny files with missing annotations. No separate write-up is needed. Make sure you acknowledge collaboration with other students.