Blog Moved to http://podwysocki.codebetter.com/

Blog Moved to http://podwysocki.codebetter.com/
posts - 277 , comments - 156 , trackbacks - 27

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;
     customerList.Add(value);
     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:

[Pure, Conditional("USE_SPECSHARP_ASSEMBLY_REWRITER")]

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.

Conclusion

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 DotNetKicks.com

Print | posted on Tuesday, January 22, 2008 12:58 AM | Filed Under [ Spec# ]

Feedback

Gravatar

# re: Design by Contract and C# (without Spec#)

Hi Matthew,

Yes, it's a shame I wasn't able to find a nice solution yet! As I see it (and given the fact that I'm aiming for Eiffel-like functionality rather than static analysis of contracts ATM) the major flaw in my current implementation is the lack of heritability. That's why I tried so many different ways to force my implementation into .NET Attributes. The current implementation is kind-of declarative, but it doesn't accumulate and truly enforce the constraints on an interface, so it lacks what I thought was the real power of 'embedded' DBC (i.e. contract enforcement coming from the framework rather than from the diligence of the developer).

No dice so far, sadly, and spec# features may be found in mainstream C# before I find a way to solve the problem elegantly. At the rate that MS drip-feeds technology to the industry, this could be years away. And I can't imagine many of my customers endorsing the use of research languages in their production code. So I guess the search will continue.

Keep fighting the good fight.

Andrew
1/22/2008 5:24 AM | Andrew Matthews
Gravatar

# re: Design by Contract and C# (without Spec#)

Andrew,

Unfortunately, unless we have some hooks into the BCL, I don't think it's easily going to happen, unless you have something like Spec# which includes the assembly rewriter and a theorem prover at compile time.

My real point of contention is that you lose a lot of the DBC constructs by not having them as part of the signature, therefore it's still guesswork and piling through the code to find it. I don't think with the current features of C#, we can make an elegant solution at this point and make it transparent to the caller and the callee about the contract.

Yes, lack of inheritance is a big flaw and unfortunately not an easy one to get around. I do wish though that they did expand Attributes for the next go around to make them a bit more powerful, and use generics in them as well. I hope that's one of the new features.

With regards to Spec#, I'm encouraged that it made it into the System.Core.dll, albeit internally. With release cycles coming every year now it seems with new .NET libraries, I don't think it's too far off as you think. Hopefully there will be some sort of announcement soon about it.
1/22/2008 11:38 AM | Matthew Podwysocki
Gravatar

# re: Design by Contract and C# (without Spec#)

You might want to try this one:

http://www.codeproject.com/KB/cs/LinFu_Part5.aspx

It's language independent, contracts can be inherited, and preconditions are weakened while postconditions are strengthened. Take a look :)
1/27/2008 9:30 AM | Philip Laureano
Gravatar

# re: Design by Contract and C# (without Spec#)

Ok, thanks, I will check it out and post about it shortly.

Matt
1/28/2008 8:19 AM | Matthew Podwysocki
Gravatar

# re: Design by Contract and C# (without Spec#)

Hi,

There is another solution using Proxies and interception. The Linfu framework tacles dbc amongst other things...check this article on the subject http://www.codeproject.com/KB/cs/LinFu_Part5.aspx
2/15/2008 6:54 AM | Stuart C
Gravatar

# re: Design by Contract and C# (without Spec#)

Stuart C,

Did you see the link above given to me by the author of that article? Anyhow, I followed up on that article here: http://geekswithblogs.net/Podwysocki/archive/2008/01/31/119165.aspx
2/15/2008 10:09 AM | Matthew Podwysocki
Post A Comment
Title:
Name:
Email:
Comment:
Verification:
 
 

Powered by: