使用支持集合实现 ICollection 时代码契约警告

Question

我有这个代码：

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＆gt;= Contract.OldValue（this.Count）
• 清除：CodeContracts：确保未经证实：this.Count == 0
• 包含：CodeContracts：确保未经验证：!Contract.Result() || this.Count > 0
• CopyTo：CodeContracts：需要未经验证：arrayIndex + this.Count <= array.Length

如何修复这些问题？有什么办法可以抑制这些吗？

Answer 1

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

编辑：
除了我对这个问题的回答之外，我还想为那些迈出代码契约第一步的人做以下说明。

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

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：

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

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

解决方案取自 DevLabs 论坛帖子：静态检查器和包装器的问题通用列表。

编辑3（由Allrameest）：

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

Answer 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/zh-CN/codecontracts/thread/acb3e1d8-8239-4b66-b842-85a1a9509d1e/