Code Contracts failing example Graph.Remove(Edge e)

Question

Here's a simple graph manipulation method which I have decorated with Code Contracts.

The ensures claim won't prove but I can't see why! I believe it claims that after calling Remove(), either the edge is no longer in the edges list OR the result is false. It claims nothing about the state of the graph if the result is true. The static checker doesn't like it and I haven't gotten Pex to tell me how (though I probably just don't know how to use it).

The lock is extraneous for this example, I believe, but I'll leave it just in case. Also, the delegate for OnRemoveEdge has no guarantees, but I'll implicitly assume for now that it is not re-entrant into the Graph code. Besides, the Assumption is after it.

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

Update: I changed the code to move the Event handler, OnRemoveEdge(), (but not the delegate, OnBeforeRemoveEdge) out of the lock. But then, what does this do for the contract's assumption related to threads? Does Code Contracts assume a single-threaded model? Hmmm.

Answer 1

From Jack Leitch's answer to a similar question:

The Code Contracts User Manual states, "The static contract checker does not yet deal with quantifiers ForAll or Exists."

True. true.