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

Question

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

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

我相信，对于这个例子来说，锁是无关紧要的，但为了以防万一，我会保留它。另外，OnRemoveEdge 的委托没有任何保证，但我现在隐式假设它不会重新进入图形代码。此外，假设是在它之后。

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 对类似问题的回答：

代码合同用户手册指出，“静态合约检查器尚未处理量词 ForAll 或 Exists。”

真的。真的。