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?

Sterile

Nobody said MVPs can't get it wrong. – Surcharge

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.

Apuleius

You mentioned that you hoped "that Microsoft will fix it in a few months" Did the situation change from when you posted this? Do you still avoid contracts on async methods? – Nucleoside

@julealgon: Unfortunately, no. I still avoid contracts on async methods. And I'm still hoping that MS will fix this. :) – Apuleius

Situation has changed since. Check out my answer below. – Lusty

Answer 2

Typed this up but forgot to hit "Post"... :)

There's not specialised support for this at the moment. The best you can do is something like this (not using async keyword, but the same idea - it's possible the rewriter will work differently under the async CTP, I haven't tried it yet):

public static Task<int> Do()
{
    Contract.Ensures(Contract.Result<Task<int>>() != null);
    Contract.Ensures(Contract.Result<Task<int>>().Result > 0);

    return Task.Factory.StartNew(() => { Thread.Sleep(3000); return 2; });
}

public static void Main(string[] args)
{
    var x = Do();
    Console.WriteLine("processing");
    Console.WriteLine(x.Result);
}

However, this means that the 'async' method won't actually return until the Task has finished evaluating, so "processing" won't be printed until 3 seconds have elapsed. This is similar to the problem with methods that lazily return IEnumerables — the Contract has to enumerate all items in the IEnumerable to ensure that the condition holds, even if the caller won't actually use all the items.

You can work around this by changing your contracts mode to Preconditions, but this means that no post-conditions will actually be checked.

The static checker also can't connect the Result with the lambda, so you'll get an "Ensures unproven" message. (In general the static checker doesn't prove things about lambdas/delegates anyway.)

I think to get proper support for Tasks/await, the Code Contracts team will have to special-case Tasks to add the precondition check only upon access of the Result field.

Hourly

Thank you for the info - I hadn't even thought about lazy-loaded collections :-/ – Sterile

Yeah, you can turn on a switch (skip quantifiers) that will ignore Contract.ForAll contracts to avoid having issues with them. There's no such switch for Tasks (yet). – Hourly

Answer 3

Posting new answer to this old thread as it is returned by google as the first answer to question about CodeContract and Async

Curently Contract on async methods returning Task are working correctly, and there is no need to avoid them.

Standart contract for async method:

[ContractClass(typeof(ContractClassForIFoo))]
public interface IFoo
{
    Task<object> MethodAsync();
}


[ContractClassFor(typeof(IFoo))]
internal abstract class ContractClassForIFoo : IFoo
{
    #region Implementation of IFoo

    public Task<object> MethodAsync()
    {
        Contract.Ensures(Contract.Result<Task<object>>() != null);
        Contract.Ensures(Contract.Result<Task<object>>().Status != TaskStatus.Created);
        Contract.Ensures(Contract.Result<object>() != null);
        throw new NotImplementedException();
    }

    #endregion
}

public class Foo : IFoo
{
    public async Task<object> MethodAsync()
    {
        var result = await Task.FromResult(new object());
        return result;
    }
}

If you think that contract does not look correct i do agree it looks misleading at the least, but it does work. And it does not look like that contract rewriter forces evaluation of task prematurely.

As Stephen raised some doubts made some more testing and contracts in my case did their thing correctly.

Code used for testing:

public static class ContractsAbbreviators
{
    [ContractAbbreviator]
    public static void EnsureTaskIsStarted()
    {
        Contract.Ensures(Contract.Result<Task>() != null);
        Contract.Ensures(Contract.Result<Task>().Status != TaskStatus.Created);
    }

}

[ContractClass(typeof(ContractClassForIFoo))]
public interface IFoo
{
    Task<int> MethodAsync(int val);
}

[ContractClassFor(typeof(IFoo))]
internal abstract class ContractClassForIFoo : IFoo
{
    public Task<int> MethodAsync(int val)
    {
        Contract.Requires(val >= 0);
        ContractsAbbreviators.EnsureTaskIsStarted();
        Contract.Ensures(Contract.Result<int>() == val);
        Contract.Ensures(Contract.Result<int>() >= 5);
        Contract.Ensures(Contract.Result<int>() < 10);
        throw new NotImplementedException();
    }
}

public class FooContractFailTask : IFoo
{
    public Task<int> MethodAsync(int val)
    {
        return new Task<int>(() => val);
        // esnure raises exception // Contract.Ensures(Contract.Result<Task>().Status != TaskStatus.Created); 
    }
}

public class FooContractFailTaskResult : IFoo
{
    public async Task<int> MethodAsync(int val)
    {
        await Task.Delay(val).ConfigureAwait(false);
        return val + 1;
        // esnure raises exception // Contract.Ensures(Contract.Result<int>() == val);
    }
}

public class Foo : IFoo
{
    public async Task<int> MethodAsync(int val)
    {
        const int maxDeapth = 9;

        await Task.Delay(val).ConfigureAwait(false);

        if (val < maxDeapth)
        {
            await MethodAsync(val + 1).ConfigureAwait(false);
        }

        return val;
    }
}

Lusty

But you can't express contracts like "the integer will be in the range [5, 10)", and I believe preconditions expressed in the implementation body also do not work as expected. – Apuleius

That doesn't work for me. If I have an async method returning Task<T> and I write Contract.Ensures(Contract.Result<T>() != null) at the beginning, it causes a BadImageFormatException. – Ader