Geeks With Blogs
Blog Moved to Blog Moved to
In a previous post, I talked about various attempts at frameworks that are trying to do Design By Contract (DBC) in .NET.  Many simply just come across as simple validation frameworks without the heart of DBC which is the contract.  Where is the contract?  Well, dig through my code and find out!  It's something that I've been harping on time and time again is that without transparency to the caller and callee of the contract, it's just another validation framework.  You'll hear either myself or Greg Young on that, I'm sure.

The only approach that has worked so far has been Spec# in the .NET world.  Unfortunately, still a research product, isn't available for us to use commercially.  So, until that time in which it is thoroughly weaved into the .NET framework as a whole outside of the internals of System.Core.dll, we have to look at alternatives.


Before we look at another framework, I just want to walk you through a sample of the original DBC language, Eiffel.  This gives you an idea what I'm talking about.

my_list.do_all (agent (s: STRING)
         not_void: s /= Void
         s.append_character (',')
         appended: s.count = old s.count + 1

As you can see, it's clearly stated as part of the language what the requirements are, and what its return will be.  That's the really slick part about it that we don't have unless we go to Eiffel.NET, but it's not using the latest and greatest .NET APIs, so it's pretty much a nonstarter.  So, let's look at yet another framework.

LinFu DesignByContract

Philip Laureano, who has done a lot with LinFu including Aspect Oriented Programming (AOP) among other things has taken a stab at DBC for all .NET languages and not just C# which Spec# has done.  He posted the LinFu.DesignByContract2 article on CodeProject that is well worth checking out. 

Earlier, he posted one about the LinFu framework on CodeProject as well which includes the following:
  • A simple IoC container
  • Design by Contract framework
  • Dynamic Proxy
  • Reflection (Mixins, Duck Typing and Multiple Dispatch)
  • Delegates with lambdas for universal event handling
But, let's get back to the DBC part, you'll remember the basic tenets of the philosophy:
  • What do we expect?
  • What do we return?
  • What do we maintain?
We also throw in a few Eiffel constructs in terms of inheritance which are also quite important.  And they are:
  • The precondition may only be weakened by inheritance
  • The postcondition can only be strengthened by inheritance
Well, enough about the basics, let's look at the framework itself.  Let's first look at a simple sample I whipped up:

public class StringCollection
   private int count;
   string[] strings = new string[5];

   public virtual void Add([NotNull] string value)
        // NotNull doing
        // Debug.Assert(!string.IsNullOrEmpty(value));

        // Add value and redefine   

        // EnsureCountIncremened 
        // Debug.Assert(count == count + 1);       

So, what you see here is that I put a postcondition making sure that the count is incremented by one as I'm adding a string to my array.  Also, I have the precondition that my string value is not null.  But, how does that work?

In order to do that we need to implement a few interfaces.  Let's look at the one for preconditions.

public interface IMethodContract
    IList<IPrecondition> Preconditions { get; }
    IList<IPostcondition> Postconditions { get; }

public interface IPrecondition : IMethodContractCheck
    bool Check(object target, InvocationInfo info);
    void ShowError(TextWriter output, object target, InvocationInfo info);

Ok, so now, I need to implement that somehow for my custom attribute.  That would look similar to this:

public sealed class NotNullAttribute : Attribute, IPrecondition
     public bool Check(object target, InvocationInfo info)
          string value = target as string;
               return true;

     public void ShowError(TextWriter output, object target, InvocationInfo info)
          output.WriteLine("string value cannot be null or blank");

     public bool AppliesTo(object target, InvocationInfo info)
          return target is string;

     public void Catch(Exception ex)


So, it's pretty interesting and clever how this is being done.  But still without the static checking of Boogie and so on, it still falls well short of real DBC. 

For those interested in postconditions and invariants, those are also supported through the interfaces as shown below:

public interface IPostcondition : IMethodContractCheck
    void BeforeMethodCall(object target, InvocationInfo info);
    bool Check(object target, InvocationInfo info, object returnValue);
    void ShowError(TextWriter output, object target, InvocationInfo info,
        object returnValue);

public interface IInvariant : IContractCheck
    bool Check(object target, InvocationInfo info, InvariantState callState);
    void ShowError(TextWriter output, object target, InvocationInfo info,
        InvariantState callState);

So, as I said, quite interesting and clever the way of handling the DBC concepts through interfaces.  The libraries were also written to support the Eiffel constructs of inheritance.  So, very well written I must admit.


I just began to scratch the surface with what you can do with this framework and it's very well written.  But, still at the end of the day, it's not statically checked through a Boogie and a theorem prover to ensure the contracts hold.  That's the crucial part missing in this equation.  I'm sure more will come to mind on the subject.  Until next time...

kick it on Posted on Thursday, January 31, 2008 7:32 PM Spec# | Back to top

Comments on this post: Design by Contract Revisited with C# and .NET

# re: Design by Contract Revisited with C# and .NET
Requesting Gravatar...
This is where you and I differ on Spec# Matt - I prefer DBC that's testable/enforceable outside of a verifying compiler. What would be really nice is if the Spec# team would leverage Boogie to provide assertable contract verification so that I can both assert the contract exists, and assert that the contract conditions are verifiably not violodated. With a verifying compiler, it's just too easy for another dev to modify the contract and what's the point of DBC if I have to write tests to cover the boundary conditions of the contract explicitly?

LinFu looks promising - I should take a look at it.

Still wishing for assertable contracts
- Phil
Left by Phil McMillan on Feb 04, 2008 12:47 PM

Your comment:
 (will show your gravatar)

Copyright © Matthew Podwysocki | Powered by: