Использование договора. Для кодовых контрактов

Хорошо, у меня есть еще один вопрос с кодовым контрактом. У меня есть контракт по методу интерфейса, который выглядит так (другие методы опущены для ясности):

[ContractClassFor(typeof(IUnboundTagGroup))]
public abstract class ContractForIUnboundTagGroup : IUnboundTagGroup
{
    public IUnboundTagGroup[] GetAllGroups()
    {
        Contract.Ensures(Contract.Result<IUnboundTagGroup[]>() != null);
        Contract.Ensures(Contract.ForAll(Contract.Result<IUnboundTagGroup[]>(), g => g != null));

        return null;
    }
}

У меня есть код, который использует интерфейс, который выглядит так:

    public void AddRequested(IUnboundTagGroup group)
    {
            foreach (IUnboundTagGroup subGroup in group.GetAllGroups())
            {
                AddRequested(subGroup);
            }
            //Other stuff omitted
    }

AddRequested требует непустого входного параметра (он реализует интерфейс, который имеет контракт Requires), и поэтому я получаю сообщение об ошибке "unproven: group!= null" в подгруппе, передаваемой в AddRequested. Я правильно использую синтаксис ForAll? Если это так, и решатель просто не понимает, есть ли другой способ помочь решателю признать контракт или мне просто нужно использовать Assume при вызове GetAllGroups()?

Ответы

Ответ 1

В "Руководство по контрактам с кодовыми контрактами" ) говорится: "Статический механизм проверки контрактов еще не имеет дело с кванторами ForAll или Exists" . Пока это не так, мне кажется, что варианты:

  • Игнорировать предупреждение.
  • Добавьте Contract.Assume(subGroup != null) перед вызовом AddRequested().
  • Добавьте запрос перед вызовом AddRequested(). Может быть, if (subGroup == null) throw new InvalidOperationException() или if (subGroup != null) AddRequested(subGroup).

Вариант 1 действительно не помогает. Вариант 2 является рискованным, потому что он обойдет AddRequested() Требует контракт, даже если IUnboundTagGroup.GetAllGroups() больше не обеспечивает пост-условие. Я бы выбрал вариант 3.