Description

Introduction

In this assignment you will prove correctness of loops using the techniques we discussed in class. Write your answers to problems 1-4 in a text file hw2/answers/hw2_answers.txt.

Problems

Problem 1 (8pts): Computing the Sum of an Integer Array

In lecture, we gave an example of an algorithm to find the sum of the integer elements of an array a[0..len-1]. Our loop had the following as part of its invariant:

sum = arr[0]+arr[1]+...+arr[i-1]

Suppose we decide to use the following slightly different invariant instead:

sum = arr[0]+arr[1]+...+arr[i]

(The difference is that the upper bound of the array section is i instead of i-1.)

Rework the code in the example to use this new invariant instead of the original one and show that the modified code is correct. (You have to use computation induction as we did in class: 1) show invariant holds before loop, 2) show if it held after k-th iteration and execution takes a (k+1)-st iteration, invariant still holds, and 3) show that your loop exit condition and the loop invariant imply the poscondition, namely that sum = arr[0] + arr[1] + … + arr[arr.length-1].) You do not need to argue termination.

After solving this problem, give a brief description of how this change to the invariant affected the algorithm. What were the major changes? Did this change make the code easier or harder to write or prove compared to the original version? Why? (You should keep your answers brief and to the point.)

Problem 2 (15pts) The Dutch National Flag Problem

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. Assume the existence of a function swap(arr, i, j) which swaps the ith and jth elements of arr.

The following picture illustrates the desired postcondition:

          0                    k                 N
         +--------------------+-----------------+
     arr |   all red          | all blue        |
         +--------------------+-----------------+

Write an expression for the postcondition.

Write a suitable loop invariant for any loops in your pseudocode.

Problem 3 (10pts): Exponentiation by squaring

Below is the pseudocode for exponentiation by squaring.

Precondtion: n >= 0
int power(int m, int n) {
  int x = m;
  int y = n;
  int result = 1;
  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

Assume that the loop invariant is m^n = result*x^y. Show that 1) the invariant holds before the loop (base case), 2) assuming invariant holds after k-th iteration, and execution takes a k+1-st iteration, the invariant still holds (inductive step), 3) the loop exit condition and the loop invariant imply the postcondition result = m^n.

Find a suitable decrementing function. Prove that the function is indeed a decrementing function.

Problem 4 (15pts): Additive Factorial

Below we give, in Dafny, the factorial function and a method with loops, which should be computing the factorial of a number as well.

Fill the annotations at the designated places. As in the example in class you can use the function (Factorial) in the annotations. Fill the two loop invariants and the assertion (the assertion states the postcondition that holds if the inner loop terminates; this postcondition can help prove partial correctness).

Next, use computation induction to prove partial correctness.

function Factorial(n: int): int
  requires n >= 0
{
  if n == 0 then 1 else n * Factorial(n-1)
}

method LoopyFactorial(n: int) returns (u: int)
  requires n >= 0
  ensures u == Factorial(n)
  {
    u := 1;
    var r := 0;
    while (r < n) 
      invariant ? YOUR ANSWER HERE
    {
      var v := u;
      var s := 1;
      while (s<=r) 
        invariant ? YOUR ANSWER HERE
      {
        u:=u+v;
        s:=s+1;
      }
      assert ? YOUR ANSWER HERE 
      r:=r+1;
    }
  }

Use Dafny to check your answer.

Collaboration (1pt)

Please answer the following questions in a file named collaboration.txt in your hw2/answers/ directory.

The standard academic integrity policy applies to this homework.

State whether or not you collaborated with other students. If you did collaborate with other students, state their names and a brief description of how you collaborated.

Reflection (1pt)

Please answer the following questions in a file named reflection.txt in your hw2/answers/ directory. Answer briefly, but in enough detail to help you improve your own practice via introspection and to enable me to improve Principles of Software in the future.

1. In retrospect, what could you have done better to reduce the time you spent solving this homework?
2. What could the Principles of Software staff have done better to improve your learning experience in this homework?
3. What do you know now that you wish you had known before beginning the homework?

Submission

You should add and commit the following files to SVN:

• hw2/answers/hw2_answers.txt
• hw2/answers/reflection.txt
• hw2/answers/collaboration.txt

Hints

When trying to come up with a loop invariant for prewritten code, it often helps to trace through the execution of the code on paper. Choose a few different starting values of variables defined outside the block of code (such as method arguments), and write down the values of all the variables used in the loop for each iteration.

Errata

Check the course Announcements page regularly. I’ll announce corrections to the homework text on the Announcements page, if they arise.