.NET-Code-Verträge: Kann es einfacher als das werden?

Question

ich um nur war in Unordnung jemandes Frage hier auf Stack-Überlauf zu beantworten, wenn ich eine statische Überprüfung Warnung aus meinem Visual Studio (2008) bemerkt:

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

Ich erhalte die Nachricht erfordert unbewiesene Quelle! = null. Es scheint mir ziemlich offensichtlich, dass dies nicht der Fall ist. Dies ist nur ein Beispiel. Auf der anderen Seite scheint etwas ziemlich nettes Zeug ziemlich gut zu funktionieren.

Ich benutze die Version 1.2.20518.12 (18. Mai). Ich finde Code-Verträge sehr interessant, aber hat jemand sonst solche Fälle? Halten Sie die aktuelle Implementierung in der Praxis für sinnvoll oder halten Sie sie an dieser Stelle für rein akademisch?

Ich habe dies ein Community Wiki, gemacht, aber ich möchte einige Meinungen hören :)

Answer 1

Es macht mehr Sinn, wenn man die beiden Anrufe aufgeteilt:

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

Jetzt zeigt es an die letzte Linie als das Problem. Mit anderen Worten, der Anruf an Array.ConvertAll weiß, dass die Quelle nicht null ist, aber der Anruf an ToArray() weiß nicht, dass nicht null sein wird.

(Ihr Beispiel ist auch etwas verwirrend aufgrund der Verwendung des Namens source in Ihrem Quellcode - der Fehler würde immer noch source verwenden, selbst wenn Sie Ihre Variable etwas völlig anderes aufgerufen hätten, da es sich auf den ersten Parameter bezieht Enumerable.ToArray.)

Grundsätzlich glaube ich, das würde alles funktionieren, wenn Array.ConvertAll eine angemessene Nicht-Nichtigkeit Nachbedingung erhält. Bis dahin wird dies den Trick:

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

Ich bin damit einverstanden diese Art der Sache ist ärgerlich, aber ich bin sicher, dass es schnell verbessern wird als MS immer mehr Verträge in den BCL hinzufügt. Es ist wichtig zu beachten, dass es ein nicht ein Problem mit dem statischen Checker selbst ist.

(Tatsächlich Array.ConvertAll entweder keine Voraussetzung - wenn Sie die source Variable oben in der zweiten Code-Schnipsel auf null, es würde sich beklagen immer noch nicht.)