Использование Contract.ForAll в кодовых контрактах - PullRequest
Новая
       55

Использование Contract.ForAll в кодовых контрактах

12 голосов
/ 23 июня 2010

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

[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 ()?

1 Ответ

10 голосов
/ 25 июня 2010

В руководстве пользователя Code Contracts говорится: «Статическая проверка контракта еще не имеет дело с квантами ForAll или Exists».Пока это не произойдет, мне кажется, варианты:

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

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

...