使用支持集合实现 ICollection 时的代码合同警告答案

【问题标题】：Code contracts warnings when implementing ICollection with backing collection使用支持集合实现 ICollection 时的代码合同警告
【发布时间】：2011-07-24 08:37:33
【问题描述】：

我有这个代码：

public class MyCollection : ICollection<string>
{
    private readonly ICollection<string> _inner = new Collection<string>();

    public void Add(string item)
    {
        _inner.Add(item);
    } // <-- CodeContracts: ensures unproven: this.Count >= Contract.OldValue(this.Count)

    public void Clear()
    {
        _inner.Clear();
    } // <-- CodeContracts: ensures unproven: this.Count == 0

    public bool Contains(string item)
    {
        return _inner.Contains(item); // <-- CodeContracts: ensures unproven: !Contract.Result<bool>() || this.Count > 0
    }

    public void CopyTo(string[] array, int arrayIndex)
    {
        _inner.CopyTo(array, arrayIndex); // <-- CodeContracts: requires unproven: arrayIndex + this.Count  <= array.Length
    }

    public IEnumerator<string> GetEnumerator()
    {
        return _inner.GetEnumerator();
    }

    IEnumerator IEnumerable.GetEnumerator()
    {
        return GetEnumerator();
    }

    public bool Remove(string item)
    {
        return _inner.Remove(item);
    }

    public int Count
    {
        get { return _inner.Count; }
    }

    public bool IsReadOnly
    {
        get { return _inner.IsReadOnly; }
    }
}

我收到以下警告：

添加：CodeContracts：确保未经证实：this.Count >= Contract.OldValue(this.Count)
清除：CodeContracts：确保未经证实：this.Count == 0
包含：CodeContracts：确保未经证实：!Contract.Result<bool>() || this.Count > 0
CopyTo：CodeContracts：需要未经证实：arrayIndex + this.Count <= array.Length

如何解决这些问题？有什么方法可以抑制这些吗？

【问题讨论】：

你实现Count返回_inner.Count了吗？
我已经编辑了我的问题以包括整个班级。所以你可以看到Count返回_inner.Count。
我无法重现警告。需要更多细节。请注意下面我帖子的编辑部分。试试它是否适合你。另外 this.Count >= Contract.OldValue(this.Count) 可能需要 _inner.Count >= Contract.OldValue(_inner.Count)。
您是否激活了代码合约？我已经在项目属性 > 代码合同中激活了它们。运行时检查、静态检查和合同参考组装：构建。
代码契约会告诉你哪一行违反了哪些契约吗？

标签： c# .net code-contracts icollection

【解决方案1】：

不确定我是否遵循了这个问题，但我尝试了以下代码（实现了所有必需的接口）和 MyCollection myCollection = new MyCollection {"test"};工作正常。如果您仍然遇到问题，请尝试多解释一下您做了什么。

编辑： 除了我对这个问题的回答之外，我想为那些正在使用代码合同迈出第一步的人做以下说明。

要让代码合同显示警告静态检查必须处于活动状态（项目属性 -> 代码合同 -> 执行静态合同检查），只有在 Visual Studio 2010 高级版上安装了代码合同高级版（非标准版）时才可用或在 2008 Team System 上。

public class MyCollection : ICollection<string>
{
    //using System;
    //using System.Collections;
    //using System.Collections.Generic;
    //using System.Collections.ObjectModel;
    //using System.Diagnostics.Contracts;

    private readonly ICollection<string> _inner = new Collection<string>();

    #region ICollection<string> Members

    public void Add(string item)
    {
        int oldCount = Count;
        _inner.Add(item);

        Contract.Assume(Count >= oldCount);
    }

    public void Clear()
    {
        _inner.Clear();

        Contract.Assume(Count == 0);
    }

    public bool Contains(string item)
    {
        bool result = _inner.Contains(item);
        // without the following assumption:
        // "ensures unproven: !Contract.Result<bool>() || this.Count > 0"
        Contract.Assume(!result || (Count > 0));

        return result;
    }

    public void CopyTo(string[] array, int arrayIndex)
    {
        Contract.Assume(arrayIndex + Count <= array.Length);
        _inner.CopyTo(array, arrayIndex);
    }

    public bool Remove(string item)
    {
        return _inner.Remove(item);
    }

    public int Count
    {
        get
        {
            Contract.Ensures(Contract.Result<int>() == _inner.Count);
            return _inner.Count;
        }
    }

    public bool IsReadOnly
    {
        get { return _inner.IsReadOnly; }
    }

    public IEnumerator<string> GetEnumerator()
    {
        return _inner.GetEnumerator();
    }

    IEnumerator IEnumerable.GetEnumerator()
    {
        return GetEnumerator();
    }

    #endregion
}

编辑 2：

有一些解决方法，选择一个最适合您的方法：

添加缺少的 Contract.Asserts，如上面的代码示例所示；
而不是实现 Collection 固有的 ICollection；
使用StringCollection

解决方案取自 DevLabs 论坛帖子：Problems with static checker and wrapper around generic list。

编辑 3（由 Allrameest 提供）：

在 KoMet 提示的 Count 属性中添加了 Contract.Ensures(Contract.Result<int>() == backEndCollection.Count);。
在 CopyTo 方法中添加了 Contract.Assume(arrayIndex + Count <= array.Length);。
从 Clear 方法中删除了 Contract.Assert(_inner.Count == 0);。

【讨论】：

我在构建或工作方面没有任何问题。但我确实收到警告。我想要零警告。而且仅仅关闭代码合约并不是一个好的解决方案。
警告CodeContracts: requires unproven: arrayIndex + this.Count <= array.Length 仍然存在。断言/假设有助于四个中的三个。但我想要零警告......
这里发布的代码只是可能的最小示例代码。在我的真实代码中，该集合不适用于字符串。而且我不能从 Collection 继承，因为我已经从 DynamicObject 继承了。
通过一些更改并使用 KoMets 代码解决了这个问题。我已经对其进行了编辑，并且在我的编辑被接受后将接受此答案。 :)
只是迟到的说明：我添加了一个 ObjectInvariant 声明 this.Count == _inner.Count ，仅此一项就解决了除 .Clear() 之外的所有警告

【解决方案2】：

根据我从多个链接中看到的情况，您需要将此行添加到 Count 属性：

Contract.Ensures(Contract.Result<int>() == backEndCollection.Count);

来源：

http://social.msdn.microsoft.com/Forums/en/codecontracts/thread/cadd0c05-144e-4b99-b7c3-4869c46a95a2

http://social.msdn.microsoft.com/Forums/en-US/codecontracts/thread/acb3e1d8-8239-4b66-b842-85a1a9509d1e/

【讨论】：