Discussion 7 handout

Group members (names & NetIDs)

Objectives

• Communicate clearly about invariants applying to regions of arrays
• Develop code from loop invariants

For this exercise, please only use while-loops (not for-loops).

Task 1: Code from loopy questions

One way to use loop invariants is to prove the correctness of some code. But they can also guide the development of that code in the first place. This is a powerful study technique, since the invariants of key algorithms are easier to memorize and more generalizable than raw code.

For the following questions, assume that c is an integer array (int[]) and that k is an integer variable. We are allowing single-letter variable names here to make the diagrams and mathematical relations less cluttered.

Establishment (Does it start right?)

To show “establishment,” you need to prove that, assuming the precondition is true, executing the initialization code will result in the loop invariant being true. Viewed in reverse, this tells us what the initialization code must do.

Assume you are developing a loop whose invariant is c[0..k) == 0 (that is, the first k elements of array c are zero). There are no non-trivial preconditions (basically, the elements of c could initially have any values). What initialization code will establish this invariant? (Your response should not modify any of the elements of c. Note that initialization code typically has O(1) complexity; otherwise it would need a loop of its own.)

Postcondition (Does it end right?)

When analyzing loop code, you need to prove that, when the loop guard is false, the loop invariant implies the postcondition (thus accomplishing the task it was written to perform). So when developing loop code, comparing the invariant with the postcondition will suggest what the loop guard must be.

Assume again that you are developing a loop whose invariant is c[0..k) == 0 and that the postcondition the loop is trying to achieve is c[0..c.length) == 0 (that is, all elments of c are 0). What should the loop guard be?

Hint: what value of k will make the invariant diagram look like the postcondition diagram?

Preservation & termination (Does the repetend keep the invariant true while making progress towards termination?)

To show preservation, you would need to prove that, assuming both the loop guard and the loop invariant are true, executing the code in the loop body (aka “repetend”) will result in the invariant still being true. And to show termination, you would need to prove that execution of the repetend means that loop guard is “closer to” becoming false. In reverse, this gives us a strategy for implementing the repetend: first, find a way to make the program state look incrementally more like the postcondition (or for the loop guard to get closer to becoming false); second, find a way to compensate for these changes in order to keep the loop invariant true.

Assume the invariant, postcondition, and loop guard from above; write a loop body that makes progress while preserving the invariant.

Task 2: Dutch national flag algorithm

Let f be an array of strings (String[]). As a precondition, we guarantee that every value is either "Red", "White", or "Blue", but we don’t know how many of each color there are or how they are arranged. Our goal is to swap elements in the array until all of the reds are at the start of the array, all of the blues are at the end of the array, and all of the whites are in the middle.

Invariant

Generalize the postcondition to come up with a loop invariant, and draw an array diagram depicting your chosen invariant. Your invariant should divide the array into four regions: reds, whites, blues, and unknowns (not necessarily in that order). You will need to introduce some index variables (e.g. i, j, k) to identify where regions start and/or end (be very clear about which side of a region boundary the index is on).

Note: there is more than one right answer; in fact, there are four possibilities for where to put the “unknown” region, and many choices for labeling region boundaries with indices. But your subsequent code will depend on these choices; code from groups who chose a different invariant will not work for you!

Initialization

Your invariant introduced some new program state in the form of some index variables. Write initialization code to assign values to these variables such that the invariant is equivalent to the precondition (all elements unknown).

Loop guard

Compare your invariant diagram to the postcondition above. Write a while-loop with a loop guard that would come after your initialization code so that, when the guard is false, your invariant is equivalent to the postcondition (no elements unknown).

Loop body

To make progress towards termination, each iteration of your loop should investigate one value from the unknown region of the array, then place it next to other elements with the same color. This should be done by swapping elements (so no strings are created or destroyed); between 0 and 2 swaps may be needed. Once the color regions have been reestablished, the index variables denoting their boundaries will need to be updated to restore the truthfullness of the invariant. Write a loop body to perform these tasks.

Complexity

What is the largest number of swaps your loop body performs during a single iteration?

What is the asymptotic complexity for how the work done by this algorithm scales with f.length?

Testing

Download DutchFlag.java and assemble the parts of your loop in the empty dutchFlag() method. Run the main method to see whether your reordering was successful.

Submission

1. Open the assignment page for “Discussion activity 7” in CMSX
2. [Recorder] Find the “Group Management” section and invite each group member
3. [Others] Refresh the page and accept your invitation
4. [Recorder] Take a picture of your work and save as either a JPEG or a PDF file named “discussion_responses”. After all invitations have been accepted, upload your picture along with your code as your group’s submission.
   • Recommended scanning apps: Microsoft Office Lens, Adobe Scan, Genius Scan, Evernote Scannable

Ensure that your group is formed and your work submitted before the Friday evening deadline.

Tips and reminders

• Discussion is not a race. Focus on the current activity being facilitated by your TA and engage your whole group to propose and explain ideas.
• Elect a recorder to maintain the “master” copy of your work (others are still encouraged to jot down ideas on scratch paper). Rotate this position each week.
• It is a violation of academic integrity to credit someone for work if they were not present when the work was done, and the whole group is accountable. Your CMS group must only include classmates who attended section with you on that day. Remember that our participation policies accommodate occasional absences without penalty.
• It is your individual responsibility to ensure that you are grouped on CMS and that your group’s work is submitted before the deadline. Log into CMS the day after section to ensure that everything is in order, and contact your groupmates if not. It would be prudent for multiple members to photograph the group’s work.
• Only one group member (typically the recorder) needs to upload a submission. But their submission must not be uploaded until after all group members have confirmed their membership in CMS (contact your TA if you have trouble grouping in CMS).