具有集合类型的 CodeContracts

Question

我的班级中有一系列子项目，并且有一个公共访问者。我想提供一个后置条件来确保集合中的项目不为空（我知道，在测试 2 和 3 中调用者可以更改集合，但现在我的目标只是确保从属性返回的集合不会不包含 null 项）。

我认为使用 Assume 和 ForAll 就足够了，但这没有帮助

这是我尝试过的包含 3 个类的示例代码。 所有 3 个案例几乎完全相同，除了第一个公开 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'
  }

我可以以某种方式定义一个契约，以便不编写 <每次我使用 Children 属性时，code>Contract.Assume(child != null) ？

---

更新：

我尝试实现 Enumerator 来确保 Current 属性 getter 中的条件不为空，正如 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'
        }

有什么想法吗？

Answer 1

我会创建自己的集合类型。例如，您可以实现 IList 并“确保”索引 getter 永远不会返回 null，并“要求”Add() 和索引 setter 永远不会接收到null 作为参数。

编辑：

为了避免 foreach 循环中的“可能在空引用上调用方法”消息，您可能还必须实现自己的枚举器类型并“确保”其 Current 属性永远不会返回 null 。

EDIT2：

由于 ObservableCollection<> 和 ReadOnlyObservableCollection<> 都装饰 IList<> 实例，因此实现 IList<> ;，我尝试了以下操作。请注意“确保未经证实”和“断言是错误的”之间的不一致。无论 result 的静态类型是 ReadOnlyObservableCollection 还是 IList，我都会收到相同的消息。我正在使用代码合同版本 1.4.40602.0。

namespace EnumerableContract
{
    public class C
    {
        public int Length { get; private set; }
    }

    public class P
    {
        public IList<C> Children
        {
            get
            {
                Contract.Ensures(Contract.Result<IList<C>>() != null);
                Contract.Ensures(Contract.ForAll(Contract.Result<IList<C>>(), c => c != null));

                var result = new ReadOnlyObservableCollection<C>(new ObservableCollection<C>(new[] { new C() }));

                Contract.Assume(Contract.ForAll(result, c => c != null));

                return result; //CodeContracts: ensures unproven Contract.ForAll(Contract.Result<IList<C>>(), c => c != null)
            }
        }

        public class Program
        {
            public static int Main(string[] args)
            {
                foreach (var item in new P().Children)
                {
                    Contract.Assert(item == null); //CodeContracts: assert is false
                    Console.WriteLine(item.Length);
                }

                return 0;
            }
        }
    }
}

EDIT3：

在 http://social.msdn.microsoft.com/Forums/en-US/codecontracts/thread/af403bbc-ca4e-4546-8b7a-3fb3dba4bb4a/；基本上，在已实现接口的契约中添加附加条件违反了里氏替换原则，因为这意味着具有附加限制的类不能在任何接受实现该接口的对象的上下文中使用。

Answer 2

我尝试实现相同的方法，我遇到的大多数情况是：

1. 声明通用 INonNullable只有一个属性确保返回非空值的接口，在 NonNullable 结构体中实现它。
2. 声明 IOnNullEnumerator;和 IOnNullEnumerable接口（很可能是无用的），与 IEnumerator 和 IEnumerable 相同，但 INonNullEnumerable 具有 IsEmpty 属性，而 GetEnumerator 要求它为 false。 NonNullEnumerator 返回 T，而不是 INonNullable。
3. 声明我的自定义集合实现 INonNullEnumerable和 IList> （为了与常见的 IEnumerable 和常识兼容），基于 NonNullable 数组。 IList 的方法使用 INonNullable 参数显式实现，但仅使用相同的隐式方法接受带有契约的 T 值。

因此，这个 Hydra 可以作为通常的 IEnumerable 参数传递，返回 INonNullable 值（静态检查器仍然需要检查空值，因为它是引用类型），而可以使用具有非空保证的 T 值在方法和 foreach 语句中（因为 foreach 使用隐式 GetEnumerator() 方法，该方法返回 INonNullEnumerator，这确保返回非 null INonNullable，即 NonNullable struct，所有这一切都有合同的支持）。

但老实说，这是一个怪物。我编写它只是为了尽最大努力让合约保证集合没有空值。然而，没有完全成功： Contract.ForAll(myList, item => item != null) 无法被证明，只是因为它使用 IEnumerable，而不是 foreach 和我的 INonNullEnumerable。

我敢打赌，这是不可能的，至少对于当前的 CodeContracts API 来说是这样。

Answer 3

更新您的 ObjectInvariant 以包含检查，以确保集合中的所有项目在每个方法调用结束时都不为 null。

  [ContractInvariantMethod]
  private void ObjectInvariant()
  {
    Contract.Invariant(_children != null && Contract.ForAll(_children, item => item != null));
    Contract.Invariant(_childrenReadOnly != null && Contract.ForAll(_childrenReadOnly, item => item != null);
  }