c# - 代码契约(Contract) : Possibly calling a method on a null reference

Question

我正在与 CodeContracts static analysis tool 争论.

我的代码:

( ASCII version )

该工具告诉我 instance.bar 可能是空引用。我认为恰恰相反。

谁是对的？我如何证明它是错误的？

Answer 1

更新:看来问题是invariants are not supported for static fields .

第二次更新: 下面概述的方法是 currently the recommended solution .

一个可能的解决方法是为 instance 创建一个属性，Ensure 是您想要保存的不变量。 (当然，您需要Assume它们才能证明Ensure。)完成此操作后，您只需使用该属性即可证明所有不变量正确。

这是您使用此方法的示例:

class Foo
{
    private static readonly Foo instance = new Foo();
    private readonly string bar;

    public static Foo Instance
    // workaround for not being able to put invariants on static fields
    {
        get
        {
            Contract.Ensures(Contract.Result<Foo>() != null);
            Contract.Ensures(Contract.Result<Foo>().bar != null);

            Contract.Assume(instance.bar != null);
            return instance;
        }
    }

    public Foo()
    {
        Contract.Ensures(bar != null);
        bar = "Hello world!";
    }

    public static int BarLength()
    {
        Contract.Assert(Instance != null);
        Contract.Assert(Instance.bar != null);
        // both of these are proven ok

        return Instance.bar.Length;
    }
}