. Kontraktów kodu .NET: czy może uzyskać więcej podstawowych niż to?

Question

właśnie bawić odpowiedzieć na czyjeś pytanie tutaj na przepełnienie stosu, kiedy zauważyłem statyczny ostrzeżenie weryfikacyjny od wewnątrz mojego Visual Studio (2008):

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

Dostaję komunikat wymaga niesprawdzone źródła! = null. Wydaje mi się oczywiste, że tak nie jest. To tylko jeden przykład. Z drugiej strony, niektóre ładne rzeczy wydają się działać całkiem nieźle.

Używam wersji 1.2.20518.12 (18 maja). Uważam, że umowy dotyczące kodu są bardzo interesujące, ale czy ktoś inny miał takie przypadki? Czy uważasz, że obecna implementacja może być użyta w praktyce, czy też uważasz ją za czysto akademicką w tym momencie?

Zrobiłem to społeczność wiki, ale chciałbym usłyszeć jakieś opinie :)

Answer 1

większy sens jeśli rozdzielić dwa połączenia w górę:

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

Teraz to wskazuje do linii last jako problemu. Innymi słowy, wywołanie Array.ConvertAll wie, że źródło nie jest puste, ale połączenie z ToArray() nie wie, że tmp nie będzie miało wartości NULL.

(Twój przykład jest nieco mylące ze względu na używanie nazwy source w kodzie źródłowym - błąd będzie nadal korzystać source nawet jeśli zadzwonił zmienna coś zupełnie innego, jak to odnosi się do pierwszego parametru Enumerable.ToArray.)

Zasadniczo wierzę, że to wszystko będzie działało, gdy Array.ConvertAll otrzyma odpowiednią wartość nieważności. Do tego czasu będzie to rade:

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

Zgadzam tego typu rzeczy jest irytujące, ale jestem pewien, że szybko poprawić jak MS dodaje coraz więcej zamówień na plc. Ważne jest, aby pamiętać, że jest to problem z samym statycznym narzędziem sprawdzającym.

(W rzeczywistości, Array.ConvertAll nie posiada warunek albo - jeśli ustawić zmienną source null w drugim fragmencie kodu powyżej, to nadal nie będzie narzekać.)