Контракты на сбор и оформление

Question

Предположим, у меня есть собственный класс коллекции, который обеспечивает некоторую внутреннюю синхронизацию потоков. Например, упрощенный метод Add может выглядеть следующим образом:

    public void Add(T item)
    {
        _lock.EnterWriteLock();
        try
        {
            _items.Add(item);
        }
        finally
        {
            _lock.ExitWriteLock();
        }
    }

Последний Кодекс Контрактов жалуется, что CodeContracts: ensures unproven: this.Count >= Contract.OldValue(this.Count). Проблема в том, что это действительно невозможно доказать. Я могу гарантировать, что внутри блокировки Count будет больше, чем его предыдущее значение. Я не могу гарантировать это, однако, на выходе из метода. После выхода из блокировки и до завершения метода другой поток может выполнить два удаления (вероятно, из разных элементов), что делает контракт недействительным.

Фундаментальная проблема здесь заключается в том, что контракты на коллекцию могут считаться действительными только в пределах определенного контекста блокировки и только в том случае, если блокировка используется последовательно во всем приложении для всего доступа к коллекции. Моя коллекция должна использоваться из нескольких потоков (при этом не конфликтующие Add и Remove являются допустимым вариантом использования), но я все же хотел бы реализовать ICollection<T>. Должен ли я просто притворяться, что могу выполнить это требование с помощью Ассума, хотя знаю, что не могу? Меня поражает, что ни одна из коллекций BCL на самом деле не может этого гарантировать.

---

EDIT:

Судя по некоторым дальнейшим исследованиям, самая большая проблема заключается в том, что переписчик контрактов может вводить неверные утверждения, что приводит к сбоям во время выполнения. Исходя из этого, я думаю, что мой единственный вариант - ограничить реализацию моего интерфейса IEnumerable<T>, поскольку контракт на ICollection<T> подразумевает, что реализующий класс не может обеспечить синхронизацию внутреннего потока (доступ всегда должен быть синхронизирован извне.) Мой конкретный случай (все клиенты, которые хотят изменить коллекцию, знают о типе класса напрямую), но мне определенно интересно узнать, есть ли другие решения для этого.

Answer 1

Как вы подразумеваете, ни один исполнитель не может выполнить этот контракт.На самом деле, как правило, в условиях многопоточности, если только контракт не может быть применен, например:

 Take Lock
 gather Old Stuff

 work

 check Contract, which may compare Old Stuff
 Release Lock

Я не понимаю, как можно выполнить любой контракт.Из того, что я вижу здесь это область, которая еще не полностью выпечена.

Я думаю, что использование Assume - лучшее, что вы можете сделать, в сущности, вы говорите ", вызывая AddЯ делаю то, что ожидает контракт ".

Answer 2

using System.Diagnostics.Contracts;

namespace ConsoleApplication1
{
    class Class1
    {
        public int numberOfAdds    { get; private set; }
        public int numberOfRemoves { get; private set; }
        public int Count
        {
            get
            {
                return numberOfAdds - numberOfRemoves;
            }
        }

        public void Add()
        {
            Contract.Ensures(numberOfAdds == Contract.OldValue(numberOfAdds) + 1);
        }

        public void Remove()
        {
            Contract.Requires(Count >= 1);
            Contract.Ensures(numberOfRemoves == Contract.OldValue(numberOfRemoves) + 1);
        }

        [ContractInvariantMethod]
        void inv()
        {
            Contract.Invariant(Contract.Result<int>() == numberOfAdds - numberOfRemoves);
        }
    }
}

Предупреждение: не используйте терку меньше, чем сравнения;Количество будет переполнено, но эти контракты должны работать в этом случае.Тест с маленьким целочисленным типом как int8.Убедитесь, что вы используете целочисленный тип, который не выбрасывает при переполнении.