c# - 代码契约(Contract)，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 

编辑 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: 这个问题能以某种方式与 this question 相关吗？ ？

Answer 1

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

合约只接受定义为[纯](无副作用)的方法。

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

报价:

Purity

All methods that are called within a contract must be pure; that is, they must not update any preexisting state. A pure method is allowed to modify objects that have been created after entry into the pure method.

Code contract tools currently assume that the following code elements are pure:

Methods that are marked with the PureAttribute.

Types that are marked with the PureAttribute (the attribute applies to all the type's methods).

Property get accessors.

Operators (static methods whose names start with "op", and that have one or two parameters and a non-void return type).

Any method whose fully qualified name begins with "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path", or "System.Type".

Any invoked delegate, provided that the delegate type itself is attributed with the PureAttribute. The delegate types System.Predicate and System.Comparison are considered pure.