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)
  • Clear: 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. StringCollectionを使用する

解決策は、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 に答える