locked
False Negative in Pex-Generated Test in QuickGraph RRS feed

  • Question

  •  

     

    Hello, everyone. I have a perplexing interaction between contracts, pex, and quickgraph and would be very grateful for advice from the more knowledgeable. I have boiled it down to a repro case where commenting out one contract makes the false negative go away, but I have been unable to diagnose it with the debugger in the time allowed because the subject code (quickgraph) has side-effects in property-getters, meaning that the debugger executes the side effects when displaying the values of the properties, interfering with the actual order of execution. 

    First a little background, then the specifics, then a pointer to a project to download and try out, should you be so inclined as to dig in! 

    I installed Pex & Moles 

    http://research.microsoft.com/en-us/projects/pex/downloads.aspx

    and CodeContracts for .NET 4.0

    http://research.microsoft.com/en-us/projects/contracts/

    I downloaded, via nuget, the most recent version of QuickGraph, which is all built for .NET 3.5. 

    http://quickgraph.codeplex.com/releases/view/55262 

    I pruned it to the minimum I needed, went into Project Properties for all, updated them all to .NET 4.0 from .NET 3.5 Client Profile, fixed one source breaking change (which was trivial and very, very unlikely to have any connection to my problem). I then went to the Code Contracts tab on every project page and enabled all static and dynamic options.

    The project has 192 unit tests, many of them Pex-generated (very nice!). To run the tests, get my project zip file from

    http://dl.dropbox.com/u/1997638/QuickGraph.zip

    Make sure you have Pex & Moles and Contracts from the links above. Open the solution, Rebuild everything, then, at the solution level, "Run All Tests In Solution" (control-R, A). All will pass. Then go to line 49 of IImplicitUndirectedGraphContracts.cs and uncomment the Contract under the large comment (inserted by me). One test, Prim12240WithDelegate will fail.

    That test exercises a graph constructor that builds edges on-the-fly by calling a user-supplied delegate in the property-getters for Edges and EdgeCount. Cute. But something goes wrong with the Contract on line 49 of IImplicitUndirecteGraphContracts.cs. 

    This is a false negative, because if I comment out this contract, the test passes. In trying to follow this in the debugger, it has something to do with the timing of the creation of the Edges in the property getters. I haven't been able to disentangle this, however, because the debugger calls these getters, the subject code calls them, the contracts code calls them, maybe statically, maybe dynamically, I just plain got lost trying to follow it, and thought I'd bring the question up to those who understand the details of contract execution better than I.

    Here is the offending contract; commenting it out makes the unit test succeed:

     

     [Pure]
     IEnumerable<TEdge> IImplicitUndirectedGraph<TVertex, TEdge>.AdjacentEdges(TVertex v)
     {
      IImplicitUndirectedGraph<TVertex, TEdge> ithis = this;
      Contract.Requires(v != null);
      Contract.Requires(ithis.ContainsVertex(v));
      Contract.Ensures(Contract.Result<IEnumerable<TEdge>>() != null);
    ~~~~~~> Contract.Ensures(
       Enumerable.All(
        Contract.Result<IEnumerable<TEdge>>(),
        edge => 
         edge != null && 
         ithis.ContainsEdge(edge.Source, edge.Target) && 
         (edge.Source.Equals(v) || edge.Target.Equals(v))
        )
       );
      return default(IEnumerable<TEdge>);
     }
    

     

     

     

    • Edited by rebcabin Sunday, January 30, 2011 8:09 PM removed redundant link
    Sunday, January 30, 2011 8:01 PM

All replies