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

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?"

Answer 2

Design by contract comes from the mathematical roots of functional programming: Preconditions and Postconditions.

You don't really need a book on it, it's at most a chapter of a Computer Science degree (most will teach the concept). The basic premise is you write the preconditions that the function expects and the output it will produce given the correct parameters. The function will not be expected to work with incorrect initial parameters. The same can be said for an algorithm: it's infallible, that is it's guaranteed to provide the expected result.

That's how I've been taught it in the degree I'm currently studying, there may be better definitions around though. The Wikipedia article on Design by contract is written with an OO slant, but pre/postconditions are language independent.

Answer 3

Umh, I don't fully understand why you put the 'Ensures' also in the default c'tor. Because it calls the main c'tor, which already does implement the full contract, the default c'tor does that as well - by definition. So this is a logical redundancy, and therefore a big 'Don't'. Maybe it could have pragmatic implications, like you say - don't know Code Contracts that good...

Regarding literature - the best sources are:

• Design By Contract, by Example (Book, Addison-Wesley)
• Wikipedia article on the issue
• An introduction to Design by Contract (Eiffel series, but the DbC principles are not language-specific)

HTH! Thomas

Answer 4

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 5

I recommend reading Object Oriented Software Construction, 2nd Edition, or maybe Touch of Class, both from Bertrand Meyer. Alternatively, you could read the 1992 article Applying "Design by Contract" from the same author.

To summarize:

• The class invariant must hold after the constructor (any of them) finishes, and before and after any public method of the class is executed.
• Method preconditions and postconditions are additional conditions which must hold on entering and exiting any public method, along with the invariant.

So in your case, focus in the invariant. Produce a correct object (one which satisfies the class invariant), no matter which constructor is invoked.

In this related answer I discussed similar topics, including an example.