CodeContracts with collection types

本文关键字:types collection with CodeContracts | 更新日期: 2023-09-27 18:15:50

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

我认为使用假设和ForAll就足够了,但这没有帮助

这是我尝试过的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);
  }
}
<<p> ——列表/strong>
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属性时都写Contract.Assume(child != null)吗?


<标题>更新:

我试图实现Enumerator,确保在Current属性getter中不为空的条件,正如 phog 所建议的那样。但是警告仍然存在(对我来说很意外)。

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'
        }

任何想法?

CodeContracts with collection types

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

编辑:

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

EDIT2:

由于ObservableCollection<>ReadOnlyObservableCollection<>都装饰了IList<>实例,因此实现了IList<>,我尝试了以下操作。注意"确保未经证实"answers"断言为假"之间的不一致。无论result的静态类型是ReadOnlyObservableCollection<C>还是IList<C>,我都得到了相同的消息。我使用Code Contracts版本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/找到了一个很好的问题总结;基本上,向已实现接口的契约添加附加条件违反了Liskov替代原则,因为这意味着具有附加限制的类不能在任何接受实现该接口的对象的上下文中使用。

我尝试过同样的方法,但我遇到的最多的是:

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

结果,这九头蛇可能作为常规IEnumerable传递参数,返回INonNullable值(由静态检查器还询问检查null,因为它是引用类型),而T值非空保证可以使用的方法和foreach语句(因为foreach使用隐式GetEnumerator()方法,它返回INonNullEnumerator,确保返回非空INonNullable, NonNullable结构,支持所有这些合同)。

但是,老实说,这是一个怪物。我编写它只是为了尽我所能使契约保证集合没有null。然而,没有完全成功:合同。ForAll(myList, item => item != null)不能被证明只是因为它使用了IEnumerable,既不是foreach也不是我的INonNullEnumerable。

我敢打赌,这是不可能的,至少目前的CodeContracts API

更新您的ObjectInvariant以包括检查,以确保在每个方法调用结束时集合中的所有项都是非空的。

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