I am using C# 4.0 and Code Contracts and I have my own custom GameRoomCollection : IEnumerable<GameRoom>.

I want to ensure, that no instances of GameRoomCollection will ever contain a null value element. I don't seem to be able to this, though. Instead of making a general rule, I have tried to do a plain and simple example. The AllGameRooms is an instance of 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 
}

Can anyone see, why I haven't proven, that gameRoom is not null?

EDIT:

Adding a reference for the object before iterating does not work either:

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:

However: If I convert the game room collection type to an array, it works fine:

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

Is this caused by the fact, that you cannot define a rule for methods of the IEnumerable<T> interface?

EDIT3: Ca

Edit
Report