Previous Table of Contents Next


The precondition and postcondition state the terms of the contract between the routine and its clients, similar to the earlier example of a human contract:

deposit Obligations Benefits
Client (Satisfy precondition:)
Use a non-negative argument.
(From postcondition:)
Get deposits list and balance updated.
Supplier (Satisfy postcondition:)
Update deposits list and balance.
(From precondition:)
No need to handle negative arguments.

The class invariant, as noted, applies to all features. It must be satisfied on exit by any creation procedures and is implicitly added to both the precondition and postcondition of every exported routine. In this respect, it is both good news and bad news for the routine implementer: good news because it guarantees that the object is initially in a stable state, averting the need in the preceding example to check that the total of all_deposits is compatible with the balance, and bad news because, in addition to its official contract as expressed by its specific postcondition, every routine must take care of restoring the invariant on exit.

A requirement on meaningful contracts is that they should be in good faith: satisfiable by an honest partner. This implies a consistency rule: If a routine is exported to a client (either generally or selectively), any feature appearing in its precondition must also be available to that client. Otherwise—for example, if the precondition included require n > 0, where n is a secret attribute—the supplier would be making demands that a good-faith client cannot possibly check for.

It should be noted in this respect that ensuring a precondition does not necessarily mean testing for it explicitly. Assuming n is indeed exported, a client can make a correct call as

   if x.n > 0 then x.r end

possibly with an else part, but this is not the only possible form: If n is known to be positive, perhaps because some preceding call set it to the sum of two squares, then there is no need for protection by an if or equivalent. In such a case, a check instruction as introduced later (section 9.10.3) is recommended if the reason for omitting the test is non-trivial.

9.8.3. Using Assertions for Built-in Reliability

The first use of assertions is purely methodological. By applying a discipline of expressing, as precisely as possible, the logical assumptions behind software elements, one can write software whose reliability is built-in: software that is developed hand-in-hand with the rationale for its correctness.

This simple observation—usually not clear to people until they have practiced design by contract thoroughly on a large-scale project—brings as much change to software practices and quality as the rest of object technology.

9.8.4. Runtime Assertion Monitoring

Assertions in Eiffel are not just wishful thinking. They can be monitored at runtime under the control of compilation options.

It should be clear from the preceding discussion that assertions are not a mechanism to test for special conditions—for example, erroneous user input. For that purpose, the usual control structures (if deposit_sum >= 0 then ...) are available, complemented in applicable cases by the exception-handling mechanism reviewed next. An assertion is instead a correctness condition governing the relationship between two software modules (not a software module and a human or a software module and an external device). If sum is negative on entry to deposit, violating the precondition, the culprit is some other software element, whose author was not careful enough to observe the terms of the deal. Bluntly:


Assertion violation rule:  
A runtime assertion violation is the manifestation of a bug.

To be more precise:

  A precondition violation signals a bug in the client, which did not observe its part of the deal.
  A postcondition (or invariant) violation signals a bug in the supplier—the routine—which did not do its job.

That violations indicate bugs explains why it is possible to enable or disable assertion monitoring through mere compilation options: for a correct system—one without bugs—assertions always hold, so the compilation option makes no difference to the semantics of the system.

Of course, for an incorrect system, the best way to find out where the bug is—or just that there is a bug—is often to check the assertions. As a result, Eiffel environments typically provide compilation options at several levels (here as supported in ISE Eiffel, which makes them settable separately for each class, with defaults at the system and cluster levels):

  no—assertions have no runtime effect.
  require—check preconditions only, on routine entry.
  ensure—preconditions on entry, postconditions on exit.
  invariant—as ensure, plus class invariant on both entry and exit for qualified calls.
  all—as invariant, plus check instructions, loop invariants, and loop variants (section 9.10.3).

An assertion violation, if detected at runtime under one of these options other than the first, causes an exception (section 9.8.6). Unless the software has an explicit “retry” plan as explained later, the violation causes production of an exception trace and termination (or, in development environment such as EiffelBench, a return to the browsing and debugging facilities of the environment at the point of failure). If present, the label of the violated subclause is displayed, serving to identify the cause precisely.


Previous Table of Contents Next