.NET代码契约:它能比这更基本吗？

Question

当我在Visual Studio(2008)内部注意到静态验证警告时,我只是在Stack Overflow上回答某人的问题:

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知道源不是null,但调用ToArray()不知道tmp不会为null.

(由于source在源代码中使用了名称,您的示例也有点混乱- source即使您将变量调用完全不同,错误仍然会使用,因为它指的是第一个参数Enumerable.ToArray.)

基本上我相信当Array.ConvertAll获得适当的非nullity后置条件时,这一切都会起作用.在那之前,这将做到这一点:

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,它仍然不会抱怨.)