10

我正在使用 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

编辑2：

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

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：这个问题可以与这个问题有关吗？

4

2 回答 2

2

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

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

一些额外的信息代码合同，寻找纯度

报价：

纯度

合约中调用的所有方法都必须是纯的；也就是说，它们不得更新任何预先存在的状态。纯方法允许修改进入纯方法后创建的对象。

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

用 PureAttribute 标记的方法。

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

属性获取访问器。

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

完全限定名称以“System.Diagnostics.Contracts.Contract”、“System.String”、“System.IO.Path”或“System.Type”开头的任何方法。

任何调用的委托，前提是委托类型本身具有 PureAttribute 属性。委托类型 System.Predicate 和 System.Comparison 被认为是纯的。

于 2011-03-02T01:47:37.510 回答
0

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);
于 2011-02-17T22:50:35.093 回答