代码契约和异步

将后置条件添加到返回Task异步方法的推荐方法是什么?

我已阅读以下建议:

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

post建议将每个方法实现为同步,签约,然后将异步对应实现为简单的包装器。 不幸的是,我不认为这是一个可行的解决方案(也许是通过我自己的误解):

  1. 异步方法虽然被假定为同步方法的包装器,但是没有任何真正的代码契约,因此可以按照自己的意愿进行。
  2. 致力于异步的代码库不太可能为所有内容实现同步对应。 因此,实现包含await其他异步方法的新方法因此被强制为异步。 这些方法本质上是异步的,不能轻易转换为同步。 它们不仅仅是包装纸。

即使我们通过说我们可以使用.Result.Wait()而不是await (这实际上会导致某些SyncContext死锁,并且无论如何都必须在异步方法中重写.Wait()来使后一点无效,我我仍然坚信第一点。

有没有其他想法,或者有什么我错过的代码合同和TPL?

正如其他人所做的那样,我已经向异步团队指出了这一点。 目前,合同和异步(几乎)是互斥的。 所以,至少微软的一些人都知道这个问题,但我不知道他们打算怎么做。

我不建议将异步方法编写为同步方法的包装器。 事实上,我倾向于做相反的事情。

先决条件可以奏效。 我最近没有尝试过; 你可能需要一个包含前置条件的异步方法的小包装器。

后置条件几乎被破坏了。

断言和假设确实正常,但静态检查器确实有限,因为后置条件被破坏了。

不变量在Async世界中没有那么多意义,因为可变状态往往会妨碍它。 (Async轻轻地将你从OOP推向一个function风格)。

希望在VS vNext中,Contracts将使用异步感知的后置条件进行更新,这也将使静态检查器能够更好地处理异步方法中的断言。

在此期间,您可以通过编写假设来进行假装后置条件:

 // Synchronous version for comparison. public static string Reverse(string s) { Contract.Requires(s != null); Contract.Ensures(Contract.Result() != null); return ...; } // First wrapper takes care of preconditions (synchronously). public static Task ReverseAsync(string s) { Contract.Requires(s != null); return ReverseWithPostconditionAsync(s); } // Second wrapper takes care of postconditions (asynchronously). private static async Task ReverseWithPostconditionAsync(string s) { var result = await ReverseImplAsync(s); // Check our "postcondition" Contract.Assume(result != null); return result; } private static async Task ReverseImplAsync(string s) { return ...; } 

代码契约的一些用法是不可能的 – 例如,在接口或基类的异步成员上指定后置条件。

就个人而言,我完全避免使用我的异步代码中的合同,希望微软能在几个月后修复它。

键入此内容但忘记点击“发布”… 🙂

目前还没有专门的支持。 你能做的最好就是这样(不使用async关键字,但是同样的想法 – 重写器在异步CTP下可能会有不同的工作方式,我还没有尝试过):

 public static Task Do() { Contract.Ensures(Contract.Result>() != null); Contract.Ensures(Contract.Result>().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的方法的问题 – 合同必须枚举IEnumerable所有项目以确保条件成立,即使调用者实际上不会使用所有项目。

您可以通过将合同模式更改为Preconditions来解决此问题,但这意味着实际上不会检查任何后置条件。

静态检查程序也无法将Result与lambda连接,因此您将收到“确认未经证实”的消息。 (一般来说,静态检查器无论如何都不能certificatelambda / delegates的内容。)

我认为为了获得对Tasks / await的适当支持,Code Contracts团队将只有在访问Result字段时才需要特殊任务来添加前置条件检查。

发布这个旧post的新答案,因为谷歌将其作为关于CodeContract和Async问题的第一个答案

对返回Task的异步方法进行Curently Contract正常工作,并且没有必要避免它们。

异步方法的标准合同:

 [ContractClass(typeof(ContractClassForIFoo))] public interface IFoo { Task MethodAsync(); } [ContractClassFor(typeof(IFoo))] internal abstract class ContractClassForIFoo : IFoo { #region Implementation of IFoo public Task MethodAsync() { Contract.Ensures(Contract.Result>() != null); Contract.Ensures(Contract.Result>().Status != TaskStatus.Created); Contract.Ensures(Contract.Result() != null); throw new NotImplementedException(); } #endregion } public class Foo : IFoo { public async Task MethodAsync() { var result = await Task.FromResult(new object()); return result; } } 

如果你认为合同看起来不正确我同意它至少看起来有误导性,但它确实有效。 并且它看起来不像合同重写者过早地强制评估任务。

正如斯蒂芬提出的一些疑问使得我的案例中的更多测试和合同正确地做了他们的事情。

用于测试的代码:

 public static class ContractsAbbreviators { [ContractAbbreviator] public static void EnsureTaskIsStarted() { Contract.Ensures(Contract.Result() != null); Contract.Ensures(Contract.Result().Status != TaskStatus.Created); } } [ContractClass(typeof(ContractClassForIFoo))] public interface IFoo { Task MethodAsync(int val); } [ContractClassFor(typeof(IFoo))] internal abstract class ContractClassForIFoo : IFoo { public Task MethodAsync(int val) { Contract.Requires(val >= 0); ContractsAbbreviators.EnsureTaskIsStarted(); Contract.Ensures(Contract.Result() == val); Contract.Ensures(Contract.Result() >= 5); Contract.Ensures(Contract.Result() < 10); throw new NotImplementedException(); } } public class FooContractFailTask : IFoo { public Task MethodAsync(int val) { return new Task(() => val); // esnure raises exception // Contract.Ensures(Contract.Result().Status != TaskStatus.Created); } } public class FooContractFailTaskResult : IFoo { public async Task MethodAsync(int val) { await Task.Delay(val).ConfigureAwait(false); return val + 1; // esnure raises exception // Contract.Ensures(Contract.Result() == val); } } public class Foo : IFoo { public async Task MethodAsync(int val) { const int maxDeapth = 9; await Task.Delay(val).ConfigureAwait(false); if (val < maxDeapth) { await MethodAsync(val + 1).ConfigureAwait(false); } return val; } }