Code Contracts: Do we have to specify Contract.Requires(…) statements redundantly in delegating methods?

Question

I'm intending to use the new .NET 4 Code Contracts feature for future development. This made me wonder if we have to specify equivalent Contract.Requires(...) statements redundantly in a chain of methods.

I think a code example is worth a thousand words:

    public bool CrushGodzilla(string weapon, int velocity)
    {
        Contract.Requires(weapon != null);

        // long code

        return false;
    }

    public bool CrushGodzilla(string weapon)
    {
        Contract.Requires(weapon != null);   // specify contract requirement here
                                             // as well???

        return this.CrushGodzilla(weapon, int.MaxValue);
    }

For runtime checking it doesn't matter much, as we will eventually always hit the requirement check, and we will get an error if it fails.

However, is it considered bad practice when we don't specify the contract requirement here in the second overload again?

Also, there will be the feature of compile time checking, and possibly also design time checking of code contracts. It seems it's not yet available for C# in Visual Studio 2010, but I think there are some languages like Spec# that already do. These engines will probably give us hints when we write code to call such a method and our argument currently can or will be null.

So I wonder if these engines will always analyze a call stack until they find a method with a contract that is currently not satisfied?

Furthermore, here I learned about the difference between Contract.Requires(...) and Contract.Assume(...). I suppose that difference is also to consider in the context of this question then?

Answer 1

I think it would be best practice to specify all the contracts on each of the public methods. A contract is more than just "what gets checked" - it's documentation too, effectively. If you call a method but don't know what contract is applied, it would be odd to get a contract failure lower down: that would suggest a bug in the method that you're calling, rather than in your method.

Note that if you're using C# 4 throughout your project, you could consider using optional parameters and named arguments to avoid having so many overloads. That's not useful if you need to call the code from a language which doesn't support them, of course.

I strongly suspect that if you don't specify the contract in the "defaulting" overload, the static checker (which is now available for all versions of VS2010) will complain that the contract might fail, and will also suggest adding the contract in.

Answer 2

Also, there will be the feature of compile time checking, and possibly also design time checking of code contracts. It seems it's not yet available for C# in Visual Studio 2010...

It is available, but for it to work you have to be using VS2010 Ultimate edition.

Warning: This is a bit speculative, but it seems to be correct from what I've learned using it;

You need to propagate the constraints through your methods manually, like you have done.

The only information that Code Contracts can see from the outside of a method is what you tell it. It can examine assumptions and assertions inside a method, but this analysis does not propagate. In other words, CC cannot "see through" your methods, so it doesn't automatically know that CrushGodzilla(string) will require weapon to be non-null.

If using static analysis, it will perform checks in CrushGodzilla(string) and realize that weapon cannot be null, using the external information about CrushGodzilla(string,int), and it will suggest that you add a Requires non-null precondition. (The non-propagation is the fact that this knowledge won't be used to analyse the rest of the program.)

I haven't actually found anywhere that documents that static analyzer very well, despite having looked.