Contratos de código, forall y enumerable personalizado

Question

Estoy usando C# 4.0 y Contratos de código y tengo mi propio GameRoomCollection : IEnumerable<GameRoom> personalizado.

Quiero asegurarme de que ninguna instancia de GameRoomCollection contendrá un elemento de valor null. No obstante, no consigo hacerlo. En lugar de hacer una regla general, he intentado hacer un ejemplo claro y simple. El AllGameRooms es una instancia de 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 
} 

¿Alguien puede ver, por qué no he demostrado, que no es gameRoomnull?

EDIT:

Adición de una referencia para el objeto antes de la iteración no funciona bien:

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:

Sin embargo: Cuando se modifica el tipo de colección sala de juegos a una matriz, funciona bien:

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

¿Esto se debe al hecho de que no se puede definir una regla para los métodos de la interfaz IEnumerable<T>?

EDIT3: ¿Puede el problema de alguna manera estar relacionado con this question?

Answer 1

Sospecho que es porque model.AllGameRooms devuelve un IEnumerable<GameRoom> que podría ser diferente en cada acceso a la propiedad.

Trate de usar:

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

Answer 2

creo que esto podría tener que ver con la pureza del método GetEnumerator. PureAttribute

Los contratos solo aceptan métodos que se definen como [Puro] (sin efectos secundarios).

alguna información extra Code Contracts, look for purity

Qoute:

Pureza

Todos los métodos que se llaman dentro de un contrato de debe ser puro; es decir, ellos no deben actualizar ningún estado preexistente. Se permite un método puro para modificar los objetos que se han creado después de la entrada en el método puro.

herramientas de contrato Código actualmente asumen que los siguientes elementos de código son pura:

métodos que están marcados con el PureAttribute.

Tipos que están marcados con el atributo PureAttribute (el atributo aplica a todos los métodos del tipo).

La propiedad obtiene los descriptores de acceso.

Operadores (métodos estáticos cuyos nombres comenzar con "op", y que tienen uno o dos parámetros y un no-vacío tipo de retorno).

Cualquier método cuyo nombre completo de comienza con "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path", o "System.Type".

Cualquier delegado invocado, siempre que el tipo de delegado se atribuya con PureAttribute. Los delegados tipos System.Predicate y System.Comparison se consideran puros.