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

Question

我正在使用 C# 4.0 和代码合约，并且有自己的自定义 GameRoomCollection : IEnumerable。

我想确保 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 

编辑2：

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

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

是这是因为您无法为 IEnumerable 接口的方法定义规则？

编辑3：问题是否与这个问题?

Answer 1

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

合约仅接受定义为的方法[纯]（无副作用）。

一些额外信息代码契约，寻找纯度

引用：

纯度

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

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

标有的方法
纯属性。

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

属性获取访问器。

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

任何具有完全限定名称的方法
开始于
“系统.诊断.合同.合同”,
“System.String”、“System.IO.Path”或
“系统.类型”。

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

Answer 2

我怀疑这是因为 model.AllGameRooms 返回一个 IEnumerable ，它在每个属性访问上可能不同。

尝试使用：

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