AdaPower Logged in as Guest
Ada Tools and Resources

Ada 95 Reference Manual
Ada Source Code Treasury
Bindings and Packages
Ada FAQ


Join >
Home >
Articles >
Getting Started >
Ada FAQ >
Source Treasury >
Books & Tutorials >
Packages for Reuse >
Latest Additions >
Ada Projects >
Press Releases >
Ada Audio / Video >
Home Pages >
Links >
Contact >
About >
Login >
Back
What are pre-conditions, post-conditions, and invariants? (Richard Riehle)

A pre-condition test (Eiffel Require assertion) guarantees that a subprogram will not be entered unless the assertion is satisfied. It can, in some environments, be applied at the class/type level, but is more often at the subprogram level. An example of this assertion is the "barrier" on a protected entry. The barrier is a lot like a pre-condition since it also evaluates a boolean expression before we can begin execution of the routine. The barrier is not precisely identical to a pre- condition, but it should give you the general idea.

A post-condition (Eiffel Ensure) guarantees that a certain set of circumstances will be true before exiting a subprogram. If the post-condition fails, an exception may be raised.

An invariant is much as it might seem to be from its name. During the life of the entity given an invariant condition, the invariant must be true.

The Require, Ensure, and Invariant conditions may be applied to a subprogram, a type, or a even some variable. The designer of Eiffel (who did not invent these ideas but incorporated them into the design of his language), calls this "design by contract." It is important to understand that this is a run-time contract.


(c) 1998-2004 All Rights Reserved David Botton