Кодекс контрактов, бланков и обычаев перечислим - PullRequest
Новая
       30

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

10 голосов
/ 18 февраля 2011

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

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: Может ли проблема как-то быть связана с этим вопросом ?

Ответы [ 2 ]

2 голосов
/ 02 марта 2011

Я думаю, что это может быть связано с чистотой метода GetEnumerator. PureAttribute

В контрактах допускаются только методы, которые определены как [Pure] (без побочных эффектов).

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

Qoute:

чистота

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

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

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

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

Недвижимость получить аксессоры.

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

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

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

0 голосов
/ 18 февраля 2011

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

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

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