Skip to main content

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.

You have attempted of activities on this page.