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

Question

Hi there

this is my 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 explanaition / question below
        _somethingElse.DoThings();
    }

 }

So, if in 1 and with the static checker on, I ll get a warning saying that _somethignElse is possibly null, if I add a contract it will give me the error

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

So whats the best thign to do here options I see

1) a guard clause , tho it seems a bit extreme 2) a Contract.Assume 3) hidden third option that I havent thought of

Please note the field is readonly so ,actually after i set teh value in ctor is not possible to change so I see the warning from code contracts 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.