6

ここで何か間違ったことをしているのか、それとも修正する必要があるのか​​わかりません...

カスタムのDictionaryラッパークラスがあります。これが必要なコードのスニペットです。

public int Count
{
    get
    {
        Contract.Ensures(Contract.Result<int>() >= 0);

        return InternalDictionary.Count;
    }
}

public bool ContainsKey(TKey key)
{
    //This contract was suggested by the warning message, if I remove it
    //I still get the same warning...
    Contract.Ensures(!Contract.Result<bool>() || Count > 0);

    return InternalDictionary.ContainsKey(key);
}

[ContainsKey]の行を追加した唯一の理由は、次の警告メッセージが表示されたためです（まだ表示されています）Codecontracts: ensures unproven: !Contract.Result<bool>() || @this.Count > 0。この行を削除しても、同じ問題が発生する可能性があります。

これらの問題を取り除くためにここで何をしますか？

アップデート：

私も試しました（提案されたように）...

public Boolean ContainsKey(TKey key)
{
    Contract.Requires(Count == 0 || InternalDictionary.ContainsKey(key));
    Contract.Ensures(!Contract.Result<bool>() || Count > 0);

    return InternalDictionary.ContainsKey(key);
}

警告5メソッド'My.Collections.Generic.ReadOnlyDictionary2.ContainsKey 2.ContainsKey(type parameter.TKey)' implements interface method 'System.Collections.Generic.IDictionary（type parameter.TKey）'、したがって、Requiresを追加できません。

4

2 に答える 2

5

「カスタムディクショナリラッパークラスがあります」-を実装しIDictionary<TKey, TValue>ます。インターフェイスメソッドはコントラクトを指定でき、それらを実装するクラスメソッドはコントラクトを満たす必要があります。この場合、IDictionary<TKey, TValue>.ContainsKey(TKey)あなたが求めている契約があります：

Contract.Ensures(!Contract.Result<bool>() || this.Count > 0);

論理的には、 （を意味する）!a || bと読むことができ、それを使用して、これを英語に翻訳することができます。a ===> bab

If ContainsKey() returns true, the dictionary must not be empty.

これは完全に賢明な要件です。空の辞書は、キーが含まれていると主張してはなりません。これはあなたが証明する必要があるものです。

これは、等しいという実装の詳細が他のメソッドが信頼できることを保証するものであることを約束するために追加するサンプルDictionaryWrapperクラスです。と同様の機能を追加して、契約も検証可能にします。Contract.EnsuresCountinnerDictionary.CountContract.EnsuresContainsKeyIDictionary<TKey, TValue>.TryGetValue

public class DictionaryWrapper<TKey, TValue> : IDictionary<TKey, TValue>
{
    IDictionary<TKey, TValue> innerDictionary;

    public DictionaryWrapper(IDictionary<TKey, TValue> innerDictionary)
    {
        Contract.Requires<ArgumentNullException>(innerDictionary != null);
        this.innerDictionary = innerDictionary;
    }

    [ContractInvariantMethod]
    private void Invariant()
    {
        Contract.Invariant(innerDictionary != null);
    }

    public void Add(TKey key, TValue value)
    {
        innerDictionary.Add(key, value);
    }

    public bool ContainsKey(TKey key)
    {
        Contract.Ensures(Contract.Result<bool>() == innerDictionary.ContainsKey(key));
        return innerDictionary.ContainsKey(key);
    }

    public ICollection<TKey> Keys
    {
        get
        {
            return innerDictionary.Keys;
        }
    }

    public bool Remove(TKey key)
    {
        return innerDictionary.Remove(key);
    }

    public bool TryGetValue(TKey key, out TValue value)
    {
        return innerDictionary.TryGetValue(key, out value);
    }

    public ICollection<TValue> Values
    {
        get
        {
            return innerDictionary.Values;
        }
    }

    public TValue this[TKey key]
    {
        get
        {
            return innerDictionary[key];
        }
        set
        {
            innerDictionary[key] = value;
        }
    }

    public void Add(KeyValuePair<TKey, TValue> item)
    {
        innerDictionary.Add(item);
    }

    public void Clear()
    {
        innerDictionary.Clear();
    }

    public bool Contains(KeyValuePair<TKey, TValue> item)
    {
        return innerDictionary.Contains(item);
    }

    public void CopyTo(KeyValuePair<TKey, TValue>[] array, int arrayIndex)
    {
        innerDictionary.CopyTo(array, arrayIndex);
    }

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

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

    public bool Remove(KeyValuePair<TKey, TValue> item)
    {
        return innerDictionary.Remove(item);
    }

    public IEnumerator<KeyValuePair<TKey, TValue>> GetEnumerator()
    {
        return innerDictionary.GetEnumerator();
    }

    IEnumerator IEnumerable.GetEnumerator()
    {
        return innerDictionary.GetEnumerator();
    }
}
于 2012-02-28T21:28:44.847 に答える
1

率直に言って、契約のポイントがわかりません。契約は

 Contract.Ensures(!Contract.Result<bool>() || Count > 0);

何を言おうとしているのですか？辞書にキーが含まれていることや、辞書に値が含まれていることを保証することはできません。したがって、この契約は常に満たされるとは限りません。それが検証者があなたに言っていることです：あなたが真実であると約束しているこの声明が真実であることを証明することはできません。

戻り値がであるtrueか、または戻り値がゼロより大きいかゼロに等しいことを確認できる最善の方法しかし、そのような契約のポイントは何ですか？発信者はすでにこれを知っています。falseCount

それを考えると、私はここでの契約をまったく気にしません。

于 2011-09-14T16:57:24.503 に答える