代码合同失败示例 Graph.Remove(Edge e)

Question

这是一个简单的图形操作方法，我用代码契约修饰了它。

确保声明无法证明，但我不明白为什么！我相信它声称在调用 Remove() 之后，边缘不再在边缘列表中，或者结果为假。如果结果为真，它不会声明图的状态。静态检查器不喜欢它，我还没有让 Pex 告诉我如何使用它（尽管我可能只是不知道如何使用它）。

我相信这个例子中的锁是无关紧要的，但我会留下它以防万一。此外， OnRemoveEdge 的委托没有任何保证，但我现在隐含地假设它不会重新进入 Graph 代码。此外，假设在它之后。

public bool Remove(E edge)
{
  Contract.Requires(edge != null);
  Contract.Ensures(!Contract.Exists(edges, e => e == edge) || !Contract.Result<bool>());

  lock (sync)
  {
    if (!OnBeforeRemoveEdge(edge)) return false;

    if (!edges.Remove(edge)) return false;
  }

  OnRemoveEdge(edge);

  Contract.Assume(!Contract.Exists(edges, e => e == edge));

  return true;
}

更新：我更改了代码以将事件处理程序 OnRemoveEdge()（但不是委托 OnBeforeRemoveEdge）移出锁定。但是，这对合约与线程相关的假设有什么作用呢？代码契约是否假设为单线程模型？嗯。

Answer 1

来自Jack Leitch's answer to a similar question：

Code Contracts User Manual 声明：“静态合约检查器尚未处理量词 ForAll 或 Exists。”

没错。真的。