Kontrakt kodu, całkowity i niestandardowy przeliczalny

Question

Używam C# 4.0 i Code Contracts i mam swój własny zwyczaj GameRoomCollection : IEnumerable<GameRoom>.

Chcę się upewnić, że żadne wystąpienia z GameRoomCollection nigdy nie zawierają elementu wartości null. Wydaje mi się jednak, że nie jestem w stanie tego zrobić. Zamiast robić ogólną zasadę, starałem się zrobić prosty i prosty przykład. AllGameRooms jest instancją GameRoomCollection.

private void SetupListeners(GameRoom newGameRoom) { 
    Contract.Requires(newGameRoom != null); 
    //... 
} 
private void SetupListeners(Model model) { 
    Contract.Requires(model != null); 
    Contract.Requires(model.AllGameRooms != null); 
    Contract.Assume(Contract.ForAll(model.AllGameRooms, g => g != null)); 
    foreach (GameRoom gameRoom in model.AllGameRooms) 
     SetupListeners(gameRoom);//<= Warning: Code Contracts: Requires unproven: newGameRoom != null 
} 

Czy ktoś może zobaczyć, dlaczego nie dowiodły, że gameRoom nie jest null?

EDIT:

Dodanie odniesienia do obiektu przed Iteracja nie działa albo:

IEnumerable<IGameRoom> gameRooms = model.AllGameRooms; 
Contract.Assume(Contract.ForAll(gameRooms, g => g != null)); 
foreach (IGameRoom gameRoom in gameRooms) 
    SetupListeners(gameRoom);//<= Warning: Code Contracts: Requires unproven: newGameRoom != null 

EDIT2:

Jednakże: Jeśli przekonwertować grę typu kolekcji pokój do tablicy działa:

IGameRoom[] gameRoomArray = model.AllGameRooms.ToArray(); 
Contract.Assume(Contract.ForAll(gameRoomArray, g => g != null)); 
foreach (IGameRoom gameRoom in gameRoomArray) 
    SetupListeners(gameRoom);//<= NO WARNING 

Jest to spowodowane tym, że nie można zdefiniować reguły dla metod interfejsu IEnumerable<T>?

EDIT3: Czy problem może być w jakiś sposób związany z this question?

Answer 1

Podejrzewam, że to dlatego, że model.AllGameRooms zwraca wartość IEnumerable<GameRoom>, która może być różna dla każdego dostępu do właściwości.

Spróbuj użyć:

var gameRooms = mode.AllGameRooms; 
Contract.Assume(Contract.ForAll(gameRooms, g => g != null)); 
foreach (IGameRoom gameRoom in gameRooms) 
    SetupListeners(gameRoom);  

Answer 2

myślę, że może to mieć związek z czystością metody GetEnumerator. PureAttribute

W kontraktach akceptowane są tylko metody zdefiniowane jako [Pure] (efekt uboczny jest bezpłatny).

Niektóre dodatkowa informacja Code Contracts, look for purity

qoute:

Purity

Wszystkie metody, które nazywane są w umowie musi być czysta; to znaczy, że nie mogą aktualizować żadnego istniejącego stanu. Metoda czysta może modyfikować obiekty utworzone po wprowadzeniu w czystej metodzie.

narzędzia kontrakt Code obecnie zakładamy że następujące elementy kodu są czystego:

Metody, które są oznaczone PureAttribute.

Typy oznaczone jako PureAttribute (dla wszystkich metod danego typu obowiązuje ).

Właściwość uzyskaj dostęp.

operatora (statyczne metody, których nazwy początek „OP”, i które mają jeden lub dwa parametry i nie pustego powrotu rodzaju).

Każda metoda, której pełna nazwa zaczyna "System.Diagnostics.Contracts.Contract" "System.String", "System.IO.Path" lub "System.Type".

Dowolnemu przywołanemu uczestnikowi, pod warunkiem że samemu typowi delegata przypisuje się atrybut PureAttribute . Delegat typy System.Predicate i System.Comparison są uważane za pure.