Into Eiffel by Ian Joyner (4/5)

One of the most significant aspects of Eiffel is that it is not only a language with which you can write executable software, but it is a language that embodies many design concepts. Thus you can use the same language for design and implementation. The notion of design by contract is a formal way to divide up the work between a routine and its caller, so that all the work is done and it is not repeated, which would cause performance problems.

Not only is design by contract a formal way of designing interfaces, but a good way to document interfaces. Often routine signatures are not enough to show how to call a routine—contract information adds the extra details.

The most noticeable language features are the pre and postconditions of routines in the requires and ensures clauses. An example is:

square_root (n: REAL): REAL is require n >= 0 do Result := ... sqrt calculation ensure n = Result * Result end -- square_root

Here the requires clause tells the caller that they are responsible for checking that the argument passed is nonnegative. The ensure clause tells us some properties of the calculation and the conditions we expect to hold after the routine is complete. Not only do these clauses document what is expected of the caller and of the routine itself, but these are checked at run time to make sure the software is operating correctly (as long as assertion monitoring is turned on—it can be turned off once you are confident that the software is working correctly).

If the assertion checks fail, an exception is raised. If the require clause fails, an exception is raised in the caller. If an ensure clause fails, an exception is raised in the routine itself. Exceptions may be caught with a rescue clause and if able to be corrected, the routine can be restarted with the retry instruction:

square_root (n: REAL): REAL is require n >= 0 do Result := ... sqrt calculation ensure n = Result * Result rescue ... clean up instructions ... if cleanup successful... retry end -- square_root

If a retry instruction is not executed in the body of the rescue clause, the routine fails, and a exception is raised in the caller. If the precondition n >= 0 fails, then the exception is raised in the caller since in design by contract, they have failed their obligation.

Not only can preconditions check parameters, but they can also check the object state to ensure that the object has been set up correctly prior to a routine call. For instance, consider a WINDOW object. Before being able to move the WINDOW, the window must be open, so a requirement of the move routine would be that the window is open.

Note that this gives a level of documentation that programmers have always wanted—what order should things be done in.

Another aspect of design by contract is the class invariant. The class invariant always makes sure that objects are in a valid state. This is closely related to creation routines because creation routines must initialise the state of an object so that the class invariant is satisfied. For normal routines to execute correctly, not only must their requires clause be met, but the class invariant must also be satisfied. A normal routine must also leave an object in a valid state, so the class invariant is always checked when a routine completes. (In fact, it is a little more complicated than this in the case where a chain of routines are called on the same object, but we needn’t concern ourselves with that here.)