Code Contracts [Type]implements interface method {Interface.Method} thus cannot add requires

Question

I have the following scenario:

public interface ISomething
{
    void DoStuff();
    //...
}

public class Something : ISomething
{
    private readonly ISomethingElse _somethingElse;
    //...

    public Something (ISomethingElse somethingElse)
    {
         Contract.Requires(somethingElse != null);
        _somethingElse = somethingElse;
    }

    public void DoStuff()
    {
        // *1* Please look at explanation / question below
        _somethingElse.DoThings();
    }
 }

At line 1 and with the static checker on, I'll get a warning saying that _somethingElse is possibly null, and if I add a contract it will give me the error

[Type]implements interface method {Interface.Method} thus cannot add requires

What's the best thing to do here? Options I see include

1. a guard clause, though it seems a bit extreme
2. a Contract.Assume
3. a hidden third option that I haven't thought of

Please note the field is readonly so after setting the value in the constructor it is not possible to change. Thus, the warning from code contracts seems a bit irrelevant.

Answer 1

Explanation

Section 3: Contract Inheritance of the user manual states that all preconditions must be defined in the root method of an inheritance/implementation chain:

If a client makes sure that they have satisfied the precondition and has a variable o whose static type is T, then the client should not get a precondition violation when they call o.M. This needs to be true even if the runtime value o has type U. Therefore, the method U.M cannot add a precondition that is stronger than the precondition of T.M.

While we could allow a weaker precondition, we have found that the complications of doing so outweigh the benefits. We just haven't seen any compelling examples where weakening the precondition is useful. So we do not allow adding any preconditions at all in a subtype.

As a consequence, method preconditions must be declared on the root method of an inheritance/implementation chain, i.e., the first virtual or abstract method declaration, or the interface method itself.

Solution

In your situation, the best course of action is to set up an invariant stating that the _somethingElse field is never null:

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

This is of course always true, as the field is marked readonly and initialised in the constructor. The static checker isn't able to infer this on its own though, so you must explicitly tell it through that invariant.

You can optionally add a postcondition Contract.Ensures(_somethingElse != null); to your constructor, but the static checker doesn't require it.