爲什麼這個代碼合同關係證明不了？

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月發行版包括：對合同上的迭代器

初步支持......但假設你使用的是最新版本，據推測，最初的支持是不夠的:)