代码合同：静态方法中不尊重不变量答案

【问题标题】：Code Contracts: Invariants not respected in static method代码合同：静态方法中不尊重不变量
【发布时间】：2016-10-18 22:11:36
【问题描述】：

我读到过类似的问题：

但我仍然感到困惑的是，这个最小的例子无法静态证明：

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];
    }
}

它给了我以下警告：

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

按照其中一个答案的建议，我尝试了多种方法来实现该只读属性，包括（显式支持字段 + 属性获取），但都没有奏效。

这是一个根本性的交易破坏因素，使我无法利用代码合同的静态验证优势。

我想知道为什么这到底行不通？我怎样才能让它发挥作用？

【问题讨论】：

标签： c# static-analysis code-contracts

【解决方案1】：

这个明确的支持字段 + 属性对我有用。您还需要属性 get 上的 ensure。

    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];
    }
}

【讨论】：