CSCI 2600 Principles of Software
In this assignment you will prove correctness of loops using the techniques we discussed in class.
Submission Instructions
• Follow the directions in the version control handout for cloning your hw02 git repo.
•
Submit your answers in a single .PDF file named hw2_answers.pdf in the answers/ directory of your repository.
You MUST type up your answers. Handwritten solutions will not be accepted or graded,
even if they are scanned into a PDF file.
We recommend using LaTeX. If you have never
used LaTeX, take a look at this tutorial.
• Be sure to commit and push the file to Submitty. Follow the directions in the version control handout for adding and committing files.
• Important: You must press the Grade My Repository button for your answers to be graded. If you do not, they will not be graded and you will receive a zero for this homework.
Problems
Below is the pseudocode for product by addition.
Precondition: n >= 0int product(int m, int n) { int x = m; int y = n; int result = 0; while (y != 0) { if (y is even) { x = x+x; y = y/2; } else { result = result+x; y = y-1; } } return result;}Postcondition: result = m*n
a) Find a suitable loop invariant. (3 pts)
b) Show that the invariant holds before
the loop (base case). (1 pts)
c) Show by induction that if the invariant
holds after k-th iteration, and execution takes a
k+1-st iteration, the invariant still holds (inductive step). (6 pts)
d) Show that the loop exit condition and
the loop invariant imply the postcondition result = m*n. (1 pts)
e) Find a suitable decrementing function.
Show that the function decreases at each iteration and that when it reaches a
minimum the loop is exited. (2 pts)
f) Implement product by addition in Dafny. (2 pts, autograded)
• Do NOT include method Main in your Dafny code that you submit on Submitty. If you use Main method for testing, make sure you comment it out before submitting on Submitty.
•
Method that implements product by addition must be named
product and have the following header:
method product(m: int, n: int) returns (result: int)
•
You will need to define an additional
prod function with the following header:
function prod(m: int, n: int): int to be used in conditions.
• To help Dafny prove that doubling x and halving y doesn't change the product, define the following lemma:
lemma double_and_halve(m:int, n:int) requires n >= 0 ensures prod(m, 2 * n) == prod(m + m, n);{ if (n != 0) { double_and_halve(m, n - 1); }}
Then use it in your code:
if y % 2 == 0 {{ double_and_halve(x, y / 2); . . .}
• Make sure to include the precondition and the postcondition, as well as your invariant and the decrementing function.
• Verify your code with Dafny before submitting.
• Submit your Dafny code as a file named problem1.dfy in the answers/ folder.
Given an array arr[0..N-1] where each of the elements can be classified as red or blue, write pseudocode to rearrange the elements of arr so that all occurrences of blue come after all occurrences of red and the variable k indicates the boundary between the regions. That is, all arr[0..k-1] elements will be red and elements arr[k..N-1] will be blue. Assume the existence of a function swap(arr, i, j) which swaps the ith and jth elements of arr. (6 pts)
The following picture illustrates the condition of the
array at exit.
0 k N +--------------------+-----------------+arr | all red | all blue |
+--------------------+-----------------+
Write an expression for the postcondition. (2 pts)
Write a suitable loop invariant for all loops in your pseudocode. (4 pts)
Implement your pseudocode in Dafny. (2 pts, autograded)
• Do NOT include method Main in your Dafny code that you submit on Submitty. If you use Main method for testing, make sure you comment it out before submitting on Submitty.
• Represent each element of arr as either character 'r' (red) or character 'b' (blue).
•
Method that solves the Simplified Dutch National Flag Problem must be named
dutch and have the following header:
method dutch(arr: array?<char>) returns (k: int)
This method modifies
arr and returns the value of
k.
• Methods that modify arr might require a modifies arr annotation.
• You may find slicing and concatenating arrays useful. See Dafny Tutorial for more details and examples.
• In cases when your method changes the array, your conditions can refer to both new (current) and the old (previous) values by using the old keyword. For example, arr[..] == old(arr[..]) means that arr has not changed.
• Make sure to include the precondition and the postcondition, as well as your invariant and the decrementing function.
• Verify your code with Dafny before submitting.
• Submit your Dafny code as a file named problem2.dfy in the answers/ folder.
Below we give, in Dafny syntax, the factorial function and a method with loops, which should be computing the factorial of a number.
Fill in the annotations at the designated places. You can use the function (Factorial) in the annotations. Fill in the two loop invariants and the assertion.
function Factorial(n: int): int
requires n >= 0{ if n == 0 then 1 else n * Factorial(n-1)}