Кодовые контракты с предупреждениями при реализации 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 >= Contract.OldValue(this.Count)
• Очистить: CodeContracts: обеспечивает недоказанность: this.Count == 0
• Содержит: CodeContracts: обеспечивает недоказанность: !Contract.Result<bool>() || this.Count > 0
• CopyTo: CodeContracts: требуется недоказанное: arrayIndex + this.Count <= array.Length

Как мне это исправить? Есть какой-то способ просто подавить это?

Answer 1

Не уверен, что я следую за вопросом, но я попробовал следующий код (реализовал все необходимые интерфейсы) и MyCollection myCollection = new MyCollection {"test"};работал нормально.Если у вас все еще есть проблемы, попробуйте объяснить немного больше, что вы сделали.

РЕДАКТИРОВАТЬ: Помимо моего ответа на вопрос, я хотел бы сделать следующее примечание для тех, ктовыполняем первые шаги с использованием контрактов кода.

Чтобы контракты кода отображали предупреждения, должна быть активна статическая проверка (Свойства проекта -> Контракты кода -> Выполнить статическую проверку контракта), которая доступна только в случае премиум-контракта кода.(не стандартная) редакция устанавливается в Visual Studio 2010 Premium или в Team System 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. Вместо реализации ICollection, присущей Collection;
3. Использовать StringCollection

Решения были взяты из сообщения на форуме DevLabs: Проблемы со статической проверкой и оберткой вокруг общего списка .

РЕДАКТИРОВАТЬ 3 (от Allrameest):

1. Добавлено Contract.Ensures(Contract.Result<int>() == backEndCollection.Count); в свойство Count, о котором упоминается KoMet.
2. В метод CopyTo добавлено Contract.Assume(arrayIndex + Count <= array.Length);.
3. Удалено Contract.Assert(_inner.Count == 0); из метода Clear.

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/en-US/codecontracts/thread/acb3e1d8-8239-4b66-b842-85a1a9509d1e/