Design by Contract: The importance of precise specifications

Design by Contract (DbC) is a pragmatic approach to the design of software that prescribes software designers to provide precise specifications in the form of preconditions, postconditions and invariants

These specifications are referred to as “contracts” and this type of programming philosophy is known as Design by contract (Dbc) programming or Contract-First development (CFD).

Design by Contract emphasizes more on evaluating Software Correctness by means of writing assertions.

This concept has been first used in Eiffel programming language.

Now, it’s available in Microsoft.Net 4.0 in the name of Code Contracts.

The central idea of DbC is a metaphor on how elements of a software system collaborate with each other, on the basis of mutual obligations and benefits. The metaphor comes from business life, where a “client” and a “supplier” agree on a “contract” which defines for example that:

• The supplier must provide a certain product (obligation) and is entitled to expect that the client has paid its fee (benefit).

• The client must pay the fee (obligation) and is entitled to get the product (benefit).

• Both parties must satisfy certain obligations, such as laws and regulations, applying to all contracts

In DbC, the contracts are very much responsible for evaluating the correctness of the software and they should be part of the design process.

Generally, developers have the habit of writing comments for the purpose of readability and documentation. They write contracts also in the form of comments.

Sometimes, there is a chance that client may misunderstand contracts written in the form of comments.

Let’s have a look at the below C# code having Pre-Condition written as comment.

/// <summary>Gets the user for the given ID. </summary>

/// <param name=”id”>Should be > 0 </param>

public User GetUserWithIdOf(int id,

UserRepository userRepository) {

return userRepository.GetById(id);

The developer has documented the Pre-Conditions in the comments. There are a few problems with this:

• If the client didn’t pay attention to the comments, there’s nothing to stop the client from passing in an invalid ID of 0.

• The client could easily pass null for userRepository. This would result in an “object reference” exception.

• What if, down the road, it becomes OK to pass 0 to the method. If the developer neglects to update the comment, then the stated business rule will conflict with the inherit business rule within the code itself.

Design by Contract allows you to transform the implicit contract, described above, into an explicit bidirectional contract. The bidirectional contract obligates both the client to invoke the method in a particular way and for the target method to guarantee a particular result. If the contract is broken, then the breaking party will be severely.

The calling contract is expressed with one or more “pre-conditions” while the response contract is expressed with one or more “post-conditions.” A pre-condition states “this is your end of the bargain which must be adhered to to call me.” A post-condition states “this is my end of the bargain which you can count on me to enforce.” What follows is a very explicit, and very inflexible, bidirectional contract:

The code described above can be written more efficiently by removing the documented contract-level comments and using exception handling as follows:

/// <summary>Gets the user for the given ID. </summary>

public User GetUserWithIdOf(int id,

UserRepository userRepository) {

// Pre-conditions

if (userRepository == null)

throw new ArgumentNullException(

“userRepository”);

if (id <= 0)

throw new ArgumentOutOfRangeException(

“id must be > 0″);

User foundUser = userRepository.GetById (id);

// Post-conditions

if (foundUser == null)

throw new KeyNotFoundException(“No user with ” +

“an ID of ” + id.ToString() +

” could be located.”);

return foundUser;

}

We can use Code contracts instead of throwing built in exceptions at the runtime.

The class library has been written for the .NET environment which addresses these issues. The beauty of code contracts is the ability to check the conditions and give the appropriate messages at the time of compilation itself.

By including pre-conditions and post-conditions which are part of code contracts, the above code can be efficiently transformed like this:

/// <summary>Gets the user for the given ID.</summary>

public User GetUserWithIdOf(int id,

UserRepository userRepository) {

// A Pre-condition to check that the userRepository is not null

Contract.Requires(userRepository != null,

“userRepository may not be null”);

Contract.Require(id > 0, “id must be > 0″);

User foundUser = userRepository.GetById(id);

// A Post-condition to check whether the specific user exists.

Contract.Ensures(foundUser != null, “No user with an ” +

“ID of ” + id.ToString() + ” could be located.”);

return foundUser;

}

Hence, by including code contracts, greater Quality Assurance can be achieved.

Sometimes, trivial programming errors cause huge business loss.

Let’s recap an unfortunate event happened due to a simple programming exception which was unhandled.

“On June 4, 1996, the maiden flight of the European Ariane 5 launcher crashed about 40 seconds after takeoff. Media reports indicated that the amount lost was half a billion dollars — uninsured.”

Can you guess the reason why it happened?

The explosion was the result of an exception that was due to a floating-point error: a conversion from a 64-bit integer to a 16-bit signed integer, which should only have been applied to a number less than 2^15, was erroneously applied to a greater number, representing the “horizontal bias” of the flight. There was no explicit exception handler to catch the exception and so it crashed the entire software.

The programming can take a different dimension with DBC approach.

Benefits of code contracts:-

. Building Robust software components

. Facilitating unit testing

. Handling exceptions in an efficient way

Here are some interesting questions for you:

1) Do you think the DBC approach is only for the large-scale and expensive projects?

2) How can code contracts lead to improved client satisfaction?

3) How can you handle “Null Reference Exceptions” by using code contracts?

The following are the links that can provide more information about DBC.

Design by contract-Overviw:-

http://www.eiffel.com/developers/presentations/dbc/partone/player.html?slide=

http://www.artima.com/intv/contracts.html

Contracts-Microsoft Research

http://research.microsoft.com/en-us/projects/contracts/

The lessons of Ariane:-

http://archive.eiffel.com/doc/manuals/technology/contract/ariane/