For each public method of each class we have provided pre- and post-conditions associated with the method. In short, the precondition suggests what must be true before the method is to be called, and the postcondition indicates what will happen if the precondition is met and the method is called. These comments are part of every method of every class, appear in the source files, and are part of the text.
In addition, we have added a separate set of javadoc comments for each method of every class. These comments describe every parameter, and the return values, if applicable. We also include the pre- and postconditions. These comments are elided from the distributed source code because they are so bulky they make it difficult for students to read the code, and they do not appear within the text.