Preconditions and Postconditions

[Page 818]

A good way to design and document loops and methods is to specify their preconditions and postconditions. A precondition is a condition that must be true before the method (or loop) starts. A postcondition is a condition that must be true after the method (or loop) completes. Although the conditions can be represented formallyusing boolean expressionsthis is not necessary. It suffices to give a clear and concise statement of the essential facts before and after the method (or loop).

Chapter 6 introduces the use of preconditions and postconditions, and Chapters 6 through 8 provide numerous examples of how to use them. It may be helpful to reread some of those examples and model your documentation after them.