c# – 代码合同,forall和custom可枚举

我使用C#4.0和代码合同,我有自己的自定义GameRoomCollection：IEnumerable< GameRoom&gt ;. 我想确保,GameRoomCollection的任何实例将不会包含一个空值元素.我似乎不能这样做.我没有做一个一般规则,而是尝试做一个简单而简单的例子. 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不是空的？

编辑：

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

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>的方法定义规则.接口？

编辑3：问题可能与this question有关吗？

解决方法

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

合同只接受定义为[纯](免除副作用)的方法.

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

Qoute：

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.