.NET代码合约：它能比这更基础吗？

Question

.NET代码合约：它能比这更基础吗？

5

我只是在Stack Overflow上回答别人的问题时随便试了一下，但是我注意到我的Visual Studio（2008）内部出现了一个静态验证警告：

string[] source = { "1", "A", "B" };
var sourceObjects = Array.ConvertAll(source, c => new Source(c)).ToArray();

我收到了“需要未经证明的源！= null”的消息。对我来说，这似乎很明显不是这种情况。当然，这只是一个例子。另一方面，一些相当棒的东西似乎运行得相当好。

我正在使用1.2.20518.12版（5月18日发布）。我认为代码合同非常有趣，但其他人是否遇到过类似情况？您是否认为当前实现在实践中可用，还是仅在学术上考虑它们？

我已将此设置为社区wiki，但我想听听一些意见 :)

- Thorarin

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- Jon Skeet · Accepted Answer

如果您将这两个调用拆分开来，那么更有意义：

string[] source = { "1", "A", "B" };
var tmp = Array.ConvertAll(source, c => new Source(c));
var sourceObjects = tmp.ToArray();

现在它将问题指向了最后一行。换句话说，调用Array.ConvertAll知道source不为null，但调用ToArray()时不知道tmp不会为null。

(由于您在源代码中使用名称source，因此您的示例也稍微令人困惑 - 即使您将变量命名为完全不同的名称，错误仍将使用source，因为它是指Enumerable.ToArray中的第一个参数。）

基本上，我认为当Array.ConvertAll获得适当的非null性后置条件时，所有这些都将起作用。在那之前，这样做就可以解决问题：

string[] source = { "1", "A", "B" };
var tmp = Array.ConvertAll(source, c => new Source(c));
Contract.Assume(tmp != null);
var sourceObjects = tmp.ToArray();

我同意这种情况很烦人，但我相信随着微软将越来越多的约束放入BCL中，这种情况会迅速得到改善。需要注意的是，这并不是静态检查器本身的问题。

(事实上，Array.ConvertAll也没有先决条件 - 如果你在上面第二个代码片段中将source变量设置为null，它仍然不会抱怨。)