代碼合同和異步

Question

將後置條件添加到返回Task<T>的異步方法的推薦方法是什麼？

我已閱讀以下建議：

http://social.msdn.microsoft.com/Forums/hu-HU/async/thread/52fc521c-473e-4bb2-a666-6c97a4dd3a39

的交建議實現每個方法同步，收縮它，然後執行一個異步對方作爲一個簡單的包裝。不幸的是，我不認爲這是一個可行的解決方案（也許通過我自己的誤解）：

1. 的異步方法，但假定爲同步方法的包裝，是留給沒有任何真正的代碼合同，因此按照自己的意願去做。
2. 致力於異步的代碼庫不太可能實現所有事物的同步對應。因此，在其他異步方法中實施包含await的新方法因此被迫爲異步。這些方法本質上是異步的，不能輕易轉換爲同步。它們不僅僅是包裝。

即使我們說我們可以使用的await.Result或.Wait()，而不是無效後一點（這實際上會導致一些SyncContext s到僵局，並且將不得不重新編寫的異步方法反正）我仍然相信第一點。

有沒有其他的想法，或者有什麼我錯過了代碼合同和TPL？

Answer 1

我已經向其他人指出了這一點。目前，Contracts和Async是（幾乎）相互排斥的。所以，至少有一些微軟的人知道這個問題，但我不知道他們打算怎麼做。

我不建議將異步方法編寫爲同步方法的包裝。事實上，我傾向於做相反的事情。

先決條件可以工作。我最近沒有嘗試過;您可能需要圍繞包含前提條件的異步方法進行小包裝。

後續條件已經非常糟糕。

斷言和假設可以正常工作，但靜態檢查器是非常有限的，因爲後置條件被破壞。

不變量在異步世界中並沒有多少意義，在異步世界中，可變狀態往往會阻礙。 （異步輕輕推開你從面向對象和功能風格）。

希望在VS vNext中，Contracts將被更新爲異步感知類型的後置條件，這也將使靜態檢查器能夠更好地使用異步方法中的斷言。

在此期間，您可以通過編寫一個假設有一個假裝，後置條件：代碼合同

// Synchronous version for comparison. 
public static string Reverse(string s) 
{ 
    Contract.Requires(s != null); 
    Contract.Ensures(Contract.Result<string>() != null); 

    return ...; 
} 

// First wrapper takes care of preconditions (synchronously). 
public static Task<string> ReverseAsync(string s) 
{ 
    Contract.Requires(s != null); 

    return ReverseWithPostconditionAsync(s); 
} 

// Second wrapper takes care of postconditions (asynchronously). 
private static async Task<string> ReverseWithPostconditionAsync(string s) 
{ 
    var result = await ReverseImplAsync(s); 

    // Check our "postcondition" 
    Contract.Assume(result != null); 

    return result; 
} 

private static async Task<string> ReverseImplAsync(string s) 
{ 
    return ...; 
} 

一些用法只是是不可能的 - 例如，在接口或基類成員的異步指定後置條件。

就個人而言，我只是完全避開了我的異步代碼中的契約，希望微軟能夠在幾個月內修復它。

Answer 2

類型化這件事，但忘了打「郵報」 ... :)

這裏沒有目前這個特殊的支持。你能做的最好的就是這樣的事情（不使用async關鍵字，但同樣的想法 - 這是可能的重寫將不同的工作異步CTP下，我還沒有嘗試過）：

public static Task<int> Do() 
{ 
    Contract.Ensures(Contract.Result<Task<int>>() != null); 
    Contract.Ensures(Contract.Result<Task<int>>().Result > 0); 

    return Task.Factory.StartNew(() => { Thread.Sleep(3000); return 2; }); 
} 

public static void Main(string[] args) 
{ 
    var x = Do(); 
    Console.WriteLine("processing"); 
    Console.WriteLine(x.Result); 
} 

然而，這意味着'異步'方法在任務完成評估之前不會實際返回，因此「處理」將在3秒後纔會打印。這類似於懶惰地返回方法的問題，合同必須枚舉IEnumerable中的所有項目以確保條件成立，即使調用方實際上不會使用所有項目。

您可以通過將合同模式更改爲Preconditions來解決此問題，但這意味着實際上不會檢查任何後置條件。

靜態檢查器也不能連接Result與lambda，所以你會得到一個「確保未經證實的」消息。 （一般情況下，靜態檢查程序無論如何都不能證明有關lambda /代表的事情。）

我認爲要獲得對任務/等待的適當支持，代碼合同團隊必須使用特殊情況任務來僅添加前提條件檢查在訪問Result字段時。

Answer 3

發佈新的答案，這個古老的線程，因爲它是由谷歌返回的第一個答案約CodeContract和異步質疑

Curently合同上的異步方法返回任務，工作正常，而且也沒有必要，以避免他們。

斯坦達特合同異步方法：

[ContractClass(typeof(ContractClassForIFoo))] 
public interface IFoo 
{ 
    Task<object> MethodAsync(); 
} 


[ContractClassFor(typeof(IFoo))] 
internal abstract class ContractClassForIFoo : IFoo 
{ 
    #region Implementation of IFoo 

    public Task<object> MethodAsync() 
    { 
     Contract.Ensures(Contract.Result<Task<object>>() != null); 
     Contract.Ensures(Contract.Result<Task<object>>().Status != TaskStatus.Created); 
     Contract.Ensures(Contract.Result<object>() != null); 
     throw new NotImplementedException(); 
    } 

    #endregion 
} 

public class Foo : IFoo 
{ 
    public async Task<object> MethodAsync() 
    { 
     var result = await Task.FromResult(new object()); 
     return result; 
    } 
} 

如果你認爲合同不看起來是正確的我不同意，它看起來誤導至少，但它確實工作。並不像合約重寫者那樣過早地強制評估任務。

由於斯蒂芬提出了一些疑問，在我的情況下做了一些更多的測試和合同，正確地做了他們的事情。用於測試

代碼：

public static class ContractsAbbreviators 
{ 
    [ContractAbbreviator] 
    public static void EnsureTaskIsStarted() 
    { 
     Contract.Ensures(Contract.Result<Task>() != null); 
     Contract.Ensures(Contract.Result<Task>().Status != TaskStatus.Created); 
    } 

} 

[ContractClass(typeof(ContractClassForIFoo))] 
public interface IFoo 
{ 
    Task<int> MethodAsync(int val); 
} 

[ContractClassFor(typeof(IFoo))] 
internal abstract class ContractClassForIFoo : IFoo 
{ 
    public Task<int> MethodAsync(int val) 
    { 
     Contract.Requires(val >= 0); 
     ContractsAbbreviators.EnsureTaskIsStarted(); 
     Contract.Ensures(Contract.Result<int>() == val); 
     Contract.Ensures(Contract.Result<int>() >= 5); 
     Contract.Ensures(Contract.Result<int>() < 10); 
     throw new NotImplementedException(); 
    } 
} 

public class FooContractFailTask : IFoo 
{ 
    public Task<int> MethodAsync(int val) 
    { 
     return new Task<int>(() => val); 
     // esnure raises exception // Contract.Ensures(Contract.Result<Task>().Status != TaskStatus.Created); 
    } 
} 

public class FooContractFailTaskResult : IFoo 
{ 
    public async Task<int> MethodAsync(int val) 
    { 
     await Task.Delay(val).ConfigureAwait(false); 
     return val + 1; 
     // esnure raises exception // Contract.Ensures(Contract.Result<int>() == val); 
    } 
} 

public class Foo : IFoo 
{ 
    public async Task<int> MethodAsync(int val) 
    { 
     const int maxDeapth = 9; 

     await Task.Delay(val).ConfigureAwait(false); 

     if (val < maxDeapth) 
     { 
      await MethodAsync(val + 1).ConfigureAwait(false); 
     } 

     return val; 
    } 
}