Discussion 3: Loop Invariants

Solutions

Download Solution Code download
Exercise 1: Second Largest Element
Given an int[] array, we'd like to determine its second-largest element. To avoid having to worry about various edge cases or ambiguities, we'll assume that the array contains at least two elements and that all of its elements are distinct. Therefore, a second-largest element must exist. 
1
2
3
4
5

/** 
 * Returns the second-largest element of the given `nums` array.
 * Requires that `nums.length >= 2` and `nums` contains distinct elements.
 */
static int secondLargest(int[] nums) { ... }
1
2
3
4
5

/** 
 * Returns the second-largest element of the given `nums` array.
 * Requires that `nums.length >= 2` and `nums` contains distinct elements.
 */
static int secondLargest(int[] nums) { ... }
We'd like our definition of secondLargest() to use only a single pass over the nums array; we can accomplish this by designing a loop invariant that keeps track of the relevant state as we traverse the array.
(a)

Let’s start by considering what variables we will need to keep track of our progress as we traverse over the array. As usual, we’ll use a variable i to keep track of our position in the array. What other local variables should we introduce?

We should introduce local variables largest and secondLargest that keep track of the largest and second-largest (respectively) array entries that we have seen so far.
(b)
Finish filling in the following array diagrams, incorporating your local variables from part (a).
(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 should initialize i = 2;, largest = Math.max(a[0],a[1]);, and secondLargest = Math.min(a[0],a[1]);. When we do this, the "left" range in our "Inv" diagram is a[0..2), which consists of only a[0] and a[1]. Both a[0] and a[1] will be at most largest, and the smaller of the two entries will be the only one that is at most secondLargest.
(d)

Using the “Post” diagram, what should be our loop guard? When we exit from the loop, what will our return value be?

If we advance the middle boundary of the "Inv" diagram all the way to the right, we obtain the "Post" diagram where i overlaps with a.length. Before this, i will always be less than a.length so we can guard the loop on the condition i < a.length. When we exit from the loop, secondLargest will hold the second largest value in the array, so we should return secondLargest;.
(e)

Open up the starter code and set up your loop in the secondLargest() method using your answers to parts (c) and (d). 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
23
24

/** 
 * Returns the second-largest element of the given `nums` array.
 * Requires that `nums.length >= 2` and `nums` contains distinct elements.
 */
 static int secondLargest(int[] nums) {
  int largest = Math.max(nums[0], nums[1]);
  int secondLargest = Math.min(nums[0], nums[1]);
  int i = 2;

  /*
   * Loop invariant: `largest` is the largest value among `nums[..i)`
   *                 `secondLargest` is the second-largest value among `nums[..i)`
   */
  while (i < nums.length) {
    if (nums[i] > largest) {
      secondLargest = largest;
      largest = nums[i];
    } else if (nums[i] > secondLargest) {
      secondLargest = nums[i];
    }
    i++;
  }
  return secondLargest;
}
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

/** 
 * Returns the second-largest element of the given `nums` array.
 * Requires that `nums.length >= 2` and `nums` contains distinct elements.
 */
 static int secondLargest(int[] nums) {
  int largest = Math.max(nums[0], nums[1]);
  int secondLargest = Math.min(nums[0], nums[1]);
  int i = 2;

  /*
   * Loop invariant: `largest` is the largest value among `nums[..i)`
   *                 `secondLargest` is the second-largest value among `nums[..i)`
   */
  while (i < nums.length) {
    if (nums[i] > largest) {
      secondLargest = largest;
      largest = nums[i];
    } else if (nums[i] > secondLargest) {
      secondLargest = nums[i];
    }
    i++;
  }
  return secondLargest;
}
(f)

Describe how the loop body maintains the loop invariant and makes progress in each iteration.

At the end of each loop iteration, we increment i, bringing it one step closer to a.length. To preserve the loop invariant, we must update largest and secondLargest to account for this slightly enlarged array range. If the newly-considered element a[i] is larger than largest, it becomes the largest element we've seen so far (and the old largest becomes the second-largest element we've seen so far). Otherwise, if a[i] is larger than secondLargest but not largest, then it becomes the new second-largest element and the largest element is unchanged. Finally, if a[i] is smaller than secondLargest, then adding it to the array range does not affect the largest or second-largest element.
Exercise 2: Mountain Detection
We say that an array of ints is a mountain if its entries (weakly) increase to the arrays 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 over 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. You may wish to draw two “Post” diagrams for different possible conditions: reaching the end of the array and certifying that it is a mountain vs. detecting that the array is not a mountain and returning early.
Note that this invariant differs slightly than the description of a mountain given by the problem. This particular invariant chooses to include the element at index i as part of the non-decreasing section. This choice gives rise to the possibility for the non-increasing section to be empty in the true postcondition and invariant if and only if goingDown = false.
(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)

Open up the starter code and set up your loop in the isMountain() method using your answers to parts (c) and (d). 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;
}
(f)

Describe how the loop body maintains the loop invariant and makes progress in each iteration.

At the end of each iteration, we increment j by 1. We are making progress towards nums.length 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 write the initialization of the loop variables i, j, and k. 
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

/**
 * 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: ...
   */
  while ( ) {
    ...
  }
}

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

/**
 * 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: ...
   */
  while ( ) {
    ...
  }
}
(b)
Adjust the “Inv” array diagram forward in time to draw the “Post” array diagram. Use this to set up a while-loop with the correct loop guard. 
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

/**
 * 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: ...
   */
  while (i < k) {
    ...
  }
}

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

/**
 * 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: ...
   */
  while (i < k) {
    ...
  }
}
(c)
Add a multi-line comment documenting the loop invariant above your loop. Use array notation in your documentation. 
 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

/**
 * 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) {
    ...
  }
}

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17

/**
 * 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) {
    ...
  }
}
(d)
Complete the body of your while-loop which should read the value of nums[i] and take different actions whether it is less than, equal to, or greater than the pivot to make progress and restore the loop invariant. 
 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;
}