.NET code contracts: can it get more basic than this?

Question

I was just messing around to answer someone's question here on Stack Overflow, when I noticed a static verification warning from inside my Visual Studio (2008):

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

I'm getting the message requires unproven source != null. It seems pretty obvious to me that this is not the case. This is just one example of course. On the other side, some pretty nifty stuff seems to be working fairly well.

I'm using the 1.2.20518.12 release (May 18th). I find code contracts very interesting, but has anyone else had cases like this? Do you consider the current implementation usable in practice, or would you consider them purely academic at this point?

I've made this a community wiki, but I'd like to hear some opinions :)

Answer 1

It makes more sense if you split the two calls up:

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

Now it points to the last line as the problem. In other words, the call to Array.ConvertAll knows that source isn't null, but the call to ToArray() doesn't know that tmp won't be null.

(Your example is also slightly confusing due to the use of the name source in your source code - the error would still use source even if you'd called your variable something completely different, as it's referring to the first parameter in Enumerable.ToArray.)

Basically I believe this would all work when Array.ConvertAll gets an appropriate non-nullity postcondition. Until then, this will do the trick:

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

I agree this kind of thing is annoying, but I'm sure it will improve rapidly as MS adds more and more contracts into the BCL. It's important to note that it's not a problem with the static checker itself.

(In fact, Array.ConvertAll doesn't have a precondition either - if you set the source variable to null in the second code snippet above, it still wouldn't complain.)