Why won't this Code Contracts relationship prove?

Question

I have a method that starts like this:

    public static UnboundTag ResolveTag(Type bindingType, string name, string address)
    {
        Contract.Requires(bindingType != null);

        var tags = GetUnboundTagsRecursively(bindingType).ToArray();

The contract for the implementation of GetUnboundTagsRecursively (implemented in the same class) looks like this:

    public static IEnumerable<UnboundTag> GetUnboundTagsRecursively(Type bindingType)
    {
        Contract.Requires(bindingType != null);
        Contract.Ensures(Contract.Result<IEnumerable<UnboundTag>>() != null);

The static analyzer is indicating a failure on the tags assignment line of ResolveTag with the message "requires unproven: source != null". I've looked through this several times and I can't figure out why this would be. I'm assuming this is a reference to the source parameter for the extension method ToArray(). My method states that it ensures that the result is not null, so this would seem to imply that the source for ToArray() is also not null. What am I missing?

---

Additional info: the method returning the IEnumerable is implemented with yield return calls. I'm wondering if maybe the enumerator magic is messing with code contracts somehow...

I just tried changing the implementation to return an empty array rather than using yield return and that passes the contracts, so apparently it's an issue with method using yield return. Does anybody know a way around this?

---

I took a look at the IL for the Contracts DLL and it's actually putting the contracts calls in MoveNext() for the enumerator implementation:

.method private hidebysig newslot virtual final 
        instance bool  MoveNext() cil managed
{
  .override [mscorlib]System.Collections.IEnumerator::MoveNext
  // Code size       410 (0x19a)
  .maxstack  3
  .locals init ([0] bool V_0,
           [1] int32 V_1)
  .try
  {
    IL_0000:  ldarg.0
    IL_0001:  ldfld      int32 PLCLink.Bind.UnboundTag/'<GetUnboundTagsRecursively>d__c'::'<>1__state'
    IL_0006:  stloc.1
    IL_0007:  ldloc.1
    IL_0008:  ldc.i4.0
    IL_0009:  beq.s      IL_0024
    IL_000b:  ldloc.1
    IL_000c:  ldc.i4.3
    IL_000d:  sub
    IL_000e:  switch     ( 
                          IL_00cd,
                          IL_018d,
                          IL_0162)
    IL_001f:  br         IL_018d
    IL_0024:  ldarg.0
    IL_0025:  ldc.i4.m1
    IL_0026:  stfld      int32 PLCLink.Bind.UnboundTag/'<GetUnboundTagsRecursively>d__c'::'<>1__state'
    IL_002b:  ldarg.0
    IL_002c:  ldfld      class PLCLink.Bind.IUnboundTagGroup PLCLink.Bind.UnboundTag/'<GetUnboundTagsRecursively>d__c'::group
    IL_0031:  ldnull
    IL_0032:  ceq
    IL_0034:  ldc.i4.0
    IL_0035:  ceq
    IL_0037:  call       void [mscorlib]System.Diagnostics.Contracts.Contract::Requires(bool)
    IL_003c:  call       !!0 [mscorlib]System.Diagnostics.Contracts.Contract::Result<class [mscorlib]System.Collections.Generic.IEnumerable`1<valuetype PLCLink.Bind.UnboundTag>>()

This is interesting, as the Contract.Result call is actually using the wrong type (since MoveNext returns a bool).

Answer 1

I suspect it's because the contract calls are ending up in the MoveNext() of the generated iterator implementation type. Try this:

public static IEnumerable<UnboundTag> GetUnboundTagsRecursively
   (Type bindingType)
{
    Contract.Requires(bindingType != null);
    Contract.Ensures(Contract.Result<IEnumerable<UnboundTag>>() != null);
    return GetUnboundTagsRecursivelyImpl(bindingType);
}

private static IEnumerable<UnboundTag> GetUnboundTagsRecursivelyImpl
    (Type bindingType)
{
    // Iterator block code here
}

Now you may need to do a bit of extra work to get those methods to compile without any contract violations. For example:

public static IEnumerable<UnboundTag> GetUnboundTagsRecursively
   (Type bindingType)
{
    Contract.Requires(bindingType != null);
    Contract.Ensures(Contract.Result<IEnumerable<UnboundTag>>() != null);
    IEnumerable<UnboundTag> ret = GetUnboundTagsRecursivelyImpl(bindingType);
    // We know it won't be null, but iterator blocks are a pain.
    Contract.Assume(ret != null);
    return ret;
}

This is slightly inefficient as it will perform the nullity check twice. It's also effectively just suppressing the warning via Assume.

I wouldn't be surprised to hear that the code contracts team are working on fixing this... I think I've heard about something similar, but I can't remember the details. The release notes for the September 2009 release include:

Initial support for contracts on iterators

... but assuming you're using a recent release, presumably that initial support isn't enough :)