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

dtb*_*dtb 7 c# .net-4.0 visual-studio-2010 code-contracts

我正在使用CodeContracts静态分析工具.

我的代码:

截图http://i40.tinypic.com/r91zq9.png

(ASCII版)

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

谁是对的?我怎么能证明它错了?

por*_*ges 2

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

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

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;
    }
}
Run Code Online (Sandbox Code Playgroud)