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

概述我和 CodeContracts static analysis tool有争执. 我的代码： Screenshot http://i40.tinypic.com/r91zq9.png (ASCII version) 该工具告诉我instance.bar可能是一个空引用.我相信相反. 谁是对的？我怎么能证明它错了？ 更新：似乎问题是 invariants are not supported for 我和 CodeContracts static analysis tool有争执.

我的代码：

Screenshot http://i40.tinypic.com/r91zq9.png

(ASCII version)

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

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

解决方法 更新：似乎问题是 invariants are not supported for static fields.

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

可能的解决方法是创建一个属性,例如确保要保留的不变量. (当然,您需要假设它们才能确保被证明.)完成此 *** 作后,您可以使用该属性,并且应该正确地证明所有不变量.

以下是使用此方法的示例：

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;    }}

总结

以上是内存溢出为你收集整理的c# – CodeContracts：可能在空引用上调用方法全部内容，希望文章能够帮你解决c# – CodeContracts：可能在空引用上调用方法所遇到的程序开发问题。

如果觉得内存溢出网站内容还不错，欢迎将内存溢出网站推荐给程序员好友。