Контракты коллекции и потоки

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

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

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

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

РЕДАКТИРОВАТЬ:

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