Alexander Beletsky's development blog

My profession is engineering

AgileBaseCamp Kiev 2011: Dmitry Mindra: Design by Contract in .NET

Disclaimer: text below is compilation of notes I made on AgileBaseCamp 2011 conference, listening to different speakers. I do it to keep knowledge I got on conference, share it with my colleagues and anyone else who interested. It is only about how I heard, interpret, write down the original speech. It also includes my subjective opinion on some topics. So it could not 100% reflects author opinion and original ideas.

Dmitry Mindra prepared very nice speech dedicated to Code Contracts. He opens ideas what the Code Contacts are and more important how to “Design by contract”. This speech has been especially interested to me, since I never heard/used such type of design.

Design by contract in short

Desing by contracts has been introduced by Bertrand Mayer. He is one of original creator of Eiffel language. No surprise that first time contract’s have been added in Eiffel. The contract consists on 3 parts: Preconditions/Postconditions/Invariants.

  • Preconditions - check that client does everything OK
  • Postconditions - check that server does everything OK
  • Invariant - check that state of object valid for next call

In Eiffel you have special sections in each method called (require, do, post) there it is possible to put contract definition.

By specifying the contract we specify exact constraints for code. Typically methods have some input parameters and return some results to outside world. For instance we have class Account with method Withdraw, we are expecting that argument that Withdraw receives are always positive and return results also is greater than zero.

Wait, I can already specify contract with my beloved exceptions

Many of us, get used to write such code..

public Amount Withdraw(Amount amountToWithdraw)
{
 if (amountToWithdraw == null)
 {
  throw new ArgumentException("amountToWithdraw");
 }
 
 if (amountToWithdraw.Value <= 0)
 {
  throw new ArgumentException("amountToWithdraw.Value");
 }
 
 var result = //.. calculate operation here.. ;
 
 if (result.Value <= 0)
 {
  throw new AccountOperationException();
 }
 
 return result;
}

It is definitely the way of creation robust application (in case of all those conditions are tested and client code properly handles exceptions). But is has several drawbacks:

  • It is only run-time mechanism
  • It is not possible to turn on or turn off the exceptions
  • This type of contract is “method-wide”, but how can you specify “class-wide” contract?
  • All of if / throw statements are “code-garbage” that make it difficult to read

What we have in .NET?

The Common Language Runtime (CLR) team is introducing a library to allow programming with contracts in the Microsoft .NET Framework 4. Adding them as a library allows all .NET languages to take advantage of contracts. This is different from Eiffel or Spec#, a language from Microsoft Research (research.microsoft.com/en-us/projects/specsharp/), where the contracts are baked into the language. Code Contracts System in .NET consists of 4 parts:

  • System.Diagnostics.Contracts contract library where Contract class is defined.
  • ccrewrite.exe tool that modifies the Microsoft Intermediate Language (MSIL) instructions of an assembly to place the contract checks where they belong.
  • cccheck.exe contract static checker, that examines code without executing it and tries to prove that all of the contracts are satisfied.
  • ccrefgen.exe which will create separate contract reference assemblies that contain only the contracts.

Why is it useful?

Let’s rewrote the previous example with code contracts:

public Amount Withdraw(Amount amountToWithdraw)
{
 // preconditions..
 Contract.Requires<NullReferenceException>(amountToWithdraw);
 Contract.Requires(amountToWithdraw.Value);

 // action
 var result = //.. calculate operation here.. ;
 
 // postconditions 
 Contract.Ensures(result.Value <= 0);
 
 return result;
}

I like the style, because this code a little reminds me TDD AAA (arrange/act/assert) pattern, code side is smaller and we are getting benefits of .NET Code Contracts.

What benefits here?

  • Static code analysis - during the compilation code is checked for contracts, if somewhere I wrote account.Withdraw(null) it would be immediately caught by cccheck.exe
  • Runtime execution - if error is missed on compilation time, it would be caught on run time and proper exception is thrown
  • I could configure to include or exclude contracts check at final assembly

Ok, I want to use it

To have a full support of Code Contracts you have to have .NET framework 4.0 and Visual Studio Premium or Ultimate. So, Code contracts are pretty expensive stuff. As far as I get from Dmitry speech it is possible to use System.Diagnostics.Contracts but limited capabilities are enabled only.

So, contract are great for building Life-critical and High-robust application where the quality / cost ratio makes sense for you.

Materials