У меня есть коллекция дочерних элементов в моем классе, и у меня есть открытый метод доступа к ней . Я хочу предоставить постусловие, чтобы гарантировать, что элементы в коллекции не равны нулю (я знаю, что в тестах 2 и 3 вызывающий может изменить коллекцию, но сейчас моя цель - просто убедиться, что эта коллекция возвращается из свойства не содержит null элементов).

Я думал, что использования Assume и ForAll будет достаточно, но это не помогает

Вот пример кода с 3 классами, которые я пробовал. {{ 1}} Все три случая практически идентичны, за исключением того, что первый предоставляет ReadOnlyObservableCollection , второй - ObservableCollection и третий - List .

- ReadOnlyObservableCollection

class Test1
{
  public Test1()
  {
    _children = new ObservableCollection<A>();
    _childrenReadOnly = new ReadOnlyObservableCollection<A>(_children);
  }

  protected readonly ObservableCollection<A> _children;
  protected readonly ReadOnlyObservableCollection<A> _childrenReadOnly;

  public ReadOnlyObservableCollection<A> Children
  {
    get
    {
      Contract.Ensures(Contract.ForAll(Contract.Result<ReadOnlyObservableCollection<A>>(), i => i != null));
      Contract.Assume(Contract.ForAll(_childrenReadOnly, i => i != null));
      return _childrenReadOnly; // CodeContracts: ensures unproven: Contract.ForAll(Contract.Result<ReadOnlyObservableCollection<A>>(), i => i != null)
    }
  }

  [ContractInvariantMethod]
  private void ObjectInvariant()
  {
    Contract.Invariant(_children != null);
    Contract.Invariant(_childrenReadOnly != null);
  }
}

- ObservableCollection

class Test2
{
  public Test2()
  {
    _children = new ObservableCollection<A>();
  }

  protected readonly ObservableCollection<A> _children;

  public ObservableCollection<A> Children
  {
    get
    {
      Contract.Ensures(Contract.ForAll(Contract.Result<ObservableCollection<A>>(), i => i != null));
      Contract.Assume(Contract.ForAll(_children, i => i != null));
      return _children; // CodeContracts: ensures unproven: Contract.ForAll(Contract.Result<ObservableCollection<A>>(), i => i != null)
    }
  }

  [ContractInvariantMethod]
  private void ObjectInvariant()
  {
    Contract.Invariant(_children != null);
  }
}

- List

class Test3
{
  protected readonly List<A> _children = new List<A>();

  public List<A> Children
  {
    get
    {
      Contract.Ensures(Contract.ForAll(Contract.Result<List<A>>(), i => i != null));
      Contract.Assume(Contract.ForAll(_children, i => i != null));
      return _children; // No warning here when using List instead of ObservableCollection
    }
  }

  [ContractInvariantMethod]
  private void ObjectInvariant()
  {
    Contract.Invariant(_children != null);
  }
}

Вот тестовый код, который использует эти классы:

  Test1 t1 = new Test1();
  foreach (A child in t1.Children)
  {
    child.SomeMethod(); // CodeContracts: Possibly calling a method on a null reference 'child'
  }

  Test2 t2 = new Test2();
  foreach (A child in t2.Children)
  {
    child.SomeMethod(); // CodeContracts: Possibly calling a method on a null reference 'child'
  }

  Test3 t3 = new Test3();
  foreach (A child in t3.Children)
  {
    child.SomeMethod(); // CodeContracts: Possibly calling a method on a null reference 'child'
  }

Могу я как-то определить контракт, чтобы не писать te Contract.Assume (child! = null) каждый раз, когда я использую свойство Children ?

Обновление:

Я пытался реализовать Enumerator , который гарантирует не нулевое условие в Current геттере свойства, как было предложено phoog . Но предупреждение по-прежнему присутствует (на удивление для меня).

public class NotNullEnumerable<T> : IEnumerable<T>
{
    private IEnumerable<T> _enumerable;
    public NotNullEnumerable(IEnumerable<T> enumerable)
    {
        _enumerable = enumerable;
    }

    #region IEnumerable<T> Members
    public IEnumerator<T> GetEnumerator()
    {
        return new NotNullEnumerator<T>(_enumerable.GetEnumerator());
    }
    #endregion

    #region IEnumerable Members
    System.Collections.IEnumerator System.Collections.IEnumerable.GetEnumerator()
    {
        return GetEnumerator();
    }
    #endregion
}

public class NotNullEnumerator<T> : IEnumerator<T>
{
    private readonly IEnumerator<T> _enumerator;
    public NotNullEnumerator(IEnumerator<T> enumerator)
    {
        _enumerator = enumerator;
    }

    #region IEnumerator<T> Members
    public T Current
    {
        get
        {
            Contract.Ensures(Contract.Result<T>() != null);
            return _enumerator.Current;
        }
    }
    #endregion

    #region IDisposable Members
    public void Dispose()
    {
        _enumerator.Dispose();
    }
    #endregion

    #region IEnumerator Members
    object System.Collections.IEnumerator.Current
    {
        get
        {
            Contract.Ensures(Contract.Result<object>() != null);
            return _enumerator.Current;
        }
    }

    public bool MoveNext()
    {
       return _enumerator.MoveNext();
    }

    public void Reset()
    {
        _enumerator.Reset();
    }
    #endregion
}

Использование в коде:

        Test1 t1 = new Test1();
        var NonNullTest1 = new NotNullEnumerable<A>(t1.Children);
        foreach (A child in NonNullTest1)
        {
            child.SomeMethod(); // CodeContracts: Possibly calling a method on a null reference 'child'
        }

Есть идеи?