Axiomatic semantics is based on mathematical logic. The logical expressions are called predicates, or assertions. An assertion immediately preceding a program statement describes the constraints on the program variables at that point in the program. An assertion immediately following a statement describes the new constaraints on those variables after execution of the statement.
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.
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 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 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.
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.
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.
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.
