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

Question

我正在与CodeContracts 静态分析工具争论。

我的代码：

（ASCII 版本）

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

谁是对的？我怎样才能证明它是错的？

Answer 1

CodeContracts 是对的。在调用该方法instance.bar = null之前，没有什么可以阻止您进行设置。BarLength()

Answer 2

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

private static Foo instance = new Foo();

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

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

事件的顺序是：

1. 拨电至Foo.BarLength()
2. 类的静态初始化Foo（如果尚未完成）
3. instance具有实例的私有静态成员的静态初始化Foo
4. 进入Foo.BarLength()

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

因此，您可能会遇到这种情况：

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

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

Answer 3

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

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

一种可能的解决方法是为您要保留的不变量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;
    }
}

Answer 4

如果您将字段'bar'标记为只读，那应该满足静态分析器，即在ctor执行后该字段永远不会设置为其他任何内容。

Answer 5

我同意你的看法。 instance并且bar都是私有的，所以 CodeContracts 应该能够知道instance.bar它永远不会设置为 null。