Code Contracts Using Documentation Comments

Here is the IndexedList documented using Java Documentation Comments (or simply Javadoc):

/**
 * IndexedList ADT.
 */
public interface IndexedList {

  /**
   * Change the value at the given index.
   *
   * @param index representing a position in this list.
   *              Pre: 0 <= index < length
   * @param value to be written at the given index.
   *              Post: this.get(index) == value
   */
  void put(int index, int value);

  /**
   * Retrieve the value stored at the given index.
   *
   * @param index representing a position in this list.
   *              Pre: 0 <= index < length
   * @return value at the given index.
   */
  int get(int index);

  /**
   * Get the declared capacity of this list.
   *
   * @return the length
   *         Inv: length() >= 0
   */
  int length();
}

Documentation comments are considered part of the specification of an ADT, as well as a general good programming practice.You are expected to follow this practice in this course.

• Preconditions are requirements that must be met when entering a method. For example, the get method specifies Pre: 0 <= index < length() which means the value for index parameter must be non-negative and smaller than the length of the list. If a client violates this condition, they cannot expect the get method to behave as it is specified.

• Postconditions describe expectations at the time the method exits. For example, the put method specifies Post: this.get(index) == value which means once the method is successfully executed, you can call get(index) and expect it to return the value.

• Invariants describe the expected state for all objects of a class. For example, the length method specifies Inv: length() >= 0 which means the length is always a non-negative value.