代码合同和异步

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