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

Question

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

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

Answer 1

В заявлении Code Contracts User Manual говорится: «Статический контролер контракта еще не имеет дело с кванторами 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.