Code contracts - Not correctly warning about readonly members?

Question

Given this class, I"m not sure why I get the Ensure unproven Result != null warning.

public class MyClass {
  private readonly string _value;

  public MyClass(string value) {
    Contract.Requires(value != null);  
    _value = value;
  }

  public string Value {
    get {
      Contract.Ensures(Contract.Result<string>() != null);
      return _value;
    }
  }
}

I can make the warning go away by adding an Invariant that _value != null, but it feels like I shouldn't have to. Is this just a limitation of the analysis?

EDIT: Adding a bit more to the question, as I think the point of my question is being missed.

public class Test {
    private string _value = "";

    public string Value {
        get {
            Contract.Ensures(Contract.Result<string>() != null);
            return _value;
        }
        set {
            Contract.Requires<ArgumentNullException>(value != null);
            _value = value;
        }
    }
}

The CC analysis seems perfectly happy with this class; a non-null value is assigned in the ctor, and the setter Requires non-null values to change _value thus Ensures is proven.

Answer 1

Your constructor does not promise that _value will be non-null. It sets _value to value, which is non-null, but that's an implementation detail, not part of the contract. Even if it were part of the contract, it wouldn't be enough, because all pre- and postconditions should remain equally valid when you add another constructor that doesn't make that same promise.

You should add the invariant that _value != null. Why does it feel like you shouldn't have to?

Edit: as an alternative, you could try adding an invariant that Value != null (which would also be useful outside of MyClass), and make Value's property getter ensure that Contract.Result<string>() == _value (merely to prove the invariant), but I'm not sure that would work.

Answer 2

Not sure the option was available when the question was asked, but I ran into a similar issue today and found that by turning on the Code Contracts option "Infer Invariants for readonly" the warning went away.