COMP 280 Assignment 9

The following problems total to 70 points.

1. (10 points) Rosen 6th ed. 4.5 #12 (reworded)

   This program computes quotients and remainders.

        positive int a
        positive int d
   
        int r
        int q
   
        r := a
        q := 0
        while r ≥ d
           r := r - d
           q := q + 1
        

   Verify the correctness of this program, i.e., that the program terminates with a=dq+r and 0≤r<d.

2. (10 points -- 5 points each part)

   In class, we discussed how to use a loop invariant I with a while loop:

        while (C) body
   

   In summary, you must prove all four of the following:
   • I holds before the loop's first iteration
   • I∧C → I′
   • I∧¬C → G, where G is our goal formula
   • ¬C is eventually true

   Describe how this process must be modified when using for loops.

   1. C-style: for (s1; C; s2) s3;
   2. Pascal-style: for i := v1 to v2 do body

   As with while loops, use the simplifying assumptions that C is a side-effect-free Boolean condition and that there is no other mechanism to break out of the loops.

3. (10 points) Rosen 6th ed. 4.5 #8 (reworded)

   Use the result of the previous problem to verify the correctness of Algorithm 8 of Section 4.4:

        procedure iterative-fibonacci(n: nonnegative integer)
        if n = 0
        then
           y := 0
        else
           x := 0
           y := 1
           for i := 1 to n-1
              z := x+y
              x := y
              y := z
        // y is the nth Fibonacci number
        

4. (10 points)

   Prove that the following program computes xn. We take 0⁰ to be 1. (A better answer might be +NaN.0, a designation for "Not a Number", but that just adds a special case to the code and its correctness proof, so we omit it for simplicity.) You may assume there is no round-off or overflow error.

        ; pow: real, natnum → real
        ; Return xn  (where we interpret 00 as 1).
        ; 
        (define (pow x n) (pow-help x n 1))
   
        ; pow-help: real, natNum, real → real
        ; Return xn × soFar  (where we interpret 00 as 1).
        ;
        (define (pow-help x n soFar)
          (cond [(zero? n) soFar]
                [(odd?  n) (pow-help (sqr x) (quotient n 2) (* soFar x))]
                [(even? n) (pow-help (sqr x) (quotient n 2) soFar)]))
   

5. (20 points — including 5 points for loop invariant and 5 points for termination proof)

   Prove that the following program computes xn. Again, we take 0⁰ to be 1. You may assume there is no round-off or overflow error.

        /* pow: return x_orign_orig,
         * where x_orig is any number, n_orig ≥ 0, 
         * and we interpret 00 as 1.
         */
        real pow( real x_orig, natnum n_orig )
        {
          real   soFar ← 1
          natnum n     ← n_orig;    
          real   x     ← x_orig;    // This will be x_orig(2i), where i is number of times through loop.
   
          // LoopInvariant: …?
          while (n > 0)
          {
            if odd?(n)   soFar ← soFar * x
            n ← quotient(n, 2)
            x ← sqr(x)
          }
   
          return soFar
        }
   

6. (10 points)

   Prove that, after the following pseudocode terminates,

   • a[h] = val;
   • for all p in the range i≤p<h, a[p]<val; and
   • for all p in the range h<p≤j, a[p]≥val.

   In particular, val is in the position in the array a[i], …, a[j] where it would be if the array were sorted.

        val = a[i]
        h = i
        for k=i+1 to j
            if (a[k] < val} {
               h = h+1
               swap(a[h],a[k])
            }
        swap(a[i],a[h])
   

   Hint: Use the following loop invariant. Also, drawing a picture of the array contents and invariant conditions may be helpful.

   • h<k;
   • for all p in the range i<p≤h, a[p]<val; and
   • for all p in the range h<p<k, a[p]≥val.

   This version of partitioning, as used in Quicksort for example, is due to Nico Lomuto.