为什么这个代码合同关系证明不了？

Question

我有开始这样的方法：

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

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

为GetUnboundTagsRecursively的实现（在同一个类中实现）的合同是这样的：

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

静态分析仪表示失败在ResolveTag的标签分配行上，并显示消息"requires unproven: source != null"。我已经看了好几遍，但我无法弄清楚为什么会这样。我假设这是对source参数的扩展方法ToArray()的参考。我的方法声明它确保结果不为空，所以这似乎意味着ToArray()的源也不为空。我错过了什么？

---

附加信息：返回IEnumerable的方法使用yield return调用实现。我想知道如果也许统计数字魔法是搞乱代码合同莫名其妙...

我只是试图改变实现返回一个空数组，而不是使用收益率回报，并通过合同，所以显然这是一个问题方法使用收益率回报。有人知道解决这个问题的方法吗？

---

我接过一看IL的合同DLL，它实际上是把合同调用的MoveNext（）来枚举实现：

.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>>() 

这很有趣，因为Contract.Result调用实际上是使用了错误的类型（因为MoveNext返回一个布尔值）。

Answer 1

我嫌疑人这是因为合同调用结束于生成的迭代器实现类型的MoveNext()。试试这个：

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 
} 

现在，你可能需要做一些额外的工作来获取这些方法没有任何违反合同编译。例如：

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

这样做效率稍低，因为它会执行两次无效检查。这也有效地通过Assume来抑制警告。

我不会惊讶地听到代码合同团队正在解决这个问题......我想我听说过类似的东西，但我不记得细节。该release notes为2009年9月发行版包括：对合同上的迭代器

初步支持......但假设你使用的是最新版本，据推测，最初的支持是不够的:)