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. Otherwisefor example, if the precondition included require n > 0, where n is a secret attributethe 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.
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 observationusually not clear to people until they have practiced design by contract thoroughly on a large-scale projectbrings as much change to software practices and quality as the rest of object technology.
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 conditionsfor 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:
That violations indicate bugs explains why it is possible to enable or disable assertion monitoring through mere compilation options: for a correct systemone without bugsassertions 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 isor just that there is a bugis 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):
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 |