Кодовые контракты, общие и пользовательские перечислимые

Я использую С# 4.0 и Code Contracts, и у меня есть свой собственный 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?

EDIT:

Добавление ссылки для объекта перед итерацией также не работает:

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>?

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

Ответы

Ответ 1

Я думаю, что это может иметь отношение к чистоте метода GetEnumerator. PureAttribute

Контракты принимают только методы, которые определены как [Pure] (свободный побочный эффект).

Дополнительная информация Кодовые контракты, посмотрите на чистоту

Qoute:

Чистота

Все методы, вызываемые внутри договор должен быть чистым; то есть они не должно обновлять существующее существо. Чистый метод разрешается изменять объекты, созданные после вход в чистый метод.

В настоящее время используются инструменты контрактного контракта что следующие элементы кода чистый:

Методы, отмеченные PureAttribute.

Типы, отмеченные PureAttribute (применяется атрибут ко всем типам методов).

Получить доступ к свойствам.

Операторы (статические методы, чьи имена начните с "op", и у вас есть один или два параметра и непустое возвращение тип).

Любой метод, чье полное имя начинается с "System.Diagnostics.Contracts.Contract", "System.String", "System.IO.Path" или "System.Type".

Любой вызванный делегат при условии, что сам тип делегата с PureAttribute. Делегат типы System.Predicate и Рассматривается система. Сравнение чистый.

Ответ 2

Я подозреваю, потому что model.AllGameRooms возвращает IEnumerable<GameRoom>, который может быть различным при каждом доступе к ресурсу.

Попробуйте использовать:

var gameRooms = mode.AllGameRooms;
Contract.Assume(Contract.ForAll(gameRooms, g => g != null));
foreach (IGameRoom gameRoom in gameRooms)
    SetupListeners(gameRoom);