Really trying to like CodeContracts in C#

Question

I am finally playing catchup with everything new that has been added in to the .NET 3.5/4.0 Frameworks. The last few days I have been working with CodeContracts and I am really trying hard to like them. I am curious what other people think of the implementation of CodeContracts in C#? Specifically, how are people organizing things like Contract classes for interfaces, contract methods for Contract Invariants etc?

I like the validation that contracts provide, at first glance they look great. With a few simple lines I can get some nice build checking before I even run my code. Unfortunately, I am having a hard time getting over the feeling that the way that code contracts are implement in C#, they are cluttering up my code more than they are documenting contracts. And to take full advantage of contracts, I am littering my code with assumptions and asserts etc (which I know some will say is a good thing); but as some of my examples below will show, it turns a single simple line in to 4 or 5 lines, and doesn't really add sufficient value in my opinion over alternative approaches (i.e., asserts, exceptions etc).

Currently, my greatest frustrations are:

Interface Contracts:

[ContractClass(typeof(IInterfaceContract))]
  public interface IInterface
  {
    Object Method(Object arg);
  }

  [ContractClassFor(typeof(IInterface))]
  internal abstract class IInterfaceContract
  {
    private IInterfaceContract() { }

    Object IInterface.Method(Object arg)
    {
      Contract.Requires(arg != null);
      Contract.Ensures(Contract.Result<Object>() != null);
      return default(Object);
    }
  }

This feels like such a cludge to me, I wish there was a cleaner way to document requirements, either via attributes or some form of built in language support. The fact that I have to implement an abstract class that implements my interface, just so I can specify the contract seems tedious at best.

Code Bloat:

typeof(Action<>).MakeGenericType(typeof(Object);

Requires several assumptions just to verify information that is readily available. I appreciate that all the analyzer knows is that it is operating on Type and thus must work on that limited knowledge, but it still frustrates me that a single line of code requires me to re-write as

var genericAction = typeof(Action<>);

Contract.Assume(genericAction.IsGenericType);
Contract.Assume(genericAction.GetGenericArguments().Length == 1);

genericAction.MakeGenericType(typeof(Object));

Just to keep things documented (yes I know I can use ContractVerificationAttribute to turn this off for a method/class etc, or SuppressMessageAttribbute to target specific messages, but that seems to defeat the purpose as your code would quickly become littered with suppressions etc.

In addition, taking a case like

  public class MyClass
    : IInterface
  {
    private readonly Object _obj;

    public Object Property
    {
      get
      {
        Contract.Ensures(Contract.Result<Object>() != null);
        return _obj;
      }
    }

    public MyClass(Object obj)
    {
      Contract.Requires(obj != null);

      _obj = obj;
    }
  }

obj is required to be not null, and is set to a readonly field that cannot be changed, yet I am still required to add a "markup" method to my class so that my property requirement to not return null can be proven:

[ContractInvariantMethod]
private void ObjectInvariant()
{
  Contract.Invariant(_obj != null);
}

There is more, but I figured I have probably ranted enough, and I would really appreciate the insight of people much smarter than me to help me "like" Code Contracts and make this feeling of code clutter go away. Any insight on how to better structure code, workaround wonkiness issues etc would be greatly appreciated.

Thanks!

Answer 1

This feels like such a cludge to me, I wish there was a cleaner way to document requirements, either via attributes or some form of built in language support.

The CC team have stated that using Attributes just isn't powerful enough, because you can't include things like lambdas in them. They could include things like [NotNull] but have chosen not to do so because they're trying to keep CC as general as possible.

One reason that CC is a library (rather than part of an extended C#) is that it is supported across all .NET languages.

You can read more about the team's reasoning here.

In terms of actually using this, so far I've just been keeping my interface contracts in the same file as the interface, which means it's all documented in the same place. It is something that should be improved upon :)

Code Bloat [...]

Your second complaint is probably something that can be implemented -- I'd suggest posting it on the code contracts forum. (EDIT: Seems someone already has, but no answers yet.)

However, it will always be the case that under-specified contracts will need more assumptions surrounding them. If you run into a case like this in the .NET framework you can request that contracts be added in the Missing Contracts on Libraries thread.

In addition, taking a case like [...]

This has been addressed. If you have an auto-property, you just have to add an non-null invariant and the pre-/post-conditions will be generated:

public class MyClass : IInterface
{
    private Object Property { get; set; }

    [ContractInvariantMethod]
    private void Invariants()
    {
        Contract.Invariant(Property != null);
    }
}

You'll probably end up with other invariants for your classes anyway, so it's not that big a deal.