Close this search box.

Design by Contract and C# (without Spec#)

After finishing the mini-lecture circuit and my often viewed dive into Spec#, I decided to see if anyone else was working in the Design By Contract (DBC) arena with C#.  Greg Young and I often talk about this subject and various scenarios where it would make sense, and where it wouldn’t.  Hopefully we’ll hear more from the Spec# team shortly about the futures.

It turns out there are two other attempts at what Spec# does, and that’s what I’m going to dive into today.

Back to Basics

So, first, let’s get back to the basics with regard to Design By Contract and what we’re trying to achieve.  Remember back in my Spec# posts, I gave a basic introduction to DBC.  If you want a more complete introduction, check out the Eiffel documentation here which covers the topic in details.  As you may remember, Eiffel was designed with DBC in mind as its key feature.

Back in 2002, Kevin McFarlane submitted an article on CodeProject called Design by Contract Framework to introduce DBC principles into a simple library for basic needs.  This was originally for the 1.0 framework, but could easily be ported if need be.  Currently this project doesn’t use generics or any of the other .NET 2.0+ features.  Anyhow, let’s get into a sample of how it works.

The class that is the heart of the operation is the Check class.  The basic listing, minus overloads, is as follows:

// Contract verifier
public static class Check
     // Preconditions
     public static bool Require(bool assertion) { ... }

     // Postconditions
     public static bool Ensure(bool assertion) { ... }

     // Invariants
     public static bool Invariant(bool assertion) { ... }

     // Assertions
     public static bool Assert(bool assertion) { ... }

// Base contract exception
public class DesignByContractException : Exception { ... }

// Preconditions exception
public class PreconditionException : DesignByContractException { ...}

// Postconditions exception
public class PostconditionException : DesignByContractException { ...}

// Invariants exception
public class InvariantException : DesignByContractException { ...}

// Assertions exception
public class AssertionException : DesignByContractException { ...}

And a simple example using this framework in a CustomerCollection would be as such:

public void Add(Customer value)
     // Check precondition
     Check.Require(value != null);

     // Check for postcondition
     int oldCount = customerList.Count;
     int newCount = customerList.Count;
     Check.Ensure(newCount == oldCount + 1);

As you can see, it’s a pretty simple implementation, but unfortunately, it requires you the developer to think extra hard about putting these things in as well as checking your invariants along the way.  Spec# or C# with the Spec# postcompiler give you that which this does not.  So, at the end of the day, it’s not much more powerful than the Validator Block inside the Enterprise Library.

What this is also missing is one of the vital pieces of DBC which is in regard to inheritance of contracts.  In an earlier post on Spec#, I covered the basics of the following:

  • Preconditions cannot be strengthened or modified
  • Postconditions cannot be weakened, but can be augmented with logical ANDs

Yet Another Approach

What the older solution lacked was using custom attributes to decorate a given class with its contract.  Andrew Matthews has taken another interesting approach in a series of blog posts.  Each one of these is interesting in its own right.

In this series, Andrew is trying to find ways to make C# work with Spec# like attributes.  It’s an interesting concept with all the munging he’s had to do.  So, here’s where he started:

First time around:

[Requires(“arg1 > 10″)]
[Requires(“arg2 < 100″)]
[Ensures(“$after(Prop1) == $before(Prop1) + 1″)]

As you can see, it’s not very type safe, nor really verifiable with the parsing.  So, something else had to be done.  C# as a language cannot accept lambdas and other constructs within custom attributes, so this approach won’t work.

Instead, this is the newer approach with the use of extension methods

public static void Require<T>(this T obj, Expression<Func<T, bool>> pred)
    var x = pred.Compile();
    if (!x(obj))
        throw new ContractException(pred.ToString());

This allows for such verifications as follows:

public void Add(string value)
     this.Require(x => !string.IsNullOrEmpty(value));

Pretty interesting approach, but at the end of the day, is it more verifiable.  Do you have a theorem prover on this?  No, and that’s the unfortunate part.  DBC isn’t as useful until the contract itself is part of the method signature.  So far Spec# has been the only option to do this.

.NET 3.5 Implementation

As you may have noted from my series, Spec# features have already been woven into the .NET framework, in particular System.Core.dll.  Anyhow, the heart of the operation is in the Contract class.  You may note when looking through .NET Reflector, the use of the conditional attribute as follows:


What this particular attribute means is that it’s going to run the Spec# post-processor on the given C# assembly to produce the theorem checks.  This is where the true value of Spec# comes from to be able to tell whether or not I am fulfilling my contract during compile time.  At runtime, it’s less than helpful in that regard.


Some people are doing some interesting things with Design By Contract and trying to shoehorn it into the .NET framework.  Unfortunately, unless tightly integrated with the BCL, I don’t think it’s going to happen.  Spec# is a great tool for this and I certainly hope/expect that it will become further part of the .NET framework in future releases.

On a side note, if you are interested in DBC and Spec#, you may be interested in the ALT.NET Open Spaces, Seattle which I am currently involved in organizing.  Both Greg Young and I will be there and don’t be surprised to find more people interested in it as well for a session.  We hope to open registration soon and I expect it will fill up fast!

kick it on
This article is part of the GWB Archives. Original Author:  Blog Moved to

Related Posts