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.

Answer 1

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