Section A.8 Preconditions and Postconditions
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 formally — using boolean expressions — this 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 the examples shown there.