Контракты кода, forall и настраиваемое перечисление

Я использую 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 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 ?

EDIT3: Может ли проблема быть каким-то образом связана с этим вопрос ?

10
задан Community 23 May 2017 в 12:30
поделиться