.NET 代码契约：还有比这更基础的吗？

Question

我只是在 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 日）。 我发现代码合约非常有趣，但是其他人有这样的案例吗？ 您认为当前的实现在实践中可用，还是认为它们目前纯粹是学术性的？

我已将其设为社区维基，但我想听听一些意见:)

Answer 1

如果您将这两个调用分开，则更有意义：

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

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

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

基本上，我相信当 Array.ConvertAll 获得适当的非空后置条件时，这一切都会起作用。 在那之前，这会起作用：

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

我同意这种事情很烦人，但我相信随着 MS 在 BCL 中添加越来越多的合同，它会迅速改善。 需要注意的是，这不是静态检查器本身的问题。

（事实上​​，Array.ConvertAll 也没有前提条件 - 如果您在上面的第二个代码片段中将 source 变量设置为 null，它仍然不会抱怨.)