Контракты кода: IEnumerator <T>.GetEnumerator () странный унаследованный контракт? - PullRequest
Новая
       30

Контракты кода: IEnumerator <T>.GetEnumerator () странный унаследованный контракт?

5 голосов
/ 05 января 2011

Я использую Кодовые контракты вместе с Расширениями Редактора контрактных кодов VS2010 надстройка.У меня есть класс, который реализует интерфейс IEnumerable<T>, и я реализовал блок итератора для метода GetEnumerator().Над ним я вижу следующий унаследованный контракт:

ensures result != null ensures result.Model == ((IEnumerable)this).Model [Pure] public IEnumerator(of IBaseMessage) GetEnumerator() {

Я понимаю первое и третье требование контракта - GetEnumerator() никогда не должен возвращать ноль, и он никогда не должен вызыватьпобочный эффект.Но что означает второе требование контракта?Что это за Model свойство IEnumerator<T> и IEnumerable?

РЕДАКТИРОВАТЬ: Как указал Damien_The_Unbeliever в своем комментарии, контракт на IEnumerable<T> и IEnumerator<T>находится в отдельном файле, справочной сборке контрактов.Используя Reflector , при разборке контракта этих двух интерфейсов (полный код здесь ), вы можете увидеть следующее: 

[return: Fresh]
[Escapes(true, false), Pure, GlobalAccess(false)]
public IEnumerator GetEnumerator()
{
    IEnumerator enumerator;
    Contract.Ensures((bool) (Contract.Result<IEnumerator>() != null), null, "Contract.Result<IEnumerator>() != null");
    Contract.Ensures((bool) (Contract.Result<IEnumerator>().Model == this.Model), null, "Contract.Result<IEnumerator>().Model == this.Model");
    Contract.Ensures((bool) (Contract.Result<IEnumerator>().CurrentIndex == -1), null, "Contract.Result<IEnumerator>().CurrentIndex == -1");
    return enumerator;
}

Интересно,в GetEnumerator() есть дополнительный контракт, который не отображается расширением редактора: 

Contract.Result<IEnumerator>().CurrentIndex == -1

и некоторые дополнительные загадки (такие как атрибуты Fresh, Escapes и GlobalAccess).

1 Ответ

2 голосов
/ 05 января 2011

Еще раз посмотрев код / ​​контракты, загруженные из C: \ Program Files \ Microsoft \ Contracts \ Contracts.NETFramework \ v4.0 \ mscorlib.Contracts.dll (как указано в моем комментарии).

Я считаю, что это может быть безопасно проигнорировано для вашей реализации. Кажется, что это связано с тем, что он пытается определить контракт таким образом, чтобы (эффективно) после итерации с вашим IEnumerator объектом он возвращал определенное количество элементов. Эти элементы фактически «моментально снимаются», когда возвращается вызов GetEnumerator, а вызовы Reset и MoveNext могут выполнять итерации только для одного и того же набора элементов.

Я думаю, что он пытается дать некоторые гарантии неизменности. Я понятия не имею, можем ли мы сами написать такие же договоры - он использует атрибут ContractModel, который, насколько я могу найти, нигде не документирован.

По поводу неизменности и т. Д .:

В основном я просматривал контракт для MoveNext для возвращенного объекта IEnumerator - в основном он говорит, что MoveNext не может изменить свойство Model (мы знаем, что это была та же модель, назначенная ему GetEnumerator) и что CurrentIndex свойство варьируется от 0 до Model.Length. После этого это просто интуиция. Я не могу указать на что-либо еще в контрактной сборке, которое дает мне больше информации.

...