Discussion 3: Loop Invariants

Solutions

Download Solution Code download
Exercise 1: Warmup
Suppose that we have a double[] array of sensor measurements. We expect all of the readings 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. 
1
2

/** Reassigns all negative entries of the `readings` array to 0. */
static void cleanData(double[] readings) { ... }
1
2

/** Reassigns all negative entries of the `readings` array to 0. */
static void cleanData(double[] readings) { ... }
(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. Let’s suppose that we want to carry out the cleaning from right to left.

How should we initialize i?

We should initialize i to the rightmost index in the array i = readings.length - 1.

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 as soon as i advances past the leftmost index in the array, or when i < 0. Negating this, we should guard our loop on the condition i >= 0.
(b)
Finish filling in the following array diagrams for the loop in cleanData().



(c)

Use your answers from parts (a) and (b) to write the definition of the cleanData() method.

Add a comment above the loop documenting the loop invariant. Then, fill in the loop body.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

/** Reassigns all negative entries of the `readings` array to 0. */
static void cleanData(double[] readings) { 
  int i = readings.length - 1;
  while (i >= 0) {
    if (readings[i] < 0) {
      readings[i] = 0;
    }
    i--;
  }
}

 1
 2
 3
 4
 5
 6
 7
 8
 9
10

/** Reassigns all negative entries of the `readings` array to 0. */
static void cleanData(double[] readings) { 
  int i = readings.length - 1;
  while (i >= 0) {
    if (readings[i] < 0) {
      readings[i] = 0;
    }
    i--;
  }
}
Exercise 2: Mountain Detection
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 i with 0 <= i < nums.length for which nums[..i] is a non-decreasing sequence and nums[i..] is a non-increasing sequence. For example,
meets these criteria when i = 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. 
1
2
3
4
5
6

/**
 * Returns whether the entries of `nums` form a *mountain*, meaning there 
 * is some index `i` such that `nums[..i]` is non-decreasing and 
 * `nums[i..]` is non-increasing. Requires that `nums.length > 0`.
 */
static boolean isMountain(int[] nums) { ... }
1
2
3
4
5
6

/**
 * Returns whether the entries of `nums` form a *mountain*, meaning there 
 * is some index `i` such that `nums[..i]` is non-decreasing and 
 * `nums[i..]` is non-increasing. Requires that `nums.length > 0`.
 */
static boolean isMountain(int[] nums) { ... }
(a)

In addition to a loop index variable j, 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 are ascending or 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.





(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 j = 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 j will be immediately after the non-decreasing section. By initializing j = 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 j = nums.length. Thus, we want to keep on iterating until j = nums.length, meaning the loop should run while j < nums.length (or j != 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)

Use your answers from parts (c) and (d) to set up your loop in the isMountain() method. Add a comment above the loop documenting the loop invariant. Then, fill in the loop body.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22

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

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22

/**
 * Returns whether the entries of `nums` form a *mountain*, meaning there is some index `i` such
 * that `nums[..i]` is non-decreasing and `nums[i..]` is non-increasing. Requires that
 * `nums.length > 0`.
*/
static boolean isMountain(int[] nums) { 
  int j = 1;
  boolean goingDown = false;
  /*
   * Loop invariant: `nums[0..j)` is mountainous, consisting of a non-decreasing section and potentially
   * followed by a non-increasing section iff `goingDown == true`. `nums[j..)` is unknown.
   */
  while (j < nums.length) {
    if (goingDown && nums[j] > nums[j-1]) {
      return false;
    } else if (nums[j] < nums[j-1]) {
      goingDown = true;
    }
    j++;
  }
  return true;
}
At the end of each iteration, we increment j 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[j] >= nums[j-1]

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

Case 2: goingDown = false && nums[j] < nums[j-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[j] <= nums[j-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 j.

Case 4: goingDown = true && nums[j] > nums[j-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.

Exercise 3: Pivot Partitioning
When we partition an array, we split its entries into disjoint pieces according to some property. In this case, we'll partition an array of ints into three segments by comparing them 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 sorting algorithm.
1
2
3
4
5
6

/**
 * Rearranges the elements of `nums` about the given `pivot` so that 
 * `nums[..i) < pivot`, `nums[i..j) == pivot` and `nums[j..] > pivot` 
 * for some indices `i,j`. Requires that `nums.length > 0`.
 */
static void partition3Way(int[] nums, int pivot) { ... }

1
2
3
4
5
6

/**
 * Rearranges the elements of `nums` about the given `pivot` so that 
 * `nums[..i) < pivot`, `nums[i..j) == pivot` and `nums[j..] > pivot` 
 * for some indices `i,j`. Requires that `nums.length > 0`.
 */
static void partition3Way(int[] nums, int pivot) { ... }
You'll develop a method that uses three int loop variables (i, j, and k) and the following loop invariant:
(a)

Adjust the “Inv” array diagram back in time to draw the “Pre” array diagram. Use this to determine the correct initializations of the loop variables i, j, and k.

We should initialize i = 0, j = nums.length, and k = nums.length.

(b)

Adjust the “Inv” array diagram forward in time to draw the “Post” array diagram. Use this to determine the condition we should use to guard our loop.

We should guard the loop on the condition i < k.

(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[k-1] and then decrement k.

nums[i] > pivot:

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

(d)

Use your answers from parts (a), (b), and (c) to write the definition of the partition3Way() method. Be sure to document your loop invariant (using proper range notation) in a multi-line comment above the loop declaration.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

/**
 * Rearranges the elements of `nums` about the given `pivot` so that `nums[..i) < pivot`,
 * `nums[i..j) == pivot` and `nums[j..] > pivot` for some indices `i,j`. Requires that
 * `nums.length > 0`.
 */
static void partition3Way(int[] nums, int pivot) { 
  int i = 0;
  int k = nums.length;
  int j = nums.length;

  /*
   * Loop invariant: nums[..i) < pivot, nums[k..j) == pivot, nums[j..] > pivot
   */
  while (i < k) {
    if (nums[i] < pivot) {
      i++; // expand the less than region
    } else if (nums[i] == pivot) {
      swap(nums, i, k - 1); // swap nums[i] into the equals region
      k--; // expand the equals region
    } else { // nums[i] > pivot
      swap(nums, i, k - 1); // swap nums[i] to the front of the equals region
      swap(nums, k - 1, j - 1); // swap front of equals region to front of < region

      k--; // expand the equals region
      j--; // expand the > region
    }
  }
}

/**
 * Swaps the entries `a[x]` and `a[y]`. Requires that `0 <= x < a.length` and `0 <= y <
 * a.length`.
 */
static void swap(int[] a, int x, int y) {
  int temp = a[x];
  a[x] = a[y];
  a[y] = temp;
}

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38

/**
 * Rearranges the elements of `nums` about the given `pivot` so that `nums[..i) < pivot`,
 * `nums[i..j) == pivot` and `nums[j..] > pivot` for some indices `i,j`. Requires that
 * `nums.length > 0`.
 */
static void partition3Way(int[] nums, int pivot) { 
  int i = 0;
  int k = nums.length;
  int j = nums.length;

  /*
   * Loop invariant: nums[..i) < pivot, nums[k..j) == pivot, nums[j..] > pivot
   */
  while (i < k) {
    if (nums[i] < pivot) {
      i++; // expand the less than region
    } else if (nums[i] == pivot) {
      swap(nums, i, k - 1); // swap nums[i] into the equals region
      k--; // expand the equals region
    } else { // nums[i] > pivot
      swap(nums, i, k - 1); // swap nums[i] to the front of the equals region
      swap(nums, k - 1, j - 1); // swap front of equals region to front of < region

      k--; // expand the equals region
      j--; // expand the > region
    }
  }
}

/**
 * Swaps the entries `a[x]` and `a[y]`. Requires that `0 <= x < a.length` and `0 <= y <
 * a.length`.
 */
static void swap(int[] a, int x, int y) {
  int temp = a[x];
  a[x] = a[y];
  a[y] = temp;
}