Home > Articles > Programming

  • Print
  • + Share This
This chapter is from the book

This chapter is from the book

1.8 Summary

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.)

  • + Share This
  • 🔖 Save To Your Account