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

[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 требует ненулевой входной параметр (он реализует интерфейс с контрактом Require), и поэтому я получаю ошибку 'require unproven: group! = null' в подгруппе, передаваемой вAddRequested, Правильно ли я использую синтаксис ForAll? Если это так, и решатель просто не понимает, есть ли другой способ помочь решателю распознать контракт, или мне просто нужно использовать Assume всякий раз, когда вызывается GetAllGroups ()?