代码合约，forall 和自定义可枚举

Question

我正在使用 C# 4.0 和代码合同，并且我有自己的自定义 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：问题是否与this question有关？

Answer 1

我认为这可能与 GetEnumerator 方法的纯度有关。 PureAttribute

合同只接受定义为 [Pure]（无副作用）的方法。

一些额外的信息Code Contracts, look for purity

引用：

纯度

在一个内部调用的所有方法 契约必须是纯粹的；也就是说，他们 不得更新任何预先存在的状态。 纯方法允许修改 之后创建的对象 进入纯方法。

代码合约工具目前假设 以下代码元素是 纯：

标有 纯属性。

标有 PureAttribute（属性适用 到所有类型的方法）。

属性获取访问器。

运算符（其名称的静态方法 以“op”开头，并且有一个或 两个参数和一个非空返回 类型）。

任何具有完全限定名称的方法 开始于 "System.Diagnostics.Contracts.Contract", “System.String”、“System.IO.Path”或 “系统类型”。

任何调用的委托，前提是 委托类型本身是有属性的 与 PureAttribute。代表 类型 System.Predicate 和 System.Comparison 被考虑 纯的。

Answer 2

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

尝试使用：

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