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有关吗？
解决方法
合同只接受定义为[纯](免除副作用)的方法.
一些额外的信息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.
