Encodo White Papers: Design by Contract (2006)

Design by Contract is a software engineering practice in which software requirements and promises − the “Contract” − are explicitly written into the code. The code is, at the same time, better documented, more reliable and easier to test against. Encodo uses this technique to ensure software quality.

A brief overview of contracts

A software contract is composed of several components: preconditions, postconditions and invariants. Preconditions are what a component requires of a client, whereas postconditions are what a component guarantees to a client. In object-oriented programming, these contracts are attached to method calls in a class. Invariants are a list of conditions that must always be true for software. An invariant is typically attached directly to a class; the runtime checks the class invariant when entering and exiting a method call.

Popular programming languages, like Java, C#, Delphi Pascal and others, lack the language constructs needed to express these contracts. However, these languages contain assertion constructs, which allow one to roughly describe the contracts. The section on emulating contracts in other languages section shows the most common technique.

Eiffel is a language whose inventor, Bertrand Meyer, pioneered Design by Contract. It includes rich support for expressing contracts, is similar to Pascal in syntax and will be used for the examples below. The FAQ offers more information on why we chose Eiffel for our examples.

Using contracts

The best way to show how the use of contracts affects software is with an example. Imagine a database connection class with a method Open. This opens a connection to the database, allocating resources for it and failing if the request is refused.

Open is
  do
    – Execute code to open the connection here
  end

Any procedural programming language is capable of formulating the code above. However, what happens if Open is called twice in a row on the same connection? One way to handle this is to simply ignore subsequent calls to Open.

Open is
  do
    if not IsOpen then
      – Execute code to open the connection here
    end
  end

This is not optimal, for several reasons:

• Clients that misbehave by repeatedly calling a powerful function like Open will never know they are doing so.
• Clients that lack the original source will have no idea that the check is already made and will check again, needlessly muddying their code and wasting performance.
• The function fails to open the connection silently, which is an extremely dangerous way of responding to a non-standard condition.

Another way to respond is to accept that this might happen, but making it non-silent, logging the occurrence to some sort of logging mechanism.

Open is
  do
    if not IsOpen then
      – Execute code to open the connection here
    else
      – Log a warning
    end
  end

This is slightly better and an entirely appropriate solution in some cases. However, the connection is quite a low-level component; it should not be responsible for deciding what to do about repeated calls to Open. We can use a contract to push the responsibility onto the client.

Open is
  require
    not IsOpen
  do
    – Execute code to open the connection here
  end

The require clause contains optionally named boolean expressions. If one evaluates to false, a precondition violation is signaled. The violator can immediately be pinpointed and repaired to conform to the contract (by adding a check for IsOpen before calling Open). What are the benefits?

• A client has a list of conditions that must be satisfied before calling a routine. The interface is clear.
• A routine has a way of devolving responsibility for certain conditions onto its clients.

The contract for this routine is not complete, as it has only published its requirements, but said nothing about guarantees. Given the name of the function, we would expect it to have the following postcondition:

Open is
  require
    not IsOpen
  do
    – Execute code to open the connection here
  ensure
    IsOpen
  end

The function is now completely defined, having explicitly detailed its requirements and guarantees. The postcondition often looks quite superfluous: the code for opening the connection is right above it, isn’t it?

Not necessarily.

If the function is deferred (abstract in Java and Pascal, virtual in C-style languages), the implementation is in a descendent. The pre- and postconditions apply to the redefinitions as well. This allows a base class to very precisely define its interface with other classes without making any decisions about implementation.

Open is
  require
    not IsOpen
  deferred
  ensure
    IsOpen
  end

The precondition can only be expanded in a descendent, whereas the postcondition can only be further constrained. That is, a descendent cannot define the precondition to be not IsOpen and DatabaseExists. A client with a reference to the ancestor class sees only the ancestor precondition and cannot be forced to conform to a contract defined in a descendent.

Likewise, the postcondition cannot be redefined to be IsOpen or ActionFailed. The original interface has already decided that if the database cannot be opened, the implementation must raise an exception. A client with a reference to the ancestor class does not have access to the ActionFailed feature and cannot accept this as a valid postcondition.

The descendent adjusts the precondition in a function like this:

Open is
  require else
    AutoCloseIfOpened
  do
    – Execute code to open the connection here
  ensure then
    not CompactOnOpen or DatabaseIsCompacted
  end

This descendent has expanded the precondition to allow a caller to call Open repeatedly only if IsOpen is false (inherited precondition) or if the AutoCloseIfOpened option has been set. Likewise, it has further constrained the postcondition to promise that, in addition to IsOpen being true (inherited postcondition), the database will be compacted if the CompactOnOpen option is set.

Emulating Contracts in other Languages

So, that’s Eiffel. How can other languages express contracts without the proper language constructs? As mentioned above, almost all modern languages include an assert function, which accepts a boolean expression and raises an exception if it is false. This function can emulate pre- and postconditions, but class invariants are largely impractical in languages without some form of pre-processor (a search for Design by Contract in C++ turns up several such libraries). Here’s Listing 5 written in Delphi Pascal:

procedure Open;
  begin
    Assert( not IsOpen );
    // Execute code to open the connection here
    Assert( IsOpen );
  end {Open};

Note how the contract is expressed in the implementation body; this makes contract inheritance difficult. The following pattern illustrates a single level of contract inheritance (which prevents descendants from removing contracts by not calling inherited methods):

procedure Open;  // Not overridable
  begin
    Assert( not IsOpen );
    DoOpen;
    Assert( IsOpen );
  end;

procedure DoOpen; virtual; abstract;

Under this pattern, descendants are required to implement DoOpen and cannot alter Open (Delphi methods are by static by default − equivalent to final in Java, sealed in C# or frozen in Eiffel). There are naturally drawbacks to this approach, especially when compared to the rich contract syntax available in Eiffel*, but the technique is sufficient for many of the desired contracts.

See the further reading below to learn about using old in postconditions and expressing class invariants

FAQ

Question 1

“Why is there no try .. finally to ensure that the postcondition is checked in Listing 8?”

A postcondition is only guaranteed when the function exits successfully. In the example, it is perfectly legitimate for Open to fail because of an external connection problem. The precondition only guarantees that the connection is not open, not that it can be opened. Such guarantees are useless because they involve performing the action in order to check that the action can be performed.

The function should raise an exception if it cannot open the connection, avoiding evaluation of the postcondition and resulting in an acceptable error condition. An implementation that fails silently will cause a postcondition violation, which is an unacceptable error condition.

Using a try .. finally construct to force evaluation of the postcondition under all circumstances would result in both the desired error (connection could not be opened) and a postcondition violation, which is not correct.

Question 2

“What if there is an exit or return statement in Listing 8?”

Question 1 proposed a using a try .. finally construct to ensure that the postcondition was always executed. As you can see from the answer, this has undesirable side effects. The simple answer is not to use instructions that break the normal instruction flow (e.g. exit or break). The usefulness of such constructs is debatable and the drawbacks are high (especially, as shown above, when the instruction avoids checking contracts).

This exposes the weakness of languages without explicit contract constructs — it requires discipline to avoid bad practices. Relying purely on discipline invites error. However, it is better than nothing at all.

Further Reading

• Object-oriented Software Construction
• Eiffel.com Presentations