Code Contract in .NET

Code Contracts is Microsoft’s implementation of Design by Contract(DbC) philosophy.It has been released as a MSDN Dev Labs project and will be a part of .NET Framework 4.0 hence present in VS 2010 Beta 1.Before getting into details of Code Contracts let us quickly cover DbC to set things in context.

The concept of DbC was proposed by Bertrand Meyer and was supported by his programming language Eiffel.In real world when two parties are working together, the contract between the two specifies a set of rules and regulations both must follow to ensure smooth operation.Similarly in object oriented parlance when one object is passing message (invoking method) to another there should be a fixed set of rules to ensure correctness of the operation.DbC focuses on clean documentation and verification of these contracts.The three key ingredients of this contract are:

  • Precondition – This refers to conditions that must be satisfied for the method to be invoked.These are mostly conditions that method arguments must satisfy.
  • Postcondition – This refers to the conditions that must be satisfied after the method has finished execution.These are mostly conditions to be satisfied by the return values.
  • Object Invariant – These are conditions that must hold true for the class before and after the method call.A common textbook example will be a BankAccount class with a property AccountNumber, where the condition AccountNumber!=null must always hold true.

The classes/attributes related to Code Contracts are all present in the System.Diagnostics.Contractsnamespace.Let us consider the following example:

public class BankAccount
 private double balance;
 public string AccountNumber{get;set;}

 public double Balance
 Contract.Ensures(balance > 0, "Balance Cannot Be Negative");
 return balance;
 balance = value;

 public void Withdraw(double amount)
 Contract.Requires(amount > 0, "Deposited Amount Cannot Be Negative");
 Balance -= amount;
 public void CheckInvariants()
 Contract.Invariant(this.AccountNumber !=null, "Account Number Cannot Be Null");


While withdrawing amount from an account the amount always has to be positive.So in the method Withdraw we are using Contract.Require to check this precondition.

The account balance can never be negative so in the getter block of Balance we are checking the postcondition using Contract.Ensures.

This BankAccount class has a AccountNumber which cannot be null for any valid banking operation.So this is an invariant.To check the invariants we need to separate method checking the individual conditions using Contract.Invariant method and this method needs to be marked with ContractInvariantMethod attribute.Here the method CheckInvariants method is doing this task.

After executing this method in VS2010 with values breaking the contract I found that no error message was shown.What happened?Are we missing something?Yes.We have to setup the Code Analysis tab in project properties.

Now an assertion error message is shown whenever the contract is broken.

Here I am using Visual Studio Standard Edition so only Runtime contract checking can be done.However with VS Team Edition static checking of the code contracts is also possible.

Apart from verifying the contracts another key aspect of DbC documentation.This can be done by checking the “Build a Contract Reference Assembly” and “Emit contracts into XML doc file” checkboxes in Code Analysis tab.Also the “XML Documentation File” in Build Tab needs to be checked.On compilation this will generate a XML file with name <<assemblyname>>.xml.In this XML contracts information is documented as shown below:

<?xml version="1.0"?>
 <member name="T:CodeContractsDemo.BankAccount">
 <invariant description="Account Number Cannot Be Null">this.AccountNumber !=null</invariant>
 <member name="M:CodeContractsDemo.BankAccount.Withdraw(System.Double)">
 <requires description="Deposited Amount Cannot Be Negative">amount > 0</requires>
 <member name="P:CodeContractsDemo.BankAccount.Balance">
 <ensures description="Balance Cannot Be Negative">balance > 0</ensures>
This entry was posted in Framework & Libraries. Bookmark the permalink.

Leave a Reply

Your email address will not be published. Required fields are marked *