Solution to the Student Exercises

Tom Kelliher, CS23

Feb. 12, 1997

Student Exercises

Determine pre- and post- conditions and loop invariants for the following:

Note: I assume that you'll be fine with the pre- and post-conditions. I'll just give the loop invariants here.

1. A function which computes the sum of the first n elements of the Fibonacci sequence

   int fibSum(int n)
   {
      int fib1 = 0;   // First number in Fibonacci sequence.
      int fib2 = 1;   // Second number in Fib. sequence.
      int fib3;
      int i;
      int sum = 1;
   
      for (i = 2; i < n; ++i)
      {
         fib3 = fib2 + fib 1;   // Generate next number in sequence.
         fib1 = fib2;           // "Move up" one sequence number.
         fib2 = fib3;
         sum += fib3;
      }
   
      return sum;
   }
   

   The invariant:

   sum is the sum of the first i members of the Fibonacci sequence.

   Upon exit from the loop, sum is the sum of the first n elements of the Fibonacci sequence.

2. A function which finds the sum of the first five positive values in an integer array with n elements

   int sumFive(int array[], int n)
   {  int count;   // # of positive elements found
      int i;       // loop counter
      int sum      // sum of positive elements
   
      for (count = i = sum = 0; i < n && count < 5; i++)
         if (array[i] > 0)
         {
            count++;
            sum += array[i];
         }
   
      if (count == 5)
         return sum;
      else
         return -1;   // Return garbage value if we can't find five
                      // positive values.
   }
   

   The invariant:

   sum is the sum of the first count positive values in array.

3. A function which iteratively performs binary search

   int binSearch(int data[], int n, int item)
   {
      int first = 0;
      int last = n - 1;
      int mid
   
      while (first < last)
      {
         mid = (first + last) / 2;
   
         if (data[mid] == item)
            return mid;
         else if (data[mid] < item)
            first = mid + 1;
         else
            last = mid - 1;
      }
   
      return -1;
   }
   

   The invariant:

   If item is in data then: .