CodeContracts：可能在空引用上调用方法
我正在使用CodeContracts静态分析工具 。
我的代码：
截图http://sofzh.miximages.com/c%23/r91zq9.png
（ ASCII版 ）
该工具告诉我instance.bar可能是一个空引用。 我相信相反。
谁是对的？ 我怎么能certificate它错了？
更新 ：似乎问题是静态字段不支持不变量 。
第二次更新： 目前推荐的解决方案是下面列出的方法。
一种可能的解决方法是创建一个属性， instance Ensure要保留的不变量。 （当然，您需要Assume它们才能Ensure被certificate。）完成此操作后，您可以使用该属性，并且应该正确地certificate所有不变量。
以下是使用此方法的示例：
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() != null); Contract.Ensures(Contract.Result ().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; } }
CodeContracts是对的。 在调用BarLength()方法之前，没有什么可以阻止您设置instance.bar = null 。
您的代码包含一个私有静态初始化实例：
private static Foo instance = new Foo();
您是否认为这意味着实例构造函数将始终在访问任何静态方法之前运行，因此确保bar已初始化？
在单线程的情况下，我认为你是对的。
事件的顺序是：
- 打电话给
Foo.BarLength() - 类
Foo静态初始化（如果尚未完成） - 使用
Fooinstance静态初始化私有静态成员instance - 进入
Foo.BarLength()
但是，每个App Domain只会触发一次类的静态初始化 – 而IIRC没有阻塞来确保在调用任何其他静态方法之前完成它。
所以，你可以有这样的场景：
- 线程Alpha：调用
Foo.BarLength() - 线程Alpha：类
Foo静态初始化（如果尚未完成）启动 - 上下文切换
- 线程测试版：调用
Foo.BarLength() - Thread Beta： No调用类
Foo静态初始化，因为它已经在进行中 - 线程测试版：进入
Foo.BarLength() - Thread Beta：访问
null静态成员instance
Contracts分析器无法知道你永远不会以multithreading的方式运行代码，所以它必须谨慎行事。
如果您将字段“bar”标记为只读，则应该满足静态分析器的要求，该字段在ctor执行后永远不会被设置为其他任何内容。
我同意你的看法。 instance和bar都是私有的，因此CodeContracts应该能够知道instance.bar永远不会设置为null。