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

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

[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