Previous | Table of Contents | Next |
Eiffel directly implements the ideas of design by contract, which enhance software reliability and provide a sound basis for software specification, documentation, and testing, as well as exception handling and the proper use of inheritance.
A systema software system in particular, but the ideas are more generalis made of a number of cooperating components. Design by contract states that their cooperation should be based on precise specificationscontractsdescribing each partys expectations and guarantees.
An Eiffel contract is similar to a real-life contract between two people or two companies, which it is convenient to express in the form of tables listing the expectations and guarantees. Here for example is how we could sketch the contract between a homeowner and the telephone company:
provide_service | Obligations | Benefits |
---|---|---|
Client | (Satisfy precondition:) Pay bill | (From postcondition:) Get telephone service |
Supplier | (Satisfy postcondition:) Provide telephone service | (From precondition:) No need to provide anything if bill not paid |
Note how the obligation for each of the parties maps onto a benefit for the other. This is a general pattern.
The clients obligation, which protects the supplier, is called a precondition. It states what the client must satisfy before requesting a certain service. The clients benefit, which describes what the supplier must do (assuming the precondition was satisfied), is called a postcondition.
In addition to preconditions and postconditions, there are also invariants applying to a class as a whole. More precisely, a class invariant must be ensured by every creation procedure (or by the default initialization if there is no creation procedure) and maintained by every exported routine of the class.
Eiffel provides syntax for expressing preconditions (require), postconditions (ensure), and class invariants (invariant), as well as other assertion constructs studied later (section 9.10.3): loop invariants and variants, check instructions.
Here is a partial update of class ACCOUNT with more assertions:
indexing description: Simple bank accounts class ACCOUNT feature -- Access balance: INTEGER -- Current balance deposit_count: INTEGER is -- Number of deposits made since opening do ... As before ... end feature -- Element change deposit (sum: INTEGER) is -- Add sum to account. require non_negative: sum >= 0 do ... As before ... ensure one_more_deposit: deposit_count = old deposit_count + 1 updated: balance = old balance + sum end feature {NONE} -- Implementation all_deposits: DEPOSIT_LIST -- List of deposits since accounts opening. invariant consistent_balance: (all_deposits /= Void) implies (balance = all_deposits.total) zero_if_no_deposits: (all_deposits = Void) implies (balance = 0) end -- class ACCOUNT
Each assertion is made of one or more subclauses, each of them a boolean expression (with the additional possibility of the old construct). If there is more than one subclause, as in the postcondition of deposit and in the invariant, they are treated as if they were connected by an and. Each clause may be preceded by a label, such as consistent_balance in the invariant, and a colon; the label is optional and does not affect the assertions semantics, except for error reporting as explained in the next section, but including it systematically is part of the recommended style as applied by this chapter. The boolean expression a implies b is true if a is false and otherwise if both a and b are true.
Because assertions benefit from the full power of boolean expressions, they may include function calls. This makes it possible to express sophisticated consistency conditions, such as the graph contains no cycle, which is not otherwise expressible through simple expressions, or even through first-order predicate calculus, but which are easy to implement as Eiffel functions returning boolean results.
The precondition of a routine expresses conditions that the routine is imposing on its clients. Here a call to deposit is correct if and only if the value of the argument is non-negative. The routine does not guarantee anything for a call that does not satisfy the precondition. It is in fact part of the Eiffel method that a routine body should never test for the precondition because it is the clients responsibility to ensure it. (An apparent paradox of design by contract, which is reflected in the bottom-right entries of the preceding and following contract tables, and should not be a paradox any more at the end of this discussion, is that one can get more reliable software by having fewer explicit checks in the software text.)
The postcondition of a routine expresses what the routine does guarantee to its clients for calls satisfying the precondition. The notation old expression, valid in postconditions (ensure clauses) only, denotes the value that expression had on entry to the routine.
Previous | Table of Contents | Next |