集合合约和线程

Question

假设我有一个提供一些内部线程同步的自定义集合类。例如，简化的 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 上的约定意味着实现类无法提供内部线程同步（访问必须始终在外部同步。）这对于我的特殊情况是可以接受的（所有希望直接改变集合的客户端都知道类类型），但我绝对有兴趣听到是否有其他解决方案这。

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 等小整数类型进行测试。确保使用不会引发溢出的整数类型。