Interactive
Software Engineering		 Assertions

[ISE Home] [ Home ] [ Release Notes ] [ Technology Papers ] [ Installation Notes ] [ About Eiffel ]

5 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 appear in the above example.

5.1 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 ACCOUNT class becomes:

    class ACCOUNT creation

    make
    feature

    ... Attributes as before: balance, minimum_balance, owner, open ...

    deposit (sum: INTEGER) is
    -- Deposit sum into the account.
    require
    sum >= 0
    do
    add (sum)
    ensure
    balance = old balance + sum
    end;


    withdraw (sum: INTEGER) is
    -- 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 ... -- As before

    make (initial: INTEGER) is
    -- Initialize account with balance initial.
    require
    initial >= minimum_balance
    do
    balance := initial
    end
    invariant

    balance >= minimum_balance
    end -- class ACCOUNT

The notation old attribute_name may only be used in a routine postcondition. It denotes the value the attribute had on routine entry.

5.2 Creation procedures

In its last version above, the class now includes a creation procedure, make. With the first version of ACCOUNT, clients used creation instructions such as old 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 creation 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. (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.)

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.

5.3 Design by Contract

Syntactically, assertions are boolean expressions, with a few extensions such as the old notation. The semicolon (see the precondition to withdraw) is equivalent to an "and", but permits individual identification of the components.

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, in particular preconditions and postconditions, 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.

5.4 The short 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 EiffelBench use assertions to produce information for client programmers, describing classes in terms of observable behavior, not implementation. In particular the short form of a class, 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 short form of the above class:

    class interface ACCOUNT creation

    make

    feature

    balance: INTEGER;
    ...

    deposit (sum: INTEGER) is
    -- Deposit sum into the account.
    require
    sum >= 0
    ensure
    balance = old balance + sum

    withdraw (sum: INTEGER) is
    -- Withdraw sum from the account.
    require
    sum >= 0;
    sum <= balance - minimum_balance
    ensure
    balance = old balance - sum
    may_withdraw ...
    end -- class 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 observations made above, the output for balance would be the same if this feature were a function rather than an attribute.

In the ISE Eiffel environment, the short form is produced by automatic tools described in the book An Object-Oriented Environment: Principles and Application; you can get a flavor for them in the on-line Web ``Guided Tour'' of EiffelBench (see the mention of the Short button of the Class Tool of EiffelBench, as part of the discussion of browsing facilities). It serves as the primary form of class documentation. A variant, the flat-short form, takes inheritance into account by including inherited features along with those introduced in the class itself.

It is also possible to evaluate assertions at run time, so as to uncover potential errors ("bugs"). The implementation 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 which evaluates to false will trigger an exception, as described next; unless the software developer has 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 checking, 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.