Code contracts, forall and custom enumerable

Question

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: Can the problem somehow be related to this question?

Answer 1

I suspect it's because model.AllGameRooms returns an IEnumerable<GameRoom> which could be different on each property access.

Try using:

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

Answer 2

I think this might have to do with purity of the GetEnumerator method. PureAttribute

Contracts only accept methods that are defined as [Pure] (side effect free).

Some extra information Code Contracts, look for purity

Qoute:

Purity

All methods that are called within a contract must be pure; that is, they must not update any preexisting state. A pure method is allowed to modify objects that have been created after entry into the pure method.

Code contract tools currently assume that the following code elements are pure:

Methods that are marked with the PureAttribute.

Types that are marked with the PureAttribute (the attribute applies to all the type's methods).

Property get accessors.

Operators (static methods whose names start with "op", and that have one or two parameters and a non-void return type).

Any method whose fully qualified name begins with "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path", or "System.Type".

Any invoked delegate, provided that the delegate type itself is attributed with the PureAttribute. The delegate types System.Predicate and System.Comparison are considered pure.