代码合同和任务

Question

代码合约简单地将任务视为任何其他变量一样处理，而不是异步等待结果。因此，以下情况将不起作用，并且会导致合约异常，因为在方法返回时，它是一个未完成的任务，在那个时间点上结果尚未设置。是否有任何合理的解决方案来解决以下情况？

public Task LoadAppModel()
{
    Contract.Ensures(app.User != null);
    Contract.Ensures(app.Security != null);
    Contract.Ensures(app.LocalSettings != null);

    return Task.WhenAll(
        store.GetUserAsync().ContinueWith(t => { app.User = t.Result; }),
        store.GetSecurityAsync().ContinueWith(t => { app.Security = t.Result; }),
        store.GetLocalSettingsAsync().ContinueWith(t => { app.LocalSettings = t.Result; }));
}

如果有任何建议，都可以提出来。 :) 我宁愿不打破合同模式。

- user3513472

---

使用Task.WaitAll()代替WhenAll()怎么样？ - Claies

这会破坏异步性。唯一不破坏异步性的方法似乎是将其拆分为多个方法。 - user3513472

但是根据你的描述，它并不是异步的？C#中的Task类在async/await特性出现之前就已经存在了，并且并不总是表示使用它们的方法旨在异步执行... - Claies

它将是异步的。等待操作发生在代码片段之外。 - user3513472

接受答案后情况发生了变化。添加此评论，因为谷歌将此线程作为CodeContract和async的首要来源之一。请查看我的答案：https://dev59.com/D2ox5IYBdhLWcg3wf0fl#40717675 - Gediminas Zimkus

Answer 1

代码合同和async不太搭配，所以您不能真正使用Contract.Ensures。

但是有一个解决方法。您可以将方法从返回Task的方法更改为返回async的方法（这样做会更清晰），并使用Contract.Assume代替：

public async Task LoadAppModel()
{
    var userTask = store.GetUserAsync();
    var securityTask = store.GetSecurityAsync();
    var settingsTask = store.GetLocalSettingsAsync();
    await Task.WhenAll(userTask, securityTask,settingsTask);

    app.User = userTask.Result;
    app.Security = securityTask.Result;
    app.LocalSettings = settingsTask.Result;

    Contract.Assume(app.User != null);
    Contract.Assume(app.Security != null);
    Contract.Assume(app.LocalSettings != null);
}

- i3arnon

---

这是个不错的技巧。然而，假设会改变上下文，使得许多代码合同派生特性（例如文档）变得无用。但我想这是最好的解决方案，直到代码合同支持异步操作。在实现异步操作之前，我会将其标记为答案。谢谢 :) - user3513472