Eiffel-style Code Contracts for .NET

Design-by-Contract was coined by Bertrand Meyer, the creator of Eiffel as a way for software designers to formally define pre and post conditions as well as object invariants such that the caller can know what to expect when executing code.  

This practice is applied in unit testing when Asserting the result of a function, however until now there have only been work arounds for achieving the same logic in-line; which can now be elegantly expressed like using Code Contracts like so:

public void Deposit(int amount)
    Contract.Requires(amount > 0);
    Contract.Ensures(Balance == Contract.OldValue(Balance) + amount);

    Balance += amount;

Microsoft through its DevLab site has released Code Contracts for .NET, a subset of its ongoing Spec# research project.  This consists offering consist of:

  • a stand-alone library that will in future ship as part of the BCL in .NET 4, 
  • a binary rewriter to support post-condition checking, 
  • and extensions to the Visual Studio 2008 IDE to support static checking after every compile.   

As part of the distribution it includes a number of helpful code snippets such as:

cr Contract.Requires(…);
ce Contract.Ensures(…);
ci Contract.Invariant(…);

Where the Contract.Invariant call is declared within a protected ObjectInvariant method (snippet cim) and defines the state of a property throughout it’s life cycle: 

protected void ObjectInvariant ()
    Contract.Invariant ( f ! = null );

I recommend watching the short channel-9 video for an introduction, or consult the manual for further details.  One feature which is not currently available will be integration with code documentation, which will be very helpful for API developers.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

%d bloggers like this: