Contrats de code .NET: peut-il être plus basique que cela?

Question

Je viens de déconner pour répondre à la question de quelqu'un ici débordement de la pile, lorsque j'ai remarqué un avertissement de vérification statique de l'intérieur de mon Visual Studio (2008):

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

Je reçois le message nécessite la source non prouvée! = null. Il me semble assez évident que ce n'est pas le cas. Ce n'est qu'un exemple bien sûr. D'un autre côté, des trucs assez chouettes semblent fonctionner assez bien. J'utilise la version 1.2.20518.12 du 18 mai. Je trouve les contrats de code très intéressants, mais quelqu'un d'autre a-t-il eu des cas comme celui-ci? Considérez-vous la mise en œuvre actuelle utilisable dans la pratique, ou considérez-vous qu'ils sont purement académiques à ce stade?

J'ai fait ce wiki communautaire, mais j'aimerais entendre des opinions :)

Answer 1

Il est plus logique si vous divisez les deux appels jusqu'à:

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

Maintenant, il pointe à la dernière ligne comme le problème. En d'autres termes, l'appel à Array.ConvertAll sait que la source n'est pas nulle, mais l'appel à ToArray() ne sait pas que tmp ne sera pas nul.

(Votre exemple est également légèrement déroutant en raison de l'utilisation du nom source dans votre code source - l'erreur utiliserait toujours source même si vous aviez appelé votre variable quelque chose de complètement différent, car il fait référence au premier paramètre de .)

Fondamentalement, je crois que tout cela fonctionnerait quand Array.ConvertAll obtient une postcondition non-nullité appropriée. Jusque-là, cela fera l'affaire:

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

Je suis d'accord ce genre de chose est ennuyeux, mais je suis sûr que cela améliorera rapidement que MS ajoute de plus en plus de contrats dans le BCL. Il est important de noter que c'est pas un problème avec le vérificateur statique lui-même.

(En fait, Array.ConvertAll n'a pas une condition préalable soit - si vous définissez la variable source à null dans le second extrait de code ci-dessus, il ne serait quand même pas se plaindre.)