代码契约和异步

本文关键字：异步 契约 代码 | 更新日期: 2023-09-27 18:23:35

向返回Task<T>的异步方法添加后处理条件的推荐方法是什么？

我已经阅读了以下建议：

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

文章建议将每个方法实现为同步的，对其进行收缩，然后将异步对应方法实现为简单的包装器。不幸的是，我不认为这是一个可行的解决方案（也许是因为我自己的误解）：

  1. async方法虽然被假定为sync方法的包装器，但没有任何实际的代码契约，因此可以随心所欲
  2. 致力于异步的代码库不太可能实现所有内容的同步对应。因此，在其他异步方法上实现包含awaits的新方法被迫是异步的。这些方法本质上是异步的，不能很容易地转换为同步的。它们不仅仅是包装纸

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

关于代码合同和TPL，有没有其他想法，或者我错过了什么？

代码契约和异步

我已经向Async团队指出了这一点，就像其他人所做的那样。目前，Contracts和Async（几乎）是互斥的。所以，至少微软的一些人已经意识到了这个问题，但我不知道他们打算怎么做

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

前提条件是可行的。我最近没试过；您可能需要在异步方法周围使用一个包含先决条件的小包装器。

后置条件几乎被破坏了。

断言和假设确实可以正常工作，但静态检查器确实受到限制，因为后置条件被破坏了。

不变量在异步世界中没有那么大的意义，在异步世界里，可变状态往往会成为阻碍。（Async轻轻地将您从OOP推向功能性风格）。

希望在VSvNext中，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 ...;
}

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

就我个人而言，我只是在异步代码中完全避免了Contracts，希望微软能在几个月内解决它。

输入了这个，但忘记点击"Post"…：）

目前还没有专门的支持。你能做的最好的事情是这样的（不使用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);
}

然而，这意味着在Task完成评估之前，"async"方法实际上不会返回，因此在3秒之后才会打印"处理"。这与延迟返回IEnumerables—Contract必须枚举IEnumerable中的所有项，以确保条件成立，即使调用者实际上不会使用所有项。

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

静态检查器也无法将Result与lambda连接起来，因此您将得到一条"确保未经验证"消息。（一般来说，静态检查器无论如何都不能证明lambdas/deletes的情况。）

我认为，为了获得对Tasks/await的适当支持，代码合同团队将不得不在访问Result字段时使用特殊情况的Tasks来添加前提条件检查。

发布这个旧线程的新答案，因为它是谷歌返回的，是关于CodeContract和Async 问题的第一个答案

Curtly对返回Task的异步方法执行Contract操作正常，没有必要避免它们。

异步方法的标准合约：

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

如果你认为这份合同看起来不正确，我同意它至少看起来有误导性，但它确实有效。而且看起来，合同重写器并没有过早地强制对任务进行评估。

由于Stephen提出了一些质疑，所以进行了更多的测试，在我的情况下，合同做得很正确。

用于测试的代码：

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;
    }
}
相关文章：