Using a very simple example of (part of) a customer manager component, we've introduced the idea that a program can contain assertions. These assertions can be used to write preconditions, postconditions, and invariants.
A precondition specifies the circumstances under which it is valid to call a feature. A postcondition specifies the effect of calling a feature. An invariant specifies unchanging properties of the objects of a class.
Assertions can be checked at runtime to help us test and debug the implementation. As an important by-product of this checking, the documentation accurately describes what the code actually does.
Assertion-checking is built into Eiffel. For other languages such as Java and C++ you can obtain preprocessors that generate the code to turn your assertions into runtime checks, thereby getting the same benefits: runtime checking and trustworthy documentation. (In Chapter 11, we present examples that use the iContract tool developed by Reto Kramer, available from Trusted Systems.)