Design by contracts and constructors

Question

I am implementing my own ArrayList for school purposes, but to spice up things a bit I'm trying to use C# 4.0 Code Contracts. All was fine until I needed to add Contracts to the constructors. Should I add Contract.Ensures() in the empty parameter constructor?

    public ArrayList(int capacity) {
        Contract.Requires(capacity > 0);
        Contract.Ensures(Size == capacity);

        _array = new T[capacity];
    }

    public ArrayList() : this(32) {
        Contract.Ensures(Size == 32);
    }

I'd say yes, each method should have a well defined contract. On the other hand, why put it if it's just delegating work to the "main" constructor? Logicwise, I wouldn't need to.

The only point I see where it'd be useful to explicitly define the contract in both constructors is if in the future we have Intelisense support for contracts. Would that happen, it'd be useful to be explicit about which contracts each method has, as that'd appear in Intelisense.

Also, are there any books around that go a bit deeper on the principles and usage of Design by Contracts? One thing is having knowledge of the syntax of how to use Contracts in a language (C#, in this case), other is knowing how and when to use it. I read several tutorials and Jon Skeet's C# in Depth article about it, but I'd like to go a bit deeper if possible.

Thanks

Answer 1

I completely disagree with Thomas's answer. As long as you are making choices in the implementation of ArrayList(), you should have a contract for it that document these choices.

Here, you are making the choice of calling the main constructor with argument 32. There are many other things that you could have decided to do (not just concerning the choice of the default size). Giving a contract to ArrayList() that is almost identical to that of ArrayList(int) documents that you decided not to do most of the silly things you could have done instead of calling it directly.

The answer "it calls the main constructor, so let the main constructor's contract do the job" completely ignores the fact that the contract is there to save you from having to look at the implementation. For a verification strategy based on run-time assertion checking, the disadvantage of writing contracts even for such short constructors/methods that almost directly call another constructor/method is that you end up checking things twice. Yes, it seems redundant, but run-time assertion checking is only one verification strategy, and DbC's principles are independent from it. The principle is: if it can be called, it needs a contract to document what it does.

Answer 2

Client code (using Code Contracts) that uses ArrayList won't know that the empty constructor Ensures that Size == 32 unless you explicitly state so using an Ensure.

So (for example):

var x = new ArrayList();
Contract.Assert(x.Size == 32)

will give you the warning "assert not proven".

You need to explicitly state all contracts; the code contracts rewriter/static checker won't "look through" a method to see any implications — see my answer to the related question "Do we have to specify Contract.Requires(…) statements redundantly in delegating methods?"