Discussion 3: Loop Invariants

The goal of today’s discussion is to practice writing “loopy” code using the tools from last Thursday’s lecture: array diagrams and loop invariants. Becoming more comfortable with these tools will help you design loops in a more principled way that lets you get the code right on the first try, saving debugging time. In addition, we’ll continue to use the language of loop invariants throughout the course as we discuss more complicated methods. During this discussion, you’ll develop three different “loopy” methods from their specifications.

Learning Outcomes

  1. Identify the loop invariant of an iterative method involving an array and visualize it using an array diagram.
  2. Use an array diagram to develop an iterative method that maintains the visualized invariant.
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:
0
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:
0
data.length
Based on your "Pre" and "Inv" diagrams, how should we initialize i?
(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:
0
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?
(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.
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:
0
nums.length
(a)
Adjust the "Inv" array diagram back in time to draw the "Pre" array diagram.
Pre:
nums:
0
nums.length
Based on your "Pre" and "Inv" diagrams, how must we initialize i, j, and k?

i =

j =

k =

(b)
Adjust the "Inv" array diagram forward in time to draw the "Post" array diagram.
Post:
nums:
0
nums.length
Based on your "Post" and "Inv" diagrams, what condition should we use to guard our loop?

(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:

nums[i] == pivot:

nums[i] > pivot:

(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.
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).
(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:
0
nums.length
Post:
true return
nums:
0
nums.length
Post:
false return
nums:
0
nums.length
Inv:
nums:
0
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.
(d)
What should be our loop guard? When we exit from the loop, what will our return value be?
(e)
Complete the definition of the isMountain() method. Document your loop invariant (using range notation) in a multi-line comment above the loop declaration.