Design by contract

Design by contract is a technique, introduced by Betrand Meyer and applied within the Eiffel programming language. The concept allows a programmer to document the rights and responsibilities of everyone who uses your code. A contract (not to be confused with a .Net WCF contract) can contain the following elements:

  • A precondition;
  • An invariant;
  • A postcondition.

Preconditions state the conditions that must be met in order to enter the method. For example a parameter “i” must have a positive value. Postconditions describe the conditions of the result of the method. An invariant states the condition which will be always be true, seen from a perspective from the calling party. Using the pre-, postconditions and invariants you can also show the correctness of a program.

A little example will show clarify the above mentioned elements.

Pre: 0<=i<10
Invariant: 0<=j<10
Post: i=10
void DoYourThing(int i, int j)
{
    for (k:=i; k<10; k++)
    {
        j := i;
    }
}

The example above will expect a value for “i” that lies between 0 and 10 and the result for I will be 10.

Code contracts in C#

By default, C# doesn’t support code contracts. However, Microsoft provides via an additional library support for it within the .Net environment. The library can be downloaded from its official site (http://research.microsoft.com/en-us/projects/contracts/). Also here is shown how you can install and use the code contracts library.

When you’ve installed the code contracts library in C#, you can begin by declaring your method and place the contract you want to be verified. In our example above, this will look like:

void DoYourThing(int i, in j)
{
    Contract.Ensures(0<=i<10);
    …
}

When the contract is violated, an exception will be thrown. Due to the nature of code contracts, we place them on public methods of our code. It is you who wrote the private members, so you should be responsible for your own to respect the guards of your private methods.

It is also possible to static checking (see http://en.wikipedia.org/wiki/Static_program_analysis) your code: the code will be checked against the code contracts and whether it will break any of the contracts. In older versions you weren’t be able to enable the static checking within Visual Studio Professional. When you wrote an API that uses code contracts, you can also offer the users of your API the contract reference assembly. In this case, they also can validate their code interacting with your API and if it doesn’t break any of the contracts on the API. To build the contract reference assembly, select under project properties “Code Contracts” and make sure “Build” is selected for “Contract Reference Assembly”. The contract build for assembly “X”, will be called “X.Contracts.dll” where “x” is the name of the assembly belonging to the validation.

Inherited contracts are also supported; this means when you write a contract for a parent, its child will at least support the contracts of its parent.

How to use code contracts properly

First of all, code contracts are a design method. I think many people forget this. It is not something that will help you to prevent you to write defensive code. Code contracts are designed to help you describing how others should use your method and what they can achieve when using it this way. However, you can use code contracts in three ways:

  1. Enable only in debug builds without any additional checks;
  2. Enable in release and debug builds;
  3. Enable code contracts only in debug builds, and not in release builds but with additional checks.

The first option is the less safe option. When you release your software and the contract is not respected, your code will be broken. This is also in contrast with writing defensive code.

You could also enable checking for coding contracts during release mode. When you write for example an API, you have to be sure that the calling party knows the type of exception you will throw when a contract is broken.

The safest way in my opinion is to enable the check for coding contracts only during debug and use defensive programming techniques to ensure the contracts are not violated.

How to start from here

In this blog entry I wanted to show the benefits of code contracts, but more than that showing how you should use it in a proper way. As I already wrote in this entry, some people think that if they write code contracts around their code it will cache any of the errors. If you use code contracts this way, it’s not the right way. In my opinion the main benefits of code contracts: a way of documenting your code and with the use of a static analysis a way of validating your code.

Posted in Best practices, C# by Bruno at March 3rd, 2013.
Tags:

Leave a Reply