代码之家 › 专栏 › 技术社区 › Dan Bryant

收集合同和线程

code-contracts static-analysis c#

9

Dan Bryant · 技术社区 · 14 年前

假设我有一个自定义集合类,它提供一些内部线程同步。例如,一个简化的添加方法可能如下所示:

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

最新的代码合同抱怨 CodeContracts: ensures unproven: this.Count >= Contract.OldValue(this.Count) . 问题是这真的无法被证明。我可以确保在锁内部,计数将大于它以前的值。但是,在方法的出口,我不能保证这一点。在退出锁之后,在方法完成之前,另一个线程可以发出两个移除(可能是不同元素的移除),从而使契约无效。

这里的基本问题是,只有在特定的锁定上下文中,并且只有在整个应用程序中一致地使用锁来访问集合时,才能将收集合同视为有效的。必须从多个线程使用我的集合(添加和删除不冲突是一个有效的用例),但我仍然希望实现 ICollection<T>

编辑:

根据进一步的调查,听起来最大的问题是合同重写器可能引入错误的断言,从而导致运行时失败。基于此,我认为我唯一的选择是将接口实现限制为 IEnumerable<T> ,作为合同 i收集<t> 这意味着实现类不能提供内部线程同步(访问必须始终在外部同步)。对于我的特定情况,这是可以接受的(所有希望直接改变集合的客户机都知道类类型),但如果有其他解决方案,我肯定会感兴趣。

2 回复 | 直到 12 年前

1

2

djna 14 年前

 Take Lock
 gather Old Stuff

 work

 check Contract, which may compare Old Stuff
 Release Lock

here

2

0

ctrl-alt-delor 12 年前

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