Contents:
In this assignment, you will practice writing code that satisfies a
specification and using reasoning to confirm that your code is correct.
Specifically, you will complete the implementation of
Natural, a class that represents non-negative integers as
a list of digits in a chosen base. Upon completion, the class will
contain methods to find the digits that represent the number in the
chosen base, to perform some simple arithmetic on numbers in the same
base, and to convert numbers between different bases.
This assignment has fewer parts than the previous homework, but each part is more complicated, and we will ask you to provide more explanations. Therefore, we recommend you to start early, and have plenty of time to ask questions to the staff.
We start the assignment with the code reasoning problem given in this worksheet. Unlike HW2, we recommend working on this part before starting the rest of the homework.
(Note: you should assume that digits is long enough that
there will never be an ArrayIndexOutOfBoundsException. The
code before the part shown in the worksheet ensures that this always is
the case.)
Feel free to rewrite the problems on a separate sheet. You do not have to turn in these exact pages with the blanks filled in (though you can do that as well). It is okay to submit a scanned copy of a hand-written document as long as it is legible, so you can also print the worksheet, write your answers on that, and scan it when done.
After finishing, submit your solution as a PDF in Gradescope. Be sure to indicate in Gradescope which pages of your PDF solved which parts of the worksheet problem. The rest of the homework will have a different submission method (as described in HW2); your PDF solution to part 1 should be the only file you submit in Gradescope.
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:
Errata: You should assume that digits.length > 0.
(The postcondition, as written, does not make sense otherwise.)
Hint: the postcondition for the method has been provided. As we discussed in class, you can often get a good loop invariant by weakening the postcondition (i.e., generalizing it so that it allows partially complete states as well as the fully complete postcondition).
Use reasoning to check that your code is correct. After you have
checked it with reasoning, run the unit tests for
leadingDigits to gain some 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. You will need to rely on your reasoning 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 whyit did not pass before.)
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. Use reasoning to check that it is correct. 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.)
Errata: The postcondition mentions "D", "n", and "ch". These are
shorthand for this.digits, this.digits.length,
and the static method Base.digitToChar, respectively.
Note that you will need to call BaseDigits.digitToChar in
your code in order to produce a state satisfying the postcondition.
In the previous two parts, we asked you to come up with a loop
invariant and then to 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. These two methods are
more complex, however, than those above. Indeed, the first of these two
methods, plus, is complex enough that we will split the work
into two parts.
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:
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.)
Change the initialization on i so that the first loop
invariant holds initially.
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.
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.
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.
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.)
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.
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:
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.
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.)
Change the initialization of i so that the loop
invariant holds initially.
Change the loop condition so that the postcondition holds when the loop exits.
Write a comment after the loop explaining why the postcondition must hold with the loop condition you wrote above.
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!)
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, though, 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.
Errata: The last condition of the invariant, which says that D[i], ..., D[n-1] are all less than 2b, while true, is too weak. In fact, we know from the first loop that D[0], ..., D[n-1] are all less than 2b-1 when the loop begins. For our reasoning to work on the last loop, we need to incorporate this information. Specifically, the loop invariant needs to be strengthened to say that D[i] < 2b and D[i+1], ..., D[n-1] are all less than 2b-1.
(Although you are free to ignore this, there are some other minor errors in the invariant provided in the code. Most notably, the last term in the sum should be D[n] bn rather than D[n-1] bn-1. Initially, D[n] = 0, so this extra term doesn't change anything. However, on the very last iteration, it is possible that D[n] will be changed to something between 1 and b-1, so we would need to include that possibility for the loop invariant to hold after the last iteration.)
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.
Complete the implementation of toBase so that it is correct
with the invariant provided. In particular, you should:
i and j
so that the invariant holds initially.
Hint: To understand the meaning of the provided invariant,
compare it to the invariant of getValue, which returns the
value of the Natural as an int. You will see
that the two invariants are extremely similar, with the main difference
being that, while getValue builds up the return value using
the variable val, which is an int,
toBase builds up its return value in a variable
r, which is a Natural. Since these two methods
have such similar loop invariants, we should expect them to have very
similar code, so you can look at the body of getValue for
hints on how to implement toBase.
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.
Your answers in Part 1 should be submitted in Gradescope, as a PDF file. This should be the only part you are submitting in Gradescope.
At the end of each assignment, you must refer to the Assignment Submission Handout and closely follow the steps listed to submit the rest of your assignment. Do not forget to double check your submission as described in that handout - you are responsible for any issues if your code does not run when we try to grade it.
Use the tag name hw3-final for this assignment. To
verify your assignment on attu, you can use the gradle task
hw-base:runNatural.
We should be able to find the file Natural.java in the hw-base/src
directory of your repository. This file should pass all the tests written in NaturalTest.java
found in the hw-base/test directory.