Part 1: Verifying Correctness of getDigits

Complete the code reasoning problem given in this worksheet.

Feel free to print out the worksheet or rewrite the problems on a separate sheet. You may submit a scanned copy of any hand-written document with the problems and your solutions as long as it is legible.

Submit your solution as a PDF in Gradescope. Be sure to indicate in Gradescope which pages of your PDF solve each problem.

Part 2: Implementing a Static Method - leadingDigit

When we release each homework assignment, we push the new starter files to your repository in GitLab, so you should obtain these new files by pulling from git.

The rest of this assignment is going to involve working in Natural.java, which is in the directory hw-base/src. Read the specification in Natural.java, make sure you understand both the overview of Natural and what each method accomplishes. Note that the first method is getDigits. This is the same method you code reviewed in Part 1, so you should already understand how it works and why it is correct.

Implement the leadingDigit method using a single loop. In addition to writing the code you must also include (at least) the following comments:

• A comment above the loop describing the loop invariant.

• A comment above each return statement explaining why the postcondition must hold.

  A template comment has been provided before the return statement. Either fill in the blanks in this comment or write your own comment providing the same information. If you add any additional return statements, those will also need explanatory comments above them.

First, use reasoning to check your code is correct.

After you have reasoned that your code is correct, run the unit tests for leadingDigits to gain additional confidence in your solution.

Your code must be correct with the invariant you described. As we discussed in HW2, passing the tests does not guarantee that this is the case, only your reasoning can be used to check this. (You are free to include asserts in the loop to double check parts of the invariant; however, any checks you include in your submission must not increase the asymptotic running time of the method.)

The unit test called testConstruction should also now be passing at this point. (The constuctor calls leadingDigit, which is why it did not pass before.)

Part 3: Implementing an Instance Method - toString

Repeat the same approach as in Part 2 to implement the toString method: fill in the method body with a single loop, document its loop invariant, and explain in the comments why the postcondition must hold. Your code must be correct with the invariant you describe which you can check using reasoning. After you have done so run the unit test for toString to double check your work.

Unlike leadingDigit, which is a static method, toString is an instance method, meaning that it has access to the fields of the class. You will need to use those in your code. You will also need to use the representation invariant as an additional part of the precondition in your reasoning. (Like the precondition, the representation invariant should be true at the top of the method body.)

Part 4: Implementing a Complex Instance Method - plus

In the previous two parts, we asked you to come up with a loop invariant and then implement the method with that invariant. In the next two parts, the invariants will be provided, and your job will only be to implement the method with that invariant. However, these two methods are more complex than those above; plus, is complex enough that we will split the work into two parts.

Working with Loops and Loop Invariants

The plus method body contains three loops. In this part, we will implement the first two. The purpose of these loops is to fill in newDigits with the element-wise sum of this.digits and other.digits. This is similar to the zipSum example from lecture except that we do not require the two arrays to have the same length. The purpose of the second loop is to handle the case where other.digits is shorter than this.digits.

Follow these steps to implement the first two loops:

1. Read through the loop invariant of the first loop. Once you understand it, write a comment above the loop explaining, in English, what it does. (This will make it easier to read, in addition to confirming for yourself that you understand the invariant.)

2. Change the initialization on i so that the first loop invariant holds initially.

3. Fill in the body of the first loop so that it makes progress toward exiting (with the loop condition already provided) and restores the loop invariant.

4. Write a comment after the first loop explaining why we know that every element of newDigits is now between 0 and 2 * this.base - 1.

5. Read through the loop invariant of the second loop. Once you understand it write a comment above the loop explaining, in English, what it does.

6. Write a comment before the second loop explaining why we know that the invariant of the second loop already holds. (I.e., we don't need any initialization code to make it true initially.)

7. Fill in the body of the second loop so that it makes progress toward exiting (with the loop condition already provided) and restores the loop invariant.

Once you have completed the parts above, you can run the unit test called testPlusTopTwoLoops to double check that your top two loops are correct. This will ensure that the top two loops put newDigits into a state where it is the element-wise sum of the this.digits and other.digits.

Finishing the Implementation

In this part, we will implement third loop in plus. A correct solution to this part can be quite short. However, the lines of a short solution are tricky enough that we will need to reason carefully to get them right.

In essence, the goal of the third loop is simply to restore the invariant that each element of newDigits is between 0 and this.base - 1 (so far, we only know that the digits are no larger than 2 * this.base - 1). However, we must do that while also not changing the number that newDigits represent. The invariant of the third loop formalizes that last condition (that it represents the same value), while also describing partial progress toward satisfying the condition that each element of newDigits is at most this.base - 1.

Follow these steps to implement the third loop:

1. Remove the two lines after the call to checkZipSum, which cause the method to always return null, as well as the comments above those lines. Now that we are ready to implement the third loop, we no longer need those lines.

2. Write a comment before the initialization of the third loop explaining why, after the first two loops, we know that newDigits represents the same number as this.getValue() + other.getValue(). (It may help to look at the postcondition of getValue to refresh your memory of what that method returns.)

3. Change the initialization of i so that the loop invariant holds initially.

4. Change the loop condition so that the postcondition holds when the loop exits.

5. Write a comment after the loop explaining why the postcondition must hold with the loop condition you wrote above.

6. Write another comment after the loop explaining why the precondition of the Natural constructor must hold. (If it does not, that line would throw an exception!)

7. Fill in the body of the loop so that the invariant is restored at the bottom of the loop body. The progress step (i = i + 1) is already provided, and you should not change it. You should not need anything beyond simple arithmetic in your code. In particular, you should not use division or mod. When completed, the body of the loop should be fairly short.

As noted above, getting the body of the third loop right requires care. Here are some additional suggestions on how to complete it:

• As we saw in lecture, you can use forward and backward reasoning to fill in the assertions just before and just after your code executes and then compare them to determine what extra conditions need to be true after your code that may not be true beforehand. Your code only needs to do whatever work is required to make those extra conditions hold, which may not be very much.

• You may want to do the work described above on paper. Whether you do it on paper or in the IDE, take this opportunity to figure out the code by reasoning. Do not resort to solving it by trial & error using the provided tests. (Soon, you will be asked to solve problems where no tests are provided for you.)

• There are some additional hints in the comments of the loop body that may be helpful if you get stuck. They will probably not make sense until you have thought about the problem on your own.

Once you have completed the parts above, you can run the unit test called testPlus to double check that your third loop is correct. The unit test called testTimes should also now be passing at this point. (The times method calls plus, which is why it did not pass before.) Note, however, that these tests do not ensure that the loop invariant holds, so they are not a perfect check of correctness. You will need to rely on reasoning to be certain that the code is right.

Part 5: Implementing a Method That Calls Other Methods

Complete the implementation of toBase so that it is correct with the invariant provided. In particular, you should:

1. Change the the initialization of i and j so that the invariant holds initially.

2. Change the loop condition so that the postcondition holds when the loop exits.

3. Fill in the body of the loop so that it makes progress toward exiting and also restores the loop invariant.

Be sure to include a comment before the return statement explaining why we know that the postcondition holds when we exit the loop.

Unlike the previous methods, which were each self-contained, your implementation of toBase is free to call other methods of the class. When reasoning through a method call, note that you must also check that the preconditions of those methods always hold.

As in Part 4, you should complete the body of the loop using reasoning. Do not resort to trial & error, relying on the tests provided. As above, it maybe useful to work this out on paper as it is purely a mental exercise.

After you have checked the correctness of your implementation using reasoning, run the unit test for toBase to double check your work.