Contratti di codice, tutti numerici e personalizzati enumerabili

Question

Sto utilizzando C# 4.0 e Contratti di codice e ho la mia personalizzata GameRoomCollection : IEnumerable<GameRoom>.

Desidero garantire che nessuna istanza di GameRoomCollection contenga mai un elemento di valore null. Non mi sembra di essere in grado di farlo, però. Invece di fare una regola generale, ho cercato di fare un semplice esempio. AllGameRooms è un'istanza di 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 
} 

chiunque può vedere, il motivo per cui non l'ho provato, che non è gameRoomnull?

EDIT:

L'aggiunta di un riferimento per l'oggetto prima iterazione non funziona neanche:

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:

Tuttavia: Se converto il tipo di raccolta sala giochi a un array, funziona perfettamente:

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

Ciò è dovuto al fatto che non è possibile definire una regola per i metodi dell'interfaccia IEnumerable<T>?

EDIT3: Il problema può essere in qualche modo correlato a this question?

Answer 1

ho il sospetto che sia perché model.AllGameRooms restituisce un IEnumerable<GameRoom> che può essere diverso per ogni accesso alle proprietà.

Provare a utilizzare:

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

Answer 2

penso che questo potrebbe avere a che fare con la purezza del metodo GetEnumerator. PureAttribute

Contratti accettano solo i metodi definiti come [Puro] (privo di effetti collaterali).

Alcune informazioni extra Code Contracts, look for purity

Qoute:

Purezza

Tutti i metodi che vengono chiamati nell'ambito di un contratto deve essere puro; ovvero, essi non devono aggiornare nessuno stato preesistente. Un metodo puro è autorizzato a modificare gli oggetti creati dopo l'immissione nel metodo puro.

strumenti contrattuali Codice attualmente assumono che i seguenti elementi di codice sono pura:

I metodi che sono contrassegnati con il PureAttribute.

Tipi contrassegnati con PureAttribute (l'attributo si applica a tutti i metodi del tipo ).

Proprietà get accessors.

Operatori (metodi statici cui nomi iniziare con "op", e che hanno uno o due parametri e un non-vuoto tipo restituito ).

Qualsiasi metodo il cui nome completo inizia con "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path", o "System.Type".

Qualsiasi delegato invocato, a condizione che il tipo di delegato stesso sia attribuito allo con PureAttribute. Il delegato tipi System.Predicate e System.Comparison sono considerati pure.