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?