I2E: Design by Contract and Assertions

If classes are to deserve their definition as abstract data type implementations, they must be known not just by the available operations, but also by the formal properties of these operations, which did not yet appear in the preceding example.

The role of assertions

Eiffel encourages software developers to express formal properties of classes by writing assertions, which may in particular appear in the following roles:

• Routine preconditions express the requirements that clients must satisfy whenever they call a routine. For example the designer of ACCOUNT may wish to permit a withdrawal operation only if it keeps the account's balance at or above the minimum. Preconditions are introduced by the keyword require.
• Routine postconditions, introduced by the keyword ensure, express conditions that the routine (the supplier) guarantees on return, if the precondition was satisfied on entry.
• A class invariant must be satisfied by every instance of the class whenever the instance is externally accessible: after creation, and after any call to an exported routine of the class. The invariant appears in a clause introduced by the keyword invariant, and represents a general consistency constraint imposed on all routines of the class.

With appropriate assertions, the class ACCOUNT becomes: class ACCOUNT create make feature ... Attributes as before: balance , minimum_balance , owner , open ... deposit (sum: INTEGER) -- Deposit sum into the account. require sum >= 0 do add (sum) ensure balance = old balance + sum end withdraw (sum: INTEGER) -- Withdraw sum from the account. require sum >= 0 sum <= balance - minimum_balance do add (-sum) ensure balance = old balance - sum end may_withdraw ... -- As before feature {NONE} add ... make (initial: INTEGER) -- Initialize account with balance initial. require initial >= minimum_balance do balance := initial end invariant balance >= minimum_balance end -- ACCOUNT

The notation old expression is only valid in a routine postcondition. It denotes the value the expression had on routine entry.

Creation procedures

In its last version above, the class now includes a creation procedure, make. With the first version, clients used creation instructions such as create acc1 to create accounts; but then the default initialization, setting balance to zero, violated the invariant. By having one or more creation procedures, listed in the create clause at the beginning of the class text, a class offers a way to override the default initializations. The effect of create acc1.make (5_500)

is to allocate the object (as with the default creation) and to call procedure make on this object, with the argument given. This call is correct since it satisfies the precondition; it will ensure the invariant.

Info: The underscore _ in the integer constant 5_500 has no semantic effect. The general rule is that you can group digits by sets of three from the right to improve the readability of integer constants.

Note that the same keyword, create, serves both to introduce creation instructions and the creation clause listing creation procedures at the beginning of the class.

A procedure listed in the creation clause, such as make, otherwise enjoys the same properties as other routines, especially for calls. Here the procedure make is secret since it appears in a clause starting with feature {NONE}

so it would be invalid for a client to include a call such as acc.make (8_000)

To make such a call valid, it would suffice to move the declaration of make to the first feature clause of class ACCOUNT, which carries no export restriction. Such a call does not create any new object, but simply resets the balance of a previously created account.

Design by Contract™

Syntactically, assertions are boolean expressions, with a few extensions such as the old notation. Also, you may split an assertion into two or more clauses, as here with the precondition of withdraw; this is as if you had separated the clauses with an and, but makes the assertion clearer, especially if it includes many conditions.

Assertions play a central part in the Eiffel method for building reliable object-oriented software. They serve to make explicit the assumptions on which programmers rely when they write software elements that they believe are correct. Writing assertions amounts to spelling out the terms of the contract which governs the relationship between a routine and its callers. The precondition binds the callers; the postcondition binds the routine.

The underlying theory of Design by Contract™, the centerpiece of the Eiffel method, views software construction as based on contracts between clients (callers) and suppliers (routines), relying on mutual obligations and benefits made explicit by the assertions.

The Contract Form

Assertions are also an indispensable tool for the documentation of reusable software components: one cannot expect large-scale reuse without a precise documentation of what every component expects (precondition), what it guarantees in return (postcondition) and what general conditions it maintains (invariant).

Documentation tools in EiffelStudio use assertions to produce information for client programmers, describing classes in terms of observable behavior, not implementation. In particular the Contract Form of a class, also called its "short form", which serves as its interface documentation, is obtained from the full text by removing all non-exported features and all implementation information such as do clauses of routines, but keeping interface information and in particular assertions. Here is the Contract Form of the above class: class interface ACCOUNT create make feature balance: INTEGER ... deposit (sum: INTEGER) -- Deposit sum into the account. require sum >= 0 ensure balance = old balance + sum withdraw (sum: INTEGER) -- Withdraw sum from the account. require sum >= 0 sum <= balance - minimum_balance ensure balance = old balance - sum may_withdraw ... end -- ACCOUNT

This is not actual Eiffel, only documentation of Eiffel classes, hence the use of slightly different syntax to avoid any confusion ( class interface rather than class). In accordance with the Uniform Access Principle (in Classes), the output for balance would be the same if this feature were a function rather than an attribute.

You will find in EiffelStudio automatic tools to produce the Contract Form of a class. You can also get the Flat Contract form, based on the same ideas but including inherited features along with those introduced in the class itself. EiffelStudio can produce these forms, and other documentation views of a class, in a variety of output formats including HTML, so that collaborative projects can automatically post the latest versions of their class interfaces on the Internet or an Intranet.

Contracts for testing and debugging

Under EiffelStudio you may also set up compilation options, for the whole system or specific classes only, to evaluate assertions at run time, to uncover potential errors ("bugs"). EiffelStudio provides several levels of assertion monitoring: preconditions only, postconditions etc. When monitoring is on, an assertion which evaluates to true has no further effect on the execution. An assertion that evaluates to false will trigger an exception, as described next; unless you have written an appropriate exception handler, the exception will cause an error message and termination with a precise message and a call trace.

This ability to check assertions provides a powerful testing and debugging mechanism, in particular because the classes of the EiffelBase Libraries, widely used in Eiffel software development, are protected by carefully written assertions.

Run-time monitoring, however, is only one application of assertions, whose role as design and documentation aids, as part of the theory of Design by Contract™, exerts a pervasive influence on the Eiffel style of software development.