代码契约和异步

Question

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

我已阅读以下建议：

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

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

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

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

是否有任何替代想法，或者我是否遗漏了有关代码契约和 TPL 的任何内容？

Answer 1

我已经向异步团队指出了这一点，正如其他人所做的那样。目前，合约和异步（几乎）是相互排斥的。所以，至少微软的一些人意识到了这个问题，但我不知道他们打算采取什么措施。

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

前提条件可以发挥作用。我最近没有尝试过；您可能需要一个包含先决条件的异步方法的小包装器。

后置条件几乎被破坏了。

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

不变量在异步世界中没有多大意义，因为可变状态往往会造成阻碍。 （异步轻轻地将您从 OOP 推向函数式风格）。

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

同时，您可以通过编写假设来拥有假装后置条件：

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

但是，这意味着“async”方法在任务完成评估之前不会真正返回，因此只有 3 秒过去后才会打印“processing”。这类似于延迟返回 IEnumerable 的方法的问题 - 合约必须枚举 IEnumerable 中的所有项目以确保条件成立，即使调用者获胜实际上并没有使用所有的物品。

您可以通过将契约模式更改为先决条件来解决此问题，但这意味着实际上不会检查后置条件。

静态检查器也无法将 Result 与 lambda 连接起来，因此您会收到“Ensures unproven”消息。 （一般来说，静态检查器无论如何都不会证明有关 lambdas/委托的事情。）

我认为为了获得对 Tasks/await 的适当支持，代码契约团队必须对特殊情况的任务进行特殊处理，以便仅在访问结果字段。

Answer 3

将新答案发布到这个旧线程，因为它是由谷歌返回的，作为有关 CodeContract 和 Async 当前合同的问题的第一个答案，

返回 Task 的异步方法工作正常，无需避免它们。

异步方法的标准合约：

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