Code Contracts and Asynchrony

Question

What is the recommended way for adding postconditions to async methods which return Task<T>?

I have read the following suggestion:

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

The post suggests implementing each method as synchronous, contracting it, and then implementing an async counterpart as a simple wrapper. Unfortunately I don't see this as a workable solution (perhaps through my own misunderstanding):

1. The async method, although assumed to be a wrapper for the sync method, is left without any real code contract and can therefore do as it wishes.
2. Codebases which are committed to asynchrony are unlikely to implement sync counterparts for everything. As a result, implementing new methods which contain awaits on other async methods are consequently forced to be async. These methods are intrinsically asynchronous and cannot easily be converted to synchronous. They are not simply wrappers.

Even if we invalidated the latter point by saying we could use .Result or .Wait() instead of await (which would actually cause some SyncContexts to deadlock, and would have to be re-written in the async method anyway), I'm still convinced about the first point.

Are there any alternative ideas, or is there anything that I've missed about code-contracts and TPL?

Answer 1

I've pointed this out to the Async team, as others have done. Currently, Contracts and Async are (almost) mutually exclusive. So, at least some people in Microsoft are aware of the problem, but I'm not aware of what they're planning to do about it.

I do not recommend writing async methods as wrappers for sync methods. In fact, I would tend to do the opposite.

Preconditions can work. I haven't tried it recently; you may need a small wrapper around your async method that includes the preconditions.

Postconditions are pretty much broken.

Assertions and assumptions do work normally, but the static checker is really limited because postconditions are broken.

Invariants don't make as much sense in the Async world, where mutable state tends to just get in the way. (Async gently pushes you away from OOP and towards a functional style).

Hopefully in VS vNext, Contracts will be updated with an async-aware sort of postcondition, which would also enable the static checker to work better with assertions in async methods.

In the meantime, you can have a pretend-postcondition by writing an assume:

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

Some usages of code contracts just aren't possible - e.g., specifying postconditions on async members of interfaces or base classes.

Personally, I've just avoided Contracts entirely in my Async code, hoping that Microsoft will fix it in a few months.