我和
CodeContracts static analysis tool有争执.
我的代码:
Screenshot http://i40.tinypic.com/r91zq9.png
该工具告诉我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; } }
原文地址:https://www.jb51.cc/csharp/99947.html
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。