Assertions -- formal specification
- require -- method call pre-condition
- ensure, promise -- post-condition
- invariant -- object invariance
slide: Formal specification of contracts
Intuitively, contracts have a clear analogy
to our business affairs in everyday life.
For instance, when buying audio equipment, as
a client you wish to know what you get for
the price you pay, whereas the dealer may require
that you pay in cash.
Following this metaphor through, we see that
the supplier may actually benefit from
imposing a (reasonable) pre-condition and that
the client has an interest in a well-stated post-condition.
Most people are not willing to pay without knowing
what they will get for their money.
Language support
The use of contracts was originally
proposed by [Meyer88], and is directly
supported by the language Eiffel,
which offers the keywords require
(to indicate a pre-condition),
ensure (to indicate a post-condition)
and invariant (to indicate the invariance condition).
See slide [3-formal].
The Eiffel environment has options to dynamically
check any of the three kinds of assertions,
even selectively per class.
The assertions, except for the invariance condition,
are directly embedded in the code.
Although less elegant, the same functionality
can be achieved in C++ by using the assert
macro defined in {\tt assert.h} as explained
in section [ASSERT], which also introduced
the require and promise macros for C++.
For dynamically checking the invariance condition,
a test should be executed when evaluating the
constructor
and before and after each method
invocation.
While a method is being executed, the invariant
need not necessarily hold,
but it is the responsibility of a method to
restore the invariant when it is disrupted.
In case object methods are recursively applied,
the invariant must be restored when returning
to the original caller.
An alternative approach to incorporating assertions
in a class description is presented in [Cline],
which introduces an extension of C++ called Annotated C++.
Instead of directly embedding assertions in the
code, Annotated C++ requires the user to
specify separately the axioms characterizing
the functionality of the methods and their
effect on the state of the object.
Interfaces
Contracts may be used to
document the method interface of a class.
Pre- and post-conditions allow the class designer
to specify in a concise manner the functional
characteristics of a method,
whereas the use of natural language often leads to
lengthy (and imprecise) descriptions.
Below, an example is given of a contract specifying an account.
class account { account
public:
account();
// assert( invariant() );
virtual float balance() { return _balance; }
void deposit(float x); to deposit money
// require( );
// promise( balance() old_balance x && invariant() );
void withdraw(float x); to withdraw money
// require( x balance() );
// promise( balance() old_balance x && invariant() );
bool invariant() { return balance() 0; }
protected:
float _balance;
};
slide: The $account$ contract
The interface for the account class
specifies in an abstract way what the user
expects of an account.
From the perspective of design, the behavioral
abstraction expressed by the axioms is exactly
what we need, in principle.
The implementation must guarantee that these constraints
are met.
System development
From the perspective of system development,
the notion of contracts has some interesting consequences.
Assertions may be used to decide
who is responsible for any erroneous behavior of the system.
See slide [3-limits].
System development
- violated pre-condition -- bug in client
- violated post-condition -- bug in supplier
A pre-condition limits the cases that
a supplier must handle!
slide: System development with contracts
For example, imagine that you are using a software
library to implement a system for financial transactions
and that your company suffers a number of losses
due to bugs in the system.
How would you find out whether the loss is your own fault
or whether it is caused by some bug in the library?
Perhaps surprisingly, the use of assertions allows
you to determine exactly whether to sue the library
vendor or not.
Assume that the classes in the library are
all annotated with assertions that can be checked
dynamically at runtime.
Now, when you replay the examples that resulted
in a loss for your company with the option
for checking pre- and post-conditions on,
it can easily be decided who is in error.
In the case that a pre-condition of a method
signals violation, you, as a client of a library
object, are in error.
However, when no pre-condition violation is signaled,
but instead a post-condition is violated, then the library
object as the supplier of a service is in error;
and you may proceed to go to court,
or do something less dramatic such as asking the
software vendor to correct the bug.
Realization
The contract specified in the account class interface
may actually be enforced
in code as illustrated below.
class account { account
public:
account() { _balance = 0; assert(invariant()); }
virtual float balance() { return _balance; }
void deposit(float x) {
require( x >= 0 ); check precondition
hold(); to save the old state
_balance += x;
promise( balance() == old_balance + x );
promise( invariant() );
}
void withdraw(float x) {
require( x <= _balance ); check precondition
hold(); to save the old state
_balance -= x;
promise( balance() == old_balance - x );
promise( invariant() );
}
virtual bool invariant() { return balance() >= 0; }
protected:
float _balance;
float old_balance; additional variable
virtual void hold() { old_balance = _balance; }
};
slide: The realization of the $account$ contract
The additional variable {\em old_balance} is needed
to compare the state preceding an operation with
the state that results afterwards.
The old state must explicitly be copied by calling hold.
In this respect, Eiffel offers better support
than C++.
Whenever proves to be less than zero,
the procedure sketched above can be used to determine whether
the error is caused by an erroneous method invocation,
for example when calling with ,
or whether the implementation code contains a bug.
For the developer of the software, pre-conditions
offer a means to limit the number of cases that a method
must be able to handle.
Often, programmers tend to anticipate all possible uses.
For instance, many programs or systems have options that
may be learned only when inspecting the source code
but are otherwise undocumented. \nop{See for example [UndocDos].}
Rather than providing all possible options,
for now and the future, it is more sensible to delineate
in a precise manner what input will be processed and what
input is considered illegal.
For the developer, this may significantly reduce
the effort of producing the software.