Code Contracts and Tasks

Question

Code contracts simply process Tasks, as it would with any other variable, instead of waiting for an asynchronous result. Thus, the following scenario will not work and will cause the exception of Contracts, since at the time the method returns, its task is incomplete, and the results will not be set at this point in time. Is there any reasonable solution 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 would prefer not to break the contract templates.

Answer 1

Code contracts and async do not go well, so you cannot use Contract.Ensures .

However, there is a workaround. You can change your method using the Task -returning method to async (which will 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); }