Collection Contracts and Threading

Suppose I have a custom collection class that provides some internal thread synchronization. For instance, a simplified Add method might look like this:

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

The latest Code Contracts complains that CodeContracts: ensures unproven: this.Count >= Contract.OldValue(this.Count). The problem is that this really can't be proven. I can ensure that, internally, within the lock, Count will be greater than its previous value. I cannot ensure this, however, at the exit of the method. After the lock is exited and before the method completes, another thread could issue two Removes (likely of different elements), invalidating the contract.

The fundamental issue here is that the collection contracts can only be considered valid from within a particular locking context and only if the locking is used consistently throughout the application for all access to the collection. My collection must be used from multiple threads (with non-conflicting Add and Remove being a valid use case), but I would still like to implement ICollection<T>. Should I simply pretend that I can meet this ensures requirement with an Assume, even though I know I can't? It strikes me that none of the BCL collections can actually ensure this either.

EDIT:

Based on some further investigation, it sounds like the biggest issue is that the contract rewriter can introdu开发者_StackOverflowce incorrect assertions, leading to runtime failures. Based on this, I think my only option is to restrict my interface implementation to IEnumerable<T>, as the contract on ICollection<T> implies that the implementing class cannot provide internal thread synchronization (access must always be synchronized externally.) This is acceptable for my particular case (all clients that wish to mutate the collection know about the class type directly), but I'm definitely interested to hear if there are other solutions to this.

As you imply, no implementer can meet this contract. Indeed generally in the face of multi-threading unless the contract can be applied like:

 Take Lock
 gather Old Stuff

 work

 check Contract, which may compare Old Stuff
 Release Lock

I don't see how any contract could be honoured. From what I can see here this is an area that's not fully baked yet.

I think that using an Assume is the best you can do, in effect you are saying "by calling Add I am doing what the contract expects".

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);
        }
    }
}

Warning: do not use grater than less than comparisons; The counts will overflow, but these contracts should work in that case. Test with a small integer type like int8. Make sure to use an integer type that does not throw on overflow.