Code Contracts and Tasks

Question

Code contracts simply treats Tasks as it would with any other variable, instead of waiting for the result asynchronously. So, the following scenario will not work, and cause a Contracts exception since at the time the method returns, its an incomplete task, and the results wouldn't be set at that point in time. Is there any reasonable workaround for the following scenario?

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

Any suggestions would be appreciated. :) I'd rather not break the contract patterns.

That breaks the asynchrony. The only way without breaking the asynchony seems to be splitting it up into numerous methods. — , Nov 24 '14 at 02:39
but the way you are describing it, it's not Async anyway? the C# `Task` Class has existed before the async/await features, and don't always indicate that the methods using them are intended to be Async... — Claies, Nov 24 '14 at 02:42
It will be asynchronous. The await happens outside of the snippet. — , Nov 24 '14 at 03:48
Situation has change after accepted answer. Adding this comment since google points to this thread as one of first sources about CodeContract and async. Check out my answer: http://stackoverflow.com/questions/9164213/code-contracts-and-asynchrony/40717675#40717675 — Gediminas Zimkus, Nov 21 '16 at 10:42

score 5 · Accepted Answer · answered Nov 24 '14 at 06:53

Code contracts and async don't go together well, so you can't really use Contract.Ensures.

There is however a workaround. You can change your method from a Task-returning method to an async one (which would be cleaner anyway) and use Contract.Assume instead:

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

That's a neat trick. Assumption, however changes the context rendering many of code contracts' derived features (documentation for example) useless. But I guess that's the best solution until code contracts supports async. Will mark this as answer, until async is implemented. Thanks :) — , Nov 24 '14 at 14:33

Code Contracts and Tasks

1 Answers1