Preconditions and Postconditions

Programmers spends significant portions of their time on code maintenance and debugging. To facilitate these tasks and to improve the overall design, programmers generally specify the expected states before and after a method's execution. These states are called preconditions and postconditions, respectively.

A method's precondition is a condition that must be true when the method is invoked. Preconditions describe method parameters and any other expectations the method has about the current state of a program. If a user fails to meet the preconditions, then the method's behavior is undefinedit may throw an exception, proceed with an illegal value or attempt to recover from the error. However, you should never rely on or expect consistent behavior if the preconditions are not satisfied.

A method's postcondition of a method is a condition that is true after the method successfully returns. Postconditions describe the return value and any other side-effects the method may have. When calling a method, you may assume that a method fulfills all of its postconditions. If you are writing your own method, you should document all postconditions so others know what to expect when they call the method.

As an example, examine String method charAt, which has one int parameteran index in the String. For a precondition, method charAt assumes that index is greater than or equal to zero and less than the length of the String. If the precondition is met, the postcondition states the method will return the character at the position in the String specified by the parameter index. Otherwise, the method throws an IndexOutOfBoundsException. We trust that method charAt satisfies its postcondition, provided that we meet the precondition. We do not need to be concerned with the details of how the method actually retrieves the character at the index. This allows the programmer to focus more on the overall design of the program rather than on the implementation details.

Some programmers state the preconditions and postconditions informally as part of the general method specification, while others prefer a more formal approach by explicitly defining them. When designing your own methods, you should state the preconditions and postconditions in a comment before the method declaration in whichever manner you prefer. Stating the preconditions and postconditions before writing a method will also help guide you as you implement the method.