6

我有这个代码：

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

我该如何解决这些问题？有什么办法可以压制这些吗？

4

2 回答 2

4

不确定我是否遵循了这个问题，但我尝试了以下代码（实现了所有必需的接口）和 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. 使用字符串集合

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

编辑 3（由 Allrameest 提供）：

  1. 添加Contract.Ensures(Contract.Result<int>() == backEndCollection.Count);到 KoMet 提示的 Count 属性中。
  2. 添加Contract.Assume(arrayIndex + Count <= array.Length);到 CopyTo 方法。
  3. Contract.Assert(_inner.Count == 0);从 Clear 方法中删除。
于 2011-03-28T13:08:43.310 回答
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/

于 2011-03-30T12:44:09.017 回答