Code Contracts: Invariants not respected in static method

Question

I read about similar questions:

• Code Contracts: Ensure unproven on string method
• Code Contracts: Why are some invariants not considered outside the class?

but it still baffles me that this minimal example cannot be statically proved:

public class Example
{
    private const string s = "123";

    public int A { get; }

    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(A >= 0);
        Contract.Invariant(A < 3);
    }

    public Example(int a)
    {
        Contract.Requires(a >= 0);
        Contract.Requires(a < 3);

        this.A = a;
    }

    public static char Test(Example x)
    {
        Contract.Requires(x != null);
        return s[x.A];
    }
}

It gives me the following warnings:

CodeContracts: Missing precondition in an externally visible method. Consider adding Contract.Requires(0 <= x.A); for parameter validation
CodeContracts: Missing precondition in an externally visible method. Consider adding Contract.Requires(x.A < 3); for parameter validation

I tried many ways to implement that readonly property including (explicit backing field + property get) as suggested in one of the answers, but none worked.

This is a fundamental deal-breaker preventing me from taking advantage of static verification benefits of Code Contracts.

I wonder why on earth does this not work? How can I make it work?

Answer 1

This explicit backing field + property get worked for me. You also need the ensures on the property get.

    public class Example
{
    private const string S = "123";
    readonly int a;

    public int A
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() < 3);
            Contract.Ensures(Contract.Result<int>() >= 0);

            return a;
        }
    }

    [ContractInvariantMethod]
    private void ObjectInvariant()
    {
        Contract.Invariant(a >= 0);
        Contract.Invariant(a < 3);
    }

    public Example(int a)
    {
        Contract.Requires(a >= 0);
        Contract.Requires(a < 3);

        this.a = a;
    }

    public static char Test(Example x)
    {
        Contract.Requires(x != null);
        return S[x.A];
    }
}