c# – 代码合同,forall和custom可枚举

我使用C#4.0和代码合同,我有自己的自定义GameRoomCollection：IEnumerable< GameRoom&gt ;. 我想确保,GameRoomCollection的任何实例将不会包含一个空值元素.我似乎不能这样做.我没有做一个一般规则,而是尝试做一个简单而简单的例子. AllGameRooms是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 
}

任何人都可以看到,为什么我没有证明,那个gameRoom不是空的？

编辑：

在迭代之前添加对象的引用不起作用：

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：

但是：如果我将游戏室集合类型转换为数组,它可以正常工作：

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

这是由事实引起的,您不能为IEnumerable< T>的方法定义规则.接口？

编辑3：问题可能与this question有关吗？