Почему эти отношения Кодекс контрактов не докажут?

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, реализован с помощью вызовов return return.Мне интересно, может быть, волшебство перечислителя каким-то образом портится с контрактными кодами ...

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

---

Я взглянул на IL для библиотеки Contracts, и она фактически помещает вызовы контрактов в 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.

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

Первоначальная поддержка контрактов на итераторах

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