locked
Why is Contract.Assume(this.List.GetEnumerator() != null); not helping indicate that the return value is not null?

    Question

  • In the following code:

    public

    IEnumerator<T> GetEnumerator()
    {
      Contract.Assume(this.List.GetEnumerator() != null);
      return this.List.GetEnumerator();
    }
    Wednesday, January 6, 2010 1:26 PM

Answers

  • Hi,

    Because you're not using it to indicate that the return value of your method is not null, you're using it to indicate that the return value of this.List.GetEnumerator() is not null and assuming that it's a deterministic method, at least for two sequential calls; i.e., you're assuming that if the first invocation returns a non-null value then the second invocation will as well.  Code Contracts won't follow that assumption (and rightfully so - it could be wrong depending upon the implementation of this.List.)

    Try the following instead:

    public IEnumerator<T> GetEnumerator()
    {
      var result = this.List.GetEnumerator();
      Contract.Assume(result != null);
      return result;
    }

    - Dave
    http://davesexton.com/blog
    • Marked as answer by Franck Jeannin Thursday, January 7, 2010 1:34 PM
    Wednesday, January 6, 2010 6:06 PM

All replies

  • Hi,

    Because you're not using it to indicate that the return value of your method is not null, you're using it to indicate that the return value of this.List.GetEnumerator() is not null and assuming that it's a deterministic method, at least for two sequential calls; i.e., you're assuming that if the first invocation returns a non-null value then the second invocation will as well.  Code Contracts won't follow that assumption (and rightfully so - it could be wrong depending upon the implementation of this.List.)

    Try the following instead:

    public IEnumerator<T> GetEnumerator()
    {
      var result = this.List.GetEnumerator();
      Contract.Assume(result != null);
      return result;
    }

    - Dave
    http://davesexton.com/blog
    • Marked as answer by Franck Jeannin Thursday, January 7, 2010 1:34 PM
    Wednesday, January 6, 2010 6:06 PM
  • You are absolutely rigth, your suggestion solved the problem (and Code Contracts cannot make the assumption I was implying). I look forward to a version of the Framework making more garanties like this one.
    • Marked as answer by Franck Jeannin Thursday, January 7, 2010 1:34 PM
    • Unmarked as answer by Franck Jeannin Thursday, January 7, 2010 1:34 PM
    Thursday, January 7, 2010 1:33 PM
  • What is the type of your "List" ? We typically do make the assumption that GetEnumerator should return non-null. Now it could be that some implementations don't derive from IEnumerable/IEnumerable<T> and that may be the problem here.
    Cheers, -MaF (Manuel Fahndrich)
    Thursday, January 14, 2010 1:44 AM
  • My list simply contains a List<T> and implements

    public

     

    IEnumerator<T> GetEnumerator()

    {

     

    return this.list.GetEnumerator();

    }

    Thursday, January 14, 2010 9:00 AM
  • When I try your example, I don't seem to need an assumption, as the contract on List.GetEnumerator already guarantees that it is non-null. Is this on VS2008 or VS2010? Which version of the tools are you using (see the Contract pane top right).
    Cheers, -MaF (Manuel Fahndrich)
    Thursday, January 14, 2010 4:11 PM
  • I'm still getting the same message

    Warning 71 CodeContracts: ensures unproven: Contract.Result<IEnumerator<T>>() != null 

    even with build 1.2.30113.1 (I'm using VSTS 2008)
    Thursday, January 14, 2010 4:28 PM
  • Okay, I need a full repro in that case (ideally small). If you don't want to post the code, you can also zip it up and send it to codconfb@microsoft.com.

    Thanks.

    Cheers, -MaF (Manuel Fahndrich)
    Thursday, January 21, 2010 12:10 AM