Контракты на код: гарантированно недоказан и требует недоказан - PullRequest
Новая
       12

Контракты на код: гарантированно недоказан и требует недоказан

6 голосов
/ 14 сентября 2011

Я не уверен, что я делаю что-то здесь не так или это нужно исправить ...

У меня есть собственный класс-обертка для словаря, и вот фрагмент кода, который необходим. 

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.ReadOnlyDictionary 2.ContainsKey(type parameter.TKey)' implements interface method 'System.Collections.Generic.IDictionary 2.ContainsKey (type parameter.TKey)', поэтому добавить его нельзя Требуется.

Ответы [ 2 ]

5 голосов
/ 29 февраля 2012

«У меня есть пользовательский класс-оболочка для словаря», который реализует IDictionary<TKey, TValue>.Методы интерфейса могут указывать контракты, а методы класса, которые их реализуют, должны соответствовать контрактам.В этом случае у IDictionary<TKey, TValue>.ContainsKey(TKey) есть контракт, о котором вы спрашиваете: 

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

Логически, !a || b может читаться как a ===> b (a подразумевает b), и с использованием этогомы можем перевести это на английский: 

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

Это вполне разумное требование.Пустой словарь не должен претендовать на то, чтобы содержать ключи. Это - это то, что вам нужно доказать.

Вот пример DictionaryWrapper класса, который добавляет Contract.Ensures, чтобы пообещать, что детали реализации Count, равные innerDictionary.Count, являютсяЖесткая гарантия того, что другие методы могут положиться.Он добавляет Contract.Ensures к ContainsKey, так что контракт IDictionary<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();
    }
}
1 голос
/ 14 сентября 2011

Честно говоря, я не понимаю суть контракта. Контракт составляет 

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

Что ты пытаешься сказать? Вы не можете гарантировать, что словарь содержит ключ, или что словарь вообще содержит какие-либо значения. Так что этот контракт не всегда может быть выполнен. Вот что говорит вам верификатор: он не может доказать, что это утверждение, которое вы обещаете быть верным, истинно.

Лучше всего убедиться, что возвращаемое значение равно true или возвращаемое значение равно false и что Count больше нуля или равно нулю Но какой смысл такого контракт? Вызывающий уже знает это.

Учитывая это, я бы вообще не стал беспокоиться о контракте.

...