Discussion 3: Loop Invariants

Solutions

Exercise 1: Warmup

Suppose that we have a double[] array of sensor measurements. We expect all of the data to be non-negative; however, occasionally the sensor will record a spurious negative value. To "clean" the data, we'd like to "clip" these negative values, replacing them with 0. For example, the array

would become

We'll define a method cleanData() to carry out this operation.

(a)

Throughout the method, we'll use the loop variable i to keep track of the index of the next array entry that we will inspect. Suppose that we want to carry out the cleaning from right to left. Fill in the details of the following array diagram to model the invariant of this loop.

Inv:

data:

data.length

(b)

Fill in the details of the "Pre" array diagram to display what we know about the data array before entering the loop.

Pre:

data:

data.length

Based on your "Pre" and "Inv" diagrams, how should we initialize i?

We should initialize i = data.length - 1. When we slide the “Inv” boundary all the way to the right, then i sits just to the left of the end of the array, which is above the cell indexed data.length - 1.

(c)

Fill in the details of the "Post" array diagram to depict the state of the data array once we exit the loop.

Post:

data:

data.length

Based on your "Post" and "Inv" diagrams, what should our loop guard be to ensure that we exit the loop immediately after inspecting all of the array entries?

We should exit the loop once i passes before the first index of the array, once i < 0. Negating this, we must continue to loop while i remains a valid array index, so our loop guard is i >= 0.

(d)

Use your answers from parts (a)-(c) to complete the definition of the cleanData() method. Add a comment above the loop documenting the loop invariant. Then, fill in the loop body.

package cs2110;

public class CleanData {
  // SHOW: SECTION 1
  /** Reassigns all negative entries of the `data` array to 0. */
  static void cleanData(double[] data) { 
    int i = data.length - 1;
    /* Loop Inv: `data(i..] >= 0` */
    while (i >= 0) {
      if (data[i] < 0) {
        data[i] = 0;
      }
      i--;
    }
  }
  // SHOW: END 1
}

Exercise 2: Pivot Partitioning

When we partition an array, we split its entries into disjoint ranges according to some property. Here, we'll partition an int array into three segments by comparing its entries to a pivot, another special int value. We'll move all the entries that are less than the pivot to the beginning of the array, followed by all the entries that are equal to the pivot, followed by all the entries that are greater than the pivot. Soon in lecture, we'll see that this type of pivot partitioning forms the basis for the Quicksort algorithm.

You'll develop a method that uses three int loop variables (i, j, and k) and the following loop invariant:

Inv:

nums:

nums.length

(a)

Adjust the "Inv" array diagram back in time to draw the "Pre" array diagram.

Pre:

nums:

nums.length

Based on your "Pre" and "Inv" diagrams, how must we initialize i, j, and k?

i = 0;

j = nums.length;

k = nums.length;

(b)

Adjust the "Inv" array diagram forward in time to draw the "Post" array diagram.

Post:

nums:

nums.length

Based on your "Post" and "Inv" diagrams, what condition should we use to guard our loop?

The loop is finished with its work once the “?” region shrinks to become empty, which happens once i == j. Negating this, we must continue to loop while i < j, which is our loop guard.

(c)

Within the while loop of the partition3Way() method, we'll start by reading the value of nums[i]. For each of the following cases, describe what must be done in the loop body to make progress and restore the loop invariant.

nums[i] < pivot:

We can increment i to absorb nums[i] into the “< pivot” range.

nums[i] == pivot:

We should swap nums[i] and nums[j-1] and then decrement j.

nums[i] > pivot:

This one’s a bit more involved since we need to shift two ranges. We should swap nums[i] and nums[j-1] and then swap nums[j-1] and nums[k-1] before decrementing both j and k.

(Note: This particular way of swapping will always work, but other strategies that seem correct can fail in certain edge cases. For example, swapping nums[i] and nums[k-1] and then swapping nums[i] and nums[j-1] does the incorrect thing when j == k.)

(d)

Use your answers from parts (a), (b), and (c) to write the definition of the partition3Way() method. You may use the provided swap() method in your definition. Document your loop invariant (using range notation) in a multi-line comment above the loop declaration.

package cs2110;

public class Partition3Way {
  /** Swaps `nums[x]` and `nums[y]`. Requires `0 <= x,y < nums.length` */
  static void swap(int[] nums, int x, int y) { 
    int temp = nums[x];
    nums[x] = nums[y];
    nums[y] = temp;
  }

  // SHOW: SECTION 1
  /** Rearranges the elements of `nums` about the given `pivot` so that 
  *  `nums[..i) < pivot`, `nums[i..k) == pivot` and `nums[k..] > pivot` 
  *  for some indices `i,k`. */
  static void partition3Way(int[] nums, int pivot) {
    int i = 0;
    int j = nums.length;
    int k = nums.length;
    
    /* Loop Inv: `nums[..i) < pivot`, `nums[j...k) == pivot`, `nums[k...] > pivot` */
    while (i < j) {
      if (nums[i] < pivot) {
        i++; // expand the < region
      } else if (nums[i] == pivot) {
        swap(nums, i, j - 1); // swap nums[i] into the = region
        j--; // expand the = region
      } else { // nums[i] > pivot
        swap(nums, i, j - 1); // swap nums[i] to the front of the = region
        swap(nums, j - 1, k - 1); // swap nums[i] to front of the > region
        j--; // expand the = region
        k--; // expand the > region
      }
    }
  }
  // SHOW: END 1
}

Exercise 3: Mountain Detection - Time Permitting

We say that an array of ints is a mountain if its entries (weakly) increase to the array's maximum value and then (weakly) decrease after this. More concretely, an array int[] nums is a mountain if there is some index j with 0 <= j < nums.length for which nums[..j] is a non-decreasing sequence and nums[j..] is a non-increasing sequence. For example,

meets these criteria when j = 3. However,

is not a mountain because it has two "peaks"; its entries increase, then decrease, then increase again. We'll develop a method isMountain() that determines whether a given int[] array is a mountain.

(a)

In addition to a loop index variable i, what other variables will you need to keep track of our progress as we traverse the array? (Hint: Our solution uses one additional boolean variable).

We will define a boolean variable called goingDown to indicate if we have started descending the mountain.

(b)

Draw "Pre", "Post", and "Inv" array diagrams to visualize the behavior of your loop. Include two "Post" diagrams to account for two possible return conditions: reaching the end of the array and certifying that it is a mountain, versus detecting that the array is not a mountain and returning early.

Pre:

nums:

nums.length

Post:

true return

nums:

nums.length

Post:

false return

nums:

nums.length

Inv:

nums:

nums.length

(c)

Using the "Pre" diagram, how should we initialize the loop variables? Briefly explain why your initialization makes the loop invariant true at the start of the loop.

We will initialize i = 1 and goingDown = false. When we do this, the invariant diagram implies that the non-increasing section is empty. This means that the indexing variable i will be immediately after the non-decreasing section. By initializing i = 1, we are consistent with the precondition diagram, where the first element is in the non-decreasing section. We can verify this since the precondition guarantees us at least an array of length 1, and a 1-element array is trivially non-decreasing.

(d)

What should be our loop guard? When we exit from the loop, what will our return value be?

We consider the true case, as the false case returns early when identifying an inconsistency in the mountain. To make the invariant look like the true postcondition diagram, we have i = nums.length. Thus, we want to keep on iterating until i = nums.length, meaning the loop should run while i < nums.length (or i != nums.length). After we exit from the loop, we have verified that the array is mountainous, and we can return true. If the array were not mountainous, somewhere through the iteration, the false postcondition would have been satisfied, and the loop would have returned early.

(e)

Complete the definition of the isMountain() method. Document your loop invariant (using range notation) in a multi-line comment above the loop declaration.

package cs2110;

public class IsMountain {
  // SHOW: SECTION 1
  /** Returns whether the entries of `nums` form a *mountain*, meaning there 
   *  is some index `j` such that `nums[..j]` is non-decreasing and 
   *  `nums[j..]` is non-increasing. Requires that `nums.length > 0`. */
  static boolean isMountain(int[] nums) { 
    int i = 1;
    boolean goingDown = false;
    /* Loop Inv: `nums[0..i)` is mountainous, consisting of a non-decreasing 
     * section, potentially followed by a non-increasing section iff 
     * `goingDown == true`. */
    while (i < nums.length) {
      if (goingDown && nums[i] > nums[i - 1]) {
        return false;
      } else if (nums[i] < nums[i - 1]) {
        goingDown = true;
      }
      i++;
    }
    return true;
  }
  // SHOW: END 1
}

At the end of each iteration, we increment i by 1. We are making progress towards nums.length in each iteration. To analyze how the loop maintains the invariant, we analyze four cases:

Case 1: goingDown = false && nums[i] >= nums[i-1]

Since we are ascending the mountain and the current element is at least the previous, nums[i] can be included as part of the non-decreasing section. No extra work is needed besides incrementing i.

Case 2: goingDown = false && nums[i] < nums[i-1]

At this point, we have reached the peak of the (potentially) mountainous array. We were going up but found an element that was less than the previous. This element must be part of the non-increasing section, which must be empty if goingDown = false. To rectify this, we set goingDown = true, which should make logical sense, since we are now descending the mountain.

Case 3: goingDown = true && nums[i] <= nums[i-1]

Much like case 1, this is consistent with the ongoing direction, i.e., continuing to go down the mountain. No extra work is needed besides incrementing i.

Case 4: goingDown = true && nums[i] > nums[i-1]

At this point, we have already hit the peak and are expecting all subsequent elements to be part of the non-increasing section. This violates the mountain property since the array is now going back uphill, so we can return false.