0

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

确保声明无法证明，但我不明白为什么！我相信它声称在调用 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）移出锁定。但是，这对合约与线程相关的假设有什么作用呢？代码契约是否假设为单线程模型？嗯。

4

1 回答 1

1

来自Jack Leitch 对类似问题的回答：

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

真的。真的。

于 2011-02-03T17:25:53.283 回答