Почему эти отношения с Кодексом не доказывают?

Question

У меня есть метод, который начинается так:

public static UnboundTag ResolveTag(Type bindingType, string name, string address) 
    { 
     Contract.Requires(bindingType != null); 

     var tags = GetUnboundTagsRecursively(bindingType).ToArray(); 

Контракт на реализацию GetUnboundTagsRecursively (реализован в одном классе) выглядит следующим образом:

public static IEnumerable<UnboundTag> GetUnboundTagsRecursively(Type bindingType) 
    { 
     Contract.Requires(bindingType != null); 
     Contract.Ensures(Contract.Result<IEnumerable<UnboundTag>>() != null); 

Статический анализатор указывает на неисправность на строке назначения тегов ResolveTag с сообщением "requires unproven: source != null". Я просмотрел это несколько раз, и я не могу понять, почему это было бы. Я предполагаю, что это ссылка на параметр source для метода расширения ToArray(). Мой метод утверждает, что он гарантирует, что результат не является нулевым, поэтому это, по-видимому, означает, что источник для ToArray() также не является нулевым. Что мне не хватает?

---

Дополнительная информация: метод, возвращающий IEnumerable, реализуется с обратными вызовами доходности. Мне интересно, возможно ли, что волшебник перечисления каким-то образом возится с кодовыми контрактами ...

Я просто попытался изменить реализацию, чтобы возвращать пустой массив, а не использовать возврат доходности и который передает контракты, так что, по-видимому, это проблема с метод с возвратом доходности. Кто-нибудь знает об этом?

---

Я посмотрел на IL для DLL контрактов, и это на самом деле положить контракты звонки в MoveNext() для реализации перечислителей:

.method private hidebysig newslot virtual final 
     instance bool MoveNext() cil managed 
{ 
    .override [mscorlib]System.Collections.IEnumerator::MoveNext 
    // Code size  410 (0x19a) 
    .maxstack 3 
    .locals init ([0] bool V_0, 
      [1] int32 V_1) 
    .try 
    { 
    IL_0000: ldarg.0 
    IL_0001: ldfld  int32 PLCLink.Bind.UnboundTag/'<GetUnboundTagsRecursively>d__c'::'<>1__state' 
    IL_0006: stloc.1 
    IL_0007: ldloc.1 
    IL_0008: ldc.i4.0 
    IL_0009: beq.s  IL_0024 
    IL_000b: ldloc.1 
    IL_000c: ldc.i4.3 
    IL_000d: sub 
    IL_000e: switch  ( 
          IL_00cd, 
          IL_018d, 
          IL_0162) 
    IL_001f: br   IL_018d 
    IL_0024: ldarg.0 
    IL_0025: ldc.i4.m1 
    IL_0026: stfld  int32 PLCLink.Bind.UnboundTag/'<GetUnboundTagsRecursively>d__c'::'<>1__state' 
    IL_002b: ldarg.0 
    IL_002c: ldfld  class PLCLink.Bind.IUnboundTagGroup PLCLink.Bind.UnboundTag/'<GetUnboundTagsRecursively>d__c'::group 
    IL_0031: ldnull 
    IL_0032: ceq 
    IL_0034: ldc.i4.0 
    IL_0035: ceq 
    IL_0037: call  void [mscorlib]System.Diagnostics.Contracts.Contract::Requires(bool) 
    IL_003c: call  !!0 [mscorlib]System.Diagnostics.Contracts.Contract::Result<class [mscorlib]System.Collections.Generic.IEnumerable`1<valuetype PLCLink.Bind.UnboundTag>>() 

Это интересно, как Contract.Result вызов фактически использует неправильный тип (поскольку MoveNext возвращает bool).

Answer 1

I подозреваемый это потому, что контракты заканчиваются в MoveNext() сгенерированного типа реализации итератора. Попробуйте это:

public static IEnumerable<UnboundTag> GetUnboundTagsRecursively 
    (Type bindingType) 
{ 
    Contract.Requires(bindingType != null); 
    Contract.Ensures(Contract.Result<IEnumerable<UnboundTag>>() != null); 
    return GetUnboundTagsRecursivelyImpl(bindingType); 
} 

private static IEnumerable<UnboundTag> GetUnboundTagsRecursivelyImpl 
    (Type bindingType) 
{ 
    // Iterator block code here 
} 

Теперь вы, возможно, придется сделать немного дополнительной работы, чтобы получить эти методы компилировать без каких-либо нарушений контракта. Например:

public static IEnumerable<UnboundTag> GetUnboundTagsRecursively 
    (Type bindingType) 
{ 
    Contract.Requires(bindingType != null); 
    Contract.Ensures(Contract.Result<IEnumerable<UnboundTag>>() != null); 
    IEnumerable<UnboundTag> ret = GetUnboundTagsRecursivelyImpl(bindingType); 
    // We know it won't be null, but iterator blocks are a pain. 
    Contract.Assume(ret != null); 
    return ret; 
} 

Это немного неэффективно, так как он будет выполнять проверку недействительности дважды. Это также эффективно подавляет предупреждение через Assume.

Я не удивлюсь, если вы услышите, что команда кодовых контрактов работает над исправлением этого ... Я думаю, что слышал о чем-то подобном, но я не могу вспомнить детали. release notes для выпуска сентября 2009 года включает в себя:

Начальной поддержку контрактов на итераторах

... но при условии, что вы используете последнюю версию, по-видимому, что начальная поддержка не хватает :)