Dan*_*ant 9 c# static-analysis code-contracts
假设我有一个自定义集合类,它提供了一些内部线程同步.例如,简化的Add方法可能如下所示:
public void Add(T item)
{
_lock.EnterWriteLock();
try
{
_items.Add(item);
}
finally
{
_lock.ExitWriteLock();
}
}
Run Code Online (Sandbox Code Playgroud)
最新的Code Contracts抱怨说CodeContracts: ensures unproven: this.Count >= Contract.OldValue(this.Count).问题是这真的无法证明.我可以确保在内部锁定内,Count将大于其先前的值.但是,在方法的退出处,我无法确保这一点.退出锁之后,在方法完成之前,另一个线程可以发出两个Removes(可能是不同的元素),使合同无效.
这里的基本问题是,只有在整个应用程序中一致地使用锁定以对集合进行所有访问时,才能认为集合合同在特定锁定上下文中是有效的.我的集合必须在多个线程中使用(非冲突的Add和Remove是一个有效的用例),但我仍然希望实现ICollection<T>.即使我知道我不能,我是否应该假装我能够满足这个确保要求的假设?令我印象深刻的是,BCL系列中没有一个能够真正确保这一点.
编辑:
基于一些进一步的调查,听起来最大的问题是合同重写者可能引入不正确的断言,导致运行时失败.基于此,我认为我唯一的选择是限制我的接口实现IEnumerable<T>,因为合同ICollection<T>暗示实现类不能提供内部线程同步(访问必须始终在外部同步.)这对我的特定情况是可接受的(所有客户端)希望改变集合直接了解类类型,但我很想知道是否有其他解决方案.
正如您所暗示的,没有实施者可以履行该合同。事实上,通常面对多线程,除非契约可以像这样应用:
Take Lock
gather Old Stuff
work
check Contract, which may compare Old Stuff
Release Lock
Run Code Online (Sandbox Code Playgroud)
我不明白如何履行任何合同。从我这里可以看到,这是一个尚未完全烘烤的区域。
我认为使用 Assume 是你能做的最好的事情,实际上你是在说“通过调用 Add 我正在做合同期望的事情”。