CodeContracts：可能在空引用上调用方法

Question

我与 CodeContracts 静态分析工具发生争执。

我的代码：

(ASCII 版本)

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

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

Answer 1

更新：问题似乎是静态字段不支持不变量。

第二次更新：下面概述的方法是目前推荐的解决方案。

一种可能的解决方法是为实例创建一个属性，确保是您想要保留的不变量。 （当然，您需要假设它们才能证明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;
    }
}

Answer 2

代码合同是对的。在调用 BarLength() 方法之前，没有什么可以阻止您设置 instance.bar = null。

Answer 3

您的代码包含一个私有静态初始化实例：

private static Foo instance = new Foo();

您是否假设这意味着实例构造函数将始终在访问任何静态方法之前运行，从而确保bar已初始化？

在单线程的情况下，我认为你是对的。

事件顺序为：

1. 调用 Foo.BarLength()
2. 类 Foo 的静态初始化（如果尚未完成）
3. 私有静态成员 instance< 的静态初始化/code> 与 Foo 实例
4. 进入 Foo.BarLength()

但是，每个应用程序域仅触发类的静态初始化一次 - 并且 IIRC 不会阻塞确保在调用任何其他静态方法之前它已完成。

因此，您可能会遇到以下情况：

1. Thread Alpha：调用 Foo.BarLength()
2. Thread Alpha：类 Foo 的静态初始化（如果尚未完成）开始
3. 上下文切换
4. 线程 Beta：调用 Foo.BarLength()
5. 线程 Beta：不调用类 Foo 的静态初始化，因为那是已经进行
6. 线程 Beta：进入 Foo.BarLength()
7. 线程 Beta：访问 null 静态成员 instance

合约分析器无法知道您永远不会以多线程方式运行代码，因此必须谨慎行事。

Answer 4

如果将字段“bar”标记为只读，则应该满足静态分析器的要求，即在构造函数执行后该字段永远不会被设置为其他任何内容。

Answer 5

我同意你的看法。 instance 和 bar 都是私有的，因此 CodeContracts 应该能够知道 instance.bar 永远不会设置为 null。