代码合同,forall和custom可枚举

Question

我正在使用C#4.0和Code Contracts,我有自己的自定义GameRoomCollection : IEnumerable<GameRoom>.

我想确保,任何实例GameRoomCollection都不会包含null值元素.不过,我似乎无法做到这一点.我试图做一个简单明了的例子,而不是制定一般规则.这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不是null吗？

编辑:

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

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>接口的方法定义规则而导致的吗？

EDIT3:问题可能与这个问题有关吗？

Answer 1

我怀疑这是因为model.AllGameRooms返回的IEnumerable<GameRoom>每个属性访问可能不同。

尝试使用：

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